From 93ee05648e1c7e4e61433510b34a7f8e9fffb48e Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 11 Feb 2019 10:56:36 -0800 Subject: [PATCH] add shortcuts for unit assertions, conflicts Signed-off-by: Nikolaj Bjorner --- src/sat/ba_solver.cpp | 4 ++ src/sat/ba_solver.h | 1 + src/sat/sat_asymm_branch.cpp | 6 +-- src/sat/sat_big.cpp | 2 +- src/sat/sat_cleaner.cpp | 4 +- src/sat/sat_elim_eqs.cpp | 6 +-- src/sat/sat_elim_vars.cpp | 2 +- src/sat/sat_extension.h | 1 + src/sat/sat_lookahead.cpp | 2 +- src/sat/sat_probing.cpp | 12 +++--- src/sat/sat_scc.cpp | 8 +++- src/sat/sat_simplifier.cpp | 76 ++++-------------------------------- src/sat/sat_solver.cpp | 5 +-- src/sat/sat_solver.h | 3 ++ src/sat/sat_watched.cpp | 10 ++++- src/sat/sat_watched.h | 5 ++- src/smt/theory_bv.cpp | 2 +- 17 files changed, 55 insertions(+), 94 deletions(-) diff --git a/src/sat/ba_solver.cpp b/src/sat/ba_solver.cpp index 7315f913b..d97e3ee94 100644 --- a/src/sat/ba_solver.cpp +++ b/src/sat/ba_solver.cpp @@ -4140,6 +4140,10 @@ namespace sat { return out << index2constraint(idx); } + std::ostream& ba_solver::display_constraint(std::ostream& out, ext_constraint_idx idx) const { + return out << index2constraint(idx); + } + void ba_solver::display(std::ostream& out, constraint const& c, bool values) const { switch (c.tag()) { case card_t: display(out, c.to_card(), values); break; diff --git a/src/sat/ba_solver.h b/src/sat/ba_solver.h index 141ca0887..dbbc48993 100644 --- a/src/sat/ba_solver.h +++ b/src/sat/ba_solver.h @@ -547,6 +547,7 @@ namespace sat { void flush_roots() override; std::ostream& display(std::ostream& out) const override; std::ostream& display_justification(std::ostream& out, ext_justification_idx idx) const override; + std::ostream& display_constraint(std::ostream& out, ext_constraint_idx idx) const override; void collect_statistics(statistics& st) const override; extension* copy(solver* s) override; extension* copy(lookahead* s, bool learned) override; diff --git a/src/sat/sat_asymm_branch.cpp b/src/sat/sat_asymm_branch.cpp index d3f7b78a0..f89b20897 100644 --- a/src/sat/sat_asymm_branch.cpp +++ b/src/sat/sat_asymm_branch.cpp @@ -367,7 +367,7 @@ namespace sat { bool asymm_branch::propagate_literal(clause const& c, literal l) { SASSERT(!s.inconsistent()); TRACE("asymm_branch_detail", tout << "assigning: " << l << "\n";); - s.assign(l, justification()); + s.assign_scoped(l); s.propagate_core(false); // must not use propagate(), since check_missed_propagation may fail for c return s.inconsistent(); } @@ -423,11 +423,11 @@ namespace sat { switch (new_sz) { case 0: - s.set_conflict(justification()); + s.set_conflict(); return false; case 1: TRACE("asymm_branch", tout << "produced unit clause: " << c[0] << "\n";); - s.assign(c[0], justification()); + s.assign_unit(c[0]); s.propagate_core(false); scoped_d.del_clause(); return false; // check_missed_propagation() may fail, since m_clauses is not in a consistent state. diff --git a/src/sat/sat_big.cpp b/src/sat/sat_big.cpp index 833c83820..f327bc607 100644 --- a/src/sat/sat_big.cpp +++ b/src/sat/sat_big.cpp @@ -199,7 +199,7 @@ namespace sat { s.add_ate(~u, v); if (find_binary_watch(wlist, ~v)) { IF_VERBOSE(10, verbose_stream() << "binary: " << ~u << "\n"); - s.assign(~u, justification()); + s.assign_unit(~u); } // could turn non-learned non-binary tautology into learned binary. s.get_wlist(~v).erase(watched(~u, w.is_learned())); diff --git a/src/sat/sat_cleaner.cpp b/src/sat/sat_cleaner.cpp index d8181a8e0..093e6221f 100644 --- a/src/sat/sat_cleaner.cpp +++ b/src/sat/sat_cleaner.cpp @@ -119,11 +119,11 @@ namespace sat { s.display_watches(tout);); switch (new_sz) { case 0: - s.set_conflict(justification()); + s.set_conflict(); s.del_clause(c); break; case 1: - s.assign(c[0], justification()); + s.assign_unit(c[0]); s.del_clause(c); break; case 2: diff --git a/src/sat/sat_elim_eqs.cpp b/src/sat/sat_elim_eqs.cpp index 612c337c8..bc69c1f5d 100644 --- a/src/sat/sat_elim_eqs.cpp +++ b/src/sat/sat_elim_eqs.cpp @@ -53,7 +53,7 @@ namespace sat { literal l2 = it->get_literal(); literal r2 = norm(roots, l2); if (r1 == r2) { - m_solver.assign(r1, justification()); + m_solver.assign_unit(r1); if (m_solver.inconsistent()) return; // consume unit @@ -179,7 +179,7 @@ namespace sat { switch (j) { case 0: - m_solver.set_conflict(justification()); + m_solver.set_conflict(); for (; it != end; ++it) { *it2 = *it; it2++; @@ -187,7 +187,7 @@ namespace sat { cs.set_end(it2); return; case 1: - m_solver.assign(c[0], justification()); + m_solver.assign_unit(c[0]); drat_delete_clause(); c.set_removed(true); m_solver.del_clause(c); diff --git a/src/sat/sat_elim_vars.cpp b/src/sat/sat_elim_vars.cpp index 4b475a181..1759ec2ad 100644 --- a/src/sat/sat_elim_vars.cpp +++ b/src/sat/sat_elim_vars.cpp @@ -169,7 +169,7 @@ namespace sat{ switch (c.size()) { case 0: - s.set_conflict(justification()); + s.set_conflict(); break; case 1: simp.propagate_unit(c[0]); diff --git a/src/sat/sat_extension.h b/src/sat/sat_extension.h index 41aebb97e..446569e84 100644 --- a/src/sat/sat_extension.h +++ b/src/sat/sat_extension.h @@ -70,6 +70,7 @@ namespace sat { virtual lbool get_phase(bool_var v) = 0; virtual std::ostream& display(std::ostream& out) const = 0; virtual std::ostream& display_justification(std::ostream& out, ext_justification_idx idx) const = 0; + virtual std::ostream& display_constraint(std::ostream& out, ext_constraint_idx idx) const = 0; virtual void collect_statistics(statistics& st) const = 0; virtual extension* copy(solver* s) = 0; virtual extension* copy(lookahead* s, bool learned) = 0; diff --git a/src/sat/sat_lookahead.cpp b/src/sat/sat_lookahead.cpp index 5c33f8d3d..3536b21db 100644 --- a/src/sat/sat_lookahead.cpp +++ b/src/sat/sat_lookahead.cpp @@ -2463,7 +2463,7 @@ namespace sat { for (unsigned i = 0; i < m_watches.size(); ++i) { watch_list const& wl = m_watches[i]; if (!wl.empty()) { - sat::display_watch_list(out << to_literal(i) << " -> ", dummy_allocator, wl); + sat::display_watch_list(out << to_literal(i) << " -> ", dummy_allocator, wl, nullptr); out << "\n"; } } diff --git a/src/sat/sat_probing.cpp b/src/sat/sat_probing.cpp index 54c1ee23d..5689112d4 100644 --- a/src/sat/sat_probing.cpp +++ b/src/sat/sat_probing.cpp @@ -69,7 +69,7 @@ namespace sat { s.m_drat.add(l, lit, true); s.m_drat.add(~l, lit, true); } - s.assign(lit, justification()); + s.assign_scoped(lit); m_num_assigned++; } } @@ -77,14 +77,14 @@ namespace sat { else { m_to_assert.reset(); s.push(); - s.assign(l, justification()); + s.assign_scoped(l); m_counter--; unsigned old_tr_sz = s.m_trail.size(); s.propagate(false); if (s.inconsistent()) { // ~l must be true s.pop(1); - s.assign(~l, justification()); + s.assign_scoped(~l); s.propagate(false); return false; } @@ -104,7 +104,7 @@ namespace sat { s.m_drat.add(l, lit, true); s.m_drat.add(~l, lit, true); } - s.assign(lit, justification()); + s.assign_scoped(lit); m_num_assigned++; } } @@ -119,13 +119,13 @@ namespace sat { m_counter--; s.push(); literal l(v, false); - s.assign(l, justification()); + s.assign_scoped(l); unsigned old_tr_sz = s.m_trail.size(); s.propagate(false); if (s.inconsistent()) { // ~l must be true s.pop(1); - s.assign(~l, justification()); + s.assign_scoped(~l); s.propagate(false); m_num_assigned++; return; diff --git a/src/sat/sat_scc.cpp b/src/sat/sat_scc.cpp index 79c599609..7ce073975 100644 --- a/src/sat/sat_scc.cpp +++ b/src/sat/sat_scc.cpp @@ -47,18 +47,22 @@ namespace sat { stopwatch m_watch; unsigned m_num_elim; unsigned m_num_elim_bin; + unsigned m_trail_size; report(scc & c): m_scc(c), m_num_elim(c.m_num_elim), - m_num_elim_bin(c.m_num_elim_bin) { + m_num_elim_bin(c.m_num_elim_bin), + m_trail_size(c.m_solver.init_trail_size()) { m_watch.start(); } ~report() { m_watch.stop(); unsigned elim_bin = m_scc.m_num_elim_bin - m_num_elim_bin; + unsigned num_units = m_scc.m_solver.init_trail_size() - m_trail_size; IF_VERBOSE(2, verbose_stream() << " (sat-scc :elim-vars " << (m_scc.m_num_elim - m_num_elim); if (elim_bin > 0) verbose_stream() << " :elim-bin " << elim_bin; + if (num_units > 0) verbose_stream() << " :units " << num_units; verbose_stream() << m_watch << ")\n";); } }; @@ -177,7 +181,7 @@ namespace sat { l2_idx = s[j]; j--; if (to_literal(l2_idx) == ~l) { - m_solver.set_conflict(justification()); + m_solver.set_conflict(); return 0; } if (m_solver.is_external(to_literal(l2_idx).var())) { diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp index 9688b1d6e..f536dda03 100644 --- a/src/sat/sat_simplifier.cpp +++ b/src/sat/sat_simplifier.cpp @@ -335,14 +335,14 @@ namespace sat { unsigned sz = c.size(); switch(sz) { case 0: - s.set_conflict(justification()); + s.set_conflict(); for (; it != end; ++it, ++it2) { *it2 = *it; } cs.set_end(it2); return; case 1: - s.assign(c[0], justification()); + s.assign_unit(c[0]); c.restore(sz0); s.del_clause(c); break; @@ -473,8 +473,9 @@ namespace sat { clause & c2 = *(*it); if (!c2.was_removed() && *l_it == null_literal) { // c2 was subsumed - if (c1.is_learned() && !c2.is_learned()) + if (c1.is_learned() && !c2.is_learned()) { s.set_learned(c1, false); + } TRACE("subsumption", tout << c1 << " subsumed " << c2 << "\n";); remove_clause(c2); m_num_subsumed++; @@ -646,7 +647,7 @@ namespace sat { inline void simplifier::propagate_unit(literal l) { unsigned old_trail_sz = s.m_trail.size(); - s.assign(l, justification()); + s.assign_scoped(l); s.propagate_core(false); // must not use propagate(), since s.m_clauses is not in a consistent state. if (s.inconsistent()) return; @@ -696,7 +697,7 @@ namespace sat { switch (sz) { case 0: TRACE("elim_lit", tout << "clause is empty\n";); - s.set_conflict(justification()); + s.set_conflict(); break; case 1: TRACE("elim_lit", tout << "clause became unit: " << c[0] << "\n";); @@ -893,7 +894,7 @@ namespace sat { unsigned sz = c.size(); switch (sz) { case 0: - s.set_conflict(justification()); + s.set_conflict(); return; case 1: c.restore(sz0); @@ -1164,7 +1165,6 @@ namespace sat { if (m_intersection.empty() && !first) { m_tautology.shrink(tsz); } - // if (first) IF_VERBOSE(0, verbose_stream() << "taut: " << m_tautology << "\n";); return first; } @@ -1222,8 +1222,6 @@ namespace sat { RI literals. */ void minimize_covered_clause(unsigned idx) { - // IF_VERBOSE(0, verbose_stream() << "minimize: " << m_covered_clause - // << " @ " << idx << "\n" << "tautology: " << m_tautology << "\n";); literal _blocked = m_covered_clause[idx]; for (literal l : m_tautology) VERIFY(s.is_marked(l)); for (literal l : m_covered_clause) s.unmark_visited(l); @@ -1234,14 +1232,6 @@ namespace sat { if (m_covered_antecedent[i] == clause_ante()) s.mark_visited(lit); if (s.is_marked(lit)) idx = i; } - if (false && _blocked.var() == 8074) { - IF_VERBOSE(0, verbose_stream() << "covered: " << m_covered_clause << "\n"; - verbose_stream() << "tautology: " << m_tautology << "\n"; - verbose_stream() << "index: " << idx << "\n"; - for (unsigned i = idx; i > 0; --i) { - m_covered_antecedent[i].display(verbose_stream(), m_covered_clause[i]); - }); - } for (unsigned i = idx; i > 0; --i) { literal lit = m_covered_clause[i]; //s.mark_visited(lit); @@ -1285,10 +1275,6 @@ namespace sat { // unsigned sz0 = m_covered_clause.size(); m_covered_clause.resize(j); VERIFY(j >= m_clause.size()); - if (false && _blocked.var() == 16774) { - IF_VERBOSE(0, verbose_stream() << "covered: " << m_covered_clause << "\n"); - } - // IF_VERBOSE(0, verbose_stream() << "reduced from size " << sz0 << " to " << m_covered_clause << "\n" << m_clause << "\n";); } /* @@ -1385,7 +1371,6 @@ namespace sat { } bool above_threshold(unsigned sz0) const { - // if (sz0 * 400 < m_covered_clause.size()) IF_VERBOSE(0, verbose_stream() << "above threshold " << sz0 << " " << m_covered_clause.size() << "\n";); return sz0 * 400 < m_covered_clause.size(); } @@ -1608,15 +1593,6 @@ namespace sat { } void block_covered_clause(clause& c, literal l, model_converter::kind k) { - if (false) { - IF_VERBOSE(0, verbose_stream() << "blocked: " << l << " @ " << c << " :covered " << m_covered_clause << "\n"; - s.m_use_list.display(verbose_stream() << "use " << l << ":", l); - s.m_use_list.display(verbose_stream() << "use " << ~l << ":", ~l); - s.s.display_watch_list(verbose_stream() << ~l << ": ", s.get_wlist(l)) << "\n"; - s.s.display_watch_list(verbose_stream() << l << ": ", s.get_wlist(~l)) << "\n"; - ); - - } TRACE("blocked_clause", tout << "new blocked clause: " << c << "\n";); SASSERT(!s.is_external(l)); model_converter::entry& new_entry = m_mc.mk(k, l.var()); @@ -1875,36 +1851,7 @@ namespace sat { } void simplifier::add_non_learned_binary_clause(literal l1, literal l2) { -#if 0 - if ((l1.var() == 2039 || l2.var() == 2039) && - (l1.var() == 27042 || l2.var() == 27042)) { - IF_VERBOSE(1, verbose_stream() << "add_bin: " << l1 << " " << l2 << "\n"); - } -#endif -#if 0 - watched* w; - watch_list & wlist1 = get_wlist(~l1); - watch_list & wlist2 = get_wlist(~l2); - w = find_binary_watch(wlist1, l2); - if (w) { - if (w->is_learned()) - w->set_learned(false); - } - else { - wlist1.push_back(watched(l2, false)); - } - - w = find_binary_watch(wlist2, l1); - if (w) { - if (w->is_learned()) - w->set_learned(false); - } - else { - wlist2.push_back(watched(l1, false)); - } -#else s.mk_bin_clause(l1, l2, false); -#endif } /** @@ -2027,13 +1974,6 @@ namespace sat { m_elim_counter -= num_pos * num_neg + before_lits; - if (false) { - literal l(v, false); - IF_VERBOSE(0, - verbose_stream() << "elim: " << l << "\n"; - s.display_watch_list(verbose_stream() << ~l << ": ", get_wlist(l)) << "\n"; - s.display_watch_list(verbose_stream() << l << ": ", get_wlist(~l)) << "\n";); - } // eliminate variable ++s.m_stats.m_elim_var_res; VERIFY(!is_external(v)); @@ -2054,7 +1994,7 @@ namespace sat { } switch (m_new_cls.size()) { case 0: - s.set_conflict(justification()); + s.set_conflict(); break; case 1: propagate_unit(m_new_cls[0]); diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 7f2fcb45d..4354d91ea 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -2356,7 +2356,7 @@ namespace sat { } m_conflict_lvl = get_max_lvl(m_not_l, m_conflict); - TRACE("sat", tout << "conflict detected at level " << m_conflict_lvl << " for "; + TRACE("sat_verbose", tout << "conflict detected at level " << m_conflict_lvl << " for "; if (m_not_l == literal()) tout << "null literal\n"; else tout << m_not_l << "\n";); @@ -2970,7 +2970,6 @@ 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 { @@ -3720,7 +3719,7 @@ namespace sat { } std::ostream& solver::display_watch_list(std::ostream& out, watch_list const& wl) const { - return sat::display_watch_list(out, cls_allocator(), wl); + return sat::display_watch_list(out, cls_allocator(), wl, m_ext.get()); } void solver::display_assignment(std::ostream & out) const { diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h index d9f738e6c..c8261397a 100644 --- a/src/sat/sat_solver.h +++ b/src/sat/sat_solver.h @@ -314,8 +314,11 @@ namespace sat { } } void assign_core(literal l, unsigned lvl, justification jst); + void assign_unit(literal l) { assign(l, justification()); } + void assign_scoped(literal l) { assign(l, justification()); } void set_conflict(justification c, literal not_l); void set_conflict(justification c) { set_conflict(c, null_literal); } + void set_conflict() { set_conflict(justification()); } lbool status(clause const & c) const; clause_offset get_offset(clause const & c) const { return cls_allocator().get_offset(&c); } void checkpoint() { diff --git a/src/sat/sat_watched.cpp b/src/sat/sat_watched.cpp index 199d12797..966bd8325 100644 --- a/src/sat/sat_watched.cpp +++ b/src/sat/sat_watched.cpp @@ -18,6 +18,7 @@ Revision History: --*/ #include "sat/sat_watched.h" #include "sat/sat_clause.h" +#include "sat/sat_extension.h" namespace sat { @@ -96,7 +97,7 @@ namespace sat { } - std::ostream& display_watch_list(std::ostream & out, clause_allocator const & ca, watch_list const & wlist) { + std::ostream& display_watch_list(std::ostream & out, clause_allocator const & ca, watch_list const & wlist, extension* ext) { bool first = true; for (watched const& w : wlist) { if (first) @@ -116,7 +117,12 @@ namespace sat { out << "(" << w.get_blocked_literal() << " " << *(ca.get_clause(w.get_clause_offset())) << ")"; break; case watched::EXT_CONSTRAINT: - out << "ext: " << w.get_ext_constraint_idx(); + if (ext) { + ext->display_constraint(out, w.get_ext_constraint_idx()); + } + else { + out << "ext: " << w.get_ext_constraint_idx(); + } break; default: UNREACHABLE(); diff --git a/src/sat/sat_watched.h b/src/sat/sat_watched.h index 09ad22ffd..a05e7c365 100644 --- a/src/sat/sat_watched.h +++ b/src/sat/sat_watched.h @@ -35,6 +35,9 @@ namespace sat { Remark: there are no clause objects for binary clauses. */ + + class extension; + class watched { public: enum kind { @@ -138,7 +141,7 @@ namespace sat { void set_ternary_learned(watch_list& wlist, literal l1, literal l2, bool learned); class clause_allocator; - std::ostream& display_watch_list(std::ostream & out, clause_allocator const & ca, watch_list const & wlist); + std::ostream& display_watch_list(std::ostream & out, clause_allocator const & ca, watch_list const & wlist, extension* ext); void conflict_cleanup(watch_list::iterator it, watch_list::iterator it2, watch_list& wlist); }; diff --git a/src/smt/theory_bv.cpp b/src/smt/theory_bv.cpp index 9ab625ede..4b9b3d1d0 100644 --- a/src/smt/theory_bv.cpp +++ b/src/smt/theory_bv.cpp @@ -448,7 +448,7 @@ namespace smt { } unsigned act = m_eq_activity[hash_u_u(v1, v2) & 0xFF]++; - if (act < 255) { + if ((act & 0xFF) != 0xFF) { return; } ++m_stats.m_num_eq_dynamic;