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