diff --git a/src/ast/euf/euf_egraph.cpp b/src/ast/euf/euf_egraph.cpp index f19a146c5c6..21bc14ba4b3 100644 --- a/src/ast/euf/euf_egraph.cpp +++ b/src/ast/euf/euf_egraph.cpp @@ -231,7 +231,7 @@ namespace euf { for (auto const& q : euf::enode_th_vars(r2)) if (p.get_id() == q.get_id()) add_th_diseq(p.get_id(), p.get_var(), q.get_var(), n); - } + } } diff --git a/src/sat/smt/bv_solver.cpp b/src/sat/smt/bv_solver.cpp index 53a00414074..e879ba30c68 100644 --- a/src/sat/smt/bv_solver.cpp +++ b/src/sat/smt/bv_solver.cpp @@ -301,6 +301,28 @@ namespace bv { bool solver::is_extended_binary(sat::ext_justification_idx idx, literal_vector& r) { return false; } bool solver::is_external(bool_var v) { return true; } + euf::enode_pair solver::get_justification_eq(size_t j) { + auto& c = bv_justification::from_index(j); + TRACE("bv", display_constraint(tout, j) << "\n";); + switch (c.m_kind) { + case bv_justification::kind_t::eq2bit: + UNREACHABLE(); + return euf::enode_pair(); + case bv_justification::kind_t::ne2bit: + UNREACHABLE(); + return euf::enode_pair(); + case bv_justification::kind_t::bit2eq: + return { var2enode(c.m_v1), var2enode(c.m_v2) }; + case bv_justification::kind_t::bit2ne: + UNREACHABLE(); + return euf::enode_pair(); + case bv_justification::kind_t::bv2int: + UNREACHABLE(); + return euf::enode_pair(); + } + return euf::enode_pair(); + } + void solver::get_antecedents(literal l, sat::ext_justification_idx idx, literal_vector& r, bool probing) { auto& c = bv_justification::from_index(idx); TRACE("bv", display_constraint(tout, idx) << "\n";); diff --git a/src/sat/smt/bv_solver.h b/src/sat/smt/bv_solver.h index df4e5c9c2e9..9cbee87f9ab 100644 --- a/src/sat/smt/bv_solver.h +++ b/src/sat/smt/bv_solver.h @@ -349,6 +349,7 @@ namespace bv { bool is_extended_binary(sat::ext_justification_idx idx, literal_vector& r) override; bool is_external(bool_var v) override; void get_antecedents(literal l, sat::ext_justification_idx idx, literal_vector & r, bool probing) override; + euf::enode_pair get_justification_eq(size_t j) override; void asserted(literal l) override; sat::check_result check() override; void push_core() override; diff --git a/src/sat/smt/euf_proof.cpp b/src/sat/smt/euf_proof.cpp index 39c9879a608..099019c6e03 100644 --- a/src/sat/smt/euf_proof.cpp +++ b/src/sat/smt/euf_proof.cpp @@ -43,6 +43,13 @@ namespace euf { m_proof_initialized = true; } + enode_pair solver::get_justification_eq(size_t j) { + auto* ext = sat::constraint_base::to_extension(j); + SASSERT(ext != this); + auto s = fid2solver(ext->get_id()); + return s->get_justification_eq(j); + } + /** * Log justifications. * is_euf - true if l is justified by congruence closure. In this case create a congruence closure proof. @@ -63,7 +70,8 @@ namespace euf { if (is_literal(e)) m_hint_lits.push_back(get_literal(e)); else { - auto [x, y] = th_explain::from_index(get_justification(e)).eq_consequent(); + SASSERT(is_justification(e)); + auto [x, y] = get_justification_eq(get_justification(e)); eqs.push_back(m.mk_eq(x->get_expr(), y->get_expr())); set_tmp_bool_var(nv, eqs.back()); m_hint_lits.push_back(literal(nv, false)); diff --git a/src/sat/smt/euf_solver.cpp b/src/sat/smt/euf_solver.cpp index efd091f6653..b866990af43 100644 --- a/src/sat/smt/euf_solver.cpp +++ b/src/sat/smt/euf_solver.cpp @@ -278,9 +278,9 @@ namespace euf { r.push_back(get_literal(e)); else { multiple_theories = true; - size_t idx = get_justification(e); + size_t idx = get_justification(e); auto* ext = sat::constraint_base::to_extension(idx); - SASSERT(ext != this); + SASSERT(ext != this); sat::literal lit = sat::null_literal; ext->get_antecedents(lit, idx, r, probing); } @@ -307,11 +307,11 @@ namespace euf { void solver::get_eq_antecedents(enode* a, enode* b, literal_vector& r) { m_egraph.begin_explain(); m_explain.reset(); - m_egraph.explain_eq(m_explain, nullptr, a, b); - for (unsigned qhead = 0; qhead < m_explain.size(); ++qhead) { - size_t* e = m_explain[qhead]; - if (is_literal(e)) - r.push_back(get_literal(e)); + m_egraph.explain_eq(m_explain, nullptr, a, b); + for (unsigned qhead = 0; qhead < m_explain.size(); ++qhead) { + size_t* e = m_explain[qhead]; + if (is_literal(e)) + r.push_back(get_literal(e)); else { size_t idx = get_justification(e); auto* ext = sat::constraint_base::to_extension(idx); diff --git a/src/sat/smt/euf_solver.h b/src/sat/smt/euf_solver.h index ec89667d5bf..22e68d2dabe 100644 --- a/src/sat/smt/euf_solver.h +++ b/src/sat/smt/euf_solver.h @@ -231,6 +231,7 @@ namespace euf { void log_antecedents(literal l, literal_vector const& r, th_proof_hint* hint); void log_justification(literal l, th_explain const& jst); void log_justifications(literal l, unsigned explain_size, bool is_euf); + enode_pair get_justification_eq(size_t j); void log_rup(literal l, literal_vector const& r); diff --git a/src/sat/smt/sat_th.cpp b/src/sat/smt/sat_th.cpp index 21e3883e8a0..4176be9857a 100644 --- a/src/sat/smt/sat_th.cpp +++ b/src/sat/smt/sat_th.cpp @@ -51,6 +51,10 @@ namespace euf { return true; } + enode_pair th_solver::get_justification_eq(size_t j) { + return th_explain::from_index(j).eq_consequent(); + } + th_euf_solver::th_euf_solver(euf::solver& ctx, symbol const& name, euf::theory_id id): th_solver(ctx.get_manager(), name, id), ctx(ctx) diff --git a/src/sat/smt/sat_th.h b/src/sat/smt/sat_th.h index cdd1292a330..37394801452 100644 --- a/src/sat/smt/sat_th.h +++ b/src/sat/smt/sat_th.h @@ -137,6 +137,8 @@ namespace euf { sat::status status() const { return sat::status::th(false, get_id()); } + virtual euf::enode_pair get_justification_eq(size_t j); + /** * Local search interface */