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 
16 {
18 }
19 
21 {
22  for(const auto &bit : bv)
23  if(!bit.is_constant())
24  set_frozen(bit);
25 }
26 
28 {
29  prop.set_frozen(a);
30 }
31 
33 {
34  freeze_all = true;
35 }
36 
38 {
39  // We can only improve Booleans.
40  if(expr.type().id() != ID_bool)
41  return expr;
42 
43  // We convert to a literal to obtain a 'small' handle
44  literalt l = convert(expr);
45 
46  // The literal may be a constant as a result of non-trivial
47  // propagation. We return constants as such.
48  if(l.is_true())
49  return true_exprt();
50  else if(l.is_false())
51  return false_exprt();
52 
53  // freeze to enable incremental use
54  set_frozen(l);
55 
56  return literal_exprt(l);
57 }
58 
59 bool prop_conv_solvert::literal(const symbol_exprt &expr, literalt &dest) const
60 {
61  PRECONDITION(expr.type().id() == ID_bool);
62 
63  const irep_idt &identifier = expr.get_identifier();
64 
65  symbolst::const_iterator result = symbols.find(identifier);
66 
67  if(result == symbols.end())
68  return true;
69 
70  dest = result->second;
71  return false;
72 }
73 
75 {
76  auto result =
77  symbols.insert(std::pair<irep_idt, literalt>(identifier, literalt()));
78 
79  if(!result.second)
80  return result.first->second;
81 
83  prop.set_variable_name(literal, identifier);
84 
85  // insert
86  result.first->second = literal;
87 
88  return literal;
89 }
90 
92 {
93  // trivial cases
94 
95  if(expr.is_true())
96  {
97  return true;
98  }
99  else if(expr.is_false())
100  {
101  return false;
102  }
103  else if(expr.id() == ID_symbol)
104  {
105  symbolst::const_iterator result =
106  symbols.find(to_symbol_expr(expr).get_identifier());
107 
108  // This may fail if the symbol isn't Boolean or
109  // not in the formula.
110  if(result == symbols.end())
111  return {};
112 
113  return prop.l_get(result->second).is_true();
114  }
115  else if(expr.id() == ID_literal)
116  {
117  return prop.l_get(to_literal_expr(expr).get_literal()).is_true();
118  }
119 
120  // sub-expressions
121 
122  if(expr.id() == ID_not)
123  {
124  if(expr.type().id() == ID_bool)
125  {
126  auto tmp = get_bool(to_not_expr(expr).op());
127  if(tmp.has_value())
128  return !*tmp;
129  else
130  return {};
131  }
132  }
133  else if(expr.id() == ID_and || expr.id() == ID_or)
134  {
135  if(expr.type().id() == ID_bool && expr.operands().size() >= 1)
136  {
137  forall_operands(it, expr)
138  {
139  auto tmp = get_bool(*it);
140  if(!tmp.has_value())
141  return {};
142 
143  if(expr.id() == ID_and)
144  {
145  if(*tmp == false)
146  return false;
147  }
148  else // or
149  {
150  if(*tmp == true)
151  return true;
152  }
153  }
154 
155  return expr.id() == ID_and;
156  }
157  }
158 
159  // check cache
160 
161  cachet::const_iterator cache_result = cache.find(expr);
162  if(cache_result == cache.end())
163  return {}; // not in formula
164  else
165  return prop.l_get(cache_result->second).is_true();
166 }
167 
169 {
170  if(!use_cache || expr.id() == ID_symbol || expr.id() == ID_constant)
171  {
172  literalt literal = convert_bool(expr);
173  if(freeze_all && !literal.is_constant())
175  return literal;
176  }
177 
178  // check cache first
179  auto result = cache.insert({expr, literalt()});
180 
181  if(!result.second)
182  return result.first->second;
183 
184  literalt literal = convert_bool(expr);
185 
186  // insert into cache
187 
188  result.first->second = literal;
189  if(freeze_all && !literal.is_constant())
191 
192 #if 0
193  std::cout << literal << "=" << expr << '\n';
194 #endif
195 
196  return literal;
197 }
198 
200 {
201  PRECONDITION(expr.type().id() == ID_bool);
202 
203  const exprt::operandst &op = expr.operands();
204 
205  if(expr.is_constant())
206  {
207  if(expr.is_true())
208  return const_literal(true);
209  else
210  {
211  INVARIANT(
212  expr.is_false(),
213  "constant expression of type bool should be either true or false");
214  return const_literal(false);
215  }
216  }
217  else if(expr.id() == ID_symbol)
218  {
219  return get_literal(to_symbol_expr(expr).get_identifier());
220  }
221  else if(expr.id() == ID_literal)
222  {
223  return to_literal_expr(expr).get_literal();
224  }
225  else if(expr.id() == ID_nondet_symbol)
226  {
227  return prop.new_variable();
228  }
229  else if(expr.id() == ID_implies)
230  {
231  const implies_exprt &implies_expr = to_implies_expr(expr);
232  return prop.limplies(
233  convert(implies_expr.op0()), convert(implies_expr.op1()));
234  }
235  else if(expr.id() == ID_if)
236  {
237  const if_exprt &if_expr = to_if_expr(expr);
238  return prop.lselect(
239  convert(if_expr.cond()),
240  convert(if_expr.true_case()),
241  convert(if_expr.false_case()));
242  }
243  else if(expr.id() == ID_constraint_select_one)
244  {
246  op.size() >= 2,
247  "constraint_select_one should have at least two operands");
248 
249  std::vector<literalt> op_bv;
250  op_bv.reserve(op.size());
251 
252  forall_operands(it, expr)
253  op_bv.push_back(convert(*it));
254 
255  // add constraints
256 
257  bvt b;
258  b.reserve(op_bv.size() - 1);
259 
260  for(unsigned i = 1; i < op_bv.size(); i++)
261  b.push_back(prop.lequal(op_bv[0], op_bv[i]));
262 
264 
265  return op_bv[0];
266  }
267  else if(
268  expr.id() == ID_or || expr.id() == ID_and || expr.id() == ID_xor ||
269  expr.id() == ID_nor || expr.id() == ID_nand)
270  {
271  INVARIANT(
272  !op.empty(),
273  "operator '" + expr.id_string() + "' takes at least one operand");
274 
275  bvt bv;
276 
277  forall_expr(it, op)
278  bv.push_back(convert(*it));
279 
280  if(!bv.empty())
281  {
282  if(expr.id() == ID_or)
283  return prop.lor(bv);
284  else if(expr.id() == ID_nor)
285  return !prop.lor(bv);
286  else if(expr.id() == ID_and)
287  return prop.land(bv);
288  else if(expr.id() == ID_nand)
289  return !prop.land(bv);
290  else if(expr.id() == ID_xor)
291  return prop.lxor(bv);
292  }
293  }
294  else if(expr.id() == ID_not)
295  {
296  INVARIANT(op.size() == 1, "not takes one operand");
297  return !convert(op.front());
298  }
299  else if(expr.id() == ID_equal || expr.id() == ID_notequal)
300  {
301  INVARIANT(op.size() == 2, "equality takes two operands");
302  bool equal = (expr.id() == ID_equal);
303 
304  if(op[0].type().id() == ID_bool && op[1].type().id() == ID_bool)
305  {
306  literalt tmp1 = convert(op[0]), tmp2 = convert(op[1]);
307  return equal ? prop.lequal(tmp1, tmp2) : prop.lxor(tmp1, tmp2);
308  }
309  }
310  else if(expr.id() == ID_let)
311  {
312  const let_exprt &let_expr = to_let_expr(expr);
313  const auto &variables = let_expr.variables();
314  const auto &values = let_expr.values();
315 
316  // first check whether this is all boolean
317  const bool all_boolean =
318  let_expr.where().type().id() == ID_bool &&
319  std::all_of(values.begin(), values.end(), [](const exprt &e) {
320  return e.type().id() == ID_bool;
321  });
322 
323  if(all_boolean)
324  {
325  for(auto &binding : make_range(variables).zip(values))
326  {
327  literalt value_converted = convert(binding.second);
328 
329  // We expect the identifier of the bound symbols to be unique,
330  // and thus, these can go straight into the symbol map.
331  // This property also allows us to cache any subexpressions.
332  const irep_idt &id = binding.first.get_identifier();
333  symbols[id] = value_converted;
334  }
335 
336  literalt result = convert(let_expr.where());
337 
338  // remove again
339  for(auto &variable : variables)
340  symbols.erase(variable.get_identifier());
341 
342  return result;
343  }
344  }
345 
346  return convert_rest(expr);
347 }
348 
350 {
351  // fall through
352  ignoring(expr);
353  return prop.new_variable();
354 }
355 
357 {
359  return true;
360 
361  // optimization for constraint of the form
362  // new_variable = value
363 
364  if(expr.lhs().id() == ID_symbol)
365  {
366  const irep_idt &identifier = to_symbol_expr(expr.lhs()).get_identifier();
367 
368  literalt tmp = convert(expr.rhs());
369 
370  std::pair<symbolst::iterator, bool> result =
371  symbols.insert(std::pair<irep_idt, literalt>(identifier, tmp));
372 
373  if(result.second)
374  return false; // ok, inserted!
375 
376  // nah, already there
377  }
378 
379  return true;
380 }
381 
383 {
384  PRECONDITION(expr.type().id() == ID_bool);
385 
386  const bool has_only_boolean_operands = std::all_of(
387  expr.operands().begin(), expr.operands().end(), [](const exprt &expr) {
388  return expr.type().id() == ID_bool;
389  });
390 
391  if(has_only_boolean_operands)
392  {
393  if(expr.id() == ID_not)
394  {
395  add_constraints_to_prop(to_not_expr(expr).op(), !value);
396  return;
397  }
398  else
399  {
400  if(value)
401  {
402  // set_to_true
403 
404  if(expr.id() == ID_and)
405  {
406  forall_operands(it, expr)
407  add_constraints_to_prop(*it, true);
408 
409  return;
410  }
411  else if(expr.id() == ID_or)
412  {
413  // Special case for a CNF-clause,
414  // i.e., a constraint that's a disjunction.
415 
416  if(!expr.operands().empty())
417  {
418  bvt bv;
419  bv.reserve(expr.operands().size());
420 
421  forall_operands(it, expr)
422  bv.push_back(convert(*it));
423 
424  prop.lcnf(bv);
425  return;
426  }
427  }
428  else if(expr.id() == ID_implies)
429  {
430  const auto &implies_expr = to_implies_expr(expr);
431  literalt l_lhs = convert(implies_expr.lhs());
432  literalt l_rhs = convert(implies_expr.rhs());
433  prop.lcnf(!l_lhs, l_rhs);
434  return;
435  }
436  else if(expr.id() == ID_equal)
437  {
439  return;
440  }
441  }
442  else
443  {
444  // set_to_false
445  if(expr.id() == ID_implies) // !(a=>b) == (a && !b)
446  {
447  const implies_exprt &implies_expr = to_implies_expr(expr);
448 
449  add_constraints_to_prop(implies_expr.op0(), true);
450  add_constraints_to_prop(implies_expr.op1(), false);
451  return;
452  }
453  else if(expr.id() == ID_or) // !(a || b) == (!a && !b)
454  {
455  forall_operands(it, expr)
456  add_constraints_to_prop(*it, false);
457  return;
458  }
459  }
460  }
461  }
462 
463  // fall back to convert
464  prop.l_set_to(convert(expr), value);
465 }
466 
468 {
469  // fall through
470 
471  log.warning() << "warning: ignoring " << expr.pretty() << messaget::eom;
472 }
473 
475 {
476 }
477 
479 {
480  // post-processing isn't incremental yet
482  {
483  log.statistics() << "Post-processing" << messaget::eom;
484  post_process();
485  post_processing_done = true;
486  }
487 
488  log.statistics() << "Solving with " << prop.solver_text() << messaget::eom;
489 
490  switch(prop.prop_solve())
491  {
493  return resultt::D_SATISFIABLE;
497  return resultt::D_ERROR;
498  }
499 
500  UNREACHABLE;
501 }
502 
504 {
505  if(expr.type().id() == ID_bool)
506  {
507  auto value = get_bool(expr);
508 
509  if(value.has_value())
510  {
511  if(*value)
512  return true_exprt();
513  else
514  return false_exprt();
515  }
516  }
517 
518  exprt tmp = expr;
519  for(auto &op : tmp.operands())
520  {
521  exprt tmp_op = get(op);
522  op.swap(tmp_op);
523  }
524  return tmp;
525 }
526 
527 void prop_conv_solvert::print_assignment(std::ostream &out) const
528 {
529  for(const auto &symbol : symbols)
530  out << symbol.first << " = " << prop.l_get(symbol.second) << '\n';
531 }
532 
534 {
536 }
537 
538 const char *prop_conv_solvert::context_prefix = "prop_conv::context$";
539 
540 void prop_conv_solvert::set_to(const exprt &expr, bool value)
541 {
542  if(assumption_stack.empty())
543  {
544  // We are in the root context.
545  add_constraints_to_prop(expr, value);
546  }
547  else
548  {
549  // We have a child context. We add context_literal ==> expr to the formula.
551  or_exprt(literal_exprt(!assumption_stack.back()), expr), value);
552  }
553 }
554 
555 void prop_conv_solvert::push(const std::vector<exprt> &assumptions)
556 {
557  // We push the given assumptions as a single context onto the stack.
558  assumption_stack.reserve(assumption_stack.size() + assumptions.size());
559  for(const auto &assumption : assumptions)
560  assumption_stack.push_back(to_literal_expr(assumption).get_literal());
561  context_size_stack.push_back(assumptions.size());
562 
564 }
565 
567 {
568  // We create a new context literal.
569  literalt context_literal = convert(symbol_exprt(
571 
572  assumption_stack.push_back(context_literal);
573  context_size_stack.push_back(1);
574 
576 }
577 
579 {
580  // We remove the context from the stack.
581  assumption_stack.resize(assumption_stack.size() - context_size_stack.back());
582  context_size_stack.pop_back();
583 
585 }
586 
587 // This method out-of-line because gcc-5.5.0-12ubuntu1 20171010 miscompiles it
588 // when inline (in certain build configurations, notably -O2 -g0) by producing
589 // a non-virtual thunk with c++03 ABI but a function body with c++11 ABI, the
590 // mismatch leading to a missing vtable entry and consequent null-pointer deref
591 // whenever this function is called.
593 {
594  return "propositional reduction";
595 }
596 
599 {
600  ::with_solver_hardness(prop, handler);
601 }
603 {
604  if(auto hardness_collector = dynamic_cast<hardness_collectort *>(&prop))
605  {
606  hardness_collector->enable_hardness_collection();
607  }
608 }
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:76
prop_conv_solvert::assumption_stack
bvt assumption_stack
Assumptions on the stack.
Definition: prop_conv_solver.h:138
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:641
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:145
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:488
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:3029
propt::resultt::P_UNSATISFIABLE
@ P_UNSATISFIABLE
if_exprt
The trinary if-then-else operator.
Definition: std_expr.h:2964
decision_proceduret::resultt::D_UNSATISFIABLE
@ D_UNSATISFIABLE
prop_conv_solvert::symbols
symbolst symbols
Definition: prop_conv_solver.h:122
prop_conv_solvert::freeze_all
bool freeze_all
Definition: prop_conv_solver.h:77
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:141
exprt
Base class for all expressions.
Definition: expr.h:53
binary_exprt::lhs
exprt & lhs()
Definition: std_expr.h:631
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:597
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:92
prop_conv_solvert::convert_bool
virtual literalt convert_bool(const exprt &expr)
Definition: prop_conv_solver.cpp:199
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:82
propt::land
virtual literalt land(literalt a, literalt b)=0
equal_exprt
Equality.
Definition: std_expr.h:1190
if_exprt::false_case
exprt & false_case()
Definition: std_expr.h:3001
exprt::is_false
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:101
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:467
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:37
prop_conv_solvert::cache
cachet cache
Definition: prop_conv_solver.h:127
prop_conv_solver.h
let_exprt::variables
binding_exprt::variablest & variables()
convenience accessor for binding().variables()
Definition: std_expr.h:4246
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
literalt::is_true
bool is_true() const
Definition: literal.h:156
prop_conv_solvert::literal
bool literal(const symbol_exprt &expr, literalt &literal) const
Definition: prop_conv_solver.cpp:59
prop_conv_solvert::set_frozen
void set_frozen(literalt)
Definition: prop_conv_solver.cpp:27
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:109
or_exprt
Boolean OR.
Definition: std_expr.h:2245
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:135
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:111
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:4289
prop_conv_solvert::post_process
virtual void post_process()
Definition: prop_conv_solver.cpp:474
literalt::is_false
bool is_false() const
Definition: literal.h:161
irept::id_string
const std::string & id_string() const
Definition: irep.h:421
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:503
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:177
decision_proceduret::resultt::D_ERROR
@ D_ERROR
prop_conv_solvert::set_all_frozen
void set_all_frozen()
Definition: prop_conv_solver.cpp:32
irept::id
const irep_idt & id() const
Definition: irep.h:418
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:55
false_exprt
The Boolean constant false.
Definition: std_expr.h:3964
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:74
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:168
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:349
prop_conv_solvert::use_cache
bool use_cache
Definition: prop_conv_solver.h:75
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:382
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:15
if_exprt::true_case
exprt & true_case()
Definition: std_expr.h:2991
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:2868
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:592
to_implies_expr
const implies_exprt & to_implies_expr(const exprt &expr)
Cast an exprt to a implies_exprt.
Definition: std_expr.h:2225
prop_conv_solvert::dec_solve
decision_proceduret::resultt dec_solve() override
Run the decision procedure to solve the problem.
Definition: prop_conv_solver.cpp:478
exprt::is_constant
bool is_constant() const
Return whether the expression is a constant.
Definition: expr.cpp:85
if_exprt::cond
exprt & cond()
Definition: std_expr.h:2981
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:1230
prop_conv_solvert::print_assignment
void print_assignment(std::ostream &out) const override
Print satisfying assignment to out.
Definition: prop_conv_solver.cpp:527
implies_exprt
Boolean implication.
Definition: std_expr.h:2200
hardness_collectort
Definition: hardness_collector.h:23
prop_conv_solvert::log
messaget log
Definition: prop_conv_solver.h:133
exprt::operands
operandst & operands()
Definition: expr.h:95
let_exprt::values
operandst & values()
Definition: std_expr.h:4235
forall_expr
#define forall_expr(it, expr)
Definition: expr.h:29
true_exprt
The Boolean constant true.
Definition: std_expr.h:3955
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:566
binary_exprt::op1
exprt & op1()
Definition: expr.h:105
prop_conv_solvert::pop
void pop() override
Pop whatever is on top of the stack.
Definition: prop_conv_solver.cpp:578
let_exprt::where
exprt & where()
convenience accessor for binding().where()
Definition: std_expr.h:4258
prop_conv_solvert::enable_hardness_collection
void enable_hardness_collection() override
Definition: prop_conv_solver.cpp:602
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:91
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:4165
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:540
binary_exprt::op0
exprt & op0()
Definition: expr.h:102
validation_modet::INVARIANT
@ INVARIANT
prop_conv_solvert::prop
propt & prop
Definition: prop_conv_solver.h:131
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:356
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:533