1 /*++
2 Copyright (c) 2011 Microsoft Corporation
3
4 Module Name:
5
6 goal2sat.cpp
7
8 Abstract:
9
10 "Compile" a goal into the SAT engine.
11 Atoms are "abstracted" into boolean variables.
12 The mapping between boolean variables and atoms
13 can be used to convert back the state of the
14 SAT engine into a goal.
15
16 The idea is to support scenarios such as:
17 1) simplify, blast, convert into SAT, and solve
18 2) convert into SAT, apply SAT for a while, learn new units, and translate back into a goal.
19 3) convert into SAT, apply SAT preprocessor (failed literal propagation, resolution, etc) and translate back into a goal.
20 4) Convert boolean structure into SAT, convert atoms into another engine, combine engines using lazy combination, solve.
21
22 Author:
23
24 Leonardo (leonardo) 2011-10-26
25
26 Notes:
27
28 --*/
29 #include "util/ref_util.h"
30 #include "ast/ast_smt2_pp.h"
31 #include "ast/ast_pp.h"
32 #include "ast/ast_smt2_pp.h"
33 #include "ast/ast_ll_pp.h"
34 #include "ast/pb_decl_plugin.h"
35 #include "ast/ast_util.h"
36 #include "ast/for_each_expr.h"
37 #include "model/model_evaluator.h"
38 #include "model/model_v2_pp.h"
39 #include "tactic/tactic.h"
40 #include "tactic/generic_model_converter.h"
41 #include "sat/sat_cut_simplifier.h"
42 #include "sat/sat_drat.h"
43 #include "sat/tactic/goal2sat.h"
44 #include "sat/smt/ba_solver.h"
45 #include "sat/smt/euf_solver.h"
46 #include "sat/smt/sat_th.h"
47 #include "sat/sat_params.hpp"
48 #include<sstream>
49
50 struct goal2sat::imp : public sat::sat_internalizer {
51 struct frame {
52 app * m_t;
53 unsigned m_root:1;
54 unsigned m_sign:1;
55 unsigned m_idx;
framegoal2sat::imp::frame56 frame(app * t, bool r, bool s, unsigned idx):
57 m_t(t), m_root(r), m_sign(s), m_idx(idx) {}
58 };
59 ast_manager & m;
60 pb_util pb;
61 svector<frame> m_frame_stack;
62 svector<sat::literal> m_result_stack;
63 obj_map<app, sat::literal> m_cache;
64 obj_hashtable<expr> m_interface_vars;
65 sat::solver_core & m_solver;
66 atom2bool_var & m_map;
67 dep2asm_map & m_dep2asm;
68 obj_map<expr, sat::bool_var>* m_expr2var_replay { nullptr };
69 sat::literal m_true;
70 bool m_ite_extra;
71 unsigned long long m_max_memory;
72 expr_ref_vector m_trail;
73 func_decl_ref_vector m_unhandled_funs;
74 bool m_default_external;
75 bool m_xor_solver;
76 bool m_euf { false };
77 bool m_drat { false };
78 bool m_is_redundant { false };
79 bool m_top_level { false };
80 sat::literal_vector aig_lits;
81
impgoal2sat::imp82 imp(ast_manager & _m, params_ref const & p, sat::solver_core & s, atom2bool_var & map, dep2asm_map& dep2asm, bool default_external):
83 m(_m),
84 pb(m),
85 m_solver(s),
86 m_map(map),
87 m_dep2asm(dep2asm),
88 m_trail(m),
89 m_unhandled_funs(m),
90 m_default_external(default_external) {
91 updt_params(p);
92 m_true = sat::null_literal;
93 }
94
~impgoal2sat::imp95 ~imp() override {}
96
97
aiggoal2sat::imp98 sat::cut_simplifier* aig() {
99 return m_solver.get_cut_simplifier();
100 }
101
updt_paramsgoal2sat::imp102 void updt_params(params_ref const & p) {
103 sat_params sp(p);
104 m_ite_extra = p.get_bool("ite_extra", true);
105 m_max_memory = megabytes_to_bytes(p.get_uint("max_memory", UINT_MAX));
106 m_xor_solver = p.get_bool("xor_solver", false);
107 m_euf = sp.euf();
108 m_drat = sp.drat_file().is_non_empty_string();
109 }
110
throw_op_not_handledgoal2sat::imp111 void throw_op_not_handled(std::string const& s) {
112 std::string s0 = "operator " + s + " not supported, apply simplifier before invoking translator";
113 throw tactic_exception(std::move(s0));
114 }
115
mk_statusgoal2sat::imp116 sat::status mk_status() const {
117 return sat::status::th(m_is_redundant, m.get_basic_family_id());
118 }
119
relevancy_enabledgoal2sat::imp120 bool relevancy_enabled() {
121 return m_euf && ensure_euf()->relevancy_enabled();
122 }
123
top_level_relevantgoal2sat::imp124 bool top_level_relevant() {
125 return m_top_level && relevancy_enabled();
126 }
127
add_dual_defgoal2sat::imp128 void add_dual_def(unsigned n, sat::literal const* lits) {
129 if (relevancy_enabled())
130 ensure_euf()->add_aux(n, lits);
131 }
132
add_dual_rootgoal2sat::imp133 void add_dual_root(unsigned n, sat::literal const* lits) {
134 if (relevancy_enabled())
135 ensure_euf()->add_root(n, lits);
136 }
137
mk_clausegoal2sat::imp138 void mk_clause(sat::literal l) {
139 mk_clause(1, &l);
140 }
141
mk_clausegoal2sat::imp142 void mk_clause(sat::literal l1, sat::literal l2) {
143 sat::literal lits[2] = { l1, l2 };
144 mk_clause(2, lits);
145 }
146
mk_clausegoal2sat::imp147 void mk_clause(sat::literal l1, sat::literal l2, sat::literal l3) {
148 sat::literal lits[3] = { l1, l2, l3 };
149 mk_clause(3, lits);
150 }
151
mk_clausegoal2sat::imp152 void mk_clause(unsigned n, sat::literal * lits) {
153 TRACE("goal2sat", tout << "mk_clause: "; for (unsigned i = 0; i < n; i++) tout << lits[i] << " "; tout << "\n";);
154 add_dual_def(n, lits);
155 m_solver.add_clause(n, lits, mk_status());
156 }
157
mk_root_clausegoal2sat::imp158 void mk_root_clause(sat::literal l) {
159 mk_root_clause(1, &l);
160 }
161
mk_root_clausegoal2sat::imp162 void mk_root_clause(sat::literal l1, sat::literal l2) {
163 sat::literal lits[2] = { l1, l2 };
164 mk_root_clause(2, lits);
165 }
166
mk_root_clausegoal2sat::imp167 void mk_root_clause(sat::literal l1, sat::literal l2, sat::literal l3) {
168 sat::literal lits[3] = { l1, l2, l3 };
169 mk_root_clause(3, lits);
170 }
171
mk_root_clausegoal2sat::imp172 void mk_root_clause(unsigned n, sat::literal * lits) {
173 TRACE("goal2sat", tout << "mk_root_clause: "; for (unsigned i = 0; i < n; i++) tout << lits[i] << " "; tout << "\n";);
174 add_dual_root(n, lits);
175 m_solver.add_clause(n, lits, m_is_redundant ? mk_status() : sat::status::input());
176 }
177
add_vargoal2sat::imp178 sat::bool_var add_var(bool is_ext, expr* n) {
179 sat::bool_var v;
180 if (m_expr2var_replay && m_expr2var_replay->find(n, v))
181 return v;
182 v = m_solver.add_var(is_ext);
183 log_def(v, n);
184 if (top_level_relevant() && !is_bool_op(n))
185 ensure_euf()->track_relevancy(v);
186 return v;
187 }
188
log_defgoal2sat::imp189 void log_def(sat::bool_var v, expr* n) {
190 if (m_drat && m_euf)
191 ensure_euf()->drat_bool_def(v, n);
192 }
193
mk_truegoal2sat::imp194 sat::literal mk_true() {
195 if (m_true == sat::null_literal) {
196 // create fake variable to represent true;
197 m_true = sat::literal(add_var(false, m.mk_true()), false);
198 mk_clause(m_true); // v is true
199 }
200 return m_true;
201 }
202
to_bool_vargoal2sat::imp203 sat::bool_var to_bool_var(expr* e) override {
204 sat::literal l;
205 sat::bool_var v = m_map.to_bool_var(e);
206 if (v != sat::null_bool_var)
207 return v;
208 if (is_app(e) && m_cache.find(to_app(e), l) && !l.sign())
209 return l.var();
210 return sat::null_bool_var;
211 }
212
213
set_expr2var_replaygoal2sat::imp214 void set_expr2var_replay(obj_map<expr, sat::bool_var>* r) override {
215 m_expr2var_replay = r;
216 }
217
mk_bool_vargoal2sat::imp218 sat::bool_var mk_bool_var(expr* t) {
219 force_push();
220 sat::bool_var v;
221 if (!m_expr2var_replay || !m_expr2var_replay->find(t, v))
222 v = add_var(true, t);
223 m_map.insert(t, v);
224 return v;
225 }
226
add_bool_vargoal2sat::imp227 sat::bool_var add_bool_var(expr* t) override {
228 sat::bool_var v = m_map.to_bool_var(t);
229 if (v == sat::null_bool_var)
230 v = mk_bool_var(t);
231 else
232 m_solver.set_external(v);
233 return v;
234 }
235
236 unsigned m_num_scopes{ 0 };
237
force_pushgoal2sat::imp238 void force_push() {
239 for (; m_num_scopes > 0; --m_num_scopes)
240 m_map.push();
241 }
242
pushgoal2sat::imp243 void push() override {
244 ++m_num_scopes;
245 }
246
popgoal2sat::imp247 void pop(unsigned n) override {
248 if (n <= m_num_scopes) {
249 m_num_scopes -= n;
250 return;
251 }
252 n -= m_num_scopes;
253 m_num_scopes = 0;
254 m_cache.reset();
255 m_map.pop(n);
256 }
257
cachegoal2sat::imp258 void cache(app* t, sat::literal l) override {
259 m_cache.insert(t, l);
260 }
261
convert_atomgoal2sat::imp262 void convert_atom(expr * t, bool root, bool sign) {
263 SASSERT(m.is_bool(t));
264 sat::literal l;
265 sat::bool_var v = m_map.to_bool_var(t);
266 if (v == sat::null_bool_var) {
267 if (m.is_true(t)) {
268 l = sign ? ~mk_true() : mk_true();
269 }
270 else if (m.is_false(t)) {
271 l = sign ? mk_true() : ~mk_true();
272 }
273 else {
274 if (m_euf) {
275 convert_euf(t, root, sign);
276 return;
277 }
278 if (!is_uninterp_const(t)) {
279 if (!is_app(t)) {
280 std::ostringstream strm;
281 strm << mk_ismt2_pp(t, m);
282 throw_op_not_handled(strm.str());
283 }
284 else
285 m_unhandled_funs.push_back(to_app(t)->get_decl());
286 }
287 v = mk_bool_var(t);
288 l = sat::literal(v, sign);
289 bool ext = m_default_external || !is_uninterp_const(t) || m_interface_vars.contains(t);
290 if (ext)
291 m_solver.set_external(v);
292 TRACE("sat", tout << "new_var: " << v << ": " << mk_bounded_pp(t, m, 2) << " " << is_uninterp_const(t) << "\n";);
293 }
294 }
295 else {
296 SASSERT(v != sat::null_bool_var);
297 l = sat::literal(v, sign);
298 m_solver.set_eliminated(v, false);
299 }
300 SASSERT(l != sat::null_literal);
301 if (root)
302 mk_root_clause(l);
303 else
304 m_result_stack.push_back(l);
305 }
306
convert_appgoal2sat::imp307 bool convert_app(app* t, bool root, bool sign) {
308 if (!m_euf && pb.is_pb(t)) {
309 m_frame_stack.push_back(frame(to_app(t), root, sign, 0));
310 return false;
311 }
312 else {
313 convert_atom(t, root, sign);
314 return true;
315 }
316 }
317
process_cachedgoal2sat::imp318 bool process_cached(app* t, bool root, bool sign) {
319 sat::literal l = sat::null_literal;
320 if (!m_cache.find(t, l))
321 return false;
322 if (sign)
323 l.neg();
324 if (root)
325 mk_root_clause(l);
326 else
327 m_result_stack.push_back(l);
328 return true;
329 }
330
visitgoal2sat::imp331 bool visit(expr * t, bool root, bool sign) {
332 SASSERT(m.is_bool(t));
333 if (!is_app(t)) {
334 convert_atom(t, root, sign);
335 return true;
336 }
337 if (process_cached(to_app(t), root, sign))
338 return true;
339 if (to_app(t)->get_family_id() != m.get_basic_family_id())
340 return convert_app(to_app(t), root, sign);
341 switch (to_app(t)->get_decl_kind()) {
342 case OP_NOT:
343 case OP_OR:
344 case OP_AND:
345 case OP_ITE:
346 case OP_XOR:
347 case OP_IMPLIES:
348 m_frame_stack.push_back(frame(to_app(t), root, sign, 0));
349 return false;
350 case OP_EQ:
351 if (m.is_bool(to_app(t)->get_arg(1))) {
352 m_frame_stack.push_back(frame(to_app(t), root, sign, 0));
353 return false;
354 }
355 else {
356 convert_atom(t, root, sign);
357 return true;
358 }
359 case OP_DISTINCT: {
360 if (m_euf) {
361 convert_euf(t, root, sign);
362 return true;
363 }
364 TRACE("goal2sat_not_handled", tout << mk_ismt2_pp(t, m) << "\n";);
365 std::ostringstream strm;
366 strm << mk_ismt2_pp(t, m);
367 throw_op_not_handled(strm.str());
368 }
369 default:
370 convert_atom(t, root, sign);
371 return true;
372 }
373 }
374
convert_orgoal2sat::imp375 void convert_or(app * t, bool root, bool sign) {
376 TRACE("goal2sat", tout << "convert_or:\n" << mk_bounded_pp(t, m, 2) << " root " << root << " stack " << m_result_stack.size() << "\n";);
377 unsigned num = t->get_num_args();
378 SASSERT(num <= m_result_stack.size());
379 unsigned old_sz = m_result_stack.size() - num;
380 if (root) {
381 SASSERT(num == m_result_stack.size());
382 if (sign) {
383 // this case should not really happen.
384 for (unsigned i = 0; i < num; i++) {
385 sat::literal l = m_result_stack[i];
386 l.neg();
387 mk_root_clause(l);
388 }
389 }
390 else {
391 mk_root_clause(m_result_stack.size(), m_result_stack.c_ptr());
392 }
393 m_result_stack.shrink(old_sz);
394 }
395 else {
396 SASSERT(num <= m_result_stack.size());
397 sat::bool_var k = add_var(false, t);
398 sat::literal l(k, false);
399 m_cache.insert(t, l);
400 sat::literal * lits = m_result_stack.end() - num;
401 for (unsigned i = 0; i < num; i++)
402 mk_clause(~lits[i], l);
403
404 m_result_stack.push_back(~l);
405 lits = m_result_stack.end() - num - 1;
406 if (aig()) {
407 aig_lits.reset();
408 aig_lits.append(num, lits);
409 }
410 // remark: mk_clause may perform destructive updated to lits.
411 // I have to execute it after the binary mk_clause above.
412 mk_clause(num+1, lits);
413 if (aig())
414 aig()->add_or(l, num, aig_lits.c_ptr());
415
416 m_solver.set_phase(~l);
417 m_result_stack.shrink(old_sz);
418 if (sign)
419 l.neg();
420 m_result_stack.push_back(l);
421 }
422 }
423
convert_andgoal2sat::imp424 void convert_and(app * t, bool root, bool sign) {
425 TRACE("goal2sat", tout << "convert_and:\n" << mk_bounded_pp(t, m, 2) << " root: " << root << " result stack: " << m_result_stack.size() << "\n";);
426
427 unsigned num = t->get_num_args();
428 unsigned old_sz = m_result_stack.size() - num;
429 SASSERT(num <= m_result_stack.size());
430 if (root) {
431 if (sign) {
432 for (unsigned i = 0; i < num; ++i) {
433 m_result_stack[i].neg();
434 }
435 mk_root_clause(m_result_stack.size(), m_result_stack.c_ptr());
436 }
437 else {
438 for (unsigned i = 0; i < num; ++i) {
439 mk_root_clause(m_result_stack[i]);
440 }
441 }
442 m_result_stack.shrink(old_sz);
443 }
444 else {
445 SASSERT(num <= m_result_stack.size());
446 sat::bool_var k = add_var(false, t);
447 sat::literal l(k, false);
448 m_cache.insert(t, l);
449 sat::literal * lits = m_result_stack.end() - num;
450
451 // l => /\ lits
452 for (unsigned i = 0; i < num; i++) {
453 mk_clause(~l, lits[i]);
454 }
455 // /\ lits => l
456 for (unsigned i = 0; i < num; ++i) {
457 m_result_stack[m_result_stack.size() - num + i].neg();
458 }
459 m_result_stack.push_back(l);
460 lits = m_result_stack.end() - num - 1;
461 if (aig()) {
462 aig_lits.reset();
463 aig_lits.append(num, lits);
464 }
465 mk_clause(num+1, lits);
466 if (aig()) {
467 aig()->add_and(l, num, aig_lits.c_ptr());
468 }
469 m_solver.set_phase(l);
470 if (sign)
471 l.neg();
472
473 m_result_stack.shrink(old_sz);
474 m_result_stack.push_back(l);
475 TRACE("goal2sat", tout << m_result_stack << "\n";);
476 }
477 }
478
convert_itegoal2sat::imp479 void convert_ite(app * n, bool root, bool sign) {
480 unsigned sz = m_result_stack.size();
481 SASSERT(sz >= 3);
482 sat::literal c = m_result_stack[sz-3];
483 sat::literal t = m_result_stack[sz-2];
484 sat::literal e = m_result_stack[sz-1];
485 m_result_stack.shrink(sz - 3);
486 if (root) {
487 SASSERT(sz == 3);
488 if (sign) {
489 mk_root_clause(~c, ~t);
490 mk_root_clause(c, ~e);
491 }
492 else {
493 mk_root_clause(~c, t);
494 mk_root_clause(c, e);
495 }
496 }
497 else {
498 sat::bool_var k = add_var(false, n);
499 sat::literal l(k, false);
500 m_cache.insert(n, l);
501 mk_clause(~l, ~c, t);
502 mk_clause(~l, c, e);
503 mk_clause(l, ~c, ~t);
504 mk_clause(l, c, ~e);
505 if (m_ite_extra) {
506 mk_clause(~t, ~e, l);
507 mk_clause(t, e, ~l);
508 }
509 if (aig()) aig()->add_ite(l, c, t, e);
510 if (sign)
511 l.neg();
512
513 m_result_stack.push_back(l);
514 }
515 }
516
convert_impliesgoal2sat::imp517 void convert_implies(app* t, bool root, bool sign) {
518 SASSERT(t->get_num_args() == 2);
519 unsigned sz = m_result_stack.size();
520 SASSERT(sz >= 2);
521 sat::literal l2 = m_result_stack[sz - 1];
522 sat::literal l1 = m_result_stack[sz - 2];
523 m_result_stack.shrink(sz - 2);
524 if (root) {
525 SASSERT(sz == 2);
526 if (sign) {
527 mk_root_clause(l1);
528 mk_root_clause(~l2);
529 }
530 else {
531 mk_root_clause(~l1, l2);
532 }
533 }
534 else {
535 sat::bool_var k = add_var(false, t);
536 sat::literal l(k, false);
537 m_cache.insert(t, l);
538 // l <=> (l1 => l2)
539 mk_clause(~l, ~l1, l2);
540 mk_clause(l1, l);
541 mk_clause(~l2, l);
542 if (sign)
543 l.neg();
544 m_result_stack.push_back(l);
545 }
546 }
547
convert_iff2goal2sat::imp548 void convert_iff2(app * t, bool root, bool sign) {
549 SASSERT(t->get_num_args() == 2);
550 unsigned sz = m_result_stack.size();
551 SASSERT(sz >= 2);
552 sat::literal l1 = m_result_stack[sz-1];
553 sat::literal l2 = m_result_stack[sz-2];
554 m_result_stack.shrink(sz - 2);
555 if (root) {
556 SASSERT(sz == 2);
557 if (sign) {
558 mk_root_clause(l1, l2);
559 mk_root_clause(~l1, ~l2);
560 }
561 else {
562 mk_root_clause(l1, ~l2);
563 mk_root_clause(~l1, l2);
564 }
565 }
566 else {
567 sat::bool_var k = add_var(false, t);
568 sat::literal l(k, false);
569 mk_clause(~l, l1, ~l2);
570 mk_clause(~l, ~l1, l2);
571 mk_clause(l, l1, l2);
572 mk_clause(l, ~l1, ~l2);
573 if (aig()) aig()->add_iff(l, l1, l2);
574 m_cache.insert(t, m.is_xor(t) ? ~l : l);
575 if (sign)
576 l.neg();
577 m_result_stack.push_back(l);
578 }
579 }
580
convert_iffgoal2sat::imp581 void convert_iff(app * t, bool root, bool sign) {
582 if (!m_euf && is_xor(t))
583 convert_ba(t, root, sign);
584 else
585 convert_iff2(t, root, sign);
586 }
587
interpreted_funsgoal2sat::imp588 func_decl_ref_vector const& interpreted_funs() {
589 auto* ext = dynamic_cast<euf::solver*>(m_solver.get_extension());
590 if (ext)
591 return ext->unhandled_functions();
592 return m_unhandled_funs;
593 }
594
ensure_eufgoal2sat::imp595 euf::solver* ensure_euf() {
596 SASSERT(m_euf);
597 sat::extension* ext = m_solver.get_extension();
598 euf::solver* euf = nullptr;
599 if (!ext) {
600 euf = alloc(euf::solver, m, *this);
601 m_solver.set_extension(euf);
602 #if 0
603 std::function<solver*(void)> mk_solver = [&]() {
604 return mk_inc_sat_solver(m, m_params, true);
605 };
606 euf->set_mk_solver(mk_solver);
607 #endif
608 }
609 else {
610 euf = dynamic_cast<euf::solver*>(ext);
611 }
612 if (!euf)
613 throw default_exception("cannot convert to euf");
614 return euf;
615 }
616
convert_eufgoal2sat::imp617 void convert_euf(expr* e, bool root, bool sign) {
618 SASSERT(m_euf);
619 TRACE("goal2sat", tout << "convert-euf " << mk_bounded_pp(e, m, 2) << " root " << root << "\n";);
620 euf::solver* euf = ensure_euf();
621 sat::literal lit;
622 {
623 flet<bool> _top(m_top_level, false);
624 lit = euf->internalize(e, sign, root, m_is_redundant);
625 }
626 if (lit == sat::null_literal)
627 return;
628 if (top_level_relevant())
629 euf->track_relevancy(lit.var());
630 if (root)
631 mk_root_clause(lit);
632 else
633 m_result_stack.push_back(lit);
634 }
635
convert_bagoal2sat::imp636 void convert_ba(app* t, bool root, bool sign) {
637 SASSERT(!m_euf);
638 sat::extension* ext = dynamic_cast<sat::ba_solver*>(m_solver.get_extension());
639 euf::th_solver* th = nullptr;
640 if (!ext) {
641 th = alloc(sat::ba_solver, m, *this, pb.get_family_id());
642 m_solver.set_extension(th);
643 th->push_scopes(m_solver.num_scopes());
644 }
645 else {
646 th = dynamic_cast<euf::th_solver*>(ext);
647 SASSERT(th);
648 }
649 auto lit = th->internalize(t, sign, root, m_is_redundant);
650 m_result_stack.shrink(m_result_stack.size() - t->get_num_args());
651 if (lit == sat::null_literal)
652 return;
653 if (root)
654 mk_root_clause(lit);
655 else
656 m_result_stack.push_back(lit);
657 }
658
convertgoal2sat::imp659 void convert(app * t, bool root, bool sign) {
660 if (t->get_family_id() == m.get_basic_family_id()) {
661 switch (to_app(t)->get_decl_kind()) {
662 case OP_OR:
663 convert_or(t, root, sign);
664 break;
665 case OP_AND:
666 convert_and(t, root, sign);
667 break;
668 case OP_ITE:
669 convert_ite(t, root, sign);
670 break;
671 case OP_EQ:
672 convert_iff(t, root, sign);
673 break;
674 case OP_XOR:
675 convert_iff(t, root, !sign);
676 break;
677 case OP_IMPLIES:
678 convert_implies(t, root, sign);
679 break;
680 default:
681 UNREACHABLE();
682 }
683 SASSERT(!root || m_result_stack.empty());
684 }
685 else if (!m_euf && pb.is_pb(t)) {
686 convert_ba(t, root, sign);
687 }
688 else {
689 UNREACHABLE();
690 }
691 }
692
is_xorgoal2sat::imp693 bool is_xor(app* t) const {
694 return m_xor_solver && m.is_iff(t) && m.is_iff(t->get_arg(1));
695 }
696
697 struct scoped_stack {
698 imp& i;
699 sat::literal_vector& r;
700 unsigned rsz;
701 svector<frame>& frames;
702 unsigned fsz;
703 bool is_root;
scoped_stackgoal2sat::imp::scoped_stack704 scoped_stack(imp& x, bool is_root) :
705 i(x), r(i.m_result_stack), rsz(r.size()), frames(x.m_frame_stack), fsz(frames.size()), is_root(is_root)
706 {}
~scoped_stackgoal2sat::imp::scoped_stack707 ~scoped_stack() {
708 if (frames.size() > fsz) {
709 frames.shrink(fsz);
710 r.shrink(rsz);
711 return;
712 }
713 SASSERT(i.m.limit().is_canceled() || frames.size() == fsz);
714 SASSERT(i.m.limit().is_canceled() || !is_root || rsz == r.size());
715 SASSERT(i.m.limit().is_canceled() || is_root || rsz + 1 == r.size());
716 }
717 };
718
processgoal2sat::imp719 void process(expr* n, bool is_root, bool redundant) {
720 TRACE("goal2sat", tout << "process-begin " << mk_bounded_pp(n, m, 3)
721 << " root: " << is_root
722 << " result-stack: " << m_result_stack.size()
723 << " frame-stack: " << m_frame_stack.size() << "\n";);
724 flet<bool> _is_redundant(m_is_redundant, redundant);
725 scoped_stack _sc(*this, is_root);
726 unsigned sz = m_frame_stack.size();
727 if (visit(n, is_root, false))
728 return;
729
730 while (m_frame_stack.size() > sz) {
731 loop:
732 if (!m.inc())
733 throw tactic_exception(m.limit().get_cancel_msg());
734 if (memory::get_allocation_size() > m_max_memory)
735 throw tactic_exception(TACTIC_MAX_MEMORY_MSG);
736 unsigned fsz = m_frame_stack.size();
737 frame const& _fr = m_frame_stack[fsz-1];
738 app * t = _fr.m_t;
739 bool root = _fr.m_root;
740 bool sign = _fr.m_sign;
741 TRACE("goal2sat_bug", tout << "result stack\n";
742 tout << "ref-count: " << t->get_ref_count() << "\n";
743 tout << mk_bounded_pp(t, m, 3) << " root: " << root << " sign: " << sign << "\n";
744 tout << m_result_stack << "\n";);
745 if (_fr.m_idx == 0 && process_cached(t, root, sign)) {
746 m_frame_stack.pop_back();
747 continue;
748 }
749 if (m.is_not(t)) {
750 m_frame_stack.pop_back();
751 visit(t->get_arg(0), root, !sign);
752 continue;
753 }
754 if (!m_euf && is_xor(t)) {
755 convert_ba(t, root, sign);
756 m_frame_stack.pop_back();
757 continue;
758 }
759 unsigned num = t->get_num_args();
760 while (m_frame_stack[fsz-1].m_idx < num) {
761 expr * arg = t->get_arg(m_frame_stack[fsz-1].m_idx);
762 m_frame_stack[fsz - 1].m_idx++;
763 if (!visit(arg, false, false))
764 goto loop;
765 TRACE("goal2sat_bug", tout << "visit " << mk_bounded_pp(t, m, 2) << " result stack: " << m_result_stack.size() << "\n";);
766 }
767 TRACE("goal2sat_bug", tout << "converting\n";
768 tout << mk_bounded_pp(t, m, 2) << " root: " << root << " sign: " << sign << "\n";
769 tout << m_result_stack << "\n";);
770 SASSERT(m_frame_stack.size() > sz);
771 convert(t, root, sign);
772 m_frame_stack.pop_back();
773 }
774 TRACE("goal2sat", tout
775 << "done process: " << mk_bounded_pp(n, m, 3)
776 << " frame-stack: " << m_frame_stack.size()
777 << " result-stack: " << m_result_stack.size() << "\n";);
778 }
779
internalizegoal2sat::imp780 sat::literal internalize(expr* n, bool redundant) override {
781 flet<bool> _top(m_top_level, false);
782 unsigned sz = m_result_stack.size();
783 (void)sz;
784 SASSERT(n->get_ref_count() > 0);
785 TRACE("goal2sat", tout << "internalize " << mk_bounded_pp(n, m, 2) << "\n";);
786 process(n, false, redundant);
787 SASSERT(m_result_stack.size() == sz + 1);
788 sat::literal result = m_result_stack.back();
789 m_result_stack.pop_back();
790 if (!result.sign() && m_map.to_bool_var(n) == sat::null_bool_var)
791 m_map.insert(n, result.var());
792 return result;
793 }
794
is_bool_opgoal2sat::imp795 bool is_bool_op(expr* t) const override {
796 if (!is_app(t))
797 return false;
798 if (to_app(t)->get_family_id() == m.get_basic_family_id()) {
799 switch (to_app(t)->get_decl_kind()) {
800 case OP_OR:
801 case OP_AND:
802 case OP_TRUE:
803 case OP_FALSE:
804 case OP_NOT:
805 case OP_IMPLIES:
806 case OP_XOR:
807 return true;
808 case OP_ITE:
809 case OP_EQ:
810 return m.is_bool(to_app(t)->get_arg(1));
811 default:
812 return false;
813 }
814 }
815 else if (!m_euf && to_app(t)->get_family_id() == pb.get_family_id())
816 return true;
817 else
818 return false;
819 }
820
processgoal2sat::imp821 void process(expr * n) {
822 flet<bool> _top(m_top_level, true);
823 VERIFY(m_result_stack.empty());
824 TRACE("goal2sat", tout << "assert: " << mk_bounded_pp(n, m, 3) << "\n";);
825 process(n, true, m_is_redundant);
826 CTRACE("goal2sat", !m_result_stack.empty(), tout << m_result_stack << "\n";);
827 SASSERT(m_result_stack.empty());
828 }
829
insert_depgoal2sat::imp830 void insert_dep(expr* dep0, expr* dep, bool sign) {
831 SASSERT(sign || dep0 == dep); // !sign || (not dep0) == dep.
832 SASSERT(!sign || m.is_not(dep0));
833 expr_ref new_dep(m), fml(m);
834 if (is_uninterp_const(dep)) {
835 new_dep = dep;
836 }
837 else {
838 new_dep = m.mk_fresh_const("dep", m.mk_bool_sort());
839 m_trail.push_back(new_dep);
840 m_interface_vars.insert(new_dep);
841 fml = m.mk_iff(new_dep, dep);
842 process(fml);
843 }
844 convert_atom(new_dep, false, false);
845 sat::literal lit = m_result_stack.back();
846 m_dep2asm.insert(dep0, sign?~lit:lit);
847 m_result_stack.pop_back();
848 }
849
operator ()goal2sat::imp850 void operator()(goal const & g) {
851 struct scoped_reset {
852 imp& i;
853 scoped_reset(imp& i) :i(i) {}
854 ~scoped_reset() {
855 i.m_interface_vars.reset();
856 i.m_cache.reset();
857 }
858 };
859 scoped_reset _reset(*this);
860 collect_boolean_interface(g, m_interface_vars);
861 unsigned size = g.size();
862 expr_ref f(m), d_new(m);
863 ptr_vector<expr> deps;
864 expr_ref_vector fmls(m);
865 for (unsigned idx = 0; idx < size; idx++) {
866 f = g.form(idx);
867 // Add assumptions.
868 if (g.dep(idx)) {
869 deps.reset();
870 fmls.reset();
871 m.linearize(g.dep(idx), deps);
872 fmls.push_back(f);
873 for (expr * d : deps) {
874 expr * d1 = d;
875 SASSERT(m.is_bool(d));
876 bool sign = m.is_not(d, d1);
877
878 insert_dep(d, d1, sign);
879 if (d == f) {
880 goto skip_dep;
881 }
882 if (sign) {
883 d_new = d1;
884 }
885 else {
886 d_new = m.mk_not(d);
887 }
888 fmls.push_back(d_new);
889 }
890 f = m.mk_or(fmls);
891 }
892 TRACE("goal2sat", tout << mk_bounded_pp(f, m, 2) << "\n";);
893 process(f);
894 skip_dep:
895 ;
896 }
897 }
898
update_modelgoal2sat::imp899 void update_model(model_ref& mdl) {
900 auto* ext = dynamic_cast<euf::solver*>(m_solver.get_extension());
901 if (ext)
902 ext->update_model(mdl);
903 }
904
user_pushgoal2sat::imp905 void user_push() {
906
907 }
908
user_popgoal2sat::imp909 void user_pop(unsigned n) {
910 m_true = sat::null_literal;
911 }
912
913 };
914
915 struct unsupported_bool_proc {
916 struct found {};
917 ast_manager & m;
unsupported_bool_procunsupported_bool_proc918 unsupported_bool_proc(ast_manager & _m):m(_m) {}
operator ()unsupported_bool_proc919 void operator()(var *) {}
operator ()unsupported_bool_proc920 void operator()(quantifier *) {}
operator ()unsupported_bool_proc921 void operator()(app * n) {
922 if (n->get_family_id() == m.get_basic_family_id()) {
923 switch (n->get_decl_kind()) {
924 case OP_DISTINCT:
925 throw found();
926 default:
927 break;
928 }
929 }
930 }
931 };
932
933 /**
934 \brief Return true if s contains an unsupported Boolean operator.
935 goal_rewriter (with the following configuration) can be used to
936 eliminate unsupported operators.
937 :elim-and true
938 :blast-distinct true
939 */
has_unsupported_bool(goal const & g)940 bool goal2sat::has_unsupported_bool(goal const & g) {
941 return false && test<unsupported_bool_proc>(g);
942 }
943
goal2sat()944 goal2sat::goal2sat():
945 m_imp(nullptr) {
946 }
947
~goal2sat()948 goal2sat::~goal2sat() {
949 dealloc(m_imp);
950 }
951
collect_param_descrs(param_descrs & r)952 void goal2sat::collect_param_descrs(param_descrs & r) {
953 insert_max_memory(r);
954 r.insert("ite_extra", CPK_BOOL, "(default: true) add redundant clauses (that improve unit propagation) when encoding if-then-else formulas");
955 }
956
957
operator ()(goal const & g,params_ref const & p,sat::solver_core & t,atom2bool_var & m,dep2asm_map & dep2asm,bool default_external)958 void goal2sat::operator()(goal const & g, params_ref const & p, sat::solver_core & t, atom2bool_var & m, dep2asm_map& dep2asm, bool default_external) {
959 if (!m_imp)
960 m_imp = alloc(imp, g.m(), p, t, m, dep2asm, default_external);
961
962 (*m_imp)(g);
963
964 if (!t.get_extension() && m_imp->interpreted_funs().empty()) {
965 dealloc(m_imp);
966 m_imp = nullptr;
967 }
968
969 }
970
get_interpreted_funs(func_decl_ref_vector & funs)971 void goal2sat::get_interpreted_funs(func_decl_ref_vector& funs) {
972 if (m_imp) {
973 funs.append(m_imp->interpreted_funs());
974 }
975 }
976
has_interpreted_funs() const977 bool goal2sat::has_interpreted_funs() const {
978 return m_imp && !m_imp->interpreted_funs().empty();
979 }
980
update_model(model_ref & mdl)981 void goal2sat::update_model(model_ref& mdl) {
982 if (m_imp)
983 m_imp->update_model(mdl);
984 }
985
user_push()986 void goal2sat::user_push() {
987 if (m_imp)
988 m_imp->user_push();
989 }
990
user_pop(unsigned n)991 void goal2sat::user_pop(unsigned n) {
992 if (m_imp)
993 m_imp->user_pop(n);
994 }
995
996
si(ast_manager & m,params_ref const & p,sat::solver_core & t,atom2bool_var & a2b,dep2asm_map & dep2asm,bool default_external)997 sat::sat_internalizer& goal2sat::si(ast_manager& m, params_ref const& p, sat::solver_core& t, atom2bool_var& a2b, dep2asm_map& dep2asm, bool default_external) {
998 if (!m_imp)
999 m_imp = alloc(imp, m, p, t, a2b, dep2asm, default_external);
1000 return *m_imp;
1001 }
1002
1003
1004
mc(ast_manager & m)1005 sat2goal::mc::mc(ast_manager& m): m(m), m_var2expr(m) {}
1006
flush_smc(sat::solver_core & s,atom2bool_var const & map)1007 void sat2goal::mc::flush_smc(sat::solver_core& s, atom2bool_var const& map) {
1008 s.flush(m_smc);
1009 m_var2expr.resize(s.num_vars());
1010 map.mk_var_inv(m_var2expr);
1011 flush_gmc();
1012 }
1013
flush_gmc()1014 void sat2goal::mc::flush_gmc() {
1015 sat::literal_vector updates;
1016 m_smc.expand(updates);
1017 if (!m_gmc) m_gmc = alloc(generic_model_converter, m, "sat2goal");
1018 // now gmc owns the model converter
1019 sat::literal_vector clause;
1020 expr_ref_vector tail(m);
1021 expr_ref def(m);
1022 auto is_literal = [&](expr* e) { expr* r; return is_uninterp_const(e) || (m.is_not(e, r) && is_uninterp_const(r)); };
1023 for (unsigned i = 0; i < updates.size(); ++i) {
1024 sat::literal l = updates[i];
1025 if (l == sat::null_literal) {
1026 sat::literal lit0 = clause[0];
1027 for (unsigned i = 1; i < clause.size(); ++i) {
1028 tail.push_back(lit2expr(~clause[i]));
1029 }
1030 def = m.mk_or(lit2expr(lit0), mk_and(tail));
1031 if (lit0.sign()) {
1032 lit0.neg();
1033 def = m.mk_not(def);
1034 }
1035 expr_ref e = lit2expr(lit0);
1036 if (is_literal(e))
1037 m_gmc->add(e, def);
1038 clause.reset();
1039 tail.reset();
1040 }
1041 // short circuit for equivalences:
1042 else if (clause.empty() && tail.empty() &&
1043 i + 5 < updates.size() &&
1044 updates[i] == ~updates[i + 3] &&
1045 updates[i + 1] == ~updates[i + 4] &&
1046 updates[i + 2] == sat::null_literal &&
1047 updates[i + 5] == sat::null_literal) {
1048 sat::literal r = ~updates[i+1];
1049 if (l.sign()) {
1050 l.neg();
1051 r.neg();
1052 }
1053
1054 expr* a = lit2expr(l);
1055 if (is_literal(a))
1056 m_gmc->add(a, lit2expr(r));
1057 i += 5;
1058 }
1059 else {
1060 clause.push_back(l);
1061 }
1062 }
1063 }
1064
translate(ast_translation & translator)1065 model_converter* sat2goal::mc::translate(ast_translation& translator) {
1066 mc* result = alloc(mc, translator.to());
1067 result->m_smc.copy(m_smc);
1068 result->m_gmc = m_gmc ? dynamic_cast<generic_model_converter*>(m_gmc->translate(translator)) : nullptr;
1069 for (expr* e : m_var2expr) {
1070 result->m_var2expr.push_back(translator(e));
1071 }
1072 return result;
1073 }
1074
set_env(ast_pp_util * visitor)1075 void sat2goal::mc::set_env(ast_pp_util* visitor) {
1076 flush_gmc();
1077 if (m_gmc) m_gmc->set_env(visitor);
1078 }
1079
display(std::ostream & out)1080 void sat2goal::mc::display(std::ostream& out) {
1081 flush_gmc();
1082 if (m_gmc) m_gmc->display(out);
1083 }
1084
get_units(obj_map<expr,bool> & units)1085 void sat2goal::mc::get_units(obj_map<expr, bool>& units) {
1086 flush_gmc();
1087 if (m_gmc) m_gmc->get_units(units);
1088 }
1089
1090
operator ()(sat::model & md)1091 void sat2goal::mc::operator()(sat::model& md) {
1092 m_smc(md);
1093 }
1094
operator ()(model_ref & md)1095 void sat2goal::mc::operator()(model_ref & md) {
1096 // apply externalized model converter
1097 CTRACE("sat_mc", m_gmc, m_gmc->display(tout << "before sat_mc\n"); model_v2_pp(tout, *md););
1098 if (m_gmc) (*m_gmc)(md);
1099 CTRACE("sat_mc", m_gmc, m_gmc->display(tout << "after sat_mc\n"); model_v2_pp(tout, *md););
1100 }
1101
1102
operator ()(expr_ref & fml)1103 void sat2goal::mc::operator()(expr_ref& fml) {
1104 flush_gmc();
1105 if (m_gmc) (*m_gmc)(fml);
1106 }
1107
insert(sat::bool_var v,expr * atom,bool aux)1108 void sat2goal::mc::insert(sat::bool_var v, expr * atom, bool aux) {
1109 SASSERT(!m_var2expr.get(v, nullptr));
1110 m_var2expr.reserve(v + 1);
1111 m_var2expr.set(v, atom);
1112 if (aux) {
1113 SASSERT(m.is_bool(atom));
1114 if (!m_gmc) m_gmc = alloc(generic_model_converter, m, "sat2goal");
1115 if (is_uninterp_const(atom))
1116 m_gmc->hide(to_app(atom)->get_decl());
1117 }
1118 TRACE("sat_mc", tout << "insert " << v << "\n";);
1119 }
1120
lit2expr(sat::literal l)1121 expr_ref sat2goal::mc::lit2expr(sat::literal l) {
1122 sat::bool_var v = l.var();
1123 if (!m_var2expr.get(v)) {
1124 app* aux = m.mk_fresh_const(nullptr, m.mk_bool_sort());
1125 m_var2expr.set(v, aux);
1126 if (!m_gmc) m_gmc = alloc(generic_model_converter, m, "sat2goal");
1127 m_gmc->hide(aux->get_decl());
1128 }
1129 VERIFY(m_var2expr.get(v));
1130 expr_ref result(m_var2expr.get(v), m);
1131 if (l.sign()) {
1132 result = m.mk_not(result);
1133 }
1134 return result;
1135 }
1136
1137
1138 struct sat2goal::imp {
1139
1140 typedef mc sat_model_converter;
1141
1142 ast_manager & m;
1143 expr_ref_vector m_lit2expr;
1144 unsigned long long m_max_memory;
1145 bool m_learned;
1146
impsat2goal::imp1147 imp(ast_manager & _m, params_ref const & p):m(_m), m_lit2expr(m) {
1148 updt_params(p);
1149 }
1150
updt_paramssat2goal::imp1151 void updt_params(params_ref const & p) {
1152 m_learned = p.get_bool("learned", false);
1153 m_max_memory = megabytes_to_bytes(p.get_uint("max_memory", UINT_MAX));
1154 }
1155
checkpointsat2goal::imp1156 void checkpoint() {
1157 if (!m.inc())
1158 throw tactic_exception(m.limit().get_cancel_msg());
1159 if (memory::get_allocation_size() > m_max_memory)
1160 throw tactic_exception(TACTIC_MAX_MEMORY_MSG);
1161 }
1162
lit2exprsat2goal::imp1163 expr * lit2expr(ref<mc>& mc, sat::literal l) {
1164 if (!m_lit2expr.get(l.index())) {
1165 SASSERT(m_lit2expr.get((~l).index()) == 0);
1166 expr* aux = mc ? mc->var2expr(l.var()) : nullptr;
1167 if (!aux) {
1168 aux = m.mk_fresh_const(nullptr, m.mk_bool_sort());
1169 if (mc) {
1170 mc->insert(l.var(), aux, true);
1171 }
1172 }
1173 sat::literal lit(l.var(), false);
1174 m_lit2expr.set(lit.index(), aux);
1175 m_lit2expr.set((~lit).index(), m.mk_not(aux));
1176 }
1177 return m_lit2expr.get(l.index());
1178 }
1179
assert_clausessat2goal::imp1180 void assert_clauses(ref<mc>& mc, sat::solver_core const & s, sat::clause_vector const& clauses, goal & r, bool asserted) {
1181 ptr_buffer<expr> lits;
1182 unsigned small_lbd = 3; // s.get_config().m_gc_small_lbd;
1183 for (sat::clause* cp : clauses) {
1184 checkpoint();
1185 lits.reset();
1186 sat::clause const & c = *cp;
1187 if (asserted || m_learned || c.glue() <= small_lbd) {
1188 for (sat::literal l : c) {
1189 lits.push_back(lit2expr(mc, l));
1190 }
1191 r.assert_expr(m.mk_or(lits));
1192 }
1193 }
1194 }
1195
operator ()sat2goal::imp1196 void operator()(sat::solver_core & s, atom2bool_var const & map, goal & r, ref<mc> & mc) {
1197 if (s.at_base_lvl() && s.inconsistent()) {
1198 r.assert_expr(m.mk_false());
1199 return;
1200 }
1201 if (r.models_enabled() && !mc) {
1202 mc = alloc(sat_model_converter, m);
1203 }
1204 if (mc) mc->flush_smc(s, map);
1205 m_lit2expr.resize(s.num_vars() * 2);
1206 map.mk_inv(m_lit2expr);
1207 // collect units
1208 unsigned trail_sz = s.init_trail_size();
1209 for (unsigned i = 0; i < trail_sz; ++i) {
1210 checkpoint();
1211 r.assert_expr(lit2expr(mc, s.trail_literal(i)));
1212 }
1213 // collect binary clauses
1214 svector<sat::solver::bin_clause> bin_clauses;
1215 s.collect_bin_clauses(bin_clauses, m_learned, false);
1216 for (sat::solver::bin_clause const& bc : bin_clauses) {
1217 checkpoint();
1218 r.assert_expr(m.mk_or(lit2expr(mc, bc.first), lit2expr(mc, bc.second)));
1219 }
1220 // collect clauses
1221 assert_clauses(mc, s, s.clauses(), r, true);
1222
1223 auto* ext = s.get_extension();
1224 if (ext) {
1225 std::function<expr_ref(sat::literal)> l2e = [&](sat::literal lit) {
1226 return expr_ref(lit2expr(mc, lit), m);
1227 };
1228 expr_ref_vector fmls(m);
1229 sat::ba_solver* ba = dynamic_cast<sat::ba_solver*>(ext);
1230 if (ba) {
1231 ba->to_formulas(l2e, fmls);
1232 }
1233 else
1234 dynamic_cast<euf::solver*>(ext)->to_formulas(l2e, fmls);
1235 for (expr* f : fmls)
1236 r.assert_expr(f);
1237 }
1238 }
1239
add_clausesat2goal::imp1240 void add_clause(ref<mc>& mc, sat::literal_vector const& lits, expr_ref_vector& lemmas) {
1241 expr_ref_vector lemma(m);
1242 for (sat::literal l : lits) {
1243 expr* e = lit2expr(mc, l);
1244 if (!e) return;
1245 lemma.push_back(e);
1246 }
1247 lemmas.push_back(mk_or(lemma));
1248 }
1249
add_clausesat2goal::imp1250 void add_clause(ref<mc>& mc, sat::clause const& c, expr_ref_vector& lemmas) {
1251 expr_ref_vector lemma(m);
1252 for (sat::literal l : c) {
1253 expr* e = lit2expr(mc, l);
1254 if (!e) return;
1255 lemma.push_back(e);
1256 }
1257 lemmas.push_back(mk_or(lemma));
1258 }
1259
1260 };
1261
sat2goal()1262 sat2goal::sat2goal():m_imp(nullptr) {
1263 }
1264
collect_param_descrs(param_descrs & r)1265 void sat2goal::collect_param_descrs(param_descrs & r) {
1266 insert_max_memory(r);
1267 r.insert("learned", CPK_BOOL, "(default: false) collect also learned clauses.");
1268 }
1269
1270 struct sat2goal::scoped_set_imp {
1271 sat2goal * m_owner;
scoped_set_impsat2goal::scoped_set_imp1272 scoped_set_imp(sat2goal * o, sat2goal::imp * i):m_owner(o) {
1273 m_owner->m_imp = i;
1274 }
~scoped_set_impsat2goal::scoped_set_imp1275 ~scoped_set_imp() {
1276 m_owner->m_imp = nullptr;
1277 }
1278 };
1279
operator ()(sat::solver_core & t,atom2bool_var const & m,params_ref const & p,goal & g,ref<mc> & mc)1280 void sat2goal::operator()(sat::solver_core & t, atom2bool_var const & m, params_ref const & p,
1281 goal & g, ref<mc> & mc) {
1282 imp proc(g.m(), p);
1283 scoped_set_imp set(this, &proc);
1284 proc(t, m, g, mc);
1285 }
1286
1287
1288