cprover
string_refinement.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: String support via creating string constraints and progressively
4  instantiating the universal constraints as needed.
5  The procedure is described in the PASS paper at HVC'13:
6  "PASS: String Solving with Parameterized Array and Interval Automaton"
7  by Guodong Li and Indradeep Ghosh
8 
9 Author: Alberto Griggio, alberto.griggio@gmail.com
10 
11 \*******************************************************************/
12 
19 
20 #ifndef CPROVER_SOLVERS_REFINEMENT_STRING_REFINEMENT_H
21 #define CPROVER_SOLVERS_REFINEMENT_STRING_REFINEMENT_H
22 
23 #include <limits>
24 #include <util/string_expr.h>
25 #include <util/replace_expr.h>
31 
32 #define DEFAULT_MAX_NB_REFINEMENT std::numeric_limits<size_t>::max()
33 
35 {
36 private:
37  struct configt
38  {
39  std::size_t refinement_bound=0;
41  bool trace=false;
43  std::size_t max_string_length;
44  };
45 public:
47  struct infot : public bv_refinementt::infot,
48  public configt
49  {
50  };
51 
52  explicit string_refinementt(const infot &);
53 
54  std::string decision_procedure_text() const override
55  { return "string refinement loop with "+prop.solver_text(); }
56 
57  exprt get(const exprt &expr) const override;
58  void set_to(const exprt &expr, bool value) override;
60 
61 private:
62  // Base class
64 
65  string_refinementt(const infot &, bool);
66 
68  std::size_t loop_bound_;
70 
71  // Simple constraints that have been given to the solver
72  std::set<exprt> seen_instances;
73 
75 
76  // Unquantified lemmas that have newly been added
77  std::vector<exprt> current_constraints;
78 
79  // See the definition in the PASS article
80  // Warning: this is indexed by array_expressions and not string expressions
81 
84 
85  std::vector<equal_exprt> equations;
86 
88 
89  void add_lemma(const exprt &lemma, bool simplify_lemma = true);
90 };
91 
92 exprt substitute_array_lists(exprt expr, std::size_t string_max_length);
93 
94 // Declaration required for unit-test:
96  std::vector<equal_exprt> &equations,
97  const namespacet &ns,
98  messaget::mstreamt &stream);
99 
100 // Declaration required for unit-test:
102  exprt expr,
103  const std::function<symbol_exprt(const irep_idt &, const typet &)>
104  &symbol_generator,
105  const bool left_propagate);
106 
107 #endif
bool trace
Concretize strings after solver is finished.
The type of an expression.
Definition: type.h:22
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
bv_refinementt supert
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
TO_BE_DOCUMENTED.
Definition: namespace.h:74
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
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...
const configt config_
Base class for all expressions.
Definition: expr.h:42
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.
string_axiomst axioms
Expression to hold a symbol (variable)
Definition: std_expr.h:90
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 &#39;with&#39; expressions are replaced by &#39;if&#39; expr...
index_set_pairt index_sets
void add_lemma(const exprt &lemma, bool simplify_lemma=true)
Add the given lemma to the solver.