cprover
string_constraint.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3  Module: String solver
4 
5  Author: Diffblue Ltd.
6 
7 \*******************************************************************/
8 
9 #include "string_constraint.h"
10 
11 #include <solvers/sat/satcheck.h>
12 #include <util/symbol_table.h>
13 
15 // non-negative.
18 static bool cannot_be_neg(const exprt &expr)
19 {
20  satcheck_no_simplifiert sat_check;
21  symbol_tablet symbol_table;
22  namespacet ns(symbol_table);
23  boolbvt solver(ns, sat_check);
24  const exprt zero = from_integer(0, expr.type());
25  const binary_relation_exprt non_neg(expr, ID_lt, zero);
26  solver << non_neg;
28 }
29 
31  const symbol_exprt &_univ_var,
32  const exprt &lower_bound,
33  const exprt &upper_bound,
34  const exprt &body)
35  : univ_var(_univ_var),
36  lower_bound(lower_bound),
37  upper_bound(upper_bound),
38  body(body)
39 {
40  INVARIANT(
42  "String constraints must have non-negative lower bound.\n" +
44  INVARIANT(
46  "String constraints must have non-negative upper bound.\n" +
48 }
49 
54 {
55  std::ostringstream out;
56  out << "forall x in [" << format(expr.univ_lower_bound) << ", "
57  << format(expr.univ_upper_bound) << "). " << format(expr.premise)
58  << " => ("
59  << "exists y in [" << format(expr.exists_lower_bound) << ", "
60  << format(expr.exists_upper_bound) << "). " << format(expr.s0)
61  << "[x+y] != " << format(expr.s1) << "[y])";
62  return out.str();
63 }
64 
65 void replace(
66  const union_find_replacet &replace_map,
68 {
69  replace_map.replace_expr(constraint.univ_lower_bound);
70  replace_map.replace_expr(constraint.univ_upper_bound);
71  replace_map.replace_expr(constraint.premise);
72  replace_map.replace_expr(constraint.exists_lower_bound);
73  replace_map.replace_expr(constraint.exists_upper_bound);
74  replace_map.replace_expr(constraint.s0);
75  replace_map.replace_expr(constraint.s1);
76 }
77 
81 {
82  return left.univ_upper_bound == right.univ_upper_bound &&
83  left.univ_lower_bound == right.univ_lower_bound &&
84  left.exists_lower_bound == right.exists_lower_bound &&
85  left.exists_upper_bound == right.exists_upper_bound &&
86  left.premise == right.premise && left.s0 == right.s0 &&
87  left.s1 == right.s1;
88 }
format
static format_containert< T > format(const T &o)
Definition: format.h:35
symbol_tablet
The symbol table.
Definition: symbol_table.h:19
string_constraintt::string_constraintt
string_constraintt()=delete
string_not_contains_constraintt::univ_upper_bound
exprt univ_upper_bound
Definition: string_constraint.h:128
irept::pretty
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:640
decision_proceduret::resultt::D_UNSATISFIABLE
replace
void replace(const union_find_replacet &replace_map, string_not_contains_constraintt &constraint)
Definition: string_constraint.cpp:65
union_find_replacet::replace_expr
bool replace_expr(exprt &expr) const
Replace subexpressions of expr by the representative element of the set they belong to.
Definition: union_find_replace.cpp:28
exprt
Base class for all expressions.
Definition: expr.h:54
to_string
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Definition: string_constraint.cpp:53
string_not_contains_constraintt::exists_upper_bound
exprt exists_upper_bound
Definition: string_constraint.h:131
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:143
string_not_contains_constraintt::premise
exprt premise
Definition: string_constraint.h:129
string_constraintt::upper_bound
exprt upper_bound
Definition: string_constraint.h:65
string_constraintt::lower_bound
exprt lower_bound
Definition: string_constraint.h:64
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:68
string_not_contains_constraintt::exists_lower_bound
exprt exists_lower_bound
Definition: string_constraint.h:130
string_not_contains_constraintt::univ_lower_bound
exprt univ_lower_bound
Definition: string_constraint.h:127
satcheck.h
string_constraint.h
union_find_replacet
Similar interface to union-find for expressions, with a function for replacing sub-expressions by the...
Definition: union_find_replace.h:16
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:123
solver
int solver(std::istream &in)
Definition: smt2_solver.cpp:360
binary_relation_exprt
A base class for relations, i.e., binary predicates.
Definition: std_expr.h:878
string_not_contains_constraintt::s0
array_string_exprt s0
Definition: string_constraint.h:132
cannot_be_neg
static bool cannot_be_neg(const exprt &expr)
Runs a solver instance to verify whether an expression can only be.
Definition: string_constraint.cpp:18
boolbvt
Definition: boolbv.h:32
string_not_contains_constraintt
Constraints to encode non containement of strings.
Definition: string_constraint.h:125
operator==
bool operator==(const string_not_contains_constraintt &left, const string_not_contains_constraintt &right)
Definition: string_constraint.cpp:78
symbol_table.h
Author: Diffblue Ltd.
string_not_contains_constraintt::s1
array_string_exprt s1
Definition: string_constraint.h:133
validation_modet::INVARIANT