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 symbol_exprt &expr, literalt &dest) const
37 {
38  PRECONDITION(expr.type().id() == ID_bool);
39 
40  const irep_idt &identifier = expr.get_identifier();
41 
42  symbolst::const_iterator result = symbols.find(identifier);
43 
44  if(result == symbols.end())
45  return true;
46 
47  dest = result->second;
48  return false;
49 }
50 
52 {
53  auto result =
54  symbols.insert(std::pair<irep_idt, literalt>(identifier, literalt()));
55 
56  if(!result.second)
57  return result.first->second;
58 
60  prop.set_variable_name(literal, identifier);
61 
62  // insert
63  result.first->second=literal;
64 
65  return literal;
66 }
67 
69 bool prop_conv_solvert::get_bool(const exprt &expr, tvt &value) const
70 {
71  // trivial cases
72 
73  if(expr.is_true())
74  {
75  value=tvt(true);
76  return false;
77  }
78  else if(expr.is_false())
79  {
80  value=tvt(false);
81  return false;
82  }
83  else if(expr.id()==ID_symbol)
84  {
85  symbolst::const_iterator result=
86  symbols.find(to_symbol_expr(expr).get_identifier());
87 
88  if(result==symbols.end())
89  return true;
90 
91  value=prop.l_get(result->second);
92  return false;
93  }
94 
95  // sub-expressions
96 
97  if(expr.id()==ID_not)
98  {
99  if(expr.type().id()==ID_bool &&
100  expr.operands().size()==1)
101  {
102  if(get_bool(expr.op0(), value))
103  return true;
104  value=!value;
105  return false;
106  }
107  }
108  else if(expr.id()==ID_and || expr.id()==ID_or)
109  {
110  if(expr.type().id()==ID_bool &&
111  expr.operands().size()>=1)
112  {
113  value=tvt(expr.id()==ID_and);
114 
115  forall_operands(it, expr)
116  {
117  tvt tmp;
118  if(get_bool(*it, tmp))
119  return true;
120 
121  if(expr.id()==ID_and)
122  {
123  if(tmp.is_false())
124  {
125  value=tvt(false);
126  return false;
127  }
128 
129  value=value && tmp;
130  }
131  else // or
132  {
133  if(tmp.is_true())
134  {
135  value=tvt(true);
136  return false;
137  }
138 
139  value=value || tmp;
140  }
141  }
142 
143  return false;
144  }
145  }
146 
147  // check cache
148 
149  cachet::const_iterator cache_result=cache.find(expr);
150  if(cache_result==cache.end())
151  return true;
152 
153  value=prop.l_get(cache_result->second);
154  return false;
155 }
156 
158 {
159  if(!use_cache ||
160  expr.id()==ID_symbol ||
161  expr.id()==ID_constant)
162  {
164  if(freeze_all && !literal.is_constant())
166  return literal;
167  }
168 
169  // check cache first
170  auto result = cache.insert({expr, literalt()});
171 
172  if(!result.second)
173  return result.first->second;
174 
176 
177  // insert into cache
178 
179  result.first->second=literal;
180  if(freeze_all && !literal.is_constant())
182 
183  #if 0
184  std::cout << literal << "=" << expr << '\n';
185  #endif
186 
187  return literal;
188 }
189 
191 {
192  PRECONDITION(expr.type().id() == ID_bool);
193 
194  const exprt::operandst &op=expr.operands();
195 
196  if(expr.is_constant())
197  {
198  if(expr.is_true())
199  return const_literal(true);
200  else
201  {
202  INVARIANT(
203  expr.is_false(),
204  "constant expression of type bool should be either true or false");
205  return const_literal(false);
206  }
207  }
208  else if(expr.id()==ID_symbol)
209  {
210  return get_literal(to_symbol_expr(expr).get_identifier());
211  }
212  else if(expr.id()==ID_literal)
213  {
214  return to_literal_expr(expr).get_literal();
215  }
216  else if(expr.id()==ID_nondet_symbol)
217  {
218  return prop.new_variable();
219  }
220  else if(expr.id()==ID_implies)
221  {
222  const implies_exprt &implies_expr = to_implies_expr(expr);
223  return prop.limplies(
224  convert(implies_expr.op0()), convert(implies_expr.op1()));
225  }
226  else if(expr.id()==ID_if)
227  {
228  const if_exprt &if_expr = to_if_expr(expr);
229  return prop.lselect(
230  convert(if_expr.cond()),
231  convert(if_expr.true_case()),
232  convert(if_expr.false_case()));
233  }
234  else if(expr.id()==ID_constraint_select_one)
235  {
237  op.size() >= 2,
238  "constraint_select_one should have at least two operands");
239 
240  std::vector<literalt> op_bv;
241  op_bv.resize(op.size());
242 
243  unsigned i=0;
244  forall_operands(it, expr)
245  op_bv[i++]=convert(*it);
246 
247  // add constraints
248 
249  bvt b;
250  b.reserve(op_bv.size()-1);
251 
252  for(unsigned i=1; i<op_bv.size(); i++)
253  b.push_back(prop.lequal(op_bv[0], op_bv[i]));
254 
256 
257  return op_bv[0];
258  }
259  else if(expr.id()==ID_or || expr.id()==ID_and || expr.id()==ID_xor ||
260  expr.id()==ID_nor || expr.id()==ID_nand)
261  {
262  INVARIANT(
263  !op.empty(),
264  "operator `" + expr.id_string() + "' takes at least one operand");
265 
266  bvt bv;
267 
268  forall_expr(it, op)
269  bv.push_back(convert(*it));
270 
271  if(!bv.empty())
272  {
273  if(expr.id()==ID_or)
274  return prop.lor(bv);
275  else if(expr.id()==ID_nor)
276  return !prop.lor(bv);
277  else if(expr.id()==ID_and)
278  return prop.land(bv);
279  else if(expr.id()==ID_nand)
280  return !prop.land(bv);
281  else if(expr.id()==ID_xor)
282  return prop.lxor(bv);
283  }
284  }
285  else if(expr.id()==ID_not)
286  {
287  INVARIANT(op.size() == 1, "not takes one operand");
288  return !convert(op.front());
289  }
290  else if(expr.id()==ID_equal || expr.id()==ID_notequal)
291  {
292  INVARIANT(op.size() == 2, "equality takes two operands");
293  bool equal=(expr.id()==ID_equal);
294 
295  if(op[0].type().id()==ID_bool &&
296  op[1].type().id()==ID_bool)
297  {
298  literalt tmp1=convert(op[0]),
299  tmp2=convert(op[1]);
300  return
301  equal?prop.lequal(tmp1, tmp2):prop.lxor(tmp1, tmp2);
302  }
303  }
304  else if(expr.id()==ID_let)
305  {
306  const let_exprt &let_expr=to_let_expr(expr);
307 
308  // first check whether this is all boolean
309  if(let_expr.value().type().id()==ID_bool &&
310  let_expr.where().type().id()==ID_bool)
311  {
312  literalt value=convert(let_expr.value());
313 
314  // We expect the identifier of the bound symbols to be unique,
315  // and thus, these can go straight into the symbol map.
316  // This property also allows us to cache any subexpressions.
317  const irep_idt &id=let_expr.symbol().get_identifier();
318  symbols[id]=value;
319  literalt result=convert(let_expr.where());
320 
321  // remove again
322  symbols.erase(id);
323  return result;
324  }
325  }
326 
327  return convert_rest(expr);
328 }
329 
331 {
332  // fall through
333  ignoring(expr);
334  return prop.new_variable();
335 }
336 
338 {
340  return true;
341 
342  // optimization for constraint of the form
343  // new_variable = value
344 
345  if(expr.lhs().id()==ID_symbol)
346  {
347  const irep_idt &identifier=
348  to_symbol_expr(expr.lhs()).get_identifier();
349 
350  literalt tmp=convert(expr.rhs());
351 
352  std::pair<symbolst::iterator, bool> result=
353  symbols.insert(std::pair<irep_idt, literalt>(identifier, tmp));
354 
355  if(result.second)
356  return false; // ok, inserted!
357 
358  // nah, already there
359  }
360 
361  return true;
362 }
363 
364 void prop_conv_solvert::set_to(const exprt &expr, bool value)
365 {
366  PRECONDITION(expr.type().id() == ID_bool);
367 
368  const bool has_only_boolean_operands = std::all_of(
369  expr.operands().begin(),
370  expr.operands().end(),
371  [](const exprt &expr) { return expr.type().id() == ID_bool; });
372 
373  if(has_only_boolean_operands)
374  {
375  if(expr.id()==ID_not)
376  {
377  if(expr.operands().size()==1)
378  {
379  set_to(expr.op0(), !value);
380  return;
381  }
382  }
383  else
384  {
385  if(value)
386  {
387  // set_to_true
388 
389  if(expr.id()==ID_and)
390  {
391  forall_operands(it, expr)
392  set_to_true(*it);
393 
394  return;
395  }
396  else if(expr.id()==ID_or)
397  {
398  // Special case for a CNF-clause,
399  // i.e., a constraint that's a disjunction.
400 
401  if(!expr.operands().empty())
402  {
403  bvt bv;
404  bv.reserve(expr.operands().size());
405 
406  forall_operands(it, expr)
407  bv.push_back(convert(*it));
408 
409  prop.lcnf(bv);
410  return;
411  }
412  }
413  else if(expr.id()==ID_implies)
414  {
415  if(expr.operands().size()==2)
416  {
417  literalt l0=convert(expr.op0());
418  literalt l1=convert(expr.op1());
419  prop.lcnf(!l0, l1);
420  return;
421  }
422  }
423  else if(expr.id()==ID_equal)
424  {
426  return;
427  }
428  }
429  else
430  {
431  // set_to_false
432  if(expr.id()==ID_implies) // !(a=>b) == (a && !b)
433  {
434  const implies_exprt &implies_expr = to_implies_expr(expr);
435 
436  set_to_true(implies_expr.op0());
437  set_to_false(implies_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 }
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
prop_conv_solvert::equality_propagation
bool equality_propagation
Definition: prop_conv.h:112
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:438
prop_convt::set_assumptions
virtual void set_assumptions(const bvt &_assumptions)
Definition: prop_conv.cpp:19
literal_exprt::get_literal
literalt get_literal() const
Definition: literal_expr.h:26
propt::solver_text
virtual const std::string solver_text()=0
prop_convt::is_in_conflict
virtual bool is_in_conflict(literalt l) const
determine whether a variable is in the final conflict
Definition: prop_conv.cpp:13
DATA_INVARIANT
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:485
bvt
std::vector< literalt > bvt
Definition: literal.h:200
irept::pretty
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:640
to_if_expr
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:3482
propt::resultt::P_UNSATISFIABLE
if_exprt
The trinary if-then-else operator.
Definition: std_expr.h:3427
decision_proceduret::resultt::D_UNSATISFIABLE
prop_conv_solvert::symbols
symbolst symbols
Definition: prop_conv.h:142
let_exprt::symbol
symbol_exprt & symbol()
Definition: std_expr.h:4646
binary_relation_exprt::rhs
exprt & rhs()
Definition: std_expr.h:931
prop_conv_solvert::freeze_all
bool freeze_all
Definition: prop_conv.h:113
propt::new_variable
virtual literalt new_variable()=0
exprt
Base class for all expressions.
Definition: expr.h:54
decision_proceduret::set_to_true
void set_to_true(const exprt &expr)
Definition: decision_procedure.h:40
binary_relation_exprt::lhs
exprt & lhs()
Definition: std_expr.h:921
exprt::op0
exprt & op0()
Definition: expr.h:84
propt::lor
virtual literalt lor(literalt a, literalt b)=0
propt::l_set_to_true
void l_set_to_true(literalt a)
Definition: prop.h:49
propt::l_set_to
virtual void l_set_to(literalt a, bool value)
Definition: prop.h:44
messaget::eom
static eomt eom
Definition: message.h:284
exprt::is_true
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:90
prop_conv_solvert::convert_bool
virtual literalt convert_bool(const exprt &expr)
Definition: prop_conv.cpp:190
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:143
propt::land
virtual literalt land(literalt a, literalt b)=0
equal_exprt
Equality.
Definition: std_expr.h:1484
UNREACHABLE
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:478
decision_proceduret::set_to_false
void set_to_false(const exprt &expr)
Definition: decision_procedure.h:43
if_exprt::false_case
exprt & false_case()
Definition: std_expr.h:3465
exprt::is_false
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:99
to_literal_expr
const literal_exprt & to_literal_expr(const exprt &expr)
Cast a generic exprt to a literal_exprt.
Definition: literal_expr.h:49
prop_conv_solvert::ignoring
virtual void ignoring(const exprt &expr)
Definition: prop_conv.cpp:454
decision_proceduret::resultt::D_SATISFIABLE
prop_conv_solvert::cache
cachet cache
Definition: prop_conv.h:147
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:68
let_exprt::value
exprt & value()
Definition: std_expr.h:4656
prop_conv_solvert::literal
bool literal(const symbol_exprt &expr, literalt &literal) const
Definition: prop_conv.cpp:36
propt::lxor
virtual literalt lxor(literalt a, literalt b)=0
tvt::tv_enumt::TV_TRUE
prop_conv_solvert::post_processing_done
bool post_processing_done
Definition: prop_conv.h:131
messaget::result
mstreamt & result() const
Definition: message.h:396
prop_conv.h
propt::limplies
virtual literalt limplies(literalt a, literalt b)=0
forall_operands
#define forall_operands(it, expr)
Definition: expr.h:20
propt::resultt::P_SATISFIABLE
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:176
prop_conv_solvert::get_bool
virtual bool get_bool(const exprt &expr, tvt &value) const
get a boolean value from counter example if not valid
Definition: prop_conv.cpp:69
to_let_expr
const let_exprt & to_let_expr(const exprt &expr)
Cast an exprt to a let_exprt.
Definition: std_expr.h:4683
prop_conv_solvert::post_process
virtual void post_process()
Definition: prop_conv.cpp:461
irept::id_string
const std::string & id_string() const
Definition: irep.h:262
prop_conv_solvert::get
exprt get(const exprt &expr) const override
Definition: prop_conv.cpp:485
exprt::op1
exprt & op1()
Definition: expr.h:87
const_literal
literalt const_literal(bool value)
Definition: literal.h:187
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:251
decision_proceduret::resultt::D_ERROR
irept::id
const irep_idt & id() const
Definition: irep.h:259
propt::set_frozen
virtual void set_frozen(literalt)
Definition: prop.h:111
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:57
false_exprt
The Boolean constant false.
Definition: std_expr.h:4452
tvt::is_false
bool is_false() const
Definition: threeval.h:26
prop_conv_solvert::get_literal
virtual literalt get_literal(const irep_idt &symbol)
Definition: prop_conv.cpp:51
tvt
Definition: threeval.h:19
prop_conv_solvert::convert
literalt convert(const exprt &expr) override
Definition: prop_conv.cpp:157
decision_proceduret::resultt
resultt
Definition: decision_procedure.h:47
prop_conv_solvert::convert_rest
virtual literalt convert_rest(const exprt &expr)
Definition: prop_conv.cpp:330
prop_conv_solvert::use_cache
bool use_cache
Definition: prop_conv.h:111
propt::set_variable_name
virtual void set_variable_name(literalt, const irep_idt &)
Definition: prop.h:90
propt::lequal
virtual literalt lequal(literalt a, literalt b)=0
prop_convt::set_frozen
virtual void set_frozen(literalt a)
Definition: prop_conv.cpp:24
if_exprt::true_case
exprt & true_case()
Definition: std_expr.h:3455
propt::l_get
virtual tvt l_get(literalt a) const =0
propt::prop_solve
virtual resultt prop_solve()=0
to_implies_expr
const implies_exprt & to_implies_expr(const exprt &expr)
Cast an exprt to a implies_exprt.
Definition: std_expr.h:2505
prop_conv_solvert::dec_solve
decision_proceduret::resultt dec_solve() override
Definition: prop_conv.cpp:465
exprt::is_constant
bool is_constant() const
Return whether the expression is a constant.
Definition: expr.cpp:83
if_exprt::cond
exprt & cond()
Definition: std_expr.h:3445
literalt
Definition: literal.h:24
to_equal_expr
const equal_exprt & to_equal_expr(const exprt &expr)
Cast an exprt to an equal_exprt.
Definition: std_expr.h:1519
prop_conv_solvert::print_assignment
void print_assignment(std::ostream &out) const override
Definition: prop_conv.cpp:509
tvt::tv_enumt::TV_UNKNOWN
implies_exprt
Boolean implication.
Definition: std_expr.h:2485
exprt::operands
operandst & operands()
Definition: expr.h:78
forall_expr
#define forall_expr(it, expr)
Definition: expr.h:31
tvt::get_value
tv_enumt get_value() const
Definition: threeval.h:40
true_exprt
The Boolean constant true.
Definition: std_expr.h:4443
messaget::warning
mstreamt & warning() const
Definition: message.h:391
tvt::tv_enumt::TV_FALSE
let_exprt::where
exprt & where()
Definition: std_expr.h:4666
propt::lselect
virtual literalt lselect(literalt a, literalt b, literalt c)=0
propt::lcnf
void lcnf(literalt l0, literalt l1)
Definition: prop.h:55
let_exprt
A let expression.
Definition: std_expr.h:4635
prop_conv_solvert::set_to
void set_to(const exprt &expr, bool value) override
Definition: prop_conv.cpp:364
validation_modet::INVARIANT
prop_conv_solvert::prop
propt & prop
Definition: prop_conv.h:152
tvt::is_true
bool is_true() const
Definition: threeval.h:25
messaget::statistics
mstreamt & statistics() const
Definition: message.h:406
prop_conv_solvert::set_equality_to_true
virtual bool set_equality_to_true(const equal_exprt &expr)
Definition: prop_conv.cpp:337