Include dependency graph for string_constraint_instantiation.h: This graph shows which files directly or indirectly include this file: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) |
| Instantiates a string constraint by substituting the quantifiers. 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) |
Detailed Description
Defines related function for string constraints.
Definition in file string_constraint_instantiation.h.
Function Documentation
◆ instantiate()
| exprt instantiate | ( | const string_constraintt & | axiom, |
| const exprt & | str, | ||
| const exprt & | val | ||
| ) |
Instantiates a string constraint by substituting the quantifiers.
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 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'\). If there are several such indexes, the conjunction of the instantiations is returned, for instance for a formula: \(\forall q. s[q+x]='a' \land s[q]=c\) we would get \(s[v] = 'a' \land s[v-x] = c \land s[v+x] = 'a' \land s[v] = c\).
- Parameters
-
axiom a universally quantified formula str an array of characters val an index expression
- Returns
axiomwith substituedqvar
Definition at line 173 of file string_constraint_instantiation.cpp.
◆ instantiate_not_contains()
|
related |
