Go to the documentation of this file.
20 #ifndef CPROVER_SOLVERS_REFINEMENT_STRING_REFINEMENT_H
21 #define CPROVER_SOLVERS_REFINEMENT_STRING_REFINEMENT_H
36 #define OPT_STRING_REFINEMENT \
37 "(no-refine-strings)" \
38 "(string-printable)" \
39 "(string-input-value):" \
40 "(string-non-empty)" \
41 "(max-nondet-string-length):"
43 #define HELP_STRING_REFINEMENT \
44 " --no-refine-strings turn off string refinement\n" \
45 " --string-printable restrict to printable strings and characters\n" \
46 " --string-non-empty restrict to non-empty strings (experimental)\n" \
47 " --string-input-value st restrict non-null strings to a fixed value st;\n" \
48 " the switch can be used multiple times to give\n" \
49 " several strings\n" \
50 " --max-nondet-string-length n bound the length of nondet (e.g. input) strings.\n" \
51 " Default is " + std::to_string(MAX_CONCRETE_STRING_SIZE - 1) + "; note that\n" \
52 " setting the value higher than this does not work\n" \
53 " with --trace or --validate-trace.\n"
57 #define OPT_STRING_REFINEMENT_CBMC \
61 #define HELP_STRING_REFINEMENT_CBMC \
62 " --refine-strings use string refinement (experimental)\n" \
63 " --string-printable restrict to printable strings (experimental)\n"
66 #define DEFAULT_MAX_NB_REFINEMENT std::numeric_limits<size_t>::max()
91 void set_to(
const exprt &expr,
bool value)
override;
129 const std::vector<equal_exprt> &equations,
137 const bool left_propagate);
string_constraint_generatort generator
virtual const std::string solver_text()=0
std::vector< exprt > current_constraints
std::size_t refinement_bound
Base class for all expressions.
index_set_pairt index_sets
Keeps track of dependencies between strings.
Magic numbers used throughout the codebase.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Generation of fresh symbols of a given type.
exprt get(const exprt &expr) const override
Evaluates the given expression in the valuation found by string_refinementt::dec_solve.
exprt substitute_array_access(exprt expr, symbol_generatort &symbol_generator, const bool left_propagate)
Create an equivalent expression where array accesses and 'with' expressions are replaced by 'if' expr...
exprt substitute_array_lists(exprt expr, std::size_t string_max_length)
union_find_replacet symbol_resolve
resultt
Result of running the decision procedure.
decision_proceduret::resultt dec_solve() override
Main decision procedure of the solver.
string_dependenciest dependencies
Defines string constraints.
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
Return a textual description of the decision procedure.
std::vector< exprt > equations
union_find_replacet string_identifiers_resolution_from_equations(const std::vector< equal_exprt > &equations, const namespacet &ns, messaget::mstreamt &stream)
Symbol resolution for expressions of type string typet.
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...
Generates string constraints to link results from string functions with their arguments.
String expressions for the string solver.
string_refinementt(const infot &)
std::set< exprt > seen_instances