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 <util/string_expr.h>
26 
27 // Defines a limit on the string witnesses we will output.
28 // Longer strings are still concidered possible by the solver but
29 // it will not output them.
30 #define MAX_CONCRETE_STRING_SIZE 500
31 
32 #define MAX_NB_REFINEMENT 100
33 
35 {
36 public:
37  // refinement_bound is a bound on the number of refinement allowed
39  const namespacet &_ns, propt &_prop, unsigned refinement_bound);
40 
41  void set_mode();
42 
43  // Should we use counter examples at each iteration?
45 
46  virtual std::string decision_procedure_text() const
47  {
48  return "string refinement loop with "+prop.solver_text();
49  }
50 
51  static exprt is_positive(const exprt &x);
52 
53 protected:
54  typedef std::set<exprt> expr_sett;
55 
56  virtual bvt convert_symbol(const exprt &expr);
58  const function_application_exprt &expr);
59 
61 
62  bvt convert_bool_bv(const exprt &boole, const exprt &orig);
63 
64 private:
65  // Base class
67 
69 
71 
72  // Simple constraints that have been given to the solver
73  expr_sett seen_instances;
74 
75  std::vector<string_constraintt> universal_axioms;
76 
77  std::vector<string_not_contains_constraintt> not_contains_axioms;
78 
79  // Unquantified lemmas that have newly been added
80  std::vector<exprt> cur;
81 
82  // See the definition in the PASS article
83  // Warning: this is indexed by array_expressions and not string expressions
84  std::map<exprt, expr_sett> current_index_set;
85  std::map<exprt, expr_sett> index_set;
86 
87  void display_index_set();
88 
89  void add_lemma(const exprt &lemma, bool add_to_index_set=true);
90 
91  bool boolbv_set_equality_to_true(const equal_exprt &expr);
92 
93  literalt convert_rest(const exprt &expr);
94 
95  void add_instantiations();
96 
97  bool check_axioms();
98 
99  void update_index_set(const exprt &formula);
100  void update_index_set(const std::vector<exprt> &cur);
101  void initial_index_set(const string_constraintt &axiom);
102  void initial_index_set(const std::vector<string_constraintt> &string_axioms);
103 
105  const string_constraintt &axiom, const exprt &str, const exprt &val);
106 
108  const string_not_contains_constraintt &axiom,
109  std::list<exprt> &new_lemmas);
110 
112  const exprt &qvar, const exprt &val, const exprt &f);
113 
114  std::map<exprt, int> map_representation_of_sum(const exprt &f) const;
115  exprt sum_over_map(std::map<exprt, int> &m, bool negated=false) const;
116 
117  exprt simplify_sum(const exprt &f) const;
118 
119  exprt get_array(const exprt &arr, const exprt &size);
120 
121  std::string string_of_array(const exprt &arr, const exprt &size) const;
122 };
123 
124 #endif
Generates string constraints to link results from string functions with their arguments.
std::map< exprt, int > map_representation_of_sum(const exprt &f) const
application of (mathematical) function
Definition: std_expr.h:3785
std::vector< exprt > cur
virtual const std::string solver_text()=0
bool boolbv_set_equality_to_true(const equal_exprt &expr)
add lemmas to the solver corresponding to the given equation
bv_refinementt supert
void add_instantiations()
compute the index set for all formulas, instantiate the formulas with the found indexes, and add them as lemmas.
void set_mode()
determine which language should be used
equality
Definition: std_expr.h:1082
exprt get_array(const exprt &arr, const exprt &size)
gets a model of an array and put it in a certain form
std::set< exprt > expr_sett
Defines string constraints.
literalt convert_rest(const exprt &expr)
if the expression is a function application, we convert it using our own convert_function_application...
TO_BE_DOCUMENTED.
Definition: namespace.h:62
bvt convert_bool_bv(const exprt &boole, const exprt &orig)
fills as many 0 as necessary in the bit vectors to have the right width
exprt simplify_sum(const exprt &f) const
string_refinementt(const namespacet &_ns, propt &_prop, unsigned refinement_bound)
bool check_axioms()
return true if the current model satisfies all the axioms
void update_index_set(const exprt &formula)
add to the index set all the indices that appear in the formula
virtual bvt convert_function_application(const function_application_exprt &expr)
generate an expression, add lemmas stating that this expression corresponds to the result of the give...
exprt compute_inverse_function(const exprt &qvar, const exprt &val, const exprt &f)
exprt instantiate(const string_constraintt &axiom, const exprt &str, const exprt &val)
TO_BE_DOCUMENTED.
Definition: prop.h:22
std::string string_of_array(const exprt &arr, const exprt &size) const
convert the content of a string to a more readable representation.
string_constraint_generatort generator
void initial_index_set(const string_constraintt &axiom)
add to the index set all the indices that appear in the formula and the upper bound minus one ...
String expressions for the string solver.
std::map< exprt, expr_sett > current_index_set
Base class for all expressions.
Definition: expr.h:46
void display_index_set()
display the current index set, for debugging
decision_proceduret::resultt dec_solve()
use a refinement loop to instantiate universal axioms, call the sat solver, and instantiate more inde...
static exprt is_positive(const exprt &x)
exprt sum_over_map(std::map< exprt, int > &m, bool negated=false) const
void instantiate_not_contains(const string_not_contains_constraintt &axiom, std::list< exprt > &new_lemmas)
std::vector< string_not_contains_constraintt > not_contains_axioms
std::map< exprt, expr_sett > index_set
std::vector< string_constraintt > universal_axioms
void add_lemma(const exprt &lemma, bool add_to_index_set=true)
add the given lemma to the solver
std::vector< literalt > bvt
Definition: literal.h:197
virtual std::string decision_procedure_text() const
virtual bvt convert_symbol(const exprt &expr)
if the expression as string type, look up for the string in the list of string symbols that we mainta...