cprover
Loading...
Searching...
No Matches
string_constraint.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: 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
9Author: 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
54{
55public:
56 // String constraints are of the form
57 // forall univ_var in [lower_bound,upper_bound[. body
62
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
75 from_integer(0, univ_var.type()),
77 body)
78 {
79 }
80
82 {
83 return and_exprt(
86 }
87
89 {
90 replace_map.replace_expr(lower_bound);
91 replace_map.replace_expr(upper_bound);
92 replace_map.replace_expr(body);
93 }
94
96 {
98 }
99};
100
104inline 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
131std::string to_string(const string_not_contains_constraintt &expr);
132
133void replace(
134 const union_find_replacet &replace_map,
136
137bool operator==(
140
141// NOLINTNEXTLINE [allow specialization within 'std']
142namespace std
143{
144template <>
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
STL namespace.
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.