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 
109 inline std::string to_string(const string_constraintt &expr)
110 {
111  std::ostringstream out;
112  out << "forall " << format(expr.univ_var) << " in ["
113  << format(expr.lower_bound) << ", " << format(expr.upper_bound) << "). "
114  << format(expr.body);
115  return out.str();
116 }
117 
126 {
134 };
135 
136 std::string to_string(const string_not_contains_constraintt &expr);
137 
138 void replace(
139  const union_find_replacet &replace_map,
140  string_not_contains_constraintt &constraint);
141 
142 bool operator==(
144  const string_not_contains_constraintt &right);
145 
146 // NOLINTNEXTLINE [allow specialization within 'std']
147 namespace std
148 {
149 template <>
150 // NOLINTNEXTLINE [struct identifier 'hash' does not end in t]
152 {
153  size_t operator()(const string_not_contains_constraintt &constraint) const
154  {
155  return irep_hash()(constraint.univ_lower_bound) ^
156  irep_hash()(constraint.univ_upper_bound) ^
157  irep_hash()(constraint.exists_lower_bound) ^
158  irep_hash()(constraint.exists_upper_bound) ^
159  irep_hash()(constraint.premise) ^ irep_hash()(constraint.s0) ^
160  irep_hash()(constraint.s1);
161  }
162 };
163 }
164 
165 #endif
Boolean negation.
Definition: std_expr.h:3308
A base class for relations, i.e., binary predicates.
Definition: std_expr.h:878
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 the representative element of the set they belong to...
void replace(const union_find_replacet &replace_map, string_not_contains_constraintt &constraint)
bool operator==(const string_not_contains_constraintt &left, const string_not_contains_constraintt &right)
STL namespace.
exprt univ_within_bounds() const
Constraints to encode non containement of strings.
Boolean AND.
Definition: std_expr.h:2409
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...
size_t operator()(const string_not_contains_constraintt &constraint) const
Base class for all expressions.
Definition: expr.h:54
std::string to_string(const string_constraintt &expr)
Used for debug printing.
Universally quantified string constraint
Expression to hold a symbol (variable)
Definition: std_expr.h:143
Abstraction Refinement Loop.
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
exprt negation() const
static format_containert< T > format(const T &o)
Definition: format.h:35