1 /*++
2 Copyright (c) 2014 Microsoft Corporation
3
4 Module Name:
5
6 inc_sat_solver.cpp
7
8 Abstract:
9
10 incremental solver based on SAT core.
11
12 Author:
13
14 Nikolaj Bjorner (nbjorner) 2014-7-30
15
16 Notes:
17
18 --*/
19
20
21 #include "util/gparams.h"
22 #include "util/stacked_value.h"
23 #include "ast/ast_pp.h"
24 #include "ast/ast_translation.h"
25 #include "ast/ast_util.h"
26 #include "solver/solver.h"
27 #include "solver/tactic2solver.h"
28 #include "solver/parallel_params.hpp"
29 #include "solver/parallel_tactic.h"
30 #include "tactic/tactical.h"
31 #include "tactic/aig/aig_tactic.h"
32 #include "tactic/core/propagate_values_tactic.h"
33 #include "tactic/bv/max_bv_sharing_tactic.h"
34 #include "tactic/arith/card2bv_tactic.h"
35 #include "tactic/bv/bit_blaster_tactic.h"
36 #include "tactic/core/simplify_tactic.h"
37 #include "tactic/bv/bit_blaster_model_converter.h"
38 #include "model/model_smt2_pp.h"
39 #include "model/model_v2_pp.h"
40 #include "model/model_evaluator.h"
41 #include "sat/sat_solver.h"
42 #include "sat/sat_params.hpp"
43 #include "sat/smt/euf_solver.h"
44 #include "sat/tactic/goal2sat.h"
45 #include "sat/tactic/sat2goal.h"
46 #include "sat/tactic/sat_tactic.h"
47 #include "sat/sat_simplifier_params.hpp"
48
49 // incremental SAT solver.
50 class inc_sat_solver : public solver {
51 ast_manager& m;
52 mutable sat::solver m_solver;
53 stacked_value<bool> m_has_uninterpreted;
54 goal2sat m_goal2sat;
55 params_ref m_params;
56 expr_ref_vector m_fmls;
57 expr_ref_vector m_asmsf;
58 unsigned_vector m_fmls_lim;
59 unsigned_vector m_asms_lim;
60 unsigned_vector m_fmls_head_lim;
61 unsigned m_fmls_head;
62 expr_ref_vector m_core;
63 atom2bool_var m_map;
64 scoped_ptr<bit_blaster_rewriter> m_bb_rewriter;
65 tactic_ref m_preprocess;
66 bool m_is_cnf;
67 unsigned m_num_scopes;
68 sat::literal_vector m_asms;
69 goal_ref_buffer m_subgoals;
70 proof_converter_ref m_pc;
71 sref_vector<model_converter> m_mcs;
72 mutable model_converter_ref m_mc0; // TBD: should be saved/retained under push/pop
73 mutable obj_hashtable<func_decl> m_inserted_const2bits;
74 mutable ref<sat2goal::mc> m_sat_mc;
75 mutable model_converter_ref m_cached_mc;
76 svector<double> m_weights;
77 std::string m_unknown;
78 // access formulas after they have been pre-processed and handled by the sat solver.
79 // this allows to access the internal state of the SAT solver and carry on partial results.
80 bool m_internalized_converted; // have internalized formulas been converted back
81 expr_ref_vector m_internalized_fmls; // formulas in internalized format
82
83 typedef obj_map<expr, sat::literal> dep2asm_t;
84
85 dep2asm_t m_dep2asm;
86
is_internalized() const87 bool is_internalized() const { return m_fmls_head == m_fmls.size(); }
88 public:
inc_sat_solver(ast_manager & m,params_ref const & p,bool incremental_mode)89 inc_sat_solver(ast_manager& m, params_ref const& p, bool incremental_mode):
90 m(m),
91 m_solver(p, m.limit()),
92 m_has_uninterpreted(false),
93 m_fmls(m),
94 m_asmsf(m),
95 m_fmls_head(0),
96 m_core(m),
97 m_map(m),
98 m_is_cnf(true),
99 m_num_scopes(0),
100 m_unknown("no reason given"),
101 m_internalized_converted(false),
102 m_internalized_fmls(m) {
103 updt_params(p);
104 m_mcs.push_back(nullptr);
105 init_preprocess();
106 m_solver.set_incremental(incremental_mode && !override_incremental());
107 }
108
override_incremental() const109 bool override_incremental() const {
110 sat_simplifier_params p(m_params);
111 return p.override_incremental();
112 }
113
is_incremental() const114 bool is_incremental() const {
115 return m_solver.get_config().m_incremental;
116 }
117
~inc_sat_solver()118 ~inc_sat_solver() override {}
119
translate(ast_manager & dst_m,params_ref const & p)120 solver* translate(ast_manager& dst_m, params_ref const& p) override {
121 if (m_num_scopes > 0) {
122 throw default_exception("Cannot translate sat solver at non-base level");
123 }
124 ast_translation tr(m, dst_m);
125 m_solver.pop_to_base_level();
126 inc_sat_solver* result = alloc(inc_sat_solver, dst_m, p, is_incremental());
127 auto* ext = get_euf();
128 if (ext) {
129 auto& si = result->m_goal2sat.si(dst_m, m_params, result->m_solver, result->m_map, result->m_dep2asm, is_incremental());
130 euf::solver::scoped_set_translate st(*ext, dst_m, si);
131 result->m_solver.copy(m_solver);
132 }
133 else {
134 result->m_solver.copy(m_solver);
135 }
136 result->m_fmls_head = m_fmls_head;
137 for (expr* f : m_fmls) result->m_fmls.push_back(tr(f));
138 for (expr* f : m_asmsf) result->m_asmsf.push_back(tr(f));
139 for (auto & kv : m_map) result->m_map.insert(tr(kv.m_key), kv.m_value);
140 for (unsigned l : m_fmls_lim) result->m_fmls_lim.push_back(l);
141 for (unsigned a : m_asms_lim) result->m_asms_lim.push_back(a);
142 for (unsigned h : m_fmls_head_lim) result->m_fmls_head_lim.push_back(h);
143 for (expr* f : m_internalized_fmls) result->m_internalized_fmls.push_back(tr(f));
144 if (m_mcs.back()) result->m_mcs.push_back(m_mcs.back()->translate(tr));
145 if (m_sat_mc) result->m_sat_mc = dynamic_cast<sat2goal::mc*>(m_sat_mc->translate(tr));
146 result->m_has_uninterpreted = m_has_uninterpreted;
147 // copy m_bb_rewriter?
148 result->m_internalized_converted = m_internalized_converted;
149 return result;
150 }
151
set_progress_callback(progress_callback * callback)152 void set_progress_callback(progress_callback * callback) override {}
153
display_weighted(std::ostream & out,unsigned sz,expr * const * assumptions,unsigned const * weights)154 void display_weighted(std::ostream& out, unsigned sz, expr * const * assumptions, unsigned const* weights) {
155 if (weights != nullptr) {
156 for (unsigned i = 0; i < sz; ++i) m_weights.push_back(weights[i]);
157 }
158 init_preprocess();
159 m_solver.pop_to_base_level();
160 m_dep2asm.reset();
161 expr_ref_vector asms(m);
162 for (unsigned i = 0; i < sz; ++i) {
163 expr_ref a(m.mk_fresh_const("s", m.mk_bool_sort()), m);
164 expr_ref fml(m.mk_implies(a, assumptions[i]), m);
165 assert_expr(fml);
166 asms.push_back(a);
167 }
168 VERIFY(l_true == internalize_formulas());
169 VERIFY(l_true == internalize_assumptions(sz, asms.data()));
170 svector<unsigned> nweights;
171 for (unsigned i = 0; i < m_asms.size(); ++i) {
172 nweights.push_back((unsigned) m_weights[i]);
173 }
174 m_weights.reset();
175 m_solver.display_wcnf(out, m_asms.size(), m_asms.data(), nweights.data());
176 }
177
is_literal(expr * e) const178 bool is_literal(expr* e) const {
179 return
180 is_uninterp_const(e) ||
181 (m.is_not(e, e) && is_uninterp_const(e));
182 }
183
check_sat_core(unsigned sz,expr * const * assumptions)184 lbool check_sat_core(unsigned sz, expr * const * assumptions) override {
185 m_solver.pop_to_base_level();
186 m_core.reset();
187 if (m_solver.inconsistent()) return l_false;
188 expr_ref_vector _assumptions(m);
189 obj_map<expr, expr*> asm2fml;
190 for (unsigned i = 0; i < sz; ++i) {
191 if (!is_literal(assumptions[i])) {
192 expr_ref a(m.mk_fresh_const("s", m.mk_bool_sort()), m);
193 expr_ref fml(m.mk_eq(a, assumptions[i]), m);
194 assert_expr(fml);
195 _assumptions.push_back(a);
196 asm2fml.insert(a, assumptions[i]);
197 }
198 else {
199 _assumptions.push_back(assumptions[i]);
200 asm2fml.insert(assumptions[i], assumptions[i]);
201 }
202 }
203
204 TRACE("sat", tout << _assumptions << "\n";);
205 m_dep2asm.reset();
206 lbool r = internalize_formulas();
207 if (r != l_true) return r;
208 r = internalize_assumptions(sz, _assumptions.data());
209 if (r != l_true) return r;
210
211 init_reason_unknown();
212 m_internalized_converted = false;
213 bool reason_set = false;
214 try {
215 // IF_VERBOSE(0, m_solver.display(verbose_stream()));
216 r = m_solver.check(m_asms.size(), m_asms.data());
217 }
218 catch (z3_exception& ex) {
219 IF_VERBOSE(1, verbose_stream() << "exception: " << ex.msg() << "\n";);
220 if (m.inc()) {
221 reason_set = true;
222 set_reason_unknown(std::string("(sat.giveup ") + ex.msg() + ')');
223 }
224 r = l_undef;
225 }
226 switch (r) {
227 case l_true:
228 if (m_has_uninterpreted()) {
229 set_reason_unknown("(sat.giveup has-uninterpreted)");
230 r = l_undef;
231 }
232 else if (sz > 0) {
233 check_assumptions();
234 }
235 break;
236 case l_false:
237 // TBD: expr_dependency core is not accounted for.
238 if (!m_asms.empty()) {
239 extract_core(asm2fml);
240 }
241 break;
242 default:
243 if (!reason_set) {
244 set_reason_unknown(m_solver.get_reason_unknown());
245 }
246 break;
247 }
248 return r;
249 }
250
push()251 void push() override {
252 try {
253 internalize_formulas();
254 }
255 catch (...) {
256 push_internal();
257 throw;
258 }
259 push_internal();
260 }
261
push_internal()262 void push_internal() {
263 m_goal2sat.user_push();
264 m_solver.user_push();
265 ++m_num_scopes;
266 m_mcs.push_back(m_mcs.back());
267 m_fmls_lim.push_back(m_fmls.size());
268 m_asms_lim.push_back(m_asmsf.size());
269 m_fmls_head_lim.push_back(m_fmls_head);
270 if (m_bb_rewriter) m_bb_rewriter->push();
271 m_map.push();
272 m_has_uninterpreted.push();
273 }
274
pop(unsigned n)275 void pop(unsigned n) override {
276 if (n > m_num_scopes) { // allow inc_sat_solver to
277 n = m_num_scopes; // take over for another solver.
278 }
279 if (m_bb_rewriter) m_bb_rewriter->pop(n);
280 m_inserted_const2bits.reset();
281 m_map.pop(n);
282 SASSERT(n <= m_num_scopes);
283 m_solver.user_pop(n);
284 m_goal2sat.user_pop(n);
285 m_num_scopes -= n;
286 // ? m_internalized_converted = false;
287 m_has_uninterpreted.pop(n);
288 while (n > 0) {
289 m_mcs.pop_back();
290 m_fmls_head = m_fmls_head_lim.back();
291 m_fmls.resize(m_fmls_lim.back());
292 m_fmls_lim.pop_back();
293 m_fmls_head_lim.pop_back();
294 m_asmsf.resize(m_asms_lim.back());
295 m_asms_lim.pop_back();
296 --n;
297 }
298 }
299
set_phase(expr * e)300 void set_phase(expr* e) override {
301 bool is_not = m.is_not(e, e);
302 sat::bool_var b = m_map.to_bool_var(e);
303 if (b != sat::null_bool_var)
304 m_solver.set_phase(sat::literal(b, is_not));
305 }
306
307 class sat_phase : public phase, public sat::literal_vector {};
308
get_phase()309 phase* get_phase() override {
310 sat_phase* p = alloc(sat_phase);
311 for (unsigned v = m_solver.num_vars(); v-- > 0; ) {
312 p->push_back(sat::literal(v, !m_solver.get_phase(v)));
313 }
314 return p;
315 }
set_phase(phase * p)316 void set_phase(phase* p) override {
317 for (auto lit : *static_cast<sat_phase*>(p))
318 m_solver.set_phase(lit);
319 }
move_to_front(expr * e)320 void move_to_front(expr* e) override {
321 m.is_not(e, e);
322 sat::bool_var b = m_map.to_bool_var(e);
323 if (b != sat::null_bool_var)
324 m_solver.move_to_front(b);
325 }
326
get_scope_level() const327 unsigned get_scope_level() const override {
328 return m_num_scopes;
329 }
330
assert_expr_core2(expr * t,expr * a)331 void assert_expr_core2(expr * t, expr * a) override {
332 if (a) {
333 m_asmsf.push_back(a);
334 if (m_is_cnf && is_literal(t) && is_literal(a)) {
335 assert_expr_core(m.mk_or(::mk_not(m, a), t));
336 }
337 else if (m_is_cnf && m.is_or(t) && is_clause(t) && is_literal(a)) {
338 expr_ref_vector args(m);
339 args.push_back(::mk_not(m, a));
340 args.append(to_app(t)->get_num_args(), to_app(t)->get_args());
341 assert_expr_core(m.mk_or(args.size(), args.data()));
342 }
343 else {
344 m_is_cnf = false;
345 assert_expr_core(m.mk_implies(a, t));
346 }
347 }
348 else {
349 assert_expr_core(t);
350 }
351 }
352
get_manager() const353 ast_manager& get_manager() const override { return m; }
assert_expr_core(expr * t)354 void assert_expr_core(expr * t) override {
355 TRACE("goal2sat", tout << mk_pp(t, m) << "\n";);
356 m_is_cnf &= is_clause(t);
357 m_fmls.push_back(t);
358 }
set_produce_models(bool f)359 void set_produce_models(bool f) override {}
collect_param_descrs(param_descrs & r)360 void collect_param_descrs(param_descrs & r) override {
361 solver::collect_param_descrs(r);
362 goal2sat::collect_param_descrs(r);
363 sat::solver::collect_param_descrs(r);
364 }
updt_params(params_ref const & p)365 void updt_params(params_ref const & p) override {
366 m_params.append(p);
367 sat_params p1(p);
368 m_params.set_bool("keep_cardinality_constraints", p1.cardinality_solver());
369 m_params.set_sym("pb.solver", p1.pb_solver());
370 m_solver.updt_params(m_params);
371 m_solver.set_incremental(is_incremental() && !override_incremental());
372 if (p1.euf() && !get_euf())
373 ensure_euf();
374 }
collect_statistics(statistics & st) const375 void collect_statistics(statistics & st) const override {
376 if (m_preprocess) m_preprocess->collect_statistics(st);
377 m_solver.collect_statistics(st);
378 }
get_unsat_core(expr_ref_vector & r)379 void get_unsat_core(expr_ref_vector & r) override {
380 r.reset();
381 r.append(m_core.size(), m_core.data());
382 }
383
get_levels(ptr_vector<expr> const & vars,unsigned_vector & depth)384 void get_levels(ptr_vector<expr> const& vars, unsigned_vector& depth) override {
385 unsigned sz = vars.size();
386 depth.resize(sz);
387 for (unsigned i = 0; i < sz; ++i) {
388 auto bv = m_map.to_bool_var(vars[i]);
389 depth[i] = bv == sat::null_bool_var ? UINT_MAX : m_solver.lvl(bv);
390 }
391 }
392
get_trail()393 expr_ref_vector get_trail() override {
394 expr_ref_vector result(m);
395 unsigned sz = m_solver.trail_size();
396 expr_ref_vector lit2expr(m);
397 lit2expr.resize(m_solver.num_vars() * 2);
398 m_map.mk_inv(lit2expr);
399 for (unsigned i = 0; i < sz; ++i) {
400 sat::literal lit = m_solver.trail_literal(i);
401 result.push_back(lit2expr[lit.index()].get());
402 }
403 return result;
404 }
405
get_proof()406 proof * get_proof() override {
407 return nullptr;
408 }
409
last_cube(bool is_sat)410 expr_ref_vector last_cube(bool is_sat) {
411 expr_ref_vector result(m);
412 result.push_back(is_sat ? m.mk_true() : m.mk_false());
413 return result;
414 }
415
cube(expr_ref_vector & vs,unsigned backtrack_level)416 expr_ref_vector cube(expr_ref_vector& vs, unsigned backtrack_level) override {
417 if (!is_internalized()) {
418 lbool r = internalize_formulas();
419 if (r != l_true) {
420 IF_VERBOSE(0, verbose_stream() << "internalize produced " << r << "\n");
421 return expr_ref_vector(m);
422 }
423 }
424 convert_internalized();
425 if (m_solver.inconsistent())
426 return last_cube(false);
427 obj_hashtable<expr> _vs;
428 for (expr* v : vs) _vs.insert(v);
429 sat::bool_var_vector vars;
430 for (auto& kv : m_map) {
431 if (_vs.empty() || _vs.contains(kv.m_key))
432 vars.push_back(kv.m_value);
433 }
434 sat::literal_vector lits;
435 lbool result = m_solver.cube(vars, lits, backtrack_level);
436 expr_ref_vector fmls(m);
437 expr_ref_vector lit2expr(m);
438 lit2expr.resize(m_solver.num_vars() * 2);
439 m_map.mk_inv(lit2expr);
440 for (sat::literal l : lits) {
441 expr* e = lit2expr.get(l.index());
442 SASSERT(e);
443 fmls.push_back(e);
444 }
445 vs.reset();
446 for (sat::bool_var v : vars) {
447 expr* x = lit2expr[sat::literal(v, false).index()].get();
448 if (x) {
449 vs.push_back(x);
450 }
451 }
452 switch (result) {
453 case l_true:
454 return last_cube(true);
455 case l_false:
456 return last_cube(false);
457 default:
458 break;
459 }
460 if (lits.empty()) {
461 set_reason_unknown(m_solver.get_reason_unknown());
462 }
463 return fmls;
464 }
465
get_consequences_core(expr_ref_vector const & assumptions,expr_ref_vector const & vars,expr_ref_vector & conseq)466 lbool get_consequences_core(expr_ref_vector const& assumptions, expr_ref_vector const& vars, expr_ref_vector& conseq) override {
467 init_preprocess();
468 TRACE("sat", tout << assumptions << "\n" << vars << "\n";);
469 sat::literal_vector asms;
470 sat::bool_var_vector bvars;
471 vector<sat::literal_vector> lconseq;
472 m_dep2asm.reset();
473 obj_map<expr, expr*> asm2fml;
474 m_solver.pop_to_base_level();
475 lbool r = internalize_formulas();
476 if (r != l_true) return r;
477 r = internalize_vars(vars, bvars);
478 if (r != l_true) return r;
479 r = internalize_assumptions(assumptions.size(), assumptions.data());
480 if (r != l_true) return r;
481 r = m_solver.get_consequences(m_asms, bvars, lconseq);
482 if (r == l_false) {
483 if (!m_asms.empty()) {
484 extract_core(asm2fml);
485 }
486 return r;
487 }
488
489 // build map from bound variables to
490 // the consequences that cover them.
491 u_map<unsigned> bool_var2conseq;
492 for (unsigned i = 0; i < lconseq.size(); ++i) {
493 TRACE("sat", tout << lconseq[i] << "\n";);
494 bool_var2conseq.insert(lconseq[i][0].var(), i);
495 }
496
497 // extract original fixed variables
498 u_map<expr*> asm2dep;
499 extract_asm2dep(asm2dep);
500 for (auto v : vars) {
501 expr_ref cons(m);
502 if (extract_fixed_variable(asm2dep, v, bool_var2conseq, lconseq, cons)) {
503 conseq.push_back(cons);
504 }
505 }
506 return r;
507 }
508
find_mutexes(expr_ref_vector const & vars,vector<expr_ref_vector> & mutexes)509 lbool find_mutexes(expr_ref_vector const& vars, vector<expr_ref_vector>& mutexes) override {
510 sat::literal_vector ls;
511 u_map<expr*> lit2var;
512 for (unsigned i = 0; i < vars.size(); ++i) {
513 expr* e = vars[i];
514 bool neg = m.is_not(e, e);
515 sat::bool_var v = m_map.to_bool_var(e);
516 if (v != sat::null_bool_var) {
517 sat::literal lit(v, neg);
518 ls.push_back(lit);
519 lit2var.insert(lit.index(), vars[i]);
520 }
521 }
522 vector<sat::literal_vector> ls_mutexes;
523 m_solver.find_mutexes(ls, ls_mutexes);
524 for (sat::literal_vector const& ls_mutex : ls_mutexes) {
525 expr_ref_vector mutex(m);
526 for (sat::literal l : ls_mutex) {
527 mutex.push_back(lit2var.find(l.index()));
528 }
529 mutexes.push_back(mutex);
530 }
531 return l_true;
532 }
533
init_reason_unknown()534 void init_reason_unknown() {
535 m_unknown = "no reason given";
536 }
537
reason_unknown() const538 std::string reason_unknown() const override {
539 return m_unknown;
540 }
541
set_reason_unknown(char const * msg)542 void set_reason_unknown(char const* msg) override {
543 m_unknown = msg;
544 }
545
set_reason_unknown(std::string && msg)546 void set_reason_unknown(std::string &&msg) {
547 m_unknown = std::move(msg);
548 }
549
get_labels(svector<symbol> & r)550 void get_labels(svector<symbol> & r) override {
551 }
552
get_num_assertions() const553 unsigned get_num_assertions() const override {
554 const_cast<inc_sat_solver*>(this)->convert_internalized();
555 if (is_internalized() && m_internalized_converted) {
556 return m_internalized_fmls.size();
557 }
558 else {
559 return m_fmls.size();
560 }
561 }
562
get_assertion(unsigned idx) const563 expr * get_assertion(unsigned idx) const override {
564 if (is_internalized() && m_internalized_converted) {
565 return m_internalized_fmls[idx];
566 }
567 return m_fmls[idx];
568 }
569
get_num_assumptions() const570 unsigned get_num_assumptions() const override {
571 return m_asmsf.size();
572 }
573
get_assumption(unsigned idx) const574 expr * get_assumption(unsigned idx) const override {
575 return m_asmsf[idx];
576 }
577
get_model_converter() const578 model_converter_ref get_model_converter() const override {
579 const_cast<inc_sat_solver*>(this)->convert_internalized();
580 if (m_cached_mc)
581 return m_cached_mc;
582 if (is_internalized() && m_internalized_converted) {
583 m_sat_mc->flush_smc(m_solver, m_map);
584 m_cached_mc = m_mcs.back();
585 m_cached_mc = concat(solver::get_model_converter().get(), m_cached_mc.get());
586 m_cached_mc = concat(m_cached_mc.get(), m_sat_mc.get());
587 TRACE("sat", m_cached_mc->display(tout););
588 return m_cached_mc;
589 }
590 else {
591 return solver::get_model_converter();
592 }
593 }
594
convert_internalized()595 void convert_internalized() {
596 m_solver.pop_to_base_level();
597 if (!is_internalized() && m_fmls_head > 0) {
598 internalize_formulas();
599 }
600 if (!is_internalized() || m_internalized_converted) return;
601 sat2goal s2g;
602 m_cached_mc = nullptr;
603 goal g(m, false, true, false);
604 s2g(m_solver, m_map, m_params, g, m_sat_mc);
605 m_internalized_fmls.reset();
606 g.get_formulas(m_internalized_fmls);
607 TRACE("sat", m_solver.display(tout); tout << m_internalized_fmls << "\n";);
608 m_internalized_converted = true;
609 }
610
init_preprocess()611 void init_preprocess() {
612 if (m_preprocess) {
613 m_preprocess->reset();
614 }
615 if (!m_bb_rewriter) {
616 m_bb_rewriter = alloc(bit_blaster_rewriter, m, m_params);
617 }
618 params_ref simp1_p = m_params;
619 simp1_p.set_bool("som", true);
620 simp1_p.set_bool("pull_cheap_ite", true);
621 simp1_p.set_bool("push_ite_bv", false);
622 simp1_p.set_bool("local_ctx", true);
623 simp1_p.set_uint("local_ctx_limit", 10000000);
624 simp1_p.set_bool("flat", true); // required by som
625 simp1_p.set_bool("hoist_mul", false); // required by som
626 simp1_p.set_bool("elim_and", true);
627 simp1_p.set_bool("blast_distinct", true);
628
629 params_ref simp2_p = m_params;
630 simp2_p.set_bool("flat", false);
631
632 sat_params sp(m_params);
633 if (sp.euf())
634 m_preprocess =
635 and_then(mk_simplify_tactic(m),
636 mk_propagate_values_tactic(m));
637 else
638 m_preprocess =
639 and_then(mk_simplify_tactic(m),
640 mk_propagate_values_tactic(m),
641 mk_card2bv_tactic(m, m_params), // updates model converter
642 using_params(mk_simplify_tactic(m), simp1_p),
643 mk_max_bv_sharing_tactic(m),
644 mk_bit_blaster_tactic(m, m_bb_rewriter.get()),
645 using_params(mk_simplify_tactic(m), simp2_p)
646 );
647 while (m_bb_rewriter->get_num_scopes() < m_num_scopes) {
648 m_bb_rewriter->push();
649 }
650 m_preprocess->reset();
651 }
652
get_euf()653 euf::solver* get_euf() {
654 return dynamic_cast<euf::solver*>(m_solver.get_extension());
655 }
656
ensure_euf()657 euf::solver* ensure_euf() {
658 auto* ext = dynamic_cast<euf::solver*>(m_solver.get_extension());
659 return ext;
660 }
661
user_propagate_init(void * ctx,solver::push_eh_t & push_eh,solver::pop_eh_t & pop_eh,solver::fresh_eh_t & fresh_eh)662 void user_propagate_init(
663 void* ctx,
664 solver::push_eh_t& push_eh,
665 solver::pop_eh_t& pop_eh,
666 solver::fresh_eh_t& fresh_eh) override {
667 ensure_euf()->user_propagate_init(ctx, push_eh, pop_eh, fresh_eh);
668 }
669
user_propagate_register_fixed(solver::fixed_eh_t & fixed_eh)670 void user_propagate_register_fixed(solver::fixed_eh_t& fixed_eh) override {
671 ensure_euf()->user_propagate_register_fixed(fixed_eh);
672 }
673
user_propagate_register_final(solver::final_eh_t & final_eh)674 void user_propagate_register_final(solver::final_eh_t& final_eh) override {
675 ensure_euf()->user_propagate_register_final(final_eh);
676 }
677
user_propagate_register_eq(solver::eq_eh_t & eq_eh)678 void user_propagate_register_eq(solver::eq_eh_t& eq_eh) override {
679 ensure_euf()->user_propagate_register_eq(eq_eh);
680 }
681
user_propagate_register_diseq(solver::eq_eh_t & diseq_eh)682 void user_propagate_register_diseq(solver::eq_eh_t& diseq_eh) override {
683 ensure_euf()->user_propagate_register_diseq(diseq_eh);
684 }
685
user_propagate_register(expr * e)686 unsigned user_propagate_register(expr* e) override {
687 return ensure_euf()->user_propagate_register(e);
688 }
689
690 private:
691
internalize_goal(goal_ref & g)692 lbool internalize_goal(goal_ref& g) {
693 m_solver.pop_to_base_level();
694 if (m_solver.inconsistent())
695 return l_false;
696
697 m_pc.reset();
698 m_subgoals.reset();
699 init_preprocess();
700 SASSERT(g->models_enabled());
701 if (g->proofs_enabled()) {
702 throw default_exception("generation of proof objects is not supported in this mode");
703 }
704 SASSERT(!g->proofs_enabled());
705 TRACE("sat", m_solver.display(tout); g->display(tout););
706 try {
707 if (m_is_cnf) {
708 m_subgoals.push_back(g.get());
709 }
710 else {
711 (*m_preprocess)(g, m_subgoals);
712 }
713 }
714 catch (tactic_exception & ex) {
715 IF_VERBOSE(1, verbose_stream() << "exception in tactic " << ex.msg() << "\n";);
716 set_reason_unknown(ex.msg());
717 TRACE("sat", tout << "exception: " << ex.msg() << "\n";);
718 m_preprocess = nullptr;
719 m_bb_rewriter = nullptr;
720 return l_undef;
721 }
722 catch (...) {
723 m_preprocess = nullptr;
724 m_bb_rewriter = nullptr;
725 throw;
726 }
727 if (m_subgoals.size() != 1) {
728 IF_VERBOSE(0, verbose_stream() << "size of subgoals is not 1, it is: " << m_subgoals.size() << "\n");
729 return l_undef;
730 }
731 g = m_subgoals[0];
732 func_decl_ref_vector funs(m);
733 m_pc = g->pc();
734 m_mcs.set(m_mcs.size()-1, concat(m_mcs.back(), g->mc()));
735 TRACE("sat", g->display_with_dependencies(tout););
736
737 // ensure that if goal is already internalized, then import mc from m_solver.
738
739 m_goal2sat(*g, m_params, m_solver, m_map, m_dep2asm, is_incremental());
740 m_goal2sat.get_interpreted_funs(funs);
741 if (!m_sat_mc) m_sat_mc = alloc(sat2goal::mc, m);
742 m_sat_mc->flush_smc(m_solver, m_map);
743 if (!funs.empty()) {
744 m_has_uninterpreted = true;
745 std::stringstream strm;
746 strm << "(sat.giveup interpreted functions sent to SAT solver " << funs <<")";
747 TRACE("sat", tout << strm.str() << "\n";);
748 IF_VERBOSE(1, verbose_stream() << strm.str() << "\n";);
749 set_reason_unknown(strm.str());
750 return l_undef;
751 }
752 return l_true;
753 }
754
internalize_assumptions(unsigned sz,expr * const * asms)755 lbool internalize_assumptions(unsigned sz, expr* const* asms) {
756 if (sz == 0 && get_num_assumptions() == 0) {
757 m_asms.shrink(0);
758 return l_true;
759 }
760 goal_ref g = alloc(goal, m, true, true); // models and cores are enabled.
761 for (unsigned i = 0; i < sz; ++i) {
762 g->assert_expr(asms[i], m.mk_leaf(asms[i]));
763 }
764 for (unsigned i = 0; i < get_num_assumptions(); ++i) {
765 g->assert_expr(get_assumption(i), m.mk_leaf(get_assumption(i)));
766 }
767 lbool res = internalize_goal(g);
768 if (res == l_true) {
769 extract_assumptions(sz, asms);
770 }
771 return res;
772 }
773
internalize_vars(expr_ref_vector const & vars,sat::bool_var_vector & bvars)774 lbool internalize_vars(expr_ref_vector const& vars, sat::bool_var_vector& bvars) {
775 for (expr* v : vars) {
776 internalize_var(v, bvars);
777 }
778 return l_true;
779 }
780
internalize_var(expr * v,sat::bool_var_vector & bvars)781 bool internalize_var(expr* v, sat::bool_var_vector& bvars) {
782 obj_map<func_decl, expr*> const2bits;
783 ptr_vector<func_decl> newbits;
784 m_bb_rewriter->get_translation(const2bits, newbits);
785 expr* bv;
786 bv_util bvutil(m);
787 bool internalized = false;
788 if (is_uninterp_const(v) && m.is_bool(v)) {
789 sat::bool_var b = m_map.to_bool_var(v);
790 if (b != sat::null_bool_var) {
791 bvars.push_back(b);
792 internalized = true;
793 }
794 }
795 else if (is_uninterp_const(v) && const2bits.find(to_app(v)->get_decl(), bv)) {
796 SASSERT(bvutil.is_bv(bv));
797 app* abv = to_app(bv);
798 internalized = true;
799 for (expr* arg : *abv) {
800 SASSERT(is_uninterp_const(arg));
801 sat::bool_var b = m_map.to_bool_var(arg);
802 if (b == sat::null_bool_var) {
803 internalized = false;
804 }
805 else {
806 bvars.push_back(b);
807 }
808 }
809 CTRACE("sat", internalized, tout << "var: " << bvars << "\n";);
810 }
811 else if (is_uninterp_const(v) && bvutil.is_bv(v)) {
812 // variable does not occur in assertions, so is unconstrained.
813 }
814 CTRACE("sat", !internalized, tout << "unhandled variable " << mk_pp(v, m) << "\n";);
815 return internalized;
816 }
817
extract_fixed_variable(u_map<expr * > & asm2dep,expr * v,u_map<unsigned> const & bool_var2conseq,vector<sat::literal_vector> const & lconseq,expr_ref & conseq)818 bool extract_fixed_variable(u_map<expr*>& asm2dep, expr* v, u_map<unsigned> const& bool_var2conseq, vector<sat::literal_vector> const& lconseq, expr_ref& conseq) {
819
820 sat::bool_var_vector bvars;
821 if (!internalize_var(v, bvars)) {
822 return false;
823 }
824 sat::literal_vector value;
825 sat::literal_set premises;
826 for (sat::bool_var bv : bvars) {
827 unsigned index;
828 if (bool_var2conseq.find(bv, index)) {
829 value.push_back(lconseq[index][0]);
830 for (unsigned j = 1; j < lconseq[index].size(); ++j) {
831 premises.insert(lconseq[index][j]);
832 }
833 }
834 else {
835 TRACE("sat", tout << "variable is not bound " << mk_pp(v, m) << "\n";);
836 return false;
837 }
838 }
839 expr_ref val(m);
840 expr_ref_vector conj(m);
841 internalize_value(value, v, val);
842 while (!premises.empty()) {
843 expr* e = nullptr;
844 VERIFY(asm2dep.find(premises.pop().index(), e));
845 conj.push_back(e);
846 }
847 conseq = m.mk_implies(mk_and(conj), val);
848 return true;
849 }
850
851 vector<rational> m_exps;
internalize_value(sat::literal_vector const & value,expr * v,expr_ref & val)852 void internalize_value(sat::literal_vector const& value, expr* v, expr_ref& val) {
853 bv_util bvutil(m);
854 if (is_uninterp_const(v) && m.is_bool(v)) {
855 SASSERT(value.size() == 1);
856 val = value[0].sign() ? m.mk_not(v) : v;
857 }
858 else if (is_uninterp_const(v) && bvutil.is_bv_sort(v->get_sort())) {
859 SASSERT(value.size() == bvutil.get_bv_size(v));
860 if (m_exps.empty()) {
861 m_exps.push_back(rational::one());
862 }
863 while (m_exps.size() < value.size()) {
864 m_exps.push_back(rational(2)*m_exps.back());
865 }
866 rational r(0);
867 for (unsigned i = 0; i < value.size(); ++i) {
868 if (!value[i].sign()) {
869 r += m_exps[i];
870 }
871 }
872 val = m.mk_eq(v, bvutil.mk_numeral(r, value.size()));
873 }
874 else {
875 UNREACHABLE();
876 }
877 }
878
is_literal(expr * n)879 bool is_literal(expr* n) {
880 return is_uninterp_const(n) || (m.is_not(n, n) && is_uninterp_const(n));
881 }
882
is_clause(expr * fml)883 bool is_clause(expr* fml) {
884 if (is_literal(fml)) {
885 return true;
886 }
887 if (!m.is_or(fml)) {
888 return false;
889 }
890 for (expr* n : *to_app(fml)) {
891 if (!is_literal(n)) {
892 return false;
893 }
894 }
895 return true;
896 }
897
internalize_formulas()898 lbool internalize_formulas() {
899 if (m_fmls_head == m_fmls.size()) {
900 return l_true;
901 }
902 goal_ref g = alloc(goal, m, true, false); // models, maybe cores are enabled
903 for (unsigned i = m_fmls_head ; i < m_fmls.size(); ++i) {
904 expr* fml = m_fmls.get(i);
905 g->assert_expr(fml);
906 }
907 lbool res = internalize_goal(g);
908 if (res != l_undef) {
909 m_fmls_head = m_fmls.size();
910 }
911 m_internalized_converted = false;
912 return res;
913 }
914
extract_assumptions(unsigned sz,expr * const * asms)915 void extract_assumptions(unsigned sz, expr* const* asms) {
916 m_asms.reset();
917 unsigned j = 0;
918 sat::literal lit;
919 sat::literal_set seen;
920 for (unsigned i = 0; i < sz; ++i) {
921 if (m_dep2asm.find(asms[i], lit)) {
922 SASSERT(lit.var() <= m_solver.num_vars());
923 if (!seen.contains(lit)) {
924 m_asms.push_back(lit);
925 seen.insert(lit);
926 if (i != j && !m_weights.empty()) {
927 m_weights[j] = m_weights[i];
928 }
929 ++j;
930 }
931 }
932 }
933 for (unsigned i = 0; i < get_num_assumptions(); ++i) {
934 if (m_dep2asm.find(get_assumption(i), lit)) {
935 SASSERT(lit.var() <= m_solver.num_vars());
936 if (!seen.contains(lit)) {
937 m_asms.push_back(lit);
938 seen.insert(lit);
939 }
940 }
941 }
942 CTRACE("sat", m_dep2asm.size() != m_asms.size(),
943 tout << m_dep2asm.size() << " vs " << m_asms.size() << "\n";
944 tout << m_asms << "\n";
945 for (auto const& kv : m_dep2asm) {
946 tout << mk_pp(kv.m_key, m) << " " << kv.m_value << "\n";
947 });
948 SASSERT(m_dep2asm.size() == m_asms.size());
949 }
950
extract_asm2dep(u_map<expr * > & asm2dep)951 void extract_asm2dep(u_map<expr*>& asm2dep) {
952 for (auto const& kv : m_dep2asm) {
953 asm2dep.insert(kv.m_value.index(), kv.m_key);
954 }
955 }
956
extract_core(obj_map<expr,expr * > const & asm2fml)957 void extract_core(obj_map<expr, expr*> const& asm2fml) {
958 u_map<expr*> asm2dep;
959 extract_asm2dep(asm2dep);
960 sat::literal_vector const& core = m_solver.get_core();
961 TRACE("sat",
962 for (auto kv : m_dep2asm) {
963 tout << mk_pp(kv.m_key, m) << " |-> " << sat::literal(kv.m_value) << "\n";
964 }
965 tout << "asm2fml: ";
966 for (auto kv : asm2fml) {
967 tout << mk_pp(kv.m_key, m) << " |-> " << mk_pp(kv.m_value, m) << "\n";
968 }
969 tout << "core: "; for (auto c : core) tout << c << " "; tout << "\n";
970 m_solver.display(tout);
971 );
972
973 m_core.reset();
974 for (sat::literal c : core) {
975 expr* e = nullptr;
976 VERIFY(asm2dep.find(c.index(), e));
977 if (asm2fml.contains(e)) {
978 e = asm2fml.find(e);
979 }
980 m_core.push_back(e);
981 }
982 }
983
check_assumptions()984 void check_assumptions() {
985 sat::model const & ll_m = m_solver.get_model();
986 for (auto const& kv : m_dep2asm) {
987 sat::literal lit = kv.m_value;
988 if (sat::value_at(lit, ll_m) != l_true) {
989 IF_VERBOSE(0, verbose_stream() << mk_pp(kv.m_key, m) << " does not evaluate to true\n";
990 verbose_stream() << m_asms << "\n";
991 m_solver.display_assignment(verbose_stream());
992 m_solver.display(verbose_stream()););
993 throw default_exception("bad state");
994 }
995 }
996 }
997
get_model_core(model_ref & mdl)998 void get_model_core(model_ref & mdl) override {
999 TRACE("sat", tout << "retrieve model " << (m_solver.model_is_current()?"present":"absent") << "\n";);
1000 if (!m_solver.model_is_current()) {
1001 mdl = nullptr;
1002 return;
1003 }
1004 if (m_fmls.size() > m_fmls_head) {
1005 mdl = nullptr;
1006 return;
1007 }
1008 TRACE("sat", m_solver.display_model(tout););
1009 CTRACE("sat", m_sat_mc, m_sat_mc->display(tout););
1010 sat::model ll_m = m_solver.get_model();
1011 mdl = alloc(model, m);
1012 if (m_sat_mc) {
1013 (*m_sat_mc)(ll_m);
1014 }
1015 expr_ref_vector var2expr(m);
1016 m_map.mk_var_inv(var2expr);
1017
1018 for (unsigned v = 0; v < var2expr.size(); ++v) {
1019 expr * n = var2expr.get(v);
1020 if (!n || !is_uninterp_const(n)) {
1021 continue;
1022 }
1023 switch (sat::value_at(v, ll_m)) {
1024 case l_true:
1025 mdl->register_decl(to_app(n)->get_decl(), m.mk_true());
1026 break;
1027 case l_false:
1028 mdl->register_decl(to_app(n)->get_decl(), m.mk_false());
1029 break;
1030 default:
1031 break;
1032 }
1033 }
1034
1035 TRACE("sat", m_solver.display(tout););
1036 if (m_sat_mc) {
1037 (*m_sat_mc)(mdl);
1038 }
1039 m_goal2sat.update_model(mdl);
1040 if (m_mcs.back()) {
1041 TRACE("sat", m_mcs.back()->display(tout););
1042 (*m_mcs.back())(mdl);
1043 }
1044 TRACE("sat", model_smt2_pp(tout, m, *mdl, 0););
1045
1046 if (!gparams::get_ref().get_bool("model_validate", false)) {
1047 return;
1048 }
1049 IF_VERBOSE(1, verbose_stream() << "Verifying solution\n";);
1050 model_evaluator eval(*mdl);
1051 eval.set_model_completion(true);
1052 bool all_true = true;
1053 for (expr * f : m_fmls) {
1054 if (has_quantifiers(f))
1055 continue;
1056 expr_ref tmp(m);
1057 eval(f, tmp);
1058 if (m.limit().is_canceled())
1059 return;
1060 CTRACE("sat", !m.is_true(tmp),
1061 tout << "Evaluation failed: " << mk_pp(f, m) << " to " << tmp << "\n";
1062 model_smt2_pp(tout, m, *(mdl.get()), 0););
1063 if (m.is_false(tmp)) {
1064 IF_VERBOSE(0, verbose_stream() << "failed to verify: " << mk_pp(f, m) << "\n");
1065 IF_VERBOSE(0, verbose_stream() << "evaluated to " << tmp << "\n");
1066 all_true = false;
1067 }
1068 }
1069 if (!all_true) {
1070 IF_VERBOSE(0, verbose_stream() << m_params << "\n");
1071 IF_VERBOSE(0, if (m_mcs.back()) m_mcs.back()->display(verbose_stream() << "mc0\n"));
1072 IF_VERBOSE(0, for (auto const& kv : m_map) verbose_stream() << mk_pp(kv.m_key, m) << " |-> " << kv.m_value << "\n");
1073 exit(0);
1074 }
1075 else {
1076 IF_VERBOSE(1, verbose_stream() << "solution verified\n");
1077 }
1078 }
1079 };
1080
1081
mk_inc_sat_solver(ast_manager & m,params_ref const & p,bool incremental_mode)1082 solver* mk_inc_sat_solver(ast_manager& m, params_ref const& p, bool incremental_mode) {
1083 return alloc(inc_sat_solver, m, p, incremental_mode);
1084 }
1085
1086
inc_sat_display(std::ostream & out,solver & _s,unsigned sz,expr * const * soft,rational const * _weights)1087 void inc_sat_display(std::ostream& out, solver& _s, unsigned sz, expr*const* soft, rational const* _weights) {
1088 inc_sat_solver& s = dynamic_cast<inc_sat_solver&>(_s);
1089 vector<unsigned> weights;
1090 for (unsigned i = 0; _weights && i < sz; ++i) {
1091 if (!_weights[i].is_unsigned()) {
1092 throw default_exception("Cannot display weights that are not integers");
1093 }
1094 weights.push_back(_weights[i].get_unsigned());
1095 }
1096 s.display_weighted(out, sz, soft, weights.data());
1097 }
1098
1099
mk_psat_tactic(ast_manager & m,params_ref const & p)1100 tactic * mk_psat_tactic(ast_manager& m, params_ref const& p) {
1101 parallel_params pp(p);
1102 return pp.enable() ? mk_parallel_tactic(mk_inc_sat_solver(m, p, false), p) : mk_sat_tactic(m);
1103 }
1104