From e7c17e68b8281996b2d3d150de958dbceae21ec8 Mon Sep 17 00:00:00 2001 From: Clemens Eisenhofer <56730610+CEisenhofer@users.noreply.github.com> Date: Sat, 28 Oct 2023 21:46:43 +0200 Subject: [PATCH] Fixed next_split call in pop (#6966) * Give users ability to see if propagation failed * Skip propagations in the new core if they are already satisfied * Fix registration in final * Don't make it too complicated... * Fixed next_split when called in pop Made delay_units available even without quantifiers * Missing push calls before "decide"-callback --- src/smt/smt_context.cpp | 1 - src/smt/theory_user_propagator.cpp | 69 +++++++++++++++++------------- src/smt/theory_user_propagator.h | 3 +- 3 files changed, 41 insertions(+), 32 deletions(-) diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index 577123ec96c..6d90653ba8b 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -4122,7 +4122,6 @@ namespace smt { // Moreover, I backtrack only one level. bool delay_forced_restart = m_fparams.m_delay_units && - internalized_quantifiers() && num_lits == 1 && conflict_lvl > m_search_lvl + 1 && !m.proofs_enabled() && diff --git a/src/smt/theory_user_propagator.cpp b/src/smt/theory_user_propagator.cpp index 6735272a148..84a6799fb3d 100644 --- a/src/smt/theory_user_propagator.cpp +++ b/src/smt/theory_user_propagator.cpp @@ -62,12 +62,12 @@ void theory_user_propagator::add_expr(expr* term, bool ensure_enode) { enode* n = ensure_enode ? this->ensure_enode(e) : ctx.get_enode(e); if (is_attached_to_var(n)) return; - + theory_var v = mk_var(n); m_var2expr.reserve(v + 1); m_var2expr[v] = term; m_expr2var.setx(term->get_id(), v, null_theory_var); - + if (m.is_bool(e) && !ctx.b_internalized(e)) { bool_var bv = ctx.mk_bool_var(e); ctx.set_var_theory(bv, get_id()); @@ -79,7 +79,6 @@ void theory_user_propagator::add_expr(expr* term, bool ensure_enode) { literal_vector explain; if (ctx.is_fixed(n, r, explain)) m_prop.push_back(prop_info(explain, v, r)); - } bool theory_user_propagator::propagate_cb( @@ -109,14 +108,19 @@ void theory_user_propagator::register_cb(expr* e) { bool theory_user_propagator::next_split_cb(expr* e, unsigned idx, lbool phase) { if (e == nullptr) { // clear - m_next_split_var = null_bool_var; + m_next_split_var = nullptr; + return true; + } + if (!ctx.e_internalized(e)) { + // We may not eagerly internalize it (might crash when done in pop) => delay + m_next_split_var = e; return true; } - ensure_enode(e); bool_var b = enode_to_bool(ctx.get_enode(e), idx); if (b == null_bool_var || ctx.get_assignment(b) != l_undef) return false; - m_next_split_var = b; + m_next_split_var = e; + m_next_split_idx = idx; m_next_split_phase = phase; return true; } @@ -150,7 +154,7 @@ final_check_status theory_user_propagator::final_check_eh() { m_final_eh(m_user_context, this); } catch (...) { - throw default_exception("Exception thrown in \"final\"-callback"); + throw default_exception("Exception thrown in \"final\"-callback"); } CTRACE("user_propagate", can_propagate(), tout << "can propagate\n"); propagate(); @@ -170,11 +174,11 @@ void theory_user_propagator::new_fixed_eh(theory_var v, expr* value, unsigned nu ctx.push_trail(insert_map(m_fixed, v)); m_id2justification.setx(v, literal_vector(num_lits, jlits), literal_vector()); try { - m_fixed_eh(m_user_context, this, var2expr(v), value); - } - catch (...) { + m_fixed_eh(m_user_context, this, var2expr(v), value); + } + catch (...) { throw default_exception("Exception thrown in \"fixed\"-callback"); - } + } } bool_var theory_user_propagator::enode_to_bool(enode* n, unsigned idx) { @@ -191,18 +195,18 @@ bool_var theory_user_propagator::enode_to_bool(enode* n, unsigned idx) { void theory_user_propagator::decide(bool_var& var, bool& is_pos) { if (!m_decide_eh) return; - + const bool_var_data& d = ctx.get_bdata(var); - - if (!d.is_enode() && !d.is_theory_atom()) + + if (!d.is_enode() && !d.is_theory_atom()) return; - - enode* original_enode = nullptr; + + enode* original_enode = nullptr; unsigned original_bit = 0; bv_util bv(m); theory* th = nullptr; theory_var v = null_theory_var; - + // get the associated theory if (!d.is_enode()) { // it might be a value that does not have an enode @@ -216,7 +220,7 @@ void theory_user_propagator::decide(bool_var& var, bool& is_pos) { th = ctx.get_theory(d.get_theory()); } } - + if (v == null_theory_var && !th) return; @@ -225,7 +229,7 @@ void theory_user_propagator::decide(bool_var& var, bool& is_pos) { if (v == null_theory_var) { // it is not a registered boolean value but it is a bitvector - auto registered_bv = ((theory_bv *) th)->get_bv_with_theory(var, get_family_id()); + auto registered_bv = ((theory_bv*) th)->get_bv_with_theory(var, get_family_id()); if (!registered_bv.first) // there is no registered bv associated with the bit return; @@ -237,6 +241,7 @@ void theory_user_propagator::decide(bool_var& var, bool& is_pos) { // call the registered callback unsigned new_bit = original_bit; + force_push(); expr *e = var2expr(v); m_decide_eh(m_user_context, this, e, new_bit, is_pos); @@ -252,12 +257,16 @@ void theory_user_propagator::decide(bool_var& var, bool& is_pos) { } bool theory_user_propagator::get_case_split(bool_var& var, bool& is_pos) { - if (m_next_split_var == null_bool_var) + if (m_next_split_var == nullptr) return false; - - var = m_next_split_var; + ensure_enode(m_next_split_var); + bool_var b = enode_to_bool(ctx.get_enode(m_next_split_var), m_next_split_idx); + if (b == null_bool_var || ctx.get_assignment(b) != l_undef) + return false; + var = b; is_pos = ctx.guess(var, m_next_split_phase); - m_next_split_var = null_bool_var; + m_next_split_var = nullptr; + m_next_split_idx = 0; m_next_split_phase = l_undef; return true; } @@ -289,11 +298,11 @@ bool theory_user_propagator::can_propagate() { void theory_user_propagator::propagate_consequence(prop_info const& prop) { justification* js; - m_lits.reset(); + m_lits.reset(); m_eqs.reset(); - for (expr* id : prop.m_ids) + for (expr* id: prop.m_ids) m_lits.append(m_id2justification[expr2var(id)]); - for (auto const& [a,b] : prop.m_eqs) + for (auto const& [a, b]: prop.m_eqs) if (a != b) m_eqs.push_back(enode_pair(get_enode(expr2var(a)), get_enode(expr2var(b)))); DEBUG_CODE(for (auto const& [a, b] : m_eqs) VERIFY(a->get_root() == b->get_root());); @@ -328,7 +337,7 @@ void theory_user_propagator::propagate_consequence(prop_info const& prop) { lit = mk_literal(fn); } else - lit = mk_literal(prop.m_conseq); + lit = mk_literal(prop.m_conseq); ctx.mark_as_relevant(lit); #if 0 @@ -339,8 +348,8 @@ void theory_user_propagator::propagate_consequence(prop_info const& prop) { ctx.assign(lit, js); #endif - -#if 1 + +#if 1 m_lits.push_back(lit); ctx.mk_th_lemma(get_id(), m_lits); #endif @@ -358,7 +367,7 @@ void theory_user_propagator::propagate() { return; TRACE("user_propagate", tout << "propagating queue head: " << m_qhead << " prop queue: " << m_prop.size() << "\n"); force_push(); - + unsigned qhead = m_to_add_qhead; if (qhead < m_to_add.size()) { for (; qhead < m_to_add.size(); ++qhead) diff --git a/src/smt/theory_user_propagator.h b/src/smt/theory_user_propagator.h index 2f045b0ba6d..4b365ef7a56 100644 --- a/src/smt/theory_user_propagator.h +++ b/src/smt/theory_user_propagator.h @@ -83,7 +83,8 @@ namespace smt { expr_ref_vector m_to_add; unsigned_vector m_to_add_lim; unsigned m_to_add_qhead = 0; - bool_var m_next_split_var = null_bool_var; + expr* m_next_split_var = nullptr; + unsigned m_next_split_idx = 0; lbool m_next_split_phase = l_undef; expr* var2expr(theory_var v) { return m_var2expr.get(v); }