cprover
boolbv_quantifier.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
9#include "boolbv.h"
10
11#include <util/arith_tools.h>
12#include <util/expr_util.h>
13#include <util/invariant.h>
14#include <util/optional.h>
15#include <util/range.h>
16#include <util/simplify_expr.h>
17
19static bool expr_eq(const exprt &expr1, const exprt &expr2)
20{
21 return skip_typecast(expr1) == skip_typecast(expr2);
22}
23
28get_quantifier_var_min(const exprt &var_expr, const exprt &quantifier_expr)
29{
30 if(quantifier_expr.id()==ID_or)
31 {
36 for(auto &x : quantifier_expr.operands())
37 {
38 if(x.id()!=ID_not)
39 continue;
40 exprt y = to_not_expr(x).op();
41 if(y.id()!=ID_ge)
42 continue;
43 const auto &y_binary = to_binary_relation_expr(y);
44 if(
45 expr_eq(var_expr, y_binary.lhs()) && y_binary.rhs().id() == ID_constant)
46 {
47 return to_constant_expr(y_binary.rhs());
48 }
49 }
50
51 if(var_expr.type().id() == ID_unsignedbv)
52 return from_integer(0, var_expr.type());
53 }
54 else if(quantifier_expr.id() == ID_and)
55 {
60 for(auto &x : quantifier_expr.operands())
61 {
62 if(x.id()!=ID_ge)
63 continue;
64 const auto &x_binary = to_binary_relation_expr(x);
65 if(
66 expr_eq(var_expr, x_binary.lhs()) && x_binary.rhs().id() == ID_constant)
67 {
68 return to_constant_expr(x_binary.rhs());
69 }
70 }
71
72 if(var_expr.type().id() == ID_unsignedbv)
73 return from_integer(0, var_expr.type());
74 }
75
76 return {};
77}
78
82get_quantifier_var_max(const exprt &var_expr, const exprt &quantifier_expr)
83{
84 if(quantifier_expr.id()==ID_or)
85 {
90 for(auto &x : quantifier_expr.operands())
91 {
92 if(x.id()!=ID_ge)
93 continue;
94 const auto &x_binary = to_binary_relation_expr(x);
95 if(
96 expr_eq(var_expr, x_binary.lhs()) && x_binary.rhs().id() == ID_constant)
97 {
98 const constant_exprt &over_expr = to_constant_expr(x_binary.rhs());
99
100 mp_integer over_i = numeric_cast_v<mp_integer>(over_expr);
101
107 over_i-=1;
108 return from_integer(over_i, x_binary.rhs().type());
109 }
110 }
111 }
112 else
113 {
118 for(auto &x : quantifier_expr.operands())
119 {
120 if(x.id()!=ID_not)
121 continue;
122 exprt y = to_not_expr(x).op();
123 if(y.id()!=ID_ge)
124 continue;
125 const auto &y_binary = to_binary_relation_expr(y);
126 if(
127 expr_eq(var_expr, y_binary.lhs()) && y_binary.rhs().id() == ID_constant)
128 {
129 const constant_exprt &over_expr = to_constant_expr(y_binary.rhs());
130 mp_integer over_i = numeric_cast_v<mp_integer>(over_expr);
131 over_i-=1;
132 return from_integer(over_i, y_binary.rhs().type());
133 }
134 }
135 }
136
137 return {};
138}
139
141 const quantifier_exprt &expr,
142 const namespacet &ns)
143{
144 if(expr.variables().size() > 1)
145 {
146 // Qx,y.P(x,y) is the same as Qx.Qy.P(x,y)
147 auto new_variables = expr.variables();
148 new_variables.pop_back();
149 auto new_expression = quantifier_exprt(
150 expr.id(),
151 expr.variables().back(),
152 quantifier_exprt(expr.id(), new_variables, expr.where()));
153 return eager_quantifier_instantiation(new_expression, ns);
154 }
155
156 const symbol_exprt &var_expr = expr.symbol();
157
163 const exprt where_simplified = simplify_expr(expr.where(), ns);
164
165 if(where_simplified.is_true() || where_simplified.is_false())
166 {
167 return where_simplified;
168 }
169
170 if(var_expr.is_boolean())
171 {
172 // Expand in full.
173 // This grows worst-case exponentially in the quantifier nesting depth.
174 if(expr.id() == ID_forall)
175 {
176 // ∀b.f(b) <===> f(0)∧f(1)
177 return and_exprt(
178 expr.instantiate({false_exprt()}), expr.instantiate({true_exprt()}));
179 }
180 else if(expr.id() == ID_exists)
181 {
182 // ∃b.f(b) <===> f(0)∨f(1)
183 return or_exprt(
184 expr.instantiate({false_exprt()}), expr.instantiate({true_exprt()}));
185 }
186 else
188 }
189
190 const optionalt<constant_exprt> min_i =
191 get_quantifier_var_min(var_expr, where_simplified);
192 const optionalt<constant_exprt> max_i =
193 get_quantifier_var_max(var_expr, where_simplified);
194
195 if(!min_i.has_value() || !max_i.has_value())
196 return nullopt;
197
198 mp_integer lb = numeric_cast_v<mp_integer>(min_i.value());
199 mp_integer ub = numeric_cast_v<mp_integer>(max_i.value());
200
201 if(lb > ub)
202 return nullopt;
203
204 auto expr_simplified =
205 quantifier_exprt(expr.id(), expr.variables(), where_simplified);
206
207 std::vector<exprt> expr_insts;
208 for(mp_integer i = lb; i <= ub; ++i)
209 {
210 exprt constraint_expr =
211 expr_simplified.instantiate({from_integer(i, var_expr.type())});
212 expr_insts.push_back(constraint_expr);
213 }
214
215 if(expr.id() == ID_forall)
216 {
217 // maintain the domain constraint if it isn't guaranteed
218 // by the instantiations (for a disjunction the domain
219 // constraint is implied by the instantiations)
220 if(where_simplified.id() == ID_and)
221 {
222 expr_insts.push_back(binary_predicate_exprt(
223 var_expr, ID_gt, from_integer(lb, var_expr.type())));
224 expr_insts.push_back(binary_predicate_exprt(
225 var_expr, ID_le, from_integer(ub, var_expr.type())));
226 }
227
228 return simplify_expr(conjunction(expr_insts), ns);
229 }
230 else if(expr.id() == ID_exists)
231 {
232 // maintain the domain constraint if it isn't trivially satisfied
233 // by the instantiations (for a conjunction the instantiations are
234 // stronger constraints)
235 if(where_simplified.id() == ID_or)
236 {
237 expr_insts.push_back(binary_predicate_exprt(
238 var_expr, ID_gt, from_integer(lb, var_expr.type())));
239 expr_insts.push_back(binary_predicate_exprt(
240 var_expr, ID_le, from_integer(ub, var_expr.type())));
241 }
242
243 return simplify_expr(disjunction(expr_insts), ns);
244 }
245
247}
248
250{
251 PRECONDITION(src.id() == ID_forall || src.id() == ID_exists);
252
253 // We first worry about the scoping of the symbols bound by the quantifier.
254 auto fresh_symbols = fresh_binding(src);
255
256 // replace in where()
257 auto where_replaced = src.instantiate(fresh_symbols);
258
259 // produce new quantifier expression
260 auto new_src =
261 quantifier_exprt(src.id(), std::move(fresh_symbols), where_replaced);
262
263 const auto res = eager_quantifier_instantiation(src, ns);
264
265 if(res)
266 return convert_bool(*res);
267
268 // we failed to instantiate here, need to pass to post-processing
269 quantifier_list.emplace_back(quantifiert(src, prop.new_variable()));
270
271 return quantifier_list.back().l;
272}
273
275{
276 if(quantifier_list.empty())
277 return;
278
279 // we do not yet have any elaborate post-processing
280 for(const auto &q : quantifier_list)
281 conversion_failed(q.expr);
282}
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
static optionalt< constant_exprt > get_quantifier_var_min(const exprt &var_expr, const exprt &quantifier_expr)
To obtain the min value for the quantifier variable of the specified forall/exists operator.
static bool expr_eq(const exprt &expr1, const exprt &expr2)
A method to detect equivalence between experts that can contain typecast.
static optionalt< exprt > eager_quantifier_instantiation(const quantifier_exprt &expr, const namespacet &ns)
static optionalt< constant_exprt > get_quantifier_var_max(const exprt &var_expr, const exprt &quantifier_expr)
To obtain the max value for the quantifier variable of the specified forall/exists operator.
Boolean AND.
Definition: std_expr.h:1974
const namespacet & ns
Definition: arrays.h:56
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two argu...
Definition: std_expr.h:643
exprt & where()
Definition: std_expr.h:2931
variablest & variables()
Definition: std_expr.h:2921
exprt instantiate(const exprt::operandst &) const
substitute free occurrences of the variables in where() by the given values
Definition: std_expr.cpp:234
binding_exprt::variablest fresh_binding(const binding_exprt &)
create new, unique variables for the given binding
Definition: boolbv.cpp:566
void finish_eager_conversion_quantifiers()
virtual literalt convert_quantifier(const quantifier_exprt &expr)
bvt conversion_failed(const exprt &expr)
Print that the expression of x has failed conversion, then return a vector of x's width.
Definition: boolbv.cpp:84
quantifier_listt quantifier_list
Definition: boolbv.h:270
A constant literal expression.
Definition: std_expr.h:2807
Base class for all expressions.
Definition: expr.h:54
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:33
bool is_boolean() const
Return whether the expression represents a Boolean.
Definition: expr.cpp:51
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:42
typet & type()
Return the type of the expression.
Definition: expr.h:82
operandst & operands()
Definition: expr.h:92
const irep_idt & id() const
Definition: irep.h:396
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
Boolean OR.
Definition: std_expr.h:2082
virtual literalt convert_bool(const exprt &expr)
virtual literalt new_variable()=0
A base class for quantifier expressions.
symbol_exprt & symbol()
Expression to hold a symbol (variable)
Definition: std_expr.h:80
const exprt & op() const
Definition: std_expr.h:293
const exprt & skip_typecast(const exprt &expr)
find the expression nested inside typecasts, if any
Definition: expr_util.cpp:216
Deprecated expression utility functions.
nonstd::optional< T > optionalt
Definition: optional.h:35
Ranges: pair of begin and end iterators, which can be initialized from containers,...
exprt simplify_expr(exprt src, const namespacet &ns)
BigInt mp_integer
Definition: smt_terms.h:12
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:503
#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:34
exprt disjunction(const exprt::operandst &op)
1) generates a disjunction for two or more operands 2) for one operand, returns the operand 3) return...
Definition: std_expr.cpp:22
const binary_relation_exprt & to_binary_relation_expr(const exprt &expr)
Cast an exprt to a binary_relation_exprt.
Definition: std_expr.h:807
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:2840
const not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_exprt.
Definition: std_expr.h:2206