mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
disable lookahead simplification when external solver is used
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
18b66a4bd7
commit
e183f8b743
|
@ -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;
|
||||
|
|
|
@ -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;
|
||||
}
|
||||
};
|
||||
|
|
|
@ -2317,7 +2317,7 @@ namespace sat {
|
|||
}
|
||||
}
|
||||
}
|
||||
m_lookahead.reset();
|
||||
m_lookahead.reset();
|
||||
}
|
||||
|
||||
|
||||
|
|
|
@ -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;
|
||||
}
|
||||
|
||||
|
|
|
@ -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;
|
||||
}
|
||||
|
||||
|
|
Loading…
Reference in a new issue