cprover
string_constraint.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Defines string constraints. These are formulas talking about strings.
4  We implemented two forms of constraints: `string_constraintt`
5  are formulas of the form $\forall univ_var \in [lb,ub[. prem => body$,
6  and not_contains_constraintt of the form:
7  $\forall x in [lb,ub[. p(x) => \exists y in [lb,ub[. s1[x+y] != s2[y]$.
8 
9 Author: Romain Brenguier, romain.brenguier@diffblue.com
10 
11 \*******************************************************************/
12 
19 
20 #ifndef CPROVER_SOLVERS_REFINEMENT_STRING_CONSTRAINT_H
21 #define CPROVER_SOLVERS_REFINEMENT_STRING_CONSTRAINT_H
22 
23 #include "bv_refinement.h"
25 
26 #include <util/format_expr.h>
27 #include <util/format_type.h>
29 #include <util/string_expr.h>
31 
58 class string_constraintt final
59 {
60 public:
61  // String constraints are of the form
62  // forall univ_var in [lower_bound,upper_bound[. body
67 
68  string_constraintt() = delete;
69 
71  symbol_exprt _univ_var,
74  exprt body)
75  : univ_var(_univ_var),
78  body(body)
79  {
80  }
81 
82  // Default bound inferior is 0
85  univ_var,
86  from_integer(0, univ_var.type()),
88  body)
89  {
90  }
91 
93  {
94  return and_exprt(
97  }
98 
99  void replace_expr(union_find_replacet &replace_map)
100  {
101  replace_map.replace_expr(lower_bound);
102  replace_map.replace_expr(upper_bound);
103  replace_map.replace_expr(body);
104  }
105 
106  exprt negation() const
107  {
109  }
110 };
111 
117 inline std::string to_string(const string_constraintt &expr)
118 {
119  std::ostringstream out;
120  out << "forall " << format(expr.univ_var) << " in ["
121  << format(expr.lower_bound) << ", " << format(expr.upper_bound) << "). "
122  << format(expr.body);
123  return out.str();
124 }
125 
128 {
129 public:
130  // string_not contains_constraintt are formula of the form:
131  // forall x in [lb,ub[. p(x) => exists y in [lb,ub[. s0[x+y] != s1[y]
132 
135  exprt univ_bound_sup,
136  exprt premise,
137  exprt exists_bound_inf,
138  exprt exists_bound_sup,
139  const array_string_exprt &s0,
140  const array_string_exprt &s1)
141  : exprt(ID_string_not_contains_constraint)
142  {
143  copy_to_operands(univ_lower_bound, univ_bound_sup, premise);
144  copy_to_operands(exists_bound_inf, exists_bound_sup, s0);
146  };
147 
148  const exprt &univ_lower_bound() const
149  {
150  return op0();
151  }
152 
153  const exprt &univ_upper_bound() const
154  {
155  return op1();
156  }
157 
158  const exprt &premise() const
159  {
160  return op2();
161  }
162 
163  const exprt &exists_lower_bound() const
164  {
165  return op3();
166  }
167 
168  const exprt &exists_upper_bound() const
169  {
170  return operands()[4];
171  }
172 
173  const array_string_exprt &s0() const
174  {
175  return to_array_string_expr(operands()[5]);
176  }
177 
178  const array_string_exprt &s1() const
179  {
180  return to_array_string_expr(operands()[6]);
181  }
182 };
183 
189 inline std::string to_string(const string_not_contains_constraintt &expr)
190 {
191  std::ostringstream out;
192  out << "forall x in [" << format(expr.univ_lower_bound()) << ", "
193  << format(expr.univ_upper_bound()) << "). " << format(expr.premise())
194  << " => ("
195  << "exists y in [" << format(expr.exists_lower_bound()) << ", "
196  << format(expr.exists_upper_bound()) << "). " << format(expr.s0())
197  << "[x+y] != " << format(expr.s1()) << "[y])";
198  return out.str();
199 }
200 
203 {
204  PRECONDITION(expr.id()==ID_string_not_contains_constraint);
206  expr.operands().size()==7,
207  string_refinement_invariantt("string_not_contains_constraintt must have 7 "
208  "operands"));
209  return static_cast<const string_not_contains_constraintt &>(expr);
210 }
211 
214 {
215  PRECONDITION(expr.id()==ID_string_not_contains_constraint);
217  expr.operands().size()==7,
218  string_refinement_invariantt("string_not_contains_constraintt must have 7 "
219  "operands"));
220  return static_cast<string_not_contains_constraintt &>(expr);
221 }
222 
223 #endif
string_constraintt(symbol_exprt _univ_var, exprt lower_bound, exprt upper_bound, exprt body)
Boolean negation.
Definition: std_expr.h:3230
A generic base class for relations, i.e., binary predicates.
Definition: std_expr.h:752
const exprt & univ_lower_bound() const
exprt & op0()
Definition: expr.h:72
string_not_contains_constraintt(exprt univ_lower_bound, exprt univ_bound_sup, exprt premise, exprt exists_bound_inf, exprt exists_bound_sup, const array_string_exprt &s0, const array_string_exprt &s1)
const string_not_contains_constraintt & to_string_not_contains_constraint(const exprt &expr)
void copy_to_operands(const exprt &expr)
Definition: expr.cpp:55
Type for string expressions used by the string solver.
void replace_expr(union_find_replacet &replace_map)
bool replace_expr(exprt &expr) const
Replace subexpressions of expr by a canonical element of the set they belong to.
exprt univ_within_bounds() const
const exprt & exists_lower_bound() const
const irep_idt & id() const
Definition: irep.h:189
Constraints to encode non containement of strings.
boolean AND
Definition: std_expr.h:2255
exprt & op1()
Definition: expr.h:75
#define PRECONDITION(CONDITION)
Definition: invariant.h:230
string_constraintt()=delete
string_constraintt(symbol_exprt univ_var, exprt upper_bound, exprt body)
String expressions for the string solver.
Similar interface to union-find for expressions, with a function for replacing sub-expressions by the...
const exprt & exists_upper_bound() const
Base class for all expressions.
Definition: expr.h:42
std::string to_string(const string_constraintt &expr)
Used for debug printing.
#define string_refinement_invariantt(reason)
Universally quantified string constraint
const exprt & univ_upper_bound() const
Expression to hold a symbol (variable)
Definition: std_expr.h:90
exprt & op2()
Definition: expr.h:78
Abstraction Refinement Loop.
int8_t s1
Definition: bytecode_info.h:59
#define DATA_INVARIANT(CONDITION, REASON)
Definition: invariant.h:257
const array_string_exprt & s0() const
operandst & operands()
Definition: expr.h:66
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
exprt negation() const
array_string_exprt & to_array_string_expr(exprt &expr)
Definition: string_expr.h:162
static format_containert< T > format(const T &o)
Definition: format.h:35
exprt & op3()
Definition: expr.h:81
const array_string_exprt & s1() const