cprover
|
Defines related function for string constraints. More...
Go to the source code of this file.
Classes | |
class | linear_functiont |
Canonical representation of linear function, for instance, expression $x + x - y + 5 - 3$ would given by constant_coefficient 2 and coefficients: x -> 2, y -> -1. More... | |
Functions | |
exprt | instantiate (const string_constraintt &axiom, const exprt &str, const exprt &val) |
Substitute qvar the universally quantified variable of axiom , by an index val , in axiom , so that the index used for str equals val . More... | |
std::vector< exprt > | instantiate_not_contains (const string_not_contains_constraintt &axiom, const std::set< std::pair< exprt, exprt >> &index_pairs, const std::unordered_map< string_not_contains_constraintt, symbol_exprt > &witnesses) |
Defines related function for string constraints.
Definition in file string_constraint_instantiation.h.
exprt instantiate | ( | const string_constraintt & | axiom, |
const exprt & | str, | ||
const exprt & | val | ||
) |
Substitute qvar
the universally quantified variable of axiom
, by an index val
, in axiom
, so that the index used for str
equals val
.
For instance, if axiom
corresponds to \(\forall q.\ s[q+x]='a' \land t[q]='b'\), instantiate(axiom,s,v)
would return an expression for \(s[v]='a' \land t[v-x]='b'\).
axiom | a universally quantified formula |
str | an array of char variable |
val | an index expression |
axiom
with substitued qvar
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.
|
related |