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/replace_expr.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  else if(quantifier_expr.id() == ID_and)
52  {
57  for(auto &x : quantifier_expr.operands())
58  {
59  if(x.id()!=ID_ge)
60  continue;
61  const auto &x_binary = to_binary_relation_expr(x);
62  if(
63  expr_eq(var_expr, x_binary.lhs()) && x_binary.rhs().id() == ID_constant)
64  {
65  return to_constant_expr(x_binary.rhs());
66  }
67  }
68  }
69 
70  return {};
71 }
72 
76 get_quantifier_var_max(const exprt &var_expr, const exprt &quantifier_expr)
77 {
78  if(quantifier_expr.id()==ID_or)
79  {
84  for(auto &x : quantifier_expr.operands())
85  {
86  if(x.id()!=ID_ge)
87  continue;
88  const auto &x_binary = to_binary_relation_expr(x);
89  if(
90  expr_eq(var_expr, x_binary.lhs()) && x_binary.rhs().id() == ID_constant)
91  {
92  const constant_exprt &over_expr = to_constant_expr(x_binary.rhs());
93 
94  mp_integer over_i = numeric_cast_v<mp_integer>(over_expr);
95 
101  over_i-=1;
102  return from_integer(over_i, x_binary.rhs().type());
103  }
104  }
105  }
106  else
107  {
112  for(auto &x : quantifier_expr.operands())
113  {
114  if(x.id()!=ID_not)
115  continue;
116  exprt y = to_not_expr(x).op();
117  if(y.id()!=ID_ge)
118  continue;
119  const auto &y_binary = to_binary_relation_expr(y);
120  if(
121  expr_eq(var_expr, y_binary.lhs()) && y_binary.rhs().id() == ID_constant)
122  {
123  const constant_exprt &over_expr = to_constant_expr(y_binary.rhs());
124  mp_integer over_i = numeric_cast_v<mp_integer>(over_expr);
125  over_i-=1;
126  return from_integer(over_i, y_binary.rhs().type());
127  }
128  }
129  }
130 
131  return {};
132 }
133 
134 static optionalt<exprt>
136 {
137  const symbol_exprt &var_expr = expr.symbol();
138 
144  const exprt re = simplify_expr(expr.where(), ns);
145 
146  if(re.is_true() || re.is_false())
147  {
148  return re;
149  }
150 
151  const optionalt<constant_exprt> min_i = get_quantifier_var_min(var_expr, re);
152  const optionalt<constant_exprt> max_i = get_quantifier_var_max(var_expr, re);
153 
154  if(!min_i.has_value() || !max_i.has_value())
155  return nullopt;
156 
157  mp_integer lb = numeric_cast_v<mp_integer>(min_i.value());
158  mp_integer ub = numeric_cast_v<mp_integer>(max_i.value());
159 
160  if(lb>ub)
161  return nullopt;
162 
163  std::vector<exprt> expr_insts;
164  for(mp_integer i=lb; i<=ub; ++i)
165  {
166  exprt constraint_expr = re;
167  replace_expr(var_expr,
168  from_integer(i, var_expr.type()),
169  constraint_expr);
170  expr_insts.push_back(constraint_expr);
171  }
172 
173  if(expr.id()==ID_forall)
174  {
175  // maintain the domain constraint if it isn't guaranteed by the
176  // instantiations (for a disjunction the domain constraint is implied by the
177  // instantiations)
178  if(re.id() == ID_and)
179  {
180  expr_insts.push_back(binary_predicate_exprt(
181  var_expr, ID_gt, from_integer(lb, var_expr.type())));
182  expr_insts.push_back(binary_predicate_exprt(
183  var_expr, ID_le, from_integer(ub, var_expr.type())));
184  }
185  return simplify_expr(conjunction(expr_insts), ns);
186  }
187  else if(expr.id() == ID_exists)
188  {
189  // maintain the domain constraint if it isn't trivially satisfied by the
190  // instantiations (for a conjunction the instantiations are stronger
191  // constraints)
192  if(re.id() == ID_or)
193  {
194  expr_insts.push_back(binary_predicate_exprt(
195  var_expr, ID_gt, from_integer(lb, var_expr.type())));
196  expr_insts.push_back(binary_predicate_exprt(
197  var_expr, ID_le, from_integer(ub, var_expr.type())));
198  }
199  return simplify_expr(disjunction(expr_insts), ns);
200  }
201 
202  UNREACHABLE;
203 }
204 
206 {
207  PRECONDITION(src.id() == ID_forall || src.id() == ID_exists);
208 
209  const auto res = instantiate_quantifier(src, ns);
210 
211  if(res)
212  return convert_bool(*res);
213 
214  // we failed to instantiate here, need to pass to post-processing
215  quantifier_list.emplace_back(quantifiert(src, prop.new_variable()));
216 
217  return quantifier_list.back().l;
218 }
219 
221 {
222  if(quantifier_list.empty())
223  return;
224 
225  // we do not yet have any elaborate post-processing
226  for(const auto &q : quantifier_list)
227  conversion_failed(q.expr);
228 }
UNREACHABLE
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:504
get_quantifier_var_min
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.
Definition: boolbv_quantifier.cpp:28
skip_typecast
const exprt & skip_typecast(const exprt &expr)
find the expression nested inside typecasts, if any
Definition: expr_util.cpp:217
conjunction
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:51
boolbvt::post_process_quantifiers
void post_process_quantifiers()
Definition: boolbv_quantifier.cpp:220
arith_tools.h
optional.h
mp_integer
BigInt mp_integer
Definition: mp_arith.h:19
invariant.h
propt::new_variable
virtual literalt new_variable()=0
exprt
Base class for all expressions.
Definition: expr.h:53
quantifier_exprt
A base class for quantifier expressions.
Definition: mathematical_expr.h:271
exprt::is_true
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:92
prop_conv_solvert::convert_bool
virtual literalt convert_bool(const exprt &expr)
Definition: prop_conv_solver.cpp:199
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:82
exprt::is_false
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:101
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
disjunction
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:29
boolbvt::conversion_failed
void conversion_failed(const exprt &expr, bvt &bv)
Definition: boolbv.h:113
binary_predicate_exprt
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two argu...
Definition: std_expr.h:694
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
quantifier_exprt::symbol
symbol_exprt & symbol()
Definition: mathematical_expr.h:286
arrayst::ns
const namespacet & ns
Definition: arrays.h:51
simplify_expr
exprt simplify_expr(exprt src, const namespacet &ns)
Definition: simplify_expr.cpp:2698
irept::id
const irep_idt & id() const
Definition: irep.h:418
unary_exprt::op
const exprt & op() const
Definition: std_expr.h:281
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
boolbvt::quantifier_list
quantifier_listt quantifier_list
Definition: boolbv.h:257
get_quantifier_var_max
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.
Definition: boolbv_quantifier.cpp:76
simplify_expr.h
expr_util.h
Deprecated expression utility functions.
binding_exprt::where
exprt & where()
Definition: std_expr.h:4152
boolbvt::quantifiert
Definition: boolbv.h:245
instantiate_quantifier
static optionalt< exprt > instantiate_quantifier(const quantifier_exprt &expr, const namespacet &ns)
Definition: boolbv_quantifier.cpp:135
to_not_expr
const not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_exprt.
Definition: std_expr.h:2868
replace_expr
bool replace_expr(const exprt &what, const exprt &by, exprt &dest)
Definition: replace_expr.cpp:12
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
literalt
Definition: literal.h:26
boolbvt::convert_quantifier
virtual literalt convert_quantifier(const quantifier_exprt &expr)
Definition: boolbv_quantifier.cpp:205
boolbv.h
replace_expr.h
exprt::operands
operandst & operands()
Definition: expr.h:95
expr_eq
static bool expr_eq(const exprt &expr1, const exprt &expr2)
A method to detect equivalence between experts that can contain typecast.
Definition: boolbv_quantifier.cpp:19
constant_exprt
A constant literal expression.
Definition: std_expr.h:3906
to_binary_relation_expr
const binary_relation_exprt & to_binary_relation_expr(const exprt &expr)
Cast an exprt to a binary_relation_exprt.
Definition: std_expr.h:774
prop_conv_solvert::prop
propt & prop
Definition: prop_conv_solver.h:131
to_constant_expr
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:3939