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 #define CHARACTER_FOR_UNKNOWN '?'
34 
36 {
37 private:
38  struct configt
39  {
40  std::size_t refinement_bound=0;
42  bool trace=false;
44  std::size_t max_string_length;
45  };
46 public:
48  struct infot : public bv_refinementt::infot,
49  public configt
50  {
51  };
52 
53  explicit string_refinementt(const infot &);
54 
55  std::string decision_procedure_text() const override
56  { return "string refinement loop with "+prop.solver_text(); }
57 
58  exprt get(const exprt &expr) const override;
59  void set_to(const exprt &expr, bool value) override;
61 
62 private:
63  // Base class
65 
66  string_refinementt(const infot &, bool);
67 
69  std::size_t loop_bound_;
70  std::size_t max_string_length;
72 
73  // Simple constraints that have been given to the solver
74  std::set<exprt> seen_instances;
75 
77 
78  // Unquantified lemmas that have newly been added
79  std::vector<exprt> current_constraints;
80 
81  // See the definition in the PASS article
82  // Warning: this is indexed by array_expressions and not string expressions
83 
86 
87  std::vector<equal_exprt> equations;
88 
90 
91  void add_lemma(const exprt &lemma, bool simplify_lemma = true);
92 };
93 
94 exprt substitute_array_lists(exprt expr, std::size_t string_max_length);
95 
96 // Declaration required for unit-test:
98  std::vector<equal_exprt> &equations,
99  const namespacet &ns,
100  messaget::mstreamt &stream);
101 
102 // Declaration required for unit-test:
104  exprt expr,
105  const std::function<symbol_exprt(const irep_idt &, const typet &)>
106  &symbol_generator,
107  const bool left_propagate);
108 
109 #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
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...
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.