cprover
prop_conv_solver.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: 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{
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 =
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 {
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;
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 {
463 return resultt::D_ERROR;
464 }
465
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
493void 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
504const char *prop_conv_solvert::context_prefix = "prop_conv::context$";
505
506void 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
521void 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.
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}
exprt & lhs()
Definition: std_expr.h:580
exprt & rhs()
Definition: std_expr.h:590
exprt & op0()
Definition: expr.h:99
exprt & op1()
Definition: expr.h:102
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
bool is_constant() const
Return whether the expression is a constant.
Definition: expr.cpp:26
typet & type()
Return the type of the expression.
Definition: expr.h:82
operandst & operands()
Definition: expr.h:92
The Boolean constant false.
Definition: std_expr.h:2865
The trinary if-then-else operator.
Definition: std_expr.h:2226
exprt & cond()
Definition: std_expr.h:2243
exprt & false_case()
Definition: std_expr.h:2263
exprt & true_case()
Definition: std_expr.h:2253
Boolean implication.
Definition: std_expr.h:2037
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:495
const std::string & id_string() const
Definition: irep.h:399
const irep_idt & id() const
Definition: irep.h:396
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
static eomt eom
Definition: message.h:297
mstreamt & status() const
Definition: message.h:414
Boolean OR.
Definition: std_expr.h:2082
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)
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 void finish_eager_conversion()
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 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 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:2856
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,...
static optionalt< smt_termt > get_identifier(const exprt &expr, const std::unordered_map< exprt, smt_identifier_termt, irep_hash > &expression_handle_identifiers, const std::unordered_map< exprt, smt_identifier_termt, irep_hash > &expression_identifiers)
#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:2291
const not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_exprt.
Definition: std_expr.h:2206
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:189
const implies_exprt & to_implies_expr(const exprt &expr)
Cast an exprt to a implies_exprt.
Definition: std_expr.h:2062
const equal_exprt & to_equal_expr(const exprt &expr)
Cast an exprt to an equal_exprt.
Definition: std_expr.h:1265
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.