cprover
Loading...
Searching...
No Matches
string_constraint_instantiation.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Defines functions related to string constraints.
4
5Author: Jesse Sigal, jesse.sigal@diffblue.com
6
7\*******************************************************************/
8
11
13#include <algorithm>
14#include <unordered_set>
15
16#include <util/arith_tools.h>
17#include <util/expr_iterator.h>
18#include <util/format_expr.h>
19
20#include "string_constraint.h"
21
24static bool contains(const exprt &index, const symbol_exprt &qvar)
25{
26 return std::find(index.depth_begin(), index.depth_end(), qvar) !=
27 index.depth_end();
28}
29
37static std::unordered_set<exprt, irep_hash>
38find_indexes(const exprt &expr, const exprt &str, const symbol_exprt &qvar)
39{
40 decltype(find_indexes(expr, str, qvar)) result;
41 auto index_str_containing_qvar = [&](const exprt &e) {
42 if(auto index_expr = expr_try_dynamic_cast<index_exprt>(e))
43 {
44 const auto &arr = index_expr->array();
45 const auto str_it = std::find(arr.depth_begin(), arr.depth_end(), str);
46 return str_it != arr.depth_end() && contains(index_expr->index(), qvar);
47 }
48 return false;
49 };
50
51 std::for_each(expr.depth_begin(), expr.depth_end(), [&](const exprt &e) {
52 if(index_str_containing_qvar(e))
53 result.insert(to_index_expr(e).index());
54 });
55 return result;
56}
57
59{
60 type = f.type();
61 // list of expressions to process with a boolean flag telling whether they
62 // appear positively or negatively (true is for positive)
63 std::list<std::pair<exprt, bool>> to_process;
64 to_process.emplace_back(f, true);
65
66 while(!to_process.empty())
67 {
68 const exprt cur = to_process.back().first;
69 bool positive = to_process.back().second;
70 to_process.pop_back();
71 if(auto integer = numeric_cast<mp_integer>(cur))
72 {
73 constant_coefficient += positive ? integer.value() : -integer.value();
74 }
75 else if(cur.id() == ID_plus)
76 {
77 for(const auto &op : cur.operands())
78 to_process.emplace_back(op, positive);
79 }
80 else if(cur.id() == ID_minus)
81 {
82 to_process.emplace_back(to_minus_expr(cur).op1(), !positive);
83 to_process.emplace_back(to_minus_expr(cur).op0(), positive);
84 }
85 else if(cur.id() == ID_unary_minus)
86 {
87 to_process.emplace_back(to_unary_minus_expr(cur).op(), !positive);
88 }
89 else
90 {
91 if(positive)
92 ++coefficients[cur];
93 else
94 --coefficients[cur];
95 }
96 }
97}
98
100{
101 PRECONDITION(type == other.type);
103 for(auto pair : other.coefficients)
104 coefficients[pair.first] += pair.second;
105}
106
107exprt linear_functiont::to_expr(bool negated) const
108{
109 exprt sum = nil_exprt{};
110 const exprt constant_expr = from_integer(constant_coefficient, type);
111 if(constant_coefficient != 0)
112 sum = negated ? (exprt)unary_minus_exprt{constant_expr} : constant_expr;
113
114 for(const auto &term : coefficients)
115 {
116 const exprt &t = term.first;
117 const mp_integer factor = negated ? (-term.second) : term.second;
118 if(factor == -1)
119 {
120 if(sum.is_nil())
121 sum = unary_minus_exprt(t);
122 else
123 sum = minus_exprt(sum, t);
124 }
125 else if(factor == 1)
126 {
127 if(sum.is_nil())
128 sum = t;
129 else
130 sum = plus_exprt(sum, t);
131 }
132 else if(factor != 0)
133 {
134 const mult_exprt to_add{t, from_integer(factor, t.type())};
135 if(sum.is_nil())
136 sum = to_add;
137 else
138 sum = plus_exprt(sum, to_add);
139 }
140 }
141 return sum.is_nil() ? from_integer(0, type) : sum;
142}
143
146 const exprt &var,
147 const exprt &val)
148{
149 auto it = f.coefficients.find(var);
150 PRECONDITION(it != f.coefficients.end());
151 PRECONDITION(it->second == 1 || it->second == -1);
152 const bool positive = it->second == 1;
153
154 // Transform `f` into `f(var <- 0)`
155 f.coefficients.erase(it);
156 // Transform `f(var <- 0)` into `f(var <- 0) - val`
158
159 // If the coefficient of var is 1 then solution `val - f(var <- 0),
160 // otherwise `f(var <- 0) - val`
161 return f.to_expr(positive);
162}
163
165{
166 std::ostringstream stream;
167 stream << constant_coefficient;
168 for(const auto &pair : coefficients)
169 stream << " + " << pair.second << " * " << ::format(pair.first);
170 return stream.str();
171}
172
174 const string_constraintt &axiom,
175 const exprt &str,
176 const exprt &val)
177{
178 exprt::operandst conjuncts;
179 for(const auto &index : find_indexes(axiom.body, str, axiom.univ_var))
180 {
181 const exprt univ_var_value =
183 implies_exprt instance(
184 and_exprt(
185 binary_relation_exprt(axiom.univ_var, ID_ge, axiom.lower_bound),
186 binary_relation_exprt(axiom.univ_var, ID_lt, axiom.upper_bound)),
187 axiom.body);
188 replace_expr(axiom.univ_var, univ_var_value, instance);
189 conjuncts.push_back(instance);
190 }
191 return conjunction(conjuncts);
192}
193
201std::vector<exprt> instantiate_not_contains(
203 const std::set<std::pair<exprt, exprt>> &index_pairs,
204 const std::unordered_map<string_not_contains_constraintt, symbol_exprt>
205 &witnesses)
206{
207 std::vector<exprt> lemmas;
208
209 const array_string_exprt s0 = axiom.s0;
210 const array_string_exprt s1 = axiom.s1;
211
212 for(const auto &pair : index_pairs)
213 {
214 // We have s0[x+f(x)] and s1[f(x)], so to have i0 indexing s0 and i1
215 // indexing s1, we need x = i0 - i1 and f(i0 - i1) = f(x) = i1.
216 const exprt &i0 = pair.first;
217 const exprt &i1 = pair.second;
218 const minus_exprt val(i0, i1);
219 const and_exprt universal_bound(
220 binary_relation_exprt(axiom.univ_lower_bound, ID_le, val),
221 binary_relation_exprt(axiom.univ_upper_bound, ID_gt, val));
222 const exprt f = index_exprt(witnesses.at(axiom), val);
223 const equal_exprt relevancy(f, i1);
224 const and_exprt premise(relevancy, axiom.premise, universal_bound);
225
226 const notequal_exprt differ(s0[i0], s1[i1]);
227 const and_exprt existential_bound(
229 binary_relation_exprt(axiom.exists_upper_bound, ID_gt, i1));
230 const and_exprt body(differ, existential_bound);
231
232 const implies_exprt lemma(premise, body);
233 lemmas.push_back(lemma);
234 }
235
236 return lemmas;
237}
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
optionalt< Target > numeric_cast(const exprt &arg)
Converts an expression to any integral type.
int8_t s1
Boolean AND.
Definition std_expr.h:2071
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition std_expr.h:707
Equality.
Definition std_expr.h:1306
Base class for all expressions.
Definition expr.h:56
std::vector< exprt > operandst
Definition expr.h:58
depth_iteratort depth_end()
Definition expr.cpp:249
depth_iteratort depth_begin()
Definition expr.cpp:247
typet & type()
Return the type of the expression.
Definition expr.h:84
Boolean implication.
Definition std_expr.h:2134
Array index operator.
Definition std_expr.h:1410
const irep_idt & id() const
Definition irep.h:396
bool is_nil() const
Definition irep.h:376
Canonical representation of linear function, for instance, expression $x + x - y + 5 - 3$ would given...
exprt to_expr(bool negated=false) const
linear_functiont(const exprt &f)
Put an expression f composed of additions and subtractions into its cannonical representation.
std::unordered_map< exprt, mp_integer, irep_hash > coefficients
std::string format()
Format the linear function as a string, can be used for debugging.
void add(const linear_functiont &other)
Make this function the sum of the current function with other.
static exprt solve(linear_functiont f, const exprt &var, const exprt &val)
Return an expression y such that f(var <- y) = val.
Binary minus.
Definition std_expr.h:1006
Binary multiplication Associativity is not specified.
Definition std_expr.h:1052
The NIL expression.
Definition std_expr.h:3026
Disequality.
Definition std_expr.h:1365
The plus expression Associativity is not specified.
Definition std_expr.h:947
std::vector< exprt > instantiate_not_contains(const string_not_contains_constraintt &axiom, const std::set< std::pair< exprt, exprt > > &index_pairs, const std::unordered_map< string_not_contains_constraintt, symbol_exprt > &witnesses)
Instantiates a quantified formula representing not_contains by substituting the quantifiers and gener...
Expression to hold a symbol (variable)
Definition std_expr.h:113
The unary minus expression.
Definition std_expr.h:423
auto expr_try_dynamic_cast(TExpr &base) -> typename detail::expr_try_dynamic_cast_return_typet< T, TExpr >::type
Try to cast a reference to a generic exprt to a specific derived class.
Definition expr_cast.h:81
Forward depth-first search iterators These iterators' copy operations are expensive,...
bool replace_expr(const exprt &what, const exprt &by, exprt &dest)
BigInt mp_integer
Definition smt_terms.h:18
#define PRECONDITION(CONDITION)
Definition invariant.h:463
exprt conjunction(const exprt::operandst &op)
1) generates a conjunction for two or more operands 2) for one operand, returns the operand 3) return...
Definition std_expr.cpp:63
const minus_exprt & to_minus_expr(const exprt &expr)
Cast an exprt to a minus_exprt.
Definition std_expr.h:1031
const unary_minus_exprt & to_unary_minus_expr(const exprt &expr)
Cast an exprt to a unary_minus_exprt.
Definition std_expr.h:453
Defines string constraints.
static bool contains(const exprt &index, const symbol_exprt &qvar)
Look for symbol qvar in the expression index and return true if found.
exprt instantiate(const string_constraintt &axiom, const exprt &str, const exprt &val)
Instantiates a string constraint by substituting the quantifiers.
Defines related function for string constraints.
Constraints to encode non containement of strings.