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);
resultt
Result of running the decision procedure.
Base class for all expressions.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
virtual const std::string solver_text()=0
Keep track of dependencies between strings.
string_constraint_generatort generator
std::string decision_procedure_text() const override
Return a textual description of the decision procedure.
union_find_replacet symbol_resolve
std::vector< exprt > equations
string_refinementt(const infot &)
decision_proceduret::resultt dec_solve() override
Main decision procedure of the solver.
std::set< exprt > seen_instances
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_dependenciest dependencies
index_set_pairt index_sets
exprt get(const exprt &expr) const override
Evaluates the given expression in the valuation found by string_refinementt::dec_solve.
std::vector< exprt > current_constraints
void add_lemma(const exprt &lemma, bool simplify_lemma=true)
Add the given lemma to the solver.
Generation of fresh symbols of a given type.
Similar interface to union-find for expressions, with a function for replacing sub-expressions by the...
Magic numbers used throughout the codebase.
Defines string constraints.
Generates string constraints to link results from string functions with their arguments.
Keeps track of dependencies between strings.
String expressions for the string solver.
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 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.
std::size_t refinement_bound
string_refinementt constructor arguments