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 <util/format_expr.h>
24 #include <util/string_expr.h>
26 
53 class string_constraintt final
54 {
55 public:
56  // String constraints are of the form
57  // forall univ_var in [lower_bound,upper_bound[. body
62 
63  string_constraintt() = delete;
64 
66  const symbol_exprt &_univ_var,
67  const exprt &lower_bound,
68  const exprt &upper_bound,
69  const exprt &body);
70 
71  // Default bound inferior is 0
74  univ_var,
75  from_integer(0, univ_var.type()),
77  body)
78  {
79  }
80 
82  {
83  return and_exprt(
86  }
87 
88  void replace_expr(union_find_replacet &replace_map)
89  {
90  replace_map.replace_expr(lower_bound);
91  replace_map.replace_expr(upper_bound);
92  replace_map.replace_expr(body);
93  }
94 
95  exprt negation() const
96  {
98  }
99 };
100 
104 inline std::string to_string(const string_constraintt &expr)
105 {
106  std::ostringstream out;
107  out << "forall " << format(expr.univ_var) << " in ["
108  << format(expr.lower_bound) << ", " << format(expr.upper_bound) << "). "
109  << format(expr.body);
110  return out.str();
111 }
112 
121 {
129 };
130 
131 std::string to_string(const string_not_contains_constraintt &expr);
132 
133 void replace(
134  const union_find_replacet &replace_map,
135  string_not_contains_constraintt &constraint);
136 
137 bool operator==(
139  const string_not_contains_constraintt &right);
140 
141 // NOLINTNEXTLINE [allow specialization within 'std']
142 namespace std
143 {
144 template <>
145 // NOLINTNEXTLINE [struct identifier 'hash' does not end in t]
147 {
148  size_t operator()(const string_not_contains_constraintt &constraint) const
149  {
150  return irep_hash()(constraint.univ_lower_bound) ^
151  irep_hash()(constraint.univ_upper_bound) ^
152  irep_hash()(constraint.exists_lower_bound) ^
153  irep_hash()(constraint.exists_upper_bound) ^
154  irep_hash()(constraint.premise) ^ irep_hash()(constraint.s0) ^
155  irep_hash()(constraint.s1);
156  }
157 };
158 } // namespace std
159 
160 #endif
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
Boolean AND.
Definition: std_expr.h:1974
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition: std_expr.h:674
Base class for all expressions.
Definition: expr.h:54
Boolean negation.
Definition: std_expr.h:2181
string_constraintt()=delete
void replace_expr(union_find_replacet &replace_map)
exprt univ_within_bounds() const
string_constraintt(symbol_exprt univ_var, exprt upper_bound, exprt body)
exprt negation() const
Expression to hold a symbol (variable)
Definition: std_expr.h:80
Similar interface to union-find for expressions, with a function for replacing sub-expressions by the...
bool replace_expr(exprt &expr) const
Replace subexpressions of expr by the representative element of the set they belong to.
static format_containert< T > format(const T &o)
Definition: format.h:37
void replace(const union_find_replacet &replace_map, string_not_contains_constraintt &constraint)
std::string to_string(const string_constraintt &expr)
Used for debug printing.
bool operator==(const string_not_contains_constraintt &left, const string_not_contains_constraintt &right)
String expressions for the string solver.
size_t operator()(const string_not_contains_constraintt &constraint) const
Constraints to encode non containement of strings.