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 <cassert>
12 
13 #include <util/arith_tools.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  assert(quantifier_expr.id()==ID_or ||
36  quantifier_expr.id()==ID_and);
37  exprt res;
38  res.make_false();
39  if(quantifier_expr.id()==ID_or)
40  {
45  for(auto &x : quantifier_expr.operands())
46  {
47  if(x.id()!=ID_not)
48  continue;
49  exprt y=x.op0();
50  if(y.id()!=ID_ge)
51  continue;
52  if(expr_eq(var_expr, y.op0()) && y.op1().id()==ID_constant)
53  {
54  return y.op1();
55  }
56  }
57  }
58  else
59  {
64  for(auto &x : quantifier_expr.operands())
65  {
66  if(x.id()!=ID_ge)
67  continue;
68  if(expr_eq(var_expr, x.op0()) && x.op1().id()==ID_constant)
69  {
70  return x.op1();
71  }
72  }
73  }
74  return res;
75 }
76 
80  const exprt &var_expr,
81  const exprt &quantifier_expr)
82 {
83  assert(quantifier_expr.id()==ID_or ||
84  quantifier_expr.id()==ID_and);
85  exprt res;
86  res.make_false();
87  if(quantifier_expr.id()==ID_or)
88  {
93  for(auto &x : quantifier_expr.operands())
94  {
95  if(x.id()!=ID_ge)
96  continue;
97  if(expr_eq(var_expr, x.op0()) && x.op1().id()==ID_constant)
98  {
99  exprt over_expr=x.op1();
100  mp_integer over_i;
101  to_integer(over_expr, over_i);
107  over_i-=1;
108  res=from_integer(over_i, x.op1().type());
109  return res;
110  }
111  }
112  }
113  else
114  {
119  for(auto &x : quantifier_expr.operands())
120  {
121  if(x.id()!=ID_not)
122  continue;
123  exprt y=x.op0();
124  if(y.id()!=ID_ge)
125  continue;
126  if(expr_eq(var_expr, y.op0()) && y.op1().id()==ID_constant)
127  {
128  exprt over_expr=y.op1();
129  mp_integer over_i;
130  to_integer(over_expr, over_i);
131  over_i-=1;
132  res=from_integer(over_i, y.op1().type());
133  return res;
134  }
135  }
136  }
137  return res;
138 }
139 
141  const namespacet &ns)
142 {
143  if(!(expr.id()==ID_forall || expr.id()==ID_exists))
144  return true;
145 
146  assert(expr.operands().size()==2);
147  assert(expr.op0().id()==ID_symbol);
148 
149  exprt var_expr=expr.op0();
150 
155  exprt re(expr);
156  exprt tmp(re.op1());
157  re.swap(tmp);
158  re=simplify_expr(re, ns);
159 
160  if(re.is_true() || re.is_false())
161  {
162  expr=re;
163  return true;
164  }
165 
166  exprt min_i=get_quantifier_var_min(var_expr, re);
167  exprt max_i=get_quantifier_var_max(var_expr, re);
168  exprt body_expr=re;
169  if(var_expr.is_false() ||
170  min_i.is_false() ||
171  max_i.is_false() ||
172  body_expr.is_false())
173  return false;
174 
175  mp_integer lb, ub;
176  to_integer(min_i, lb);
177  to_integer(max_i, ub);
178 
179  if(lb>ub)
180  return false;
181 
182  bool res=true;
183  std::vector<exprt> expr_insts;
184  for(mp_integer i=lb; i<=ub; ++i)
185  {
186  exprt constraint_expr=body_expr;
187  replace_expr(var_expr,
188  from_integer(i, var_expr.type()),
189  constraint_expr);
190  expr_insts.push_back(constraint_expr);
191  }
192  if(expr.id()==ID_forall)
193  {
194  expr=conjunction(expr_insts);
195  }
196  if(expr.id()==ID_exists)
197  {
198  expr=disjunction(expr_insts);
199  }
200 
201  return res;
202 }
203 
205 {
206  exprt expr(src);
207  if(!instantiate_quantifier(expr, ns))
208  return SUB::convert_rest(src);
209 
210  quantifiert quantifier;
211  quantifier.expr=expr;
212  quantifier_list.push_back(quantifier);
213 
215  quantifier_list.back().l=l;
216 
217  return l;
218 }
219 
221 {
222  std::set<exprt> instances;
223 
224  if(quantifier_list.empty())
225  return;
226 
227  for(auto it=quantifier_list.begin();
228  it!=quantifier_list.end();
229  ++it)
230  {
231  prop.set_equal(convert_bool(it->expr), it->l);
232  }
233 }
BigInt mp_integer
Definition: mp_arith.h:22
exprt & op0()
Definition: expr.h:72
exprt simplify_expr(const exprt &src, const namespacet &ns)
bool is_false() const
Definition: expr.cpp:131
bool is_true() const
Definition: expr.cpp:124
virtual literalt convert_bool(const exprt &expr)
Definition: prop_conv.cpp:195
typet & type()
Definition: expr.h:56
virtual literalt convert_quantifier(const exprt &expr)
virtual void set_equal(literalt a, literalt b)
asserts a==b in the propositional formula
Definition: prop.cpp:14
exprt conjunction(const exprt::operandst &op)
Definition: std_expr.cpp:48
const irep_idt & id() const
Definition: irep.h:189
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...
exprt & op1()
Definition: expr.h:75
TO_BE_DOCUMENTED.
Definition: namespace.h:74
const namespacet & ns
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
exprt disjunction(const exprt::operandst &op)
Definition: std_expr.cpp:24
void post_process_quantifiers()
Base class for all expressions.
Definition: expr.h:42
var_not l
Definition: literal.h:181
void make_false()
Definition: expr.cpp:150
bool instantiate_quantifier(exprt &expr, const namespacet &ns)
virtual literalt convert_rest(const exprt &expr)
Definition: prop_conv.cpp:331
void swap(irept &irep)
Definition: irep.h:231
bool expr_eq(const exprt &expr1, const exprt &expr2)
A method to detect equivalence between experts that can contain typecast.
bool to_integer(const exprt &expr, mp_integer &int_value)
Definition: arith_tools.cpp:17
operandst & operands()
Definition: expr.h:66
constant_exprt from_integer(const mp_integer &int_value, const typet &type)