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/replace_expr.h>
17 #include <util/simplify_expr.h>
18 
20 static bool expr_eq(const exprt &expr1, const exprt &expr2)
21 {
22  return skip_typecast(expr1) == skip_typecast(expr2);
23 }
24 
29 get_quantifier_var_min(const exprt &var_expr, const exprt &quantifier_expr)
30 {
31  if(quantifier_expr.id()==ID_or)
32  {
37  for(auto &x : quantifier_expr.operands())
38  {
39  if(x.id()!=ID_not)
40  continue;
41  exprt y = to_not_expr(x).op();
42  if(y.id()!=ID_ge)
43  continue;
44  const auto &y_binary = to_binary_relation_expr(y);
45  if(
46  expr_eq(var_expr, y_binary.lhs()) && y_binary.rhs().id() == ID_constant)
47  {
48  return to_constant_expr(y_binary.rhs());
49  }
50  }
51  }
52  else if(quantifier_expr.id() == ID_and)
53  {
58  for(auto &x : quantifier_expr.operands())
59  {
60  if(x.id()!=ID_ge)
61  continue;
62  const auto &x_binary = to_binary_relation_expr(x);
63  if(
64  expr_eq(var_expr, x_binary.lhs()) && x_binary.rhs().id() == ID_constant)
65  {
66  return to_constant_expr(x_binary.rhs());
67  }
68  }
69  }
70 
71  return {};
72 }
73 
77 get_quantifier_var_max(const exprt &var_expr, const exprt &quantifier_expr)
78 {
79  if(quantifier_expr.id()==ID_or)
80  {
85  for(auto &x : quantifier_expr.operands())
86  {
87  if(x.id()!=ID_ge)
88  continue;
89  const auto &x_binary = to_binary_relation_expr(x);
90  if(
91  expr_eq(var_expr, x_binary.lhs()) && x_binary.rhs().id() == ID_constant)
92  {
93  const constant_exprt &over_expr = to_constant_expr(x_binary.rhs());
94 
95  mp_integer over_i = numeric_cast_v<mp_integer>(over_expr);
96 
102  over_i-=1;
103  return from_integer(over_i, x_binary.rhs().type());
104  }
105  }
106  }
107  else
108  {
113  for(auto &x : quantifier_expr.operands())
114  {
115  if(x.id()!=ID_not)
116  continue;
117  exprt y = to_not_expr(x).op();
118  if(y.id()!=ID_ge)
119  continue;
120  const auto &y_binary = to_binary_relation_expr(y);
121  if(
122  expr_eq(var_expr, y_binary.lhs()) && y_binary.rhs().id() == ID_constant)
123  {
124  const constant_exprt &over_expr = to_constant_expr(y_binary.rhs());
125  mp_integer over_i = numeric_cast_v<mp_integer>(over_expr);
126  over_i-=1;
127  return from_integer(over_i, y_binary.rhs().type());
128  }
129  }
130  }
131 
132  return {};
133 }
134 
135 static optionalt<exprt>
137 {
138  const symbol_exprt &var_expr = expr.symbol();
139 
145  const exprt re = simplify_expr(expr.where(), ns);
146 
147  if(re.is_true() || re.is_false())
148  {
149  return re;
150  }
151 
152  const optionalt<constant_exprt> min_i = get_quantifier_var_min(var_expr, re);
153  const optionalt<constant_exprt> max_i = get_quantifier_var_max(var_expr, re);
154 
155  if(!min_i.has_value() || !max_i.has_value())
156  return nullopt;
157 
158  mp_integer lb = numeric_cast_v<mp_integer>(min_i.value());
159  mp_integer ub = numeric_cast_v<mp_integer>(max_i.value());
160 
161  if(lb>ub)
162  return nullopt;
163 
164  std::vector<exprt> expr_insts;
165  for(mp_integer i=lb; i<=ub; ++i)
166  {
167  exprt constraint_expr = re;
168  replace_expr(var_expr,
169  from_integer(i, var_expr.type()),
170  constraint_expr);
171  expr_insts.push_back(constraint_expr);
172  }
173 
174  if(expr.id()==ID_forall)
175  {
176  // maintain the domain constraint if it isn't guaranteed by the
177  // instantiations (for a disjunction the domain constraint is implied by the
178  // instantiations)
179  if(re.id() == ID_and)
180  {
181  expr_insts.push_back(binary_predicate_exprt(
182  var_expr, ID_gt, from_integer(lb, var_expr.type())));
183  expr_insts.push_back(binary_predicate_exprt(
184  var_expr, ID_le, from_integer(ub, var_expr.type())));
185  }
186  return simplify_expr(conjunction(expr_insts), ns);
187  }
188  else if(expr.id() == ID_exists)
189  {
190  // maintain the domain constraint if it isn't trivially satisfied by the
191  // instantiations (for a conjunction the instantiations are stronger
192  // constraints)
193  if(re.id() == ID_or)
194  {
195  expr_insts.push_back(binary_predicate_exprt(
196  var_expr, ID_gt, from_integer(lb, var_expr.type())));
197  expr_insts.push_back(binary_predicate_exprt(
198  var_expr, ID_le, from_integer(ub, var_expr.type())));
199  }
200  return simplify_expr(disjunction(expr_insts), ns);
201  }
202 
203  UNREACHABLE;
204 }
205 
207 {
208  PRECONDITION(src.id() == ID_forall || src.id() == ID_exists);
209 
210  // We first worry about the scoping of the symbols bound by the quantifier.
211  auto fresh_symbols = fresh_binding(src);
212 
213  // replace in where()
214  auto where_replaced = src.instantiate(fresh_symbols);
215 
216  // produce new quantifier expression
217  auto new_src =
218  quantifier_exprt(src.id(), std::move(fresh_symbols), where_replaced);
219 
220  const auto res = instantiate_quantifier(src, ns);
221 
222  if(res)
223  return convert_bool(*res);
224 
225  // we failed to instantiate here, need to pass to post-processing
226  quantifier_list.emplace_back(quantifiert(src, prop.new_variable()));
227 
228  return quantifier_list.back().l;
229 }
230 
232 {
233  if(quantifier_list.empty())
234  return;
235 
236  // we do not yet have any elaborate post-processing
237  for(const auto &q : quantifier_list)
238  conversion_failed(q.expr);
239 }
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
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< exprt > instantiate_quantifier(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.
const namespacet & ns
Definition: arrays.h:54
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:2877
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:562
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:266
void post_process_quantifiers()
A constant literal expression.
Definition: std_expr.h:2753
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_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:407
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
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:215
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,...
bool replace_expr(const exprt &what, const exprt &by, exprt &dest)
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:2786
const not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_exprt.
Definition: std_expr.h:2152
const binary_relation_exprt & to_binary_relation_expr(const exprt &expr)
Cast an exprt to a binary_relation_exprt.
Definition: std_expr.h:807