From e183f8b7434d4f2db72c7b6eac3778b2f639396c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 9 Feb 2018 21:46:45 -0800 Subject: [PATCH] disable lookahead simplification when external solver is used Signed-off-by: Nikolaj Bjorner --- src/sat/ba_solver.cpp | 2 ++ src/sat/sat_integrity_checker.cpp | 60 +++++++++++++++---------------- src/sat/sat_lookahead.cpp | 2 +- src/sat/sat_simplifier.cpp | 8 +---- src/sat/sat_solver.cpp | 22 ++++-------- 5 files changed, 40 insertions(+), 54 deletions(-) diff --git a/src/sat/ba_solver.cpp b/src/sat/ba_solver.cpp index 117c9c6f8..412b81ccc 100644 --- a/src/sat/ba_solver.cpp +++ b/src/sat/ba_solver.cpp @@ -2248,6 +2248,8 @@ namespace sat { display(verbose_stream(), c, true); if (c.lit() != null_literal) verbose_stream() << value(c.lit()) << "\n";); + IF_VERBOSE(0, s().display_watches(verbose_stream())); + UNREACHABLE(); exit(1); return false; diff --git a/src/sat/sat_integrity_checker.cpp b/src/sat/sat_integrity_checker.cpp index e0e285d56..7f56e2b36 100644 --- a/src/sat/sat_integrity_checker.cpp +++ b/src/sat/sat_integrity_checker.cpp @@ -38,7 +38,7 @@ namespace sat { if (w.is_clause()) { if (w.get_clause_offset() == cls_off) { // the blocked literal must be in the clause. - SASSERT(c.contains(w.get_blocked_literal())); + VERIFY(c.contains(w.get_blocked_literal())); return true; } } @@ -50,12 +50,12 @@ namespace sat { bool integrity_checker::check_clause(clause const & c) const { SASSERT(!c.was_removed()); for (unsigned i = 0; i < c.size(); i++) { - SASSERT(c[i].var() <= s.num_vars()); + VERIFY(c[i].var() <= s.num_vars()); CTRACE("sat_bug", s.was_eliminated(c[i].var()), tout << "l: " << c[i].var() << "\n"; tout << "c: " << c << "\n"; s.display(tout);); - SASSERT(!s.was_eliminated(c[i].var())); + VERIFY(!s.was_eliminated(c[i].var())); } SASSERT(c.check_approx()); @@ -88,7 +88,7 @@ namespace sat { CTRACE("sat_bug", s.value(c[i]) != l_false, tout << c << " status: " << s.status(c) << "\n"; for (unsigned i = 0; i < c.size(); i++) tout << "val(" << i << "): " << s.value(c[i]) << "\n";); - SASSERT(s.value(c[i]) == l_false); + VERIFY(s.value(c[i]) == l_false); } } } @@ -102,7 +102,7 @@ namespace sat { bool integrity_checker::check_clauses(clause * const * begin, clause * const * end) const { for (clause * const * it = begin; it != end; ++it) { - SASSERT(check_clause(*(*it))); + VERIFY(check_clause(*(*it))); } return true; } @@ -128,23 +128,23 @@ namespace sat { } bool integrity_checker::check_bool_vars() const { - SASSERT(s.m_watches.size() == s.num_vars() * 2); - SASSERT(s.m_assignment.size() == s.num_vars() * 2); - SASSERT(s.m_lit_mark.size() == s.num_vars() * 2); - SASSERT(s.m_justification.size() == s.num_vars()); - SASSERT(s.m_decision.size() == s.num_vars()); - SASSERT(s.m_eliminated.size() == s.num_vars()); - SASSERT(s.m_external.size() == s.num_vars()); - SASSERT(s.m_level.size() == s.num_vars()); - SASSERT(s.m_mark.size() == s.num_vars()); - SASSERT(s.m_activity.size() == s.num_vars()); - SASSERT(s.m_phase.size() == s.num_vars()); - SASSERT(s.m_prev_phase.size() == s.num_vars()); - SASSERT(s.m_assigned_since_gc.size() == s.num_vars()); + VERIFY(s.m_watches.size() == s.num_vars() * 2); + VERIFY(s.m_assignment.size() == s.num_vars() * 2); + VERIFY(s.m_lit_mark.size() == s.num_vars() * 2); + VERIFY(s.m_justification.size() == s.num_vars()); + VERIFY(s.m_decision.size() == s.num_vars()); + VERIFY(s.m_eliminated.size() == s.num_vars()); + VERIFY(s.m_external.size() == s.num_vars()); + VERIFY(s.m_level.size() == s.num_vars()); + VERIFY(s.m_mark.size() == s.num_vars()); + VERIFY(s.m_activity.size() == s.num_vars()); + VERIFY(s.m_phase.size() == s.num_vars()); + VERIFY(s.m_prev_phase.size() == s.num_vars()); + VERIFY(s.m_assigned_since_gc.size() == s.num_vars()); for (bool_var v = 0; v < s.num_vars(); v++) { if (s.was_eliminated(v)) { - SASSERT(s.get_wlist(literal(v, false)).empty()); - SASSERT(s.get_wlist(literal(v, true)).empty()); + VERIFY(s.get_wlist(literal(v, false)).empty()); + VERIFY(s.get_wlist(literal(v, true)).empty()); } } return true; @@ -158,7 +158,7 @@ namespace sat { for (watched const& w : wlist) { switch (w.get_kind()) { case watched::BINARY: - SASSERT(!s.was_eliminated(w.get_literal().var())); + VERIFY(!s.was_eliminated(w.get_literal().var())); CTRACE("sat_watched_bug", !s.get_wlist(~(w.get_literal())).contains(watched(l, w.is_learned())), tout << "l: " << l << " l2: " << w.get_literal() << "\n"; tout << "was_eliminated1: " << s.was_eliminated(l.var()); @@ -176,7 +176,7 @@ namespace sat { VERIFY(w.get_literal1().index() < w.get_literal2().index()); break; case watched::CLAUSE: - SASSERT(!s.m_cls_allocator.get_clause(w.get_clause_offset())->was_removed()); + VERIFY(!s.m_cls_allocator.get_clause(w.get_clause_offset())->was_removed()); break; default: break; @@ -194,7 +194,7 @@ namespace sat { tout << "l: " << l << "\n"; s.display_watches(tout); s.display(tout);); - SASSERT(!s.was_eliminated(l.var()) || wlist.empty()); + VERIFY(!s.was_eliminated(l.var()) || wlist.empty()); if (!check_watches(l, wlist)) return false; } @@ -203,7 +203,7 @@ namespace sat { bool integrity_checker::check_reinit_stack() const { for (auto const& c : s.m_clauses_to_reinit) { - SASSERT(c.is_binary() || c.get_clause()->on_reinit_stack()); + VERIFY(c.is_binary() || c.get_clause()->on_reinit_stack()); } return true; } @@ -225,12 +225,12 @@ namespace sat { bool integrity_checker::operator()() const { if (s.inconsistent()) return true; - SASSERT(check_clauses()); - SASSERT(check_learned_clauses()); - SASSERT(check_watches()); - SASSERT(check_bool_vars()); - SASSERT(check_reinit_stack()); - SASSERT(check_disjoint_clauses()); + VERIFY(check_clauses()); + VERIFY(check_learned_clauses()); + VERIFY(check_watches()); + VERIFY(check_bool_vars()); + VERIFY(check_reinit_stack()); + VERIFY(check_disjoint_clauses()); return true; } }; diff --git a/src/sat/sat_lookahead.cpp b/src/sat/sat_lookahead.cpp index cd3b0e19b..460695edd 100644 --- a/src/sat/sat_lookahead.cpp +++ b/src/sat/sat_lookahead.cpp @@ -2317,7 +2317,7 @@ namespace sat { } } } - m_lookahead.reset(); + m_lookahead.reset(); } diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp index f773b05e7..b4f5ffeca 100644 --- a/src/sat/sat_simplifier.cpp +++ b/src/sat/sat_simplifier.cpp @@ -188,9 +188,6 @@ namespace sat { void simplifier::operator()(bool learned) { - integrity_checker si(s); - si.check_watches(); - if (s.inconsistent()) return; if (!m_subsumption && !bce_enabled() && !bca_enabled() && !elim_vars_enabled()) @@ -255,14 +252,12 @@ namespace sat { cleanup_clauses(s.m_learned, true, vars_eliminated, m_learned_in_use_lists); cleanup_clauses(s.m_clauses, false, vars_eliminated, true); } - si.check_watches(); CASSERT("sat_solver", s.check_invariant()); TRACE("after_simplifier", s.display(tout); tout << "model_converter:\n"; s.m_mc.display(tout);); finalize(); - si.check_watches(); } /** @@ -285,7 +280,7 @@ namespace sat { break; } } - wlist.set_end(itprev); + wlist.set_end(itprev); } } @@ -1948,7 +1943,6 @@ namespace sat { return true; } } - return true; } diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 84a875d55..9db241199 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -1505,8 +1505,6 @@ namespace sat { if (m_conflicts_since_init < m_next_simplify) { return; } - integrity_checker si(*this); - si.check_watches(); m_simplifications++; IF_VERBOSE(2, verbose_stream() << "(sat.simplify :simplifications " << m_simplifications << ")\n";); @@ -1518,17 +1516,14 @@ namespace sat { m_cleaner(); CASSERT("sat_simplify_bug", check_invariant()); - si.check_watches(); m_scc(); CASSERT("sat_simplify_bug", check_invariant()); - si.check_watches(); m_simplifier(false); CASSERT("sat_simplify_bug", check_invariant()); CASSERT("sat_missed_prop", check_missed_propagation()); - si.check_watches(); if (!m_learned.empty()) { m_simplifier(true); CASSERT("sat_missed_prop", check_missed_propagation()); @@ -1540,26 +1535,18 @@ namespace sat { m_probing(); CASSERT("sat_missed_prop", check_missed_propagation()); CASSERT("sat_simplify_bug", check_invariant()); - m_asymm_branch(false); CASSERT("sat_missed_prop", check_missed_propagation()); CASSERT("sat_simplify_bug", check_invariant()); - if (m_ext) { m_ext->clauses_modifed(); m_ext->simplify(); } - - if (m_config.m_lookahead_simplify) { + if (m_config.m_lookahead_simplify && !m_ext) { lookahead lh(*this); lh.simplify(true); lh.collect_statistics(m_aux_stats); } - if (false && m_config.m_lookahead_simplify) { - lookahead lh(*this); - lh.simplify(false); - lh.collect_statistics(m_aux_stats); - } TRACE("sat", display(tout << "consistent: " << (!inconsistent()) << "\n");); @@ -1574,6 +1561,7 @@ namespace sat { m_next_simplify = m_conflicts_since_init + m_config.m_simplify_max; } + if (m_par) m_par->set_phase(*this); #if 0 @@ -1756,6 +1744,8 @@ namespace sat { void solver::gc() { if (m_conflicts_since_gc <= m_gc_threshold) return; + if (m_config.m_gc_strategy == GC_DYN_PSM && !at_base_lvl()) + return; IF_VERBOSE(10, verbose_stream() << "(sat.gc)\n";); CASSERT("sat_gc_bug", check_invariant()); switch (m_config.m_gc_strategy) { @@ -3233,8 +3223,8 @@ namespace sat { bool solver::check_invariant() const { if (!m_rlimit.inc()) return true; integrity_checker checker(*this); - SASSERT(checker()); - SASSERT(!m_ext || m_ext->validate()); + VERIFY(checker()); + VERIFY(!m_ext || m_ext->validate()); return true; }