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