12 #ifndef CPROVER_SOLVERS_REFINEMENT_STRING_CONSTRAINT_INSTANTIATION_H
13 #define CPROVER_SOLVERS_REFINEMENT_STRING_CONSTRAINT_INSTANTIATION_H
34 const std::set<std::pair<exprt, exprt>> &index_pairs,
35 const std::unordered_map<string_not_contains_constraintt, symbol_exprt>
Base class for all expressions.
Canonical representation of linear function, for instance, expression $x + x - y + 5 - 3$ would given...
exprt to_expr(bool negated=false) const
static exprt solve(linear_functiont f, const exprt &var, const exprt &val)
Return an expression y such that f(var <- y) = val.
linear_functiont(const exprt &f)
Put an expression f composed of additions and subtractions into its cannonical representation.
std::unordered_map< exprt, mp_integer, irep_hash > coefficients
std::string format()
Format the linear function as a string, can be used for debugging.
void add(const linear_functiont &other)
Make this function the sum of the current function with other.
mp_integer constant_coefficient
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)
Instantiates a quantified formula representing not_contains by substituting the quantifiers and gener...
The type of an expression, extends irept.
Defines string constraints.
Generates string constraints to link results from string functions with their arguments.
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,...
Constraints to encode non containement of strings.