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/invariant.h>
13 #include <util/optional.h>
14 #include <util/replace_expr.h>
15 #include <util/simplify_expr.h>
16 
18 bool expr_eq(const exprt &expr1, const exprt &expr2)
19 {
20  exprt e1=expr1, e2=expr2;
21  if(expr1.id()==ID_typecast)
22  e1=expr1.op0();
23  if(expr2.id()==ID_typecast)
24  e2=expr2.op0();
25  return e1==e2;
26 }
27 
32  const exprt &var_expr,
33  const exprt &quantifier_expr)
34 {
35  PRECONDITION(quantifier_expr.id() == ID_or || quantifier_expr.id() == ID_and);
36 
37  exprt res = false_exprt();
38  if(quantifier_expr.id()==ID_or)
39  {
44  for(auto &x : quantifier_expr.operands())
45  {
46  if(x.id()!=ID_not)
47  continue;
48  exprt y=x.op0();
49  if(y.id()!=ID_ge)
50  continue;
51  if(expr_eq(var_expr, y.op0()) && y.op1().id()==ID_constant)
52  {
53  return y.op1();
54  }
55  }
56  }
57  else
58  {
63  for(auto &x : quantifier_expr.operands())
64  {
65  if(x.id()!=ID_ge)
66  continue;
67  if(expr_eq(var_expr, x.op0()) && x.op1().id()==ID_constant)
68  {
69  return x.op1();
70  }
71  }
72  }
73  return res;
74 }
75 
79  const exprt &var_expr,
80  const exprt &quantifier_expr)
81 {
82  PRECONDITION(quantifier_expr.id() == ID_or || quantifier_expr.id() == ID_and);
83  exprt res = false_exprt();
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  if(expr_eq(var_expr, x.op0()) && x.op1().id()==ID_constant)
95  {
96  exprt over_expr=x.op1();
97  mp_integer over_i = numeric_cast_v<mp_integer>(over_expr);
103  over_i-=1;
104  res=from_integer(over_i, x.op1().type());
105  return res;
106  }
107  }
108  }
109  else
110  {
115  for(auto &x : quantifier_expr.operands())
116  {
117  if(x.id()!=ID_not)
118  continue;
119  exprt y=x.op0();
120  if(y.id()!=ID_ge)
121  continue;
122  if(expr_eq(var_expr, y.op0()) && y.op1().id()==ID_constant)
123  {
124  exprt over_expr=y.op1();
125  mp_integer over_i = numeric_cast_v<mp_integer>(over_expr);
126  over_i-=1;
127  res=from_integer(over_i, y.op1().type());
128  return res;
129  }
130  }
131  }
132  return res;
133 }
134 
137 {
138  PRECONDITION(expr.id() == ID_forall || expr.id() == ID_exists);
139 
140  const symbol_exprt &var_expr = expr.symbol();
141 
147  const exprt &re = simplify_expr(expr.where(), ns);
148 
149  if(re.is_true() || re.is_false())
150  {
151  return re;
152  }
153 
154  const exprt &min_i = get_quantifier_var_min(var_expr, re);
155  const exprt &max_i = get_quantifier_var_max(var_expr, re);
156 
157  if(min_i.is_false() || max_i.is_false())
158  return nullopt;
159 
160  mp_integer lb = numeric_cast_v<mp_integer>(min_i);
161  mp_integer ub = numeric_cast_v<mp_integer>(max_i);
162 
163  if(lb>ub)
164  return nullopt;
165 
166  std::vector<exprt> expr_insts;
167  for(mp_integer i=lb; i<=ub; ++i)
168  {
169  exprt constraint_expr = re;
170  replace_expr(var_expr,
171  from_integer(i, var_expr.type()),
172  constraint_expr);
173  expr_insts.push_back(constraint_expr);
174  }
175 
176  if(expr.id()==ID_forall)
177  {
178  return conjunction(expr_insts);
179  }
180  else if(expr.id() == ID_exists)
181  {
182  return disjunction(expr_insts);
183  }
184 
185  UNREACHABLE;
186  return nullopt;
187 }
188 
190 {
191  PRECONDITION(src.id() == ID_forall || src.id() == ID_exists);
192 
193  quantifier_exprt expr(src);
194  const auto res = instantiate_quantifier(expr, ns);
195 
196  if(!res)
197  {
198  return SUB::convert_rest(src);
199  }
200 
201  quantifiert quantifier;
202  quantifier.expr = *res;
203  quantifier_list.push_back(quantifier);
204 
206  quantifier_list.back().l=l;
207 
208  return l;
209 }
210 
212 {
213  std::set<exprt> instances;
214 
215  if(quantifier_list.empty())
216  return;
217 
218  for(auto it=quantifier_list.begin();
219  it!=quantifier_list.end();
220  ++it)
221  {
222  prop.set_equal(convert_bool(it->expr), it->l);
223  }
224 }
BigInt mp_integer
Definition: mp_arith.h:22
exprt & op0()
Definition: expr.h:84
exprt simplify_expr(const exprt &src, const namespacet &ns)
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:99
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:90
virtual literalt convert_bool(const exprt &expr)
Definition: prop_conv.cpp:190
typet & type()
Return the type of the expression.
Definition: expr.h:68
symbol_exprt & symbol()
Definition: std_expr.h:4719
virtual void set_equal(literalt a, literalt b)
asserts a==b in the propositional formula
Definition: prop.cpp:12
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:50
const irep_idt & id() const
Definition: irep.h:259
bool replace_expr(const exprt &what, const exprt &by, exprt &dest)
virtual literalt new_variable()=0
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.
nonstd::optional< T > optionalt
Definition: optional.h:35
exprt & op1()
Definition: expr.h:87
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
#define PRECONDITION(CONDITION)
Definition: invariant.h:438
const namespacet & ns
exprt & where()
Definition: std_expr.h:4729
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.
quantifier_listt quantifier_list
Definition: boolbv.h:248
The Boolean constant false.
Definition: std_expr.h:4452
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:26
void post_process_quantifiers()
optionalt< exprt > instantiate_quantifier(const quantifier_exprt &expr, const namespacet &ns)
Base class for all expressions.
Definition: expr.h:54
var_not l
Definition: literal.h:181
A base class for quantifier expressions.
Definition: std_expr.h:4708
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:478
virtual literalt convert_rest(const exprt &expr)
Definition: prop_conv.cpp:330
Expression to hold a symbol (variable)
Definition: std_expr.h:143
bool expr_eq(const exprt &expr1, const exprt &expr2)
A method to detect equivalence between experts that can contain typecast.
operandst & operands()
Definition: expr.h:78
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
virtual literalt convert_quantifier(const quantifier_exprt &expr)