From 39414d8b8d23ac4817f1d1465810c511e23c5cfa Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 31 Jul 2014 22:29:47 -0700 Subject: [PATCH] testing inc_sat Signed-off-by: Nikolaj Bjorner --- src/opt/inc_sat_solver.cpp | 140 +++++++++++++++++++++---------- src/opt/maxres.cpp | 6 +- src/opt/maxsmt.cpp | 2 - src/opt/mus.cpp | 9 +- src/sat/sat_justification.h | 21 +++++ src/sat/sat_solver.cpp | 76 ++++++++++------- src/sat/sat_solver.h | 1 + src/sat/tactic/atom2bool_var.cpp | 16 ++-- src/sat/tactic/goal2sat.cpp | 24 ++++-- 9 files changed, 200 insertions(+), 95 deletions(-) diff --git a/src/opt/inc_sat_solver.cpp b/src/opt/inc_sat_solver.cpp index d6404808e..72cff950a 100644 --- a/src/opt/inc_sat_solver.cpp +++ b/src/opt/inc_sat_solver.cpp @@ -1,3 +1,21 @@ +/*++ +Copyright (c) 2014 Microsoft Corporation + +Module Name: + + inc_sat_solver.cpp + +Abstract: + + incremental solver based on SAT core. + +Author: + + Nikolaj Bjorner (nbjorner) 2014-7-30 + +Notes: + +--*/ #include "solver.h" #include "tactical.h" @@ -28,6 +46,10 @@ class inc_sat_solver : public solver { statistics m_stats; unsigned m_num_scopes; sat::literal_vector m_asms; + goal_ref_buffer m_subgoals; + proof_converter_ref m_pc; + model_converter_ref m_mc2; + expr_dependency_ref m_dep_core; typedef obj_map dep2asm_t; @@ -35,7 +57,8 @@ public: inc_sat_solver(ast_manager& m, params_ref const& p): m(m), m_solver(p,0), m_params(p), m_fmls(m), m_core(m), m_map(m), - m_num_scopes(0) { + m_num_scopes(0), + m_dep_core(m) { m_params.set_bool("elim_vars", false); m_solver.updt_params(m_params); params_ref simp2_p = p; @@ -53,7 +76,8 @@ public: using_params(mk_simplify_tactic(m), simp2_p), mk_max_bv_sharing_tactic(m), mk_bit_blaster_tactic(m), - mk_aig_tactic()); + mk_aig_tactic(), + using_params(mk_simplify_tactic(m), simp2_p)); } @@ -64,44 +88,14 @@ public: } virtual lbool check_sat(unsigned num_assumptions, expr * const * assumptions) { m_solver.pop_to_base_level(); - goal_ref_buffer result; - proof_converter_ref pc; - model_converter_ref mc; - expr_dependency_ref core(m); dep2asm_t dep2asm; - if (!m_fmls.empty() || num_assumptions > 0) { - goal_ref g = alloc(goal, m, true, num_assumptions > 0); // models, maybe cores are enabled - SASSERT(num_assumptions == 0 || g->unsat_core_enabled()); - SASSERT(g->models_enabled()); - SASSERT(!g->proofs_enabled()); - for (unsigned i = 0; i < m_fmls.size(); ++i) { - g->assert_expr(m_fmls[i].get()); - } - for (unsigned i = 0; i < num_assumptions; ++i) { - g->assert_expr(assumptions[i], m.mk_leaf(assumptions[i])); - } - TRACE("opt", g->display_with_dependencies(tout);); - m_fmls.reset(); - try { - (*m_preprocess)(g, result, mc, pc, core); - } - catch (tactic_exception & ex) { - IF_VERBOSE(0, verbose_stream() << "exception in tactic " << ex.msg() << "\n";); - m_preprocess->collect_statistics(m_stats); - return l_undef; - } - m_mc = concat(m_mc.get(), mc.get()); - if (result.size() != 1) { - IF_VERBOSE(0, verbose_stream() << "size of result is not 1, it is: " << result.size() << "\n";); - return l_undef; - } - g = result[0]; - TRACE("opt", g->display_with_dependencies(tout);); - m_goal2sat(*g, m_params, m_solver, m_map, dep2asm, true); - } + lbool r = internalize_formulas(); + if (r != l_true) return r; + r = internalize_assumptions(num_assumptions, assumptions, dep2asm); extract_assumptions(dep2asm, m_asms); - lbool r = m_solver.check(m_asms.size(), m_asms.c_ptr()); + if (r != l_true) return r; + r = m_solver.check(m_asms.size(), m_asms.c_ptr()); switch (r) { case l_true: extract_model(); @@ -128,6 +122,9 @@ public: ++m_num_scopes; } virtual void pop(unsigned n) { + if (n < m_num_scopes) { // allow inc_sat_solver to + n = m_num_scopes; // take over for another solver. + } SASSERT(n >= m_num_scopes); m_solver.user_pop(n); m_num_scopes -= n; @@ -180,6 +177,57 @@ public: private: + lbool internalize_goal(goal_ref& g, dep2asm_t& dep2asm) { + m_mc2.reset(); + m_pc.reset(); + m_dep_core.reset(); + m_subgoals.reset(); + SASSERT(g->models_enabled()); + SASSERT(!g->proofs_enabled()); + TRACE("opt", g->display(tout);); + try { + (*m_preprocess)(g, m_subgoals, m_mc2, m_pc, m_dep_core); + } + catch (tactic_exception & ex) { + IF_VERBOSE(0, verbose_stream() << "exception in tactic " << ex.msg() << "\n";); + m_preprocess->collect_statistics(m_stats); + return l_undef; + } + m_mc = concat(m_mc.get(), m_mc2.get()); + if (m_subgoals.size() != 1) { + IF_VERBOSE(0, verbose_stream() << "size of subgoals is not 1, it is: " << m_subgoals.size() << "\n";); + return l_undef; + } + g = m_subgoals[0]; + TRACE("opt", g->display_with_dependencies(tout);); + m_goal2sat(*g, m_params, m_solver, m_map, dep2asm, true); + return l_true; + } + + lbool internalize_assumptions(unsigned sz, expr* const* asms, dep2asm_t& dep2asm) { + if (sz == 0) { + return l_true; + } + goal_ref g = alloc(goal, m, true, true); // models and cores are enabled. + for (unsigned i = 0; i < sz; ++i) { + g->assert_expr(asms[i], m.mk_leaf(asms[i])); + } + return internalize_goal(g, dep2asm); + } + + lbool internalize_formulas() { + if (m_fmls.empty()) { + return l_true; + } + dep2asm_t dep2asm; + goal_ref g = alloc(goal, m, true, false); // models, maybe cores are enabled + for (unsigned i = 0; i < m_fmls.size(); ++i) { + g->assert_expr(m_fmls[i].get()); + } + m_fmls.reset(); + return internalize_goal(g, dep2asm); + } + void extract_assumptions(dep2asm_t& dep2asm, sat::literal_vector& asms) { asms.reset(); dep2asm_t::iterator it = dep2asm.begin(), end = dep2asm.end(); @@ -196,6 +244,16 @@ private: } sat::literal_vector const& core = m_solver.get_core(); + m_core.reset(); + for (unsigned i = 0; i < core.size(); ++i) { + expr* e; + if (asm2dep.find(core[i].index(), e)) { + if (core[i].sign()) { + e = m.mk_not(e); + } + m_core.push_back(e); + } + } TRACE("opt", dep2asm_t::iterator it = dep2asm.begin(); dep2asm_t::iterator end = dep2asm.end(); @@ -204,16 +262,12 @@ private: } tout << "core: "; for (unsigned i = 0; i < core.size(); ++i) { - tout << core[i] << " "; + tout << core[i] << ": " << mk_pp(m_core[i].get(), m) << " "; } tout << "\n"; ); - for (unsigned i = 0; i < core.size(); ++i) { - expr* e; - if (asm2dep.find(core[i].index(), e)) - m_core.push_back(e); - } + } void extract_model() { diff --git a/src/opt/maxres.cpp b/src/opt/maxres.cpp index 98abb7bfd..58cd241d0 100644 --- a/src/opt/maxres.cpp +++ b/src/opt/maxres.cpp @@ -78,6 +78,7 @@ public: } void new_assumption(expr* e, app* cls, rational const& w) { + TRACE("opt", tout << "insert: " << mk_pp(e, m) << " : " << w << "\n";); info inf(cls, w); m_asm2info.insert(e, inf); m_asms.push_back(e); @@ -186,7 +187,8 @@ public: for (unsigned i = 0; i < core.size(); ++i) { rational w2 = get_weight(core[i]); if (w2 > w) { - new_assumption(core[i], get_clause(core[i]), w2 - w); + rational w3 = w2 - w; + new_assumption(core[i], get_clause(core[i]), w3); } } return w; @@ -194,7 +196,7 @@ public: void display_vec(std::ostream& out, unsigned sz, expr* const* args) { for (unsigned i = 0; i < sz; ++i) { - out << mk_pp(args[i], m) << " "; + out << mk_pp(args[i], m) << " : " << get_weight(args[i]) << " "; } out << "\n"; } diff --git a/src/opt/maxsmt.cpp b/src/opt/maxsmt.cpp index 821113e28..347f4bf3a 100644 --- a/src/opt/maxsmt.cpp +++ b/src/opt/maxsmt.cpp @@ -135,8 +135,6 @@ namespace opt { for (unsigned i = 0; i < sz; ++i) { sat_solver->assert_expr(s().get_assertion(i)); } - unsigned lvl = m_s->get_scope_level(); - while (lvl > 0) { sat_solver->push(); --lvl; } m_s = sat_solver; } diff --git a/src/opt/mus.cpp b/src/opt/mus.cpp index 9ce2dd187..9204371bc 100644 --- a/src/opt/mus.cpp +++ b/src/opt/mus.cpp @@ -98,6 +98,7 @@ struct mus::imp { } lbool get_mus(unsigned_vector& mus) { + // SASSERT: mus does not have duplicates. TRACE("opt", for (unsigned i = 0; i < m_cls2lits.size(); ++i) { display_vec(tout, m_cls2lits[i]); @@ -107,12 +108,16 @@ struct mus::imp { for (unsigned i = 0; i < m_cls2expr.size(); ++i) { core.push_back(i); } + if (core.size() == 1) { + mus.push_back(core.back()); + return l_true; + } mus.reset(); expr_ref_vector assumptions(m); svector model; ptr_vector core_exprs; model.resize(m_vars.size()); - while (!core.empty()) { + while (!core.empty()) { IF_VERBOSE(1, verbose_stream() << "(opt.mus reducing core: " << core.size() << " new core: " << mus.size() << ")\n";); unsigned cls_id = core.back(); TRACE("opt", @@ -160,6 +165,7 @@ struct mus::imp { break; } } +#if 0 DEBUG_CODE( assumptions.reset(); for (unsigned i = 0; i < mus.size(); ++i) { @@ -168,6 +174,7 @@ struct mus::imp { lbool is_sat = m_s->check_sat(assumptions.size(), assumptions.c_ptr()); SASSERT(is_sat == l_false); ); +#endif return l_true; } diff --git a/src/sat/sat_justification.h b/src/sat/sat_justification.h index dd803feeb..b162662e8 100644 --- a/src/sat/sat_justification.h +++ b/src/sat/sat_justification.h @@ -52,6 +52,27 @@ namespace sat { bool is_ext_justification() const { return m_val2 == EXT_JUSTIFICATION; } ext_justification_idx get_ext_justification_idx() const { return m_val1; } }; + + inline std::ostream & operator<<(std::ostream & out, justification const & j) { + switch (j.get_kind()) { + case justification::NONE: + out << "none"; + break; + case justification::BINARY: + out << "binary " << j.get_literal(); + break; + case justification::TERNARY: + out << "ternary " << j.get_literal1() << " " << j.get_literal2(); + break; + case justification::CLAUSE: + out << "clause"; + break; + case justification::EXT_JUSTIFICATION: + out << "external"; + break; + } + return out; + } }; #endif diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 911c49c74..cfd83955d 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -163,8 +163,8 @@ namespace sat { } clause * solver::mk_clause_core(unsigned num_lits, literal * lits, bool learned) { + TRACE("sat", tout << "mk_clause: " << mk_lits_pp(num_lits, lits) << "\n";); if (!learned) { - TRACE("sat_mk_clause", tout << "mk_clause: " << mk_lits_pp(num_lits, lits) << "\n";); bool keep = simplify_clause(num_lits, lits); TRACE("sat_mk_clause", tout << "mk_clause (after simp), keep: " << keep << "\n" << mk_lits_pp(num_lits, lits) << "\n";); if (!keep) { @@ -468,9 +468,7 @@ namespace sat { void solver::set_conflict(justification c, literal not_l) { if (m_inconsistent) return; - TRACE("sat_conflict", tout << "conflict\n";); - // int * p = 0; - // *p = 0; + TRACE("sat", tout << "conflict: " << not_l << "\n";); m_inconsistent = true; m_conflict = c; m_not_l = not_l; @@ -707,9 +705,12 @@ namespace sat { try { if (inconsistent()) return l_false; init_search(); + propagate(false); + if (inconsistent()) return l_false; init_assumptions(num_lits, lits); propagate(false); if (inconsistent()) { + TRACE("sat", tout << "initialized -> inconsistent\n";); if (tracking_assumptions()) resolve_conflict(); return l_false; @@ -721,7 +722,7 @@ namespace sat { if (r != l_undef) return r; pop(scope_lvl()); - reinit_assumptions(); + SASSERT(scope_lvl() == 1); m_conflicts_since_restart = 0; m_restart_threshold = m_config.m_restart_initial; } @@ -820,7 +821,7 @@ namespace sat { SASSERT(phase != l_undef); literal next_lit(next, phase == l_false); assign(next_lit, justification()); - TRACE("sat_decide", tout << "next-case-split: " << next_lit << "\n";); + TRACE("sat_decide", tout << scope_lvl() << ": next-case-split: " << next_lit << "\n";); return true; } @@ -839,8 +840,10 @@ namespace sat { return l_undef; if (scope_lvl() == 0) { cleanup(); // cleaner may propagate frozen clauses - if (inconsistent()) + if (inconsistent()) { + TRACE("sat", tout << "conflict at level 0\n";); return l_false; + } gc(); } } @@ -883,25 +886,24 @@ namespace sat { SASSERT(is_external((_l_).var())); \ m_assumption_set.insert(_l_); \ m_assumptions.push_back(_l_); \ - mk_clause_core(1, &(_l_), false); \ + assign(_l_, justification()); \ - for (unsigned i = 0; i < num_lits; ++i) { + for (unsigned i = 0; !inconsistent() && i < num_lits; ++i) { literal lit = lits[i]; _INSERT_LIT(lit); } - for (unsigned i = 0; i < m_user_scope_literals.size(); ++i) { + for (unsigned i = 0; !inconsistent() && i < m_user_scope_literals.size(); ++i) { literal nlit = ~m_user_scope_literals[i]; _INSERT_LIT(nlit); } - TRACE("sat", display(tout);); } void solver::reinit_assumptions() { - if (tracking_assumptions()) { + if (tracking_assumptions() && scope_lvl() == 0) { push(); - for (unsigned i = 0; i < m_assumptions.size(); ++i) { + for (unsigned i = 0; !inconsistent() && i < m_assumptions.size(); ++i) { literal l = m_assumptions[i]; - mk_clause_core(1, &l, false); + assign(l, justification()); } } } @@ -927,17 +929,15 @@ namespace sat { m_next_simplify = 0; m_stopwatch.reset(); m_stopwatch.start(); + m_core.reset(); + TRACE("sat", display(tout);); } /** \brief Apply all simplifications. */ void solver::simplify_problem() { - - if (tracking_assumptions()) { - // NB. simplification is disabled when tracking assumptions. - return; - } + pop_core(scope_lvl()); SASSERT(scope_lvl() == 0); @@ -972,6 +972,7 @@ namespace sat { m_ext->clauses_modifed(); m_ext->simplify(); } + reinit_assumptions(); } void solver::sort_watch_lits() { @@ -993,7 +994,7 @@ namespace sat { } TRACE("sat_mc_bug", m_mc.display(tout);); m_mc(m_model); - TRACE("sat_model", for (bool_var v = 0; v < num; v++) tout << v << ": " << m_model[v] << "\n";); + TRACE("sat", for (bool_var v = 0; v < num; v++) tout << v << ": " << m_model[v] << "\n";); #ifndef _EXTERNAL_RELEASE IF_VERBOSE(SAT_VB_LVL, verbose_stream() << "\"checking model\"\n";); @@ -1043,7 +1044,7 @@ namespace sat { } if (!m_mc.check_model(m)) ok = false; - CTRACE("sat_model_bug", !ok, tout << m << "\n";); + TRACE("sat", tout << "checl: " << ok << "\n" << m << "\n";); return ok; } @@ -1055,7 +1056,6 @@ namespace sat { << " :time " << std::fixed << std::setprecision(2) << m_stopwatch.get_current_seconds() << ")\n";); IF_VERBOSE(30, display_status(verbose_stream());); pop(scope_lvl()); - reinit_assumptions(); m_conflicts_since_restart = 0; switch (m_config.m_restart) { case RS_GEOMETRIC: @@ -1328,7 +1328,7 @@ namespace sat { break; } } - TRACE("sat_gc", tout << "after cleanup:\n" << mk_lits_pp(j, c.begin()) << "\n";); + TRACE("sat", tout << "after cleanup:\n" << mk_lits_pp(j, c.begin()) << "\n";); unsigned new_sz = j; switch (new_sz) { case 0: @@ -1393,11 +1393,14 @@ namespace sat { m_conflicts_since_gc++; m_conflict_lvl = get_max_lvl(m_not_l, m_conflict); + TRACE("sat", tout << "conflict detected at level " << m_conflict_lvl << " for "; + if (m_not_l == literal()) tout << "null literal\n"; + else tout << m_not_l << "\n";); + if (m_conflict_lvl <= 1 && tracking_assumptions()) { resolve_conflict_for_unsat_core(); return false; } - TRACE("sat_conflict", tout << "conflict detected\n";); if (m_conflict_lvl == 0) { return false; } @@ -1530,7 +1533,7 @@ namespace sat { } void solver::resolve_conflict_for_unsat_core() { - TRACE("sat_conflict", display(tout);); + TRACE("sat", display(tout);); if (m_conflict_lvl == 0) { return; @@ -1541,8 +1544,11 @@ namespace sat { int idx = skip_literals_above_conflict_level(); if (m_not_l != null_literal) { - TRACE("sat_conflict", tout << "not_l: " << m_not_l << "\n";); + TRACE("sat", tout << "not_l: " << m_not_l << "\n";); process_antecedent_for_unsat_core(m_not_l); + if (is_assumption(~m_not_l)) { + m_core.push_back(~m_not_l); + } } @@ -1550,8 +1556,8 @@ namespace sat { justification js = m_conflict; do { - TRACE("sat_conflict_detail", tout << "processing consequent: " << consequent << "\n"; - tout << "js kind: " << js.get_kind() << "\n";); + TRACE("sat", tout << "processing consequent: " << consequent << "\n"; + tout << "js kind: " << js << "\n";); switch (js.get_kind()) { case justification::NONE: break; @@ -1902,6 +1908,7 @@ namespace sat { for (; i < sz; i++) { literal l = m_lemma[i]; if (implied_by_marked(l)) { + TRACE("sat", tout << "drop: " << l << "\n";); m_unmark.push_back(l.var()); } else { @@ -2063,6 +2070,7 @@ namespace sat { // ----------------------- void solver::push() { SASSERT(!inconsistent()); + TRACE("sat", tout << "q:" << m_qhead << " trail: " << m_trail.size() << "\n";); SASSERT(m_qhead == m_trail.size()); m_scopes.push_back(scope()); scope & s = m_scopes.back(); @@ -2075,6 +2083,11 @@ namespace sat { } void solver::pop(unsigned num_scopes) { + pop_core(num_scopes); + reinit_assumptions(); + } + + void solver::pop_core(unsigned num_scopes) { if (num_scopes == 0) return; if (m_ext) @@ -2144,9 +2157,6 @@ namespace sat { // void solver::user_push() { - if (m_level.size() == 0) { - return; - } literal lit; if (m_user_scope_literal_pool.empty()) { bool_var new_v = mk_var(true, false); @@ -2189,7 +2199,7 @@ namespace sat { void solver::user_pop(unsigned num_scopes) { pop_to_base_level(); - while (num_scopes > 0 && !m_user_scope_literals.empty()) { + while (num_scopes > 0) { literal lit = m_user_scope_literals.back(); m_user_scope_literal_pool.push_back(lit); m_user_scope_literals.pop_back(); @@ -2203,6 +2213,8 @@ namespace sat { } void solver::pop_to_base_level() { + m_assumptions.reset(); + m_assumption_set.reset(); pop(scope_lvl()); } diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h index 8c39599bb..8e4c9911b 100644 --- a/src/sat/sat_solver.h +++ b/src/sat/sat_solver.h @@ -352,6 +352,7 @@ namespace sat { // ----------------------- void push(); void pop(unsigned num_scopes); + void pop_core(unsigned num_scopes); void unassign_vars(unsigned old_sz); void reinit_clauses(unsigned old_sz); diff --git a/src/sat/tactic/atom2bool_var.cpp b/src/sat/tactic/atom2bool_var.cpp index 58abc2807..48ad85152 100644 --- a/src/sat/tactic/atom2bool_var.cpp +++ b/src/sat/tactic/atom2bool_var.cpp @@ -90,18 +90,22 @@ struct collect_boolean_interface_proc { template void operator()(T const & g) { unsigned sz = g.size(); - ptr_vector deps; + ptr_vector deps, all_deps; for (unsigned i = 0; i < sz; i++) { - process(g.form(i)); if (g.dep(i)) { deps.reset(); m.linearize(g.dep(i), deps); - for (unsigned j = 0; j < deps.size(); ++j) { - quick_for_each_expr(proc, tvisited, deps[j]); - } - + all_deps.append(deps); } } + + for (unsigned i = 0; i < all_deps.size(); i++) { + quick_for_each_expr(proc, tvisited, all_deps[i]); + } + for (unsigned i = 0; i < sz; i++) { + process(g.form(i)); + } + } void operator()(unsigned sz, expr * const * fs) { diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp index 636e8920f..5d9753a82 100644 --- a/src/sat/tactic/goal2sat.cpp +++ b/src/sat/tactic/goal2sat.cpp @@ -394,7 +394,6 @@ struct goal2sat::imp { expr_ref_vector fmls(m); for (unsigned idx = 0; idx < size; idx++) { f = g.form(idx); - TRACE("sat", tout << "Formula: " << mk_pp(f, m) << "\n";); // Add assumptions. if (g.dep(idx)) { deps.reset(); @@ -403,21 +402,28 @@ struct goal2sat::imp { fmls.push_back(f); for (unsigned i = 0; i < deps.size(); ++i) { expr * d = deps[i]; - expr * d1; + expr * d1 = d; SASSERT(m.is_bool(d)); - if (m.is_not(d, d1)) { - insert_dep(d1, true); - fmls.push_back(d1); + bool sign = m.is_not(d, d1); + + insert_dep(d1, sign); + if (d == f) { + goto skip_dep; + } + if (sign) { + d_new = d1; } else { - insert_dep(d, false); - fmls.push_back(m.mk_not(d)); + d_new = m.mk_not(d); } - } + fmls.push_back(d_new); + } f = m.mk_or(fmls.size(), fmls.c_ptr()); - TRACE("sat", tout << mk_pp(f, m) << "\n";); } + TRACE("sat", tout << mk_pp(f, m) << "\n";); process(f); + skip_dep: + ; } }