20 #ifndef CPROVER_SOLVERS_REFINEMENT_STRING_REFINEMENT_H 21 #define CPROVER_SOLVERS_REFINEMENT_STRING_REFINEMENT_H 32 #define DEFAULT_MAX_NB_REFINEMENT std::numeric_limits<size_t>::max() 33 #define CHARACTER_FOR_UNKNOWN '?' 59 void set_to(
const exprt &expr,
bool value)
override;
98 std::vector<equal_exprt> &equations,
107 const bool left_propagate);
bool trace
Concretize strings after solver is finished.
The type of an expression.
std::size_t max_string_length
Generates string constraints to link results from string functions with their arguments.
std::vector< equal_exprt > equations
virtual const std::string solver_text()=0
string_refinementt constructor arguments
string_dependenciest dependencies
string_refinementt(const infot &)
exprt substitute_array_lists(exprt expr, std::size_t string_max_length)
Defines string constraints.
union_find_replacet symbol_resolve
std::size_t max_string_length
decision_proceduret::resultt dec_solve() override
Main decision procedure of the solver.
Keep track of dependencies between strings.
string_constraint_generatort generator
String expressions for the string solver.
Similar interface to union-find for expressions, with a function for replacing sub-expressions by the...
Base class for all expressions.
void set_to(const exprt &expr, bool value) override
Record the constraints to ensure that the expression is true when the boolean is true and false other...
std::set< exprt > seen_instances
std::string decision_procedure_text() const override
union_find_replacet string_identifiers_resolution_from_equations(std::vector< equal_exprt > &equations, const namespacet &ns, messaget::mstreamt &stream)
Symbol resolution for expressions of type string typet.
std::size_t refinement_bound
Expression to hold a symbol (variable)
std::vector< exprt > current_constraints
exprt substitute_array_access(exprt expr, const std::function< symbol_exprt(const irep_idt &, const typet &)> &symbol_generator, const bool left_propagate)
Create an equivalent expression where array accesses and 'with' expressions are replaced by 'if' expr...
index_set_pairt index_sets
void add_lemma(const exprt &lemma, bool simplify_lemma=true)
Add the given lemma to the solver.