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 <langapi/language_ui.h>
26 
28 {
29 public:
30  // String constraints are of the form
31  // forall univ_var in [lower_bound,upper_bound[. premise => body
32 
33  const exprt &premise() const
34  {
35  return op0();
36  }
37 
38  const exprt &body() const
39  {
40  return op1();
41  }
42 
43  const symbol_exprt &univ_var() const
44  {
45  return to_symbol_expr(op2());
46  }
47 
48  const exprt &upper_bound() const
49  {
50  return op3();
51  }
52 
53  const exprt &lower_bound() const
54  {
55  return operands()[4];
56  }
57 
58 
59  private:
61 
62  public:
64  const symbol_exprt &_univ_var,
65  const exprt &bound_inf,
66  const exprt &bound_sup,
67  const exprt &prem,
68  const exprt &body):
69  exprt(ID_string_constraint)
70  {
71  copy_to_operands(prem, body);
72  copy_to_operands(_univ_var, bound_sup, bound_inf);
73  }
74 
75  // Default bound inferior is 0
77  const symbol_exprt &_univ_var,
78  const exprt &bound_sup,
79  const exprt &prem,
80  const exprt &body):
82  _univ_var,
83  from_integer(0, _univ_var.type()),
84  bound_sup,
85  prem,
86  body)
87  {}
88 
89  // Default premise is true
91  const symbol_exprt &_univ_var,
92  const exprt &bound_sup,
93  const exprt &body):
94  string_constraintt(_univ_var, bound_sup, true_exprt(), body)
95  {}
96 
98  {
99  return and_exprt(
102  }
103 };
104 
105 extern inline const string_constraintt &to_string_constraint(const exprt &expr)
106 {
107  assert(expr.id()==ID_string_constraint && expr.operands().size()==5);
108  return static_cast<const string_constraintt &>(expr);
109 }
110 
112 {
113  assert(expr.id()==ID_string_constraint && expr.operands().size()==5);
114  return static_cast<string_constraintt &>(expr);
115 }
116 
118 {
119 public:
120  // string_not contains_constraintt are formula of the form:
121  // forall x in [lb,ub[. p(x) => exists y in [lb,ub[. s0[x+y] != s1[y]
122 
125  exprt univ_bound_sup,
126  exprt premise,
127  exprt exists_bound_inf,
128  exprt exists_bound_sup,
129  const string_exprt &s0,
130  const string_exprt &s1):
131  exprt(ID_string_not_contains_constraint)
132  {
133  copy_to_operands(univ_lower_bound, univ_bound_sup, premise);
134  copy_to_operands(exists_bound_inf, exists_bound_sup, s0);
136  };
137 
138  const exprt &univ_lower_bound() const
139  {
140  return op0();
141  }
142 
143  const exprt &univ_upper_bound() const
144  {
145  return op1();
146  }
147 
148  const exprt &premise() const
149  {
150  return op2();
151  }
152 
153  const exprt &exists_lower_bound() const
154  {
155  return op3();
156  }
157 
158  const exprt &exists_upper_bound() const
159  {
160  return operands()[4];
161  }
162 
163  const string_exprt &s0() const
164  {
165  return to_string_expr(operands()[5]);
166  }
167 
168  const string_exprt &s1() const
169  {
170  return to_string_expr(operands()[6]);
171  }
172 };
173 
176 {
177  assert(expr.id()==ID_string_not_contains_constraint);
178  assert(expr.operands().size()==7);
179  return static_cast<const string_not_contains_constraintt &>(expr);
180 }
181 
184 {
185  assert(expr.id()==ID_string_not_contains_constraint);
186  assert(expr.operands().size()==7);
187  return static_cast<string_not_contains_constraintt &>(expr);
188 }
189 
190 #endif
string_constraintt(const symbol_exprt &_univ_var, const exprt &bound_sup, const exprt &prem, const exprt &body)
string_constraintt(const symbol_exprt &_univ_var, const exprt &bound_sup, const exprt &body)
A generic base class for relations, i.e., binary predicates.
Definition: std_expr.h:568
const exprt & univ_lower_bound() const
string_exprt & to_string_expr(exprt &expr)
Definition: string_expr.h:133
exprt & op0()
Definition: expr.h:84
const string_not_contains_constraintt & to_string_not_contains_constraint(const exprt &expr)
void copy_to_operands(const exprt &expr)
Definition: expr.cpp:61
Type for string expressions used by the string solver.
const symbol_exprt & univ_var() const
typet & type()
Definition: expr.h:60
exprt univ_within_bounds() const
const exprt & upper_bound() const
const exprt & exists_lower_bound() const
const irep_idt & id() const
Definition: irep.h:189
The boolean constant true.
Definition: std_expr.h:3742
string_constraintt(const symbol_exprt &_univ_var, const exprt &bound_inf, const exprt &bound_sup, const exprt &prem, const exprt &body)
const exprt & lower_bound() const
boolean AND
Definition: std_expr.h:1852
exprt & op1()
Definition: expr.h:87
string_not_contains_constraintt(exprt univ_lower_bound, exprt univ_bound_sup, exprt premise, exprt exists_bound_inf, exprt exists_bound_sup, const string_exprt &s0, const string_exprt &s1)
const exprt & exists_upper_bound() const
Base class for all expressions.
Definition: expr.h:46
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
Definition: std_expr.h:202
const exprt & univ_upper_bound() const
Expression to hold a symbol (variable)
Definition: std_expr.h:82
exprt & op2()
Definition: expr.h:90
Abstraction Refinement Loop.
int8_t s1
Definition: bytecode_info.h:59
const string_constraintt & to_string_constraint(const exprt &expr)
operandst & operands()
Definition: expr.h:70
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
const exprt & premise() const
const exprt & body() const
const string_exprt & s0() const
const string_exprt & s1() const
exprt & op3()
Definition: expr.h:93