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  const symbol_exprt &_univ_var,
72  const exprt &lower_bound,
73  const exprt &upper_bound,
74  const exprt &body);
75 
76  // Default bound inferior is 0
79  univ_var,
80  from_integer(0, univ_var.type()),
82  body)
83  {
84  }
85 
87  {
88  return and_exprt(
91  }
92 
93  void replace_expr(union_find_replacet &replace_map)
94  {
95  replace_map.replace_expr(lower_bound);
96  replace_map.replace_expr(upper_bound);
97  replace_map.replace_expr(body);
98  }
99 
100  exprt negation() const
101  {
103  }
104 };
105 
111 inline std::string to_string(const string_constraintt &expr)
112 {
113  std::ostringstream out;
114  out << "forall " << format(expr.univ_var) << " in ["
115  << format(expr.lower_bound) << ", " << format(expr.upper_bound) << "). "
116  << format(expr.body);
117  return out.str();
118 }
119 
122 {
123 public:
124  // string_not contains_constraintt are formula of the form:
125  // forall x in [lb,ub[. p(x) => exists y in [lb,ub[. s0[x+y] != s1[y]
126 
129  exprt univ_bound_sup,
130  exprt premise,
131  exprt exists_bound_inf,
132  exprt exists_bound_sup,
133  const array_string_exprt &s0,
134  const array_string_exprt &s1)
135  : exprt(ID_string_not_contains_constraint)
136  {
137  copy_to_operands(univ_lower_bound, univ_bound_sup, premise);
138  copy_to_operands(exists_bound_inf, exists_bound_sup, s0);
140  };
141 
142  const exprt &univ_lower_bound() const
143  {
144  return op0();
145  }
146 
147  const exprt &univ_upper_bound() const
148  {
149  return op1();
150  }
151 
152  const exprt &premise() const
153  {
154  return op2();
155  }
156 
157  const exprt &exists_lower_bound() const
158  {
159  return op3();
160  }
161 
162  const exprt &exists_upper_bound() const
163  {
164  return operands()[4];
165  }
166 
167  const array_string_exprt &s0() const
168  {
169  return to_array_string_expr(operands()[5]);
170  }
171 
172  const array_string_exprt &s1() const
173  {
174  return to_array_string_expr(operands()[6]);
175  }
176 };
177 
183 inline std::string to_string(const string_not_contains_constraintt &expr)
184 {
185  std::ostringstream out;
186  out << "forall x in [" << format(expr.univ_lower_bound()) << ", "
187  << format(expr.univ_upper_bound()) << "). " << format(expr.premise())
188  << " => ("
189  << "exists y in [" << format(expr.exists_lower_bound()) << ", "
190  << format(expr.exists_upper_bound()) << "). " << format(expr.s0())
191  << "[x+y] != " << format(expr.s1()) << "[y])";
192  return out.str();
193 }
194 
197 {
198  PRECONDITION(expr.id()==ID_string_not_contains_constraint);
200  expr.operands().size()==7,
201  string_refinement_invariantt("string_not_contains_constraintt must have 7 "
202  "operands"));
203  return static_cast<const string_not_contains_constraintt &>(expr);
204 }
205 
208 {
209  PRECONDITION(expr.id()==ID_string_not_contains_constraint);
211  expr.operands().size()==7,
212  string_refinement_invariantt("string_not_contains_constraintt must have 7 "
213  "operands"));
214  return static_cast<string_not_contains_constraintt &>(expr);
215 }
216 
217 #endif
Boolean negation.
Definition: std_expr.h:3228
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:259
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:242
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:278
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