From 36cddd0c46f87ea1ca1543366ef078f054295831 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 11 Mar 2020 10:55:56 -0700 Subject: [PATCH] fix #3235 - return early during lookaehad, avoid checking invariant when context is inconsistent Signed-off-by: Nikolaj Bjorner --- src/smt/smt_context.cpp | 29 ++++++++++++++--------------- src/smt/smt_lookahead.cpp | 8 +++++++- src/smt/theory_bv.cpp | 4 +++- 3 files changed, 24 insertions(+), 17 deletions(-) diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index fbcf87d65..512d4bbe5 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -311,9 +311,6 @@ namespace smt { } void context::assign_core(literal l, b_justification j, bool decision) { - CTRACE("assign_core", l.var() == 13, tout << (decision?"decision: ":"propagating: ") << l << " "; - display_literal_smt2(tout, l) << " level: " << m_scope_lvl << "\n"; - display(tout << "relevant: " << is_relevant_core(l) << "\n", j);); m_assigned_literals.push_back(l); m_assignment[l.index()] = l_true; m_assignment[(~l).index()] = l_false; @@ -327,26 +324,25 @@ namespace smt { } d.m_phase_available = true; d.m_phase = !l.sign(); + CTRACE("assign_core", l.var() == 13, tout << (decision?"decision: ":"propagating: ") << l << " "; + /*display_literal(tout, l);*/ + tout << "relevant: " << is_relevant_core(l) << " level: " << m_scope_lvl << " is atom " << d.is_atom() << "\n"; + /*display(tout, j);*/ + ); TRACE("phase_selection", tout << "saving phase, is_pos: " << d.m_phase << " l: " << l << "\n";); - TRACE("relevancy", + CTRACE("relevancy", l.var() == 13, tout << "is_atom: " << d.is_atom() << " is relevant: " << is_relevant_core(l) << " relevancy-lvl: " << relevancy_lvl() << "\n";); - if (d.is_atom() && (relevancy_lvl() == 0 || (relevancy_lvl() == 1 && !d.is_quantifier()) || is_relevant_core(l))) + if (d.is_atom() && (relevancy_lvl() == 0 || (relevancy_lvl() == 1 && !d.is_quantifier()) || is_relevant_core(l))) { + CTRACE("assign_core", l.var() == 13, tout << "propagation queue\n";); m_atom_propagation_queue.push_back(l); + } if (m.has_trace_stream()) trace_assign(l, j, decision); m_case_split_queue->assign_lit_eh(l); - - // a unit is asserted at search level. Mark it as relevant. - // this addresses bug... where a literal becomes fixed to true (false) - // as a conflict gets assigned misses relevancy (and quantifier instantiation). - // - if (false && !decision && relevancy() && at_search_level() && !is_relevant_core(l)) { - mark_as_relevant(l); - } } bool context::bcp() { @@ -1356,13 +1352,14 @@ namespace smt { */ bool context::propagate_atoms() { SASSERT(!inconsistent()); + CTRACE("propagate_atoms", !m_atom_propagation_queue.empty(), tout << m_atom_propagation_queue << "\n";); for (unsigned i = 0; i < m_atom_propagation_queue.size() && !get_cancel_flag(); i++) { SASSERT(!inconsistent()); literal l = m_atom_propagation_queue[i]; bool_var v = l.var(); bool_var_data & d = get_bdata(v); lbool val = get_assignment(v); - TRACE("propagate_atoms", tout << "propagating atom, #" << bool_var2expr(v)->get_id() << ", is_enode(): " << d.is_enode() + CTRACE("propagate_atoms", v == 13, tout << "propagating atom, #" << bool_var2expr(v)->get_id() << ", is_enode(): " << d.is_enode() << " tag: " << (d.is_eq()?"eq":"") << (d.is_theory_atom()?"th":"") << (d.is_quantifier()?"q":"") << " " << l << "\n";); SASSERT(val != l_undef); if (d.is_enode()) @@ -2070,7 +2067,7 @@ namespace smt { while (i != old_lim) { --i; literal l = m_assigned_literals[i]; - CTRACE("assign_core", l.var() == 1573 || l.var() == 1253, tout << "unassign " << l << "\n";); + CTRACE("assign_core", l.var() == 13, tout << "unassign " << l << "\n";); m_assignment[l.index()] = l_undef; m_assignment[(~l).index()] = l_undef; bool_var v = l.var(); @@ -2443,6 +2440,8 @@ namespace smt { m_asserted_formulas.pop_scope(num_scopes); + CTRACE("propagate_atoms", !m_atom_propagation_queue.empty(), tout << m_atom_propagation_queue << "\n";); + m_eq_propagation_queue.reset(); m_th_eq_propagation_queue.reset(); m_th_diseq_propagation_queue.reset(); diff --git a/src/smt/smt_lookahead.cpp b/src/smt/smt_lookahead.cpp index 363687b1b..879e9baee 100644 --- a/src/smt/smt_lookahead.cpp +++ b/src/smt/smt_lookahead.cpp @@ -82,7 +82,10 @@ namespace smt { unsigned nf = 0, nc = 0, ns = 0, bound = 2000, n = 0; for (bool_var v : vars) { if (!ctx.bool_var2expr(v)) continue; - literal lit(v, false); + literal lit(v, false); + ctx.propagate(); + if (ctx.inconsistent()) + return expr_ref(m.mk_false(), m); ctx.push_scope(); ctx.assign(lit, b_justification::mk_axiom(), true); ctx.propagate(); @@ -96,6 +99,9 @@ namespace smt { continue; } + ctx.propagate(); + if (ctx.inconsistent()) + return expr_ref(m.mk_false(), m); ctx.push_scope(); ctx.assign(~lit, b_justification::mk_axiom(), true); ctx.propagate(); diff --git a/src/smt/theory_bv.cpp b/src/smt/theory_bv.cpp index c59fecdc3..4baae8b2a 100644 --- a/src/smt/theory_bv.cpp +++ b/src/smt/theory_bv.cpp @@ -1457,7 +1457,7 @@ namespace smt { m_diseq_watch_lim.shrink(m_diseq_watch_lim.size()-num_scopes); #endif theory::pop_scope_eh(num_scopes); - TRACE("bv", m_find.display(tout << get_context().get_scope_level() << " - " + TRACE("bv_verbose", m_find.display(tout << get_context().get_scope_level() << " - " << num_scopes << " = " << (get_context().get_scope_level() - num_scopes) << "\n");); } @@ -1888,6 +1888,8 @@ namespace smt { } bool theory_bv::check_invariant() { + if (get_context().inconsistent()) + return true; unsigned num = get_num_vars(); for (unsigned v = 0; v < num; v++) { check_assignment(v);