cprover
string_constraint.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: String solver
4
5Author: Diffblue Ltd.
6
7\*******************************************************************/
8
9#include "string_constraint.h"
10
11#include <util/namespace.h>
12#include <util/symbol_table.h>
13
16
21static bool cannot_be_neg(const exprt &expr)
22{
23 // this is an internal check, no need for user visibility
25 satcheck_no_simplifiert sat_check(null_message_handler);
26 symbol_tablet symbol_table;
27 namespacet ns(symbol_table);
28 boolbvt solver{ns, sat_check, null_message_handler};
29 const exprt zero = from_integer(0, expr.type());
30 const binary_relation_exprt non_neg(expr, ID_lt, zero);
31 solver << non_neg;
33}
34
36 const symbol_exprt &_univ_var,
37 const exprt &lower_bound,
38 const exprt &upper_bound,
39 const exprt &body)
40 : univ_var(_univ_var),
41 lower_bound(lower_bound),
42 upper_bound(upper_bound),
43 body(body)
44{
47 "String constraints must have non-negative lower bound.\n" +
51 "String constraints must have non-negative upper bound.\n" +
53}
54
59{
60 std::ostringstream out;
61 out << "forall x in [" << format(expr.univ_lower_bound) << ", "
62 << format(expr.univ_upper_bound) << "). " << format(expr.premise)
63 << " => ("
64 << "exists y in [" << format(expr.exists_lower_bound) << ", "
65 << format(expr.exists_upper_bound) << "). " << format(expr.s0)
66 << "[x+y] != " << format(expr.s1) << "[y])";
67 return out.str();
68}
69
71 const union_find_replacet &replace_map,
73{
74 replace_map.replace_expr(constraint.univ_lower_bound);
75 replace_map.replace_expr(constraint.univ_upper_bound);
76 replace_map.replace_expr(constraint.premise);
77 replace_map.replace_expr(constraint.exists_lower_bound);
78 replace_map.replace_expr(constraint.exists_upper_bound);
79 replace_map.replace_expr(constraint.s0);
80 replace_map.replace_expr(constraint.s1);
81}
82
86{
87 return left.univ_upper_bound == right.univ_upper_bound &&
88 left.univ_lower_bound == right.univ_lower_bound &&
91 left.premise == right.premise && left.s0 == right.s0 &&
92 left.s1 == right.s1;
93}
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition: std_expr.h:674
Definition: boolbv.h:44
Base class for all expressions.
Definition: expr.h:54
typet & type()
Return the type of the expression.
Definition: expr.h:82
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:495
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
string_constraintt()=delete
Expression to hold a symbol (variable)
Definition: std_expr.h:80
The symbol table.
Definition: symbol_table.h:14
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
int solver(std::istream &in)
void replace(const union_find_replacet &replace_map, string_not_contains_constraintt &constraint)
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
static bool cannot_be_neg(const exprt &expr)
Runs a solver instance to verify whether an expression can only be non-negative.
bool operator==(const string_not_contains_constraintt &left, const string_not_contains_constraintt &right)
Defines string constraints.
Constraints to encode non containement of strings.
Author: Diffblue Ltd.
null_message_handlert null_message_handler
Definition: message.cpp:14