cprover
prop_conv.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 "prop_conv.h"
10 
11 #include <cassert>
12 #include <cstdlib>
13 #include <map>
14 
15 #include <util/std_expr.h>
16 #include <util/symbol.h>
17 #include <util/threeval.h>
18 
19 #include "prop.h"
20 #include "literal_expr.h"
21 
24 {
25  assert(false);
26  return false;
27 }
28 
30 {
31  assert(false);
32 }
33 
35 {
36  assert(false);
37 }
38 
39 void prop_convt::set_frozen(const bvt &bv)
40 {
41  for(unsigned i=0; i<bv.size(); i++)
42  if(!bv[i].is_constant())
43  set_frozen(bv[i]);
44 }
45 
46 bool prop_conv_solvert::literal(const exprt &expr, literalt &dest) const
47 {
48  assert(expr.type().id()==ID_bool);
49 
50  if(expr.id()==ID_symbol)
51  {
52  const irep_idt &identifier=
54 
55  symbolst::const_iterator result=symbols.find(identifier);
56 
57  if(result==symbols.end())
58  return true;
59  dest=result->second;
60  return false;
61  }
62 
63  throw "found no literal for expression";
64 }
65 
67 {
68  std::pair<symbolst::iterator, bool> result=
69  symbols.insert(std::pair<irep_idt, literalt>(identifier, literalt()));
70 
71  if(!result.second)
72  return result.first->second;
73 
74  // produce new variable
75  literalt literal=prop.new_variable();
76 
77  // set the name of the new variable
78  prop.set_variable_name(literal, id2string(identifier));
79 
80  // insert
81  result.first->second=literal;
82 
83  return literal;
84 }
85 
87 bool prop_conv_solvert::get_bool(const exprt &expr, tvt &value) const
88 {
89  // trivial cases
90 
91  if(expr.is_true())
92  {
93  value=tvt(true);
94  return false;
95  }
96  else if(expr.is_false())
97  {
98  value=tvt(false);
99  return false;
100  }
101  else if(expr.id()==ID_symbol)
102  {
103  symbolst::const_iterator result=
104  symbols.find(to_symbol_expr(expr).get_identifier());
105 
106  if(result==symbols.end())
107  return true;
108 
109  value=prop.l_get(result->second);
110  return false;
111  }
112 
113  // sub-expressions
114 
115  if(expr.id()==ID_not)
116  {
117  if(expr.type().id()==ID_bool &&
118  expr.operands().size()==1)
119  {
120  if(get_bool(expr.op0(), value))
121  return true;
122  value=!value;
123  return false;
124  }
125  }
126  else if(expr.id()==ID_and || expr.id()==ID_or)
127  {
128  if(expr.type().id()==ID_bool &&
129  expr.operands().size()>=1)
130  {
131  value=tvt(expr.id()==ID_and);
132 
133  forall_operands(it, expr)
134  {
135  tvt tmp;
136  if(get_bool(*it, tmp))
137  return true;
138 
139  if(expr.id()==ID_and)
140  {
141  if(tmp.is_false())
142  {
143  value=tvt(false);
144  return false;
145  }
146 
147  value=value && tmp;
148  }
149  else // or
150  {
151  if(tmp.is_true())
152  {
153  value=tvt(true);
154  return false;
155  }
156 
157  value=value || tmp;
158  }
159  }
160 
161  return false;
162  }
163  }
164 
165  // check cache
166 
167  cachet::const_iterator cache_result=cache.find(expr);
168  if(cache_result==cache.end())
169  return true;
170 
171  value=prop.l_get(cache_result->second);
172  return false;
173 }
174 
176 {
177  if(!use_cache ||
178  expr.id()==ID_symbol ||
179  expr.id()==ID_constant)
180  {
181  literalt literal=convert_bool(expr);
182  if(freeze_all && !literal.is_constant())
183  prop.set_frozen(literal);
184  return literal;
185  }
186  // check cache first
187 
188  std::pair<cachet::iterator, bool> result=
189  cache.insert(std::pair<exprt, literalt>(expr, literalt()));
190 
191  if(!result.second)
192  return result.first->second;
193 
194  literalt literal=convert_bool(expr);
195 
196  // insert into cache
197 
198  result.first->second=literal;
199  if(freeze_all && !literal.is_constant())
200  prop.set_frozen(literal);
201 
202  #if 0
203  std::cout << literal << "=" << expr << '\n';
204  #endif
205 
206  return literal;
207 }
208 
210 {
211  if(expr.type().id()!=ID_bool)
212  {
213  std::string msg="prop_convt::convert_bool got "
214  "non-boolean expression: ";
215  msg+=expr.pretty();
216  throw msg;
217  }
218 
219  const exprt::operandst &op=expr.operands();
220 
221  if(expr.is_constant())
222  {
223  if(expr.is_true())
224  return const_literal(true);
225  else if(expr.is_false())
226  return const_literal(false);
227  else
228  throw "unknown boolean constant: "+expr.pretty();
229  }
230  else if(expr.id()==ID_symbol)
231  {
232  return get_literal(to_symbol_expr(expr).get_identifier());
233  }
234  else if(expr.id()==ID_literal)
235  {
236  return to_literal_expr(expr).get_literal();
237  }
238  else if(expr.id()==ID_nondet_symbol)
239  {
240  return prop.new_variable();
241  }
242  else if(expr.id()==ID_implies)
243  {
244  if(op.size()!=2)
245  throw "implication takes two operands";
246 
247  return prop.limplies(convert(op[0]), convert(op[1]));
248  }
249  else if(expr.id()==ID_if)
250  {
251  if(op.size()!=3)
252  throw "if takes three operands";
253 
254  return prop.lselect(convert(op[0]), convert(op[1]), convert(op[2]));
255  }
256  else if(expr.id()==ID_constraint_select_one)
257  {
258  if(op.size()<2)
259  throw "constraint_select_one takes at least two operands";
260 
261  std::vector<literalt> op_bv;
262  op_bv.resize(op.size());
263 
264  unsigned i=0;
265  forall_operands(it, expr)
266  op_bv[i++]=convert(*it);
267 
268  // add constraints
269 
270  bvt b;
271  b.reserve(op_bv.size()-1);
272 
273  for(unsigned i=1; i<op_bv.size(); i++)
274  b.push_back(prop.lequal(op_bv[0], op_bv[i]));
275 
276  prop.l_set_to_true(prop.lor(b));
277 
278  return op_bv[0];
279  }
280  else if(expr.id()==ID_or || expr.id()==ID_and || expr.id()==ID_xor ||
281  expr.id()==ID_nor || expr.id()==ID_nand)
282  {
283  if(op.empty())
284  throw "operator `"+expr.id_string()+"' takes at least one operand";
285 
286  bvt bv;
287 
288  forall_expr(it, op)
289  bv.push_back(convert(*it));
290 
291  if(!bv.empty())
292  {
293  if(expr.id()==ID_or)
294  return prop.lor(bv);
295  else if(expr.id()==ID_nor)
296  return !prop.lor(bv);
297  else if(expr.id()==ID_and)
298  return prop.land(bv);
299  else if(expr.id()==ID_nand)
300  return !prop.land(bv);
301  else if(expr.id()==ID_xor)
302  return prop.lxor(bv);
303  }
304  }
305  else if(expr.id()==ID_not)
306  {
307  if(op.size()!=1)
308  throw "not takes one operand";
309 
310  return !convert(op.front());
311  }
312  else if(expr.id()==ID_equal || expr.id()==ID_notequal)
313  {
314  if(op.size()!=2)
315  throw "equality takes two operands";
316 
317  bool equal=(expr.id()==ID_equal);
318 
319  if(op[0].type().id()==ID_bool &&
320  op[1].type().id()==ID_bool)
321  {
322  literalt tmp1=convert(op[0]),
323  tmp2=convert(op[1]);
324  return
325  equal?prop.lequal(tmp1, tmp2):prop.lxor(tmp1, tmp2);
326  }
327  }
328  else if(expr.id()==ID_let)
329  {
330  // const let_exprt &let_expr=to_let_expr(expr);
331  throw "let is todo";
332  }
333 
334  return convert_rest(expr);
335 }
336 
338 {
339  // fall through
340  ignoring(expr);
341  return prop.new_variable();
342 }
343 
345 {
346  if(!equality_propagation)
347  return true;
348 
349  // optimization for constraint of the form
350  // new_variable = value
351 
352  if(expr.lhs().id()==ID_symbol)
353  {
354  const irep_idt &identifier=
355  to_symbol_expr(expr.lhs()).get_identifier();
356 
357  literalt tmp=convert(expr.rhs());
358 
359  std::pair<symbolst::iterator, bool> result=
360  symbols.insert(std::pair<irep_idt, literalt>(identifier, tmp));
361 
362  if(result.second)
363  return false; // ok, inserted!
364 
365  // nah, already there
366  }
367 
368  return true;
369 }
370 
371 void prop_conv_solvert::set_to(const exprt &expr, bool value)
372 {
373  if(expr.type().id()!=ID_bool)
374  {
375  std::string msg="prop_convt::set_to got "
376  "non-boolean expression: ";
377  msg+=expr.pretty();
378  throw msg;
379  }
380 
381  bool boolean=true;
382 
383  forall_operands(it, expr)
384  if(it->type().id()!=ID_bool)
385  {
386  boolean=false;
387  break;
388  }
389 
390  if(boolean)
391  {
392  if(expr.id()==ID_not)
393  {
394  if(expr.operands().size()==1)
395  {
396  set_to(expr.op0(), !value);
397  return;
398  }
399  }
400  else
401  {
402  if(value)
403  {
404  // set_to_true
405 
406  if(expr.id()==ID_and)
407  {
408  forall_operands(it, expr)
409  set_to_true(*it);
410 
411  return;
412  }
413  else if(expr.id()==ID_or)
414  {
415  // Special case for a CNF-clause,
416  // i.e., a constraint that's a disjunction.
417 
418  if(!expr.operands().empty())
419  {
420  bvt bv;
421  bv.reserve(expr.operands().size());
422 
423  forall_operands(it, expr)
424  bv.push_back(convert(*it));
425 
426  prop.lcnf(bv);
427  return;
428  }
429  }
430  else if(expr.id()==ID_implies)
431  {
432  if(expr.operands().size()==2)
433  {
434  literalt l0=convert(expr.op0());
435  literalt l1=convert(expr.op1());
436  prop.lcnf(!l0, l1);
437  return;
438  }
439  }
440  else if(expr.id()==ID_equal)
441  {
442  if(!set_equality_to_true(to_equal_expr(expr)))
443  return;
444  }
445  }
446  else
447  {
448  // set_to_false
449  if(expr.id()==ID_implies) // !(a=>b) == (a && !b)
450  {
451  assert(expr.operands().size()==2);
452  set_to_true(expr.op0());
453  set_to_false(expr.op1());
454  return;
455  }
456  else if(expr.id()==ID_or) // !(a || b) == (!a && !b)
457  {
458  forall_operands(it, expr)
459  set_to_false(*it);
460  return;
461  }
462  }
463  }
464  }
465 
466  // fall back to convert
467  prop.l_set_to(convert(expr), value);
468 }
469 
471 {
472  // fall through
473 
474  warning() << "warning: ignoring " << expr.pretty() << eom;
475 }
476 
478 {
479 }
480 
482 {
483  // post-processing isn't incremental yet
484  if(!post_processing_done)
485  {
486  statistics() << "Post-processing" << eom;
487  post_process();
488  post_processing_done=true;
489  }
490 
491  statistics() << "Solving with " << prop.solver_text() << eom;
492 
493  propt::resultt result=prop.prop_solve();
494 
495  switch(result)
496  {
499  default: return resultt::D_ERROR;
500  }
501 
502  return resultt::D_ERROR;
503 }
504 
506 {
507  tvt value;
508 
509  if(expr.type().id()==ID_bool &&
510  !get_bool(expr, value))
511  {
512  switch(value.get_value())
513  {
514  case tvt::tv_enumt::TV_TRUE: return true_exprt();
515  case tvt::tv_enumt::TV_FALSE: return false_exprt();
516  case tvt::tv_enumt::TV_UNKNOWN: return false_exprt(); // default
517  }
518  }
519 
520  exprt tmp=expr;
521 
522  Forall_operands(it, tmp)
523  {
524  exprt tmp_op=get(*it);
525  it->swap(tmp_op);
526  }
527 
528  return tmp;
529 }
530 
531 void prop_conv_solvert::print_assignment(std::ostream &out) const
532 {
533  for(symbolst::const_iterator it=symbols.begin();
534  it!=symbols.end();
535  it++)
536  out << it->first << " = " << prop.l_get(it->second) << "\n";
537 }
mstreamt & warning()
Definition: message.h:228
bool is_false() const
Definition: threeval.h:26
mstreamt & result()
Definition: message.h:233
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
virtual bool set_equality_to_true(const equal_exprt &expr)
Definition: prop_conv.cpp:344
virtual literalt convert(const exprt &expr) override
Definition: prop_conv.cpp:175
Symbol table entry.
exprt & op0()
Definition: expr.h:84
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:641
virtual exprt get(const exprt &expr) const override
Definition: prop_conv.cpp:505
const irep_idt & get_identifier() const
Definition: std_expr.h:120
#define forall_expr(it, expr)
Definition: expr.h:28
bool is_false() const
Definition: expr.cpp:140
const equal_exprt & to_equal_expr(const exprt &expr)
Cast a generic exprt to an equal_exprt.
Definition: std_expr.h:1105
bool is_true() const
Definition: expr.cpp:133
virtual bool is_in_conflict(literalt l) const
determine whether a variable is in the final conflict
Definition: prop_conv.cpp:23
virtual literalt convert_bool(const exprt &expr)
Definition: prop_conv.cpp:209
typet & type()
Definition: expr.h:60
virtual decision_proceduret::resultt dec_solve() override
Definition: prop_conv.cpp:481
static mstreamt & eom(mstreamt &m)
Definition: message.h:193
virtual void set_to(const exprt &expr, bool value) override
Definition: prop_conv.cpp:371
virtual void post_process()
Definition: prop_conv.cpp:477
virtual bool literal(const exprt &expr, literalt &literal) const
Definition: prop_conv.cpp:46
equality
Definition: std_expr.h:1082
const irep_idt & id() const
Definition: irep.h:189
virtual void print_assignment(std::ostream &out) const override
Definition: prop_conv.cpp:531
The boolean constant true.
Definition: std_expr.h:3742
API to expression classes.
Definition: threeval.h:19
exprt & op1()
Definition: expr.h:87
virtual literalt convert(const exprt &expr)=0
#define forall_operands(it, expr)
Definition: expr.h:17
resultt
Definition: prop.h:94
virtual void set_to(const exprt &expr, bool value)=0
The boolean constant false.
Definition: std_expr.h:3753
mstreamt & statistics()
Definition: message.h:243
bool is_constant() const
Definition: expr.cpp:128
bool is_true() const
Definition: threeval.h:25
std::vector< exprt > operandst
Definition: expr.h:49
literalt const_literal(bool value)
Definition: literal.h:187
virtual literalt get_literal(const irep_idt &symbol)
Definition: prop_conv.cpp:66
void set_to_false(const exprt &expr)
bool is_constant() const
Definition: literal.h:165
literalt get_literal() const
Definition: literal_expr.h:26
Base class for all expressions.
Definition: expr.h:46
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
Definition: std_expr.h:202
void set_to_true(const exprt &expr)
virtual bool get_bool(const exprt &expr, tvt &value) const
get a boolean value from counter example if not valid
Definition: prop_conv.cpp:87
virtual literalt convert_rest(const exprt &expr)
Definition: prop_conv.cpp:337
const std::string & id_string() const
Definition: irep.h:192
void swap(irept &irep)
Definition: irep.h:231
#define Forall_operands(it, expr)
Definition: expr.h:23
tv_enumt get_value() const
Definition: threeval.h:40
virtual void set_frozen(literalt a)
Definition: prop_conv.cpp:34
const literal_exprt & to_literal_expr(const exprt &expr)
Cast a generic exprt to a literal_exprt.
Definition: literal_expr.h:49
operandst & operands()
Definition: expr.h:70
virtual void ignoring(const exprt &expr)
Definition: prop_conv.cpp:470
std::vector< literalt > bvt
Definition: literal.h:197
virtual void set_assumptions(const bvt &_assumptions)
Definition: prop_conv.cpp:29