cprover
|
Defines related function for string constraints. More...
#include "string_constraint_instantiation.h"
#include <algorithm>
#include <unordered_set>
#include <util/expr_iterator.h>
Go to the source code of this file.
Functions | |
static bool | contains (const exprt &index, const symbol_exprt &qvar) |
Look for symbol qvar in the expression index and return true if found. More... | |
static std::unordered_set< exprt, irep_hash > | find_indexes (const exprt &expr, const exprt &str, const symbol_exprt &qvar) |
Find indexes of str used in expr that contains qvar , for instance with arguments (str[k+1]=='a') , str , and k , the function should return k+1 . More... | |
exprt | instantiate (const string_constraintt &axiom, const exprt &str, const exprt &val) |
Instantiates a string constraint by substituting the quantifiers. More... | |
Defines related function for string constraints.
Definition in file string_constraint_instantiation.cpp.
|
static |
Look for symbol qvar
in the expression index
and return true if found.
qvar
appears in index
. Definition at line 19 of file string_constraint_instantiation.cpp.
|
static |
Find indexes of str
used in expr
that contains qvar
, for instance with arguments (str[k+1]=='a')
, str
, and k
, the function should return k+1
.
[in] | expr | the expression to search |
[in] | str | the string which must be indexed |
[in] | qvar | the universal variable that must be in the index |
expr
on str
containing qvar
. Definition at line 33 of file string_constraint_instantiation.cpp.
exprt instantiate | ( | const string_constraintt & | axiom, |
const exprt & | str, | ||
const exprt & | val | ||
) |
Instantiates a string constraint by substituting the quantifiers.
Substitute qvar
the universally quantified variable of axiom
, by an index val
, in axiom
, so that the index used for str
equals val
.
For a string constraint of the form forall q. P(x)
, substitute q
the universally quantified variable of axiom
, by an index
, in axiom
, so that the index used for str
equals val
. For instance, if axiom
is ‘forall q. s[q+x] = 'a’ && t[q] = 'b',
instantiate(axiom,s,v)would return the expression
s[v] = 'a' && t[v-x] = 'b'`. If there are several such indexes, the conjunction of the instantiations is returned, for instance for a formula: ‘forall q. s[q+x]='a’ && s[q]=cwe would get
s[v] = 'a' && s[v-x] = c && s[v+x] = 'a' && s[v] = c`.
axiom | a universally quantified formula |
str | an array of characters |
val | an index expression |
Definition at line 183 of file string_constraint_instantiation.cpp.