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 }
static bool cannot_be_neg(const exprt &expr)
Runs a solver instance to verify whether an expression can only be.
A generic base class for relations, i.e., binary predicates.
Definition: std_expr.h:752
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:641
typet & type()
Definition: expr.h:56
#define INVARIANT(CONDITION, REASON)
Definition: invariant.h:204
Definition: boolbv.h:31
Defines string constraints.
int solver(std::istream &in)
The symbol table.
Definition: symbol_table.h:19
TO_BE_DOCUMENTED.
Definition: namespace.h:74
Author: Diffblue Ltd.
string_constraintt()=delete
Base class for all expressions.
Definition: expr.h:42
Expression to hold a symbol (variable)
Definition: std_expr.h:90
constant_exprt from_integer(const mp_integer &int_value, const typet &type)