cprover
prop_conv_solver.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_solver.h"
10 
11 #include <util/range.h>
12 
13 #include <algorithm>
14 #include <chrono>
15 
16 #include "literal_expr.h"
17 
19 {
21 }
22 
24 {
25  for(const auto &bit : bv)
26  if(!bit.is_constant())
27  set_frozen(bit);
28 }
29 
31 {
32  prop.set_frozen(a);
33 }
34 
36 {
37  freeze_all = true;
38 }
39 
41 {
42  // We can only improve Booleans.
43  if(expr.type().id() != ID_bool)
44  return expr;
45 
46  // We convert to a literal to obtain a 'small' handle
47  literalt l = convert(expr);
48 
49  // The literal may be a constant as a result of non-trivial
50  // propagation. We return constants as such.
51  if(l.is_true())
52  return true_exprt();
53  else if(l.is_false())
54  return false_exprt();
55 
56  // freeze to enable incremental use
57  set_frozen(l);
58 
59  return literal_exprt(l);
60 }
61 
63 {
64  auto result =
65  symbols.insert(std::pair<irep_idt, literalt>(identifier, literalt()));
66 
67  if(!result.second)
68  return result.first->second;
69 
70  literalt literal = prop.new_variable();
71  prop.set_variable_name(literal, identifier);
72 
73  // insert
74  result.first->second = literal;
75 
76  return literal;
77 }
78 
80 {
81  // trivial cases
82 
83  if(expr.is_true())
84  {
85  return true;
86  }
87  else if(expr.is_false())
88  {
89  return false;
90  }
91  else if(expr.id() == ID_symbol)
92  {
93  symbolst::const_iterator result =
94  symbols.find(to_symbol_expr(expr).get_identifier());
95 
96  // This may fail if the symbol isn't Boolean or
97  // not in the formula.
98  if(result == symbols.end())
99  return {};
100 
101  return prop.l_get(result->second).is_true();
102  }
103  else if(expr.id() == ID_literal)
104  {
105  return prop.l_get(to_literal_expr(expr).get_literal()).is_true();
106  }
107 
108  // sub-expressions
109 
110  if(expr.id() == ID_not)
111  {
112  if(expr.type().id() == ID_bool)
113  {
114  auto tmp = get_bool(to_not_expr(expr).op());
115  if(tmp.has_value())
116  return !*tmp;
117  else
118  return {};
119  }
120  }
121  else if(expr.id() == ID_and || expr.id() == ID_or)
122  {
123  if(expr.type().id() == ID_bool && expr.operands().size() >= 1)
124  {
125  forall_operands(it, expr)
126  {
127  auto tmp = get_bool(*it);
128  if(!tmp.has_value())
129  return {};
130 
131  if(expr.id() == ID_and)
132  {
133  if(*tmp == false)
134  return false;
135  }
136  else // or
137  {
138  if(*tmp == true)
139  return true;
140  }
141  }
142 
143  return expr.id() == ID_and;
144  }
145  }
146 
147  // check cache
148 
149  cachet::const_iterator cache_result = cache.find(expr);
150  if(cache_result == cache.end())
151  return {}; // not in formula
152  else
153  return prop.l_get(cache_result->second).is_true();
154 }
155 
157 {
158  if(!use_cache || expr.id() == ID_symbol || expr.id() == ID_constant)
159  {
160  literalt literal = convert_bool(expr);
161  if(freeze_all && !literal.is_constant())
162  prop.set_frozen(literal);
163  return literal;
164  }
165 
166  // check cache first
167  auto result = cache.insert({expr, literalt()});
168 
169  // get a reference to the cache entry
170  auto &cache_entry = result.first->second;
171 
172  if(!result.second) // found in cache
173  return cache_entry;
174 
175  // The following may invalidate the iterator result.first,
176  // but note that the _reference_ is guaranteed to remain valid.
177  literalt literal = convert_bool(expr);
178 
179  // store the literal in the cache using the reference
180  cache_entry = literal;
181 
182  if(freeze_all && !literal.is_constant())
183  prop.set_frozen(literal);
184 
185 #if 0
186  std::cout << literal << "=" << expr << '\n';
187 #endif
188 
189  return literal;
190 }
191 
193 {
194  PRECONDITION(expr.type().id() == ID_bool);
195 
196  const exprt::operandst &op = expr.operands();
197 
198  if(expr.is_constant())
199  {
200  if(expr.is_true())
201  return const_literal(true);
202  else
203  {
204  INVARIANT(
205  expr.is_false(),
206  "constant expression of type bool should be either true or false");
207  return const_literal(false);
208  }
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  const implies_exprt &implies_expr = to_implies_expr(expr);
225  return prop.limplies(
226  convert(implies_expr.op0()), convert(implies_expr.op1()));
227  }
228  else if(expr.id() == ID_if)
229  {
230  const if_exprt &if_expr = to_if_expr(expr);
231  return prop.lselect(
232  convert(if_expr.cond()),
233  convert(if_expr.true_case()),
234  convert(if_expr.false_case()));
235  }
236  else if(expr.id() == ID_constraint_select_one)
237  {
239  op.size() >= 2,
240  "constraint_select_one should have at least two operands");
241 
242  std::vector<literalt> op_bv;
243  op_bv.reserve(op.size());
244 
245  forall_operands(it, expr)
246  op_bv.push_back(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(
261  expr.id() == ID_or || expr.id() == ID_and || expr.id() == ID_xor ||
262  expr.id() == ID_nor || expr.id() == ID_nand)
263  {
264  INVARIANT(
265  !op.empty(),
266  "operator '" + expr.id_string() + "' takes at least one operand");
267 
268  bvt bv;
269 
270  for(const auto &operand : op)
271  bv.push_back(convert(operand));
272 
273  if(!bv.empty())
274  {
275  if(expr.id() == ID_or)
276  return prop.lor(bv);
277  else if(expr.id() == ID_nor)
278  return !prop.lor(bv);
279  else if(expr.id() == ID_and)
280  return prop.land(bv);
281  else if(expr.id() == ID_nand)
282  return !prop.land(bv);
283  else if(expr.id() == ID_xor)
284  return prop.lxor(bv);
285  }
286  }
287  else if(expr.id() == ID_not)
288  {
289  INVARIANT(op.size() == 1, "not takes one operand");
290  return !convert(op.front());
291  }
292  else if(expr.id() == ID_equal || expr.id() == ID_notequal)
293  {
294  INVARIANT(op.size() == 2, "equality takes two operands");
295  bool equal = (expr.id() == ID_equal);
296 
297  if(op[0].type().id() == ID_bool && op[1].type().id() == ID_bool)
298  {
299  literalt tmp1 = convert(op[0]), tmp2 = convert(op[1]);
300  return equal ? prop.lequal(tmp1, tmp2) : prop.lxor(tmp1, tmp2);
301  }
302  }
303 
304  return convert_rest(expr);
305 }
306 
308 {
309  // fall through
310  ignoring(expr);
311  return prop.new_variable();
312 }
313 
315 {
317  return true;
318 
319  // optimization for constraint of the form
320  // new_variable = value
321 
322  if(expr.lhs().id() == ID_symbol)
323  {
324  const irep_idt &identifier = to_symbol_expr(expr.lhs()).get_identifier();
325 
326  literalt tmp = convert(expr.rhs());
327 
328  std::pair<symbolst::iterator, bool> result =
329  symbols.insert(std::pair<irep_idt, literalt>(identifier, tmp));
330 
331  if(result.second)
332  return false; // ok, inserted!
333 
334  // nah, already there
335  }
336 
337  return true;
338 }
339 
341 {
342  PRECONDITION(expr.type().id() == ID_bool);
343 
344  const bool has_only_boolean_operands = std::all_of(
345  expr.operands().begin(), expr.operands().end(), [](const exprt &expr) {
346  return expr.type().id() == ID_bool;
347  });
348 
349  if(has_only_boolean_operands)
350  {
351  if(expr.id() == ID_not)
352  {
353  add_constraints_to_prop(to_not_expr(expr).op(), !value);
354  return;
355  }
356  else
357  {
358  if(value)
359  {
360  // set_to_true
361 
362  if(expr.id() == ID_and)
363  {
364  forall_operands(it, expr)
365  add_constraints_to_prop(*it, true);
366 
367  return;
368  }
369  else if(expr.id() == ID_or)
370  {
371  // Special case for a CNF-clause,
372  // i.e., a constraint that's a disjunction.
373 
374  if(!expr.operands().empty())
375  {
376  bvt bv;
377  bv.reserve(expr.operands().size());
378 
379  forall_operands(it, expr)
380  bv.push_back(convert(*it));
381 
382  prop.lcnf(bv);
383  return;
384  }
385  }
386  else if(expr.id() == ID_implies)
387  {
388  const auto &implies_expr = to_implies_expr(expr);
389  literalt l_lhs = convert(implies_expr.lhs());
390  literalt l_rhs = convert(implies_expr.rhs());
391  prop.lcnf(!l_lhs, l_rhs);
392  return;
393  }
394  else if(expr.id() == ID_equal)
395  {
397  return;
398  }
399  }
400  else
401  {
402  // set_to_false
403  if(expr.id() == ID_implies) // !(a=>b) == (a && !b)
404  {
405  const implies_exprt &implies_expr = to_implies_expr(expr);
406 
407  add_constraints_to_prop(implies_expr.op0(), true);
408  add_constraints_to_prop(implies_expr.op1(), false);
409  return;
410  }
411  else if(expr.id() == ID_or) // !(a || b) == (!a && !b)
412  {
413  forall_operands(it, expr)
414  add_constraints_to_prop(*it, false);
415  return;
416  }
417  }
418  }
419  }
420 
421  // fall back to convert
422  prop.l_set_to(convert(expr), value);
423 }
424 
426 {
427  // fall through
428 
429  log.warning() << "warning: ignoring " << expr.pretty() << messaget::eom;
430 }
431 
433 {
434 }
435 
437 {
438  // post-processing isn't incremental yet
440  {
441  const auto post_process_start = std::chrono::steady_clock::now();
442 
443  log.statistics() << "Post-processing" << messaget::eom;
444  post_process();
445  post_processing_done = true;
446 
447  const auto post_process_stop = std::chrono::steady_clock::now();
448  std::chrono::duration<double> post_process_runtime =
449  std::chrono::duration<double>(post_process_stop - post_process_start);
450  log.status() << "Runtime Post-process: " << post_process_runtime.count()
451  << "s" << messaget::eom;
452  }
453 
454  log.statistics() << "Solving with " << prop.solver_text() << messaget::eom;
455 
456  switch(prop.prop_solve())
457  {
459  return resultt::D_SATISFIABLE;
463  return resultt::D_ERROR;
464  }
465 
466  UNREACHABLE;
467 }
468 
470 {
471  if(expr.type().id() == ID_bool)
472  {
473  auto value = get_bool(expr);
474 
475  if(value.has_value())
476  {
477  if(*value)
478  return true_exprt();
479  else
480  return false_exprt();
481  }
482  }
483 
484  exprt tmp = expr;
485  for(auto &op : tmp.operands())
486  {
487  exprt tmp_op = get(op);
488  op.swap(tmp_op);
489  }
490  return tmp;
491 }
492 
493 void prop_conv_solvert::print_assignment(std::ostream &out) const
494 {
495  for(const auto &symbol : symbols)
496  out << symbol.first << " = " << prop.l_get(symbol.second) << '\n';
497 }
498 
500 {
502 }
503 
504 const char *prop_conv_solvert::context_prefix = "prop_conv::context$";
505 
506 void prop_conv_solvert::set_to(const exprt &expr, bool value)
507 {
508  if(assumption_stack.empty())
509  {
510  // We are in the root context.
511  add_constraints_to_prop(expr, value);
512  }
513  else
514  {
515  // We have a child context. We add context_literal ==> expr to the formula.
517  or_exprt(literal_exprt(!assumption_stack.back()), expr), value);
518  }
519 }
520 
521 void prop_conv_solvert::push(const std::vector<exprt> &assumptions)
522 {
523  // We push the given assumptions as a single context onto the stack.
524  assumption_stack.reserve(assumption_stack.size() + assumptions.size());
525  for(const auto &assumption : assumptions)
526  assumption_stack.push_back(to_literal_expr(assumption).get_literal());
527  context_size_stack.push_back(assumptions.size());
528 
530 }
531 
533 {
534  // We create a new context literal.
535  literalt context_literal = convert(symbol_exprt(
537 
538  assumption_stack.push_back(context_literal);
539  context_size_stack.push_back(1);
540 
542 }
543 
545 {
546  // We remove the context from the stack.
547  assumption_stack.resize(assumption_stack.size() - context_size_stack.back());
548  context_size_stack.pop_back();
549 
551 }
552 
553 // This method out-of-line because gcc-5.5.0-12ubuntu1 20171010 miscompiles it
554 // when inline (in certain build configurations, notably -O2 -g0) by producing
555 // a non-virtual thunk with c++03 ABI but a function body with c++11 ABI, the
556 // mismatch leading to a missing vtable entry and consequent null-pointer deref
557 // whenever this function is called.
559 {
560  return "propositional reduction";
561 }
562 
565 {
566  ::with_solver_hardness(prop, handler);
567 }
569 {
570  if(auto hardness_collector = dynamic_cast<hardness_collectort *>(&prop))
571  {
572  hardness_collector->enable_hardness_collection();
573  }
574 }
exprt & op1()
Definition: expr.h:102
exprt & lhs()
Definition: std_expr.h:580
exprt & op0()
Definition: expr.h:99
exprt & rhs()
Definition: std_expr.h:590
The Boolean type.
Definition: std_types.h:36
resultt
Result of running the decision procedure.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
Equality.
Definition: std_expr.h:1225
Base class for all expressions.
Definition: expr.h:54
std::vector< exprt > operandst
Definition: expr.h:56
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:33
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:42
typet & type()
Return the type of the expression.
Definition: expr.h:82
bool is_constant() const
Return whether the expression is a constant.
Definition: expr.cpp:26
operandst & operands()
Definition: expr.h:92
The Boolean constant false.
Definition: std_expr.h:2811
std::function< void(solver_hardnesst &)> handlert
The trinary if-then-else operator.
Definition: std_expr.h:2172
exprt & true_case()
Definition: std_expr.h:2199
exprt & false_case()
Definition: std_expr.h:2209
exprt & cond()
Definition: std_expr.h:2189
Boolean implication.
Definition: std_expr.h:1983
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:495
const std::string & id_string() const
Definition: irep.h:410
const irep_idt & id() const
Definition: irep.h:407
literalt get_literal() const
Definition: literal_expr.h:26
bool is_true() const
Definition: literal.h:156
bool is_constant() const
Definition: literal.h:166
bool is_false() const
Definition: literal.h:161
mstreamt & statistics() const
Definition: message.h:419
mstreamt & warning() const
Definition: message.h:404
mstreamt & status() const
Definition: message.h:414
static eomt eom
Definition: message.h:297
Boolean OR.
Definition: std_expr.h:2028
void pop() override
Pop whatever is on top of the stack.
decision_proceduret::resultt dec_solve() override
Run the decision procedure to solve the problem.
virtual bool set_equality_to_true(const equal_exprt &expr)
virtual literalt convert_bool(const exprt &expr)
virtual void post_process()
void set_frozen(literalt)
std::vector< size_t > context_size_stack
assumption_stack is segmented in contexts; Number of assumptions in each context on the stack
std::size_t context_literal_counter
To generate unique literal names for contexts.
std::size_t get_number_of_solver_calls() const override
Return the number of incremental solver calls.
virtual optionalt< bool > get_bool(const exprt &expr) const
Get a boolean value from the model if the formula is satisfiable.
virtual literalt get_literal(const irep_idt &symbol)
std::string decision_procedure_text() const override
Return a textual description of the decision procedure.
virtual void ignoring(const exprt &expr)
void with_solver_hardness(handlert handler) override
void add_constraints_to_prop(const exprt &expr, bool value)
Helper method used by set_to for adding the constraints to prop.
void push() override
Push a new context on the stack This context becomes a child context nested in the current context.
literalt convert(const exprt &expr) override
Convert a Boolean expression and return the corresponding literal.
exprt get(const exprt &expr) const override
Return expr with variables replaced by values from satisfying assignment if available.
bvt assumption_stack
Assumptions on the stack.
virtual literalt convert_rest(const exprt &expr)
void set_to(const exprt &expr, bool value) override
For a Boolean expression expr, add the constraint 'current_context => expr' if value is true,...
exprt handle(const exprt &expr) override
Generate a handle, which is an expression that has the same value as the argument in any model that i...
static const char * context_prefix
bool is_in_conflict(const exprt &expr) const override
Returns true if an expression is in the final conflict leading to UNSAT.
void enable_hardness_collection() override
void print_assignment(std::ostream &out) const override
Print satisfying assignment to out.
void l_set_to_true(literalt a)
Definition: prop.h:50
virtual literalt land(literalt a, literalt b)=0
std::size_t get_number_of_solver_calls() const
Definition: prop.cpp:35
virtual void set_variable_name(literalt, const irep_idt &)
Definition: prop.h:91
virtual literalt limplies(literalt a, literalt b)=0
virtual literalt lselect(literalt a, literalt b, literalt c)=0
virtual void set_frozen(literalt)
Definition: prop.h:112
virtual void l_set_to(literalt a, bool value)
Definition: prop.h:45
virtual literalt lxor(literalt a, literalt b)=0
virtual void set_assumptions(const bvt &)
Definition: prop.h:86
void lcnf(literalt l0, literalt l1)
Definition: prop.h:56
resultt prop_solve()
Definition: prop.cpp:29
virtual literalt new_variable()=0
virtual literalt lequal(literalt a, literalt b)=0
virtual literalt lor(literalt a, literalt b)=0
virtual bool is_in_conflict(literalt l) const =0
Returns true if an assumption is in the final conflict.
virtual tvt l_get(literalt a) const =0
virtual const std::string solver_text()=0
Expression to hold a symbol (variable)
Definition: std_expr.h:80
const irep_idt & get_identifier() const
Definition: std_expr.h:109
The Boolean constant true.
Definition: std_expr.h:2802
bool is_true() const
Definition: threeval.h:25
#define forall_operands(it, expr)
Definition: expr.h:18
std::vector< literalt > bvt
Definition: literal.h:201
literalt const_literal(bool value)
Definition: literal.h:188
const literal_exprt & to_literal_expr(const exprt &expr)
Cast a generic exprt to a literal_exprt.
Definition: literal_expr.h:56
nonstd::optional< T > optionalt
Definition: optional.h:35
Ranges: pair of begin and end iterators, which can be initialized from containers,...
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:503
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:510
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:2237
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:189
const not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_exprt.
Definition: std_expr.h:2152
const equal_exprt & to_equal_expr(const exprt &expr)
Cast an exprt to an equal_exprt.
Definition: std_expr.h:1265
const implies_exprt & to_implies_expr(const exprt &expr)
Cast an exprt to a implies_exprt.
Definition: std_expr.h:2008
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.