cprover
boolbv_quantifier.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: 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 
19 static bool expr_eq(const exprt &expr1, const exprt &expr2)
20 {
21  return skip_typecast(expr1) == skip_typecast(expr2);
22 }
23 
28 get_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 
82 get_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
187  UNREACHABLE;
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 
246  UNREACHABLE;
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< exprt > eager_quantifier_instantiation(const quantifier_exprt &expr, const namespacet &ns)
static bool expr_eq(const exprt &expr1, const exprt &expr2)
A method to detect equivalence between experts that can contain typecast.
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 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
exprt instantiate(const exprt::operandst &) const
substitute free occurrences of the variables in where() by the given values
Definition: std_expr.cpp:234
variablest & variables()
Definition: std_expr.h:2921
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 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
const binary_relation_exprt & to_binary_relation_expr(const exprt &expr)
Cast an exprt to a binary_relation_exprt.
Definition: std_expr.h:807