Go to the documentation of this file.
20 #ifndef CPROVER_SOLVERS_REFINEMENT_STRING_REFINEMENT_H
21 #define CPROVER_SOLVERS_REFINEMENT_STRING_REFINEMENT_H
33 #define OPT_STRING_REFINEMENT \
34 "(no-refine-strings)" \
35 "(string-printable)" \
36 "(string-input-value):" \
37 "(string-non-empty)" \
38 "(max-nondet-string-length):"
40 #define HELP_STRING_REFINEMENT \
41 " --no-refine-strings turn off string refinement\n" \
42 " --string-printable restrict to printable strings (experimental)\n" \
43 " --string-non-empty restrict to non-empty strings (experimental)\n" \
44 " --string-printable st restrict non-null strings to a fixed value st;\n" \
45 " the switch can be used multiple times to give\n" \
46 " several strings\n" \
47 " --max-nondet-string-length n bound the length of nondet (e.g. input) strings\n"
51 #define OPT_STRING_REFINEMENT_CBMC \
55 #define HELP_STRING_REFINEMENT_CBMC \
56 " --refine-strings use string refinement (experimental)\n" \
57 " --string-printable restrict to printable strings (experimental)\n"
60 #define DEFAULT_MAX_NB_REFINEMENT std::numeric_limits<size_t>::max()
83 void set_to(
const exprt &expr,
bool value)
override;
121 std::vector<equal_exprt> &equations,
130 const bool left_propagate);
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
string_constraint_generatort generator
virtual const std::string solver_text()=0
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...
The type of an expression, extends irept.
std::vector< exprt > current_constraints
std::size_t refinement_bound
std::vector< equal_exprt > equations
Base class for all expressions.
index_set_pairt index_sets
Expression to hold a symbol (variable)
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
exprt get(const exprt &expr) const override
Evaluates the given expression in the valuation found by string_refinementt::dec_solve.
exprt substitute_array_lists(exprt expr, std::size_t string_max_length)
union_find_replacet symbol_resolve
decision_proceduret::resultt dec_solve() override
Main decision procedure of the solver.
string_dependenciest dependencies
Similar interface to union-find for expressions, with a function for replacing sub-expressions by the...
Keep track of dependencies between strings.
std::string decision_procedure_text() const override
void add_lemma(const exprt &lemma, bool simplify_lemma=true)
Add the given lemma to the solver.
string_refinementt constructor arguments
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...
string_refinementt(const infot &)
std::set< exprt > seen_instances
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.