diff --git a/src/sat/sat_extension.h b/src/sat/sat_extension.h index 8f15f5f68..d6a956a32 100644 --- a/src/sat/sat_extension.h +++ b/src/sat/sat_extension.h @@ -89,7 +89,7 @@ namespace sat { virtual bool unit_propagate() = 0; virtual bool is_external(bool_var v) { return false; } virtual double get_reward(literal l, ext_constraint_idx idx, literal_occs_fun& occs) const { return 0; } - virtual void get_antecedents(literal l, ext_justification_idx idx, literal_vector & r, bool probing, proof_hint*& ph) = 0; + virtual void get_antecedents(literal l, ext_justification_idx idx, literal_vector & r, bool probing) = 0; virtual bool is_extended_binary(ext_justification_idx idx, literal_vector & r) { return false; } virtual bool decide(bool_var& var, lbool& phase) { return false; } virtual bool get_case_split(bool_var& var, lbool& phase) { return false; } diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 7f7b34ea8..8f9938dbb 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -2890,8 +2890,7 @@ namespace sat { SASSERT(m_ext); auto idx = js.get_ext_justification_idx(); m_ext_antecedents.reset(); - proof_hint* ph = nullptr; - m_ext->get_antecedents(consequent, idx, m_ext_antecedents, probing, ph); + m_ext->get_antecedents(consequent, idx, m_ext_antecedents, probing); } bool solver::is_two_phase() const { diff --git a/src/sat/smt/arith_solver.cpp b/src/sat/smt/arith_solver.cpp index 5db5688b3..f7e3f6293 100644 --- a/src/sat/smt/arith_solver.cpp +++ b/src/sat/smt/arith_solver.cpp @@ -1476,7 +1476,7 @@ namespace arith { return r; } - void solver::get_antecedents(literal l, sat::ext_justification_idx idx, literal_vector& r, bool probing, sat::proof_hint*& ph) { + void solver::get_antecedents(literal l, sat::ext_justification_idx idx, literal_vector& r, bool probing) { auto& jst = euf::th_explain::from_index(idx); ctx.get_antecedents(l, jst, r, probing); } diff --git a/src/sat/smt/arith_solver.h b/src/sat/smt/arith_solver.h index 672477df2..3d3f1ddd7 100644 --- a/src/sat/smt/arith_solver.h +++ b/src/sat/smt/arith_solver.h @@ -485,7 +485,7 @@ namespace arith { solver(euf::solver& ctx, theory_id id); ~solver() override; bool is_external(bool_var v) override { return false; } - void get_antecedents(literal l, sat::ext_justification_idx idx, literal_vector& r, bool probing, sat::proof_hint*& ph) override; + void get_antecedents(literal l, sat::ext_justification_idx idx, literal_vector& r, bool probing) override; void asserted(literal l) override; sat::check_result check() override; void simplify() override {} diff --git a/src/sat/smt/array_solver.h b/src/sat/smt/array_solver.h index f161af01a..5c2708842 100644 --- a/src/sat/smt/array_solver.h +++ b/src/sat/smt/array_solver.h @@ -278,7 +278,7 @@ namespace array { solver(euf::solver& ctx, theory_id id); ~solver() override; bool is_external(bool_var v) override { return false; } - void get_antecedents(literal l, sat::ext_justification_idx idx, literal_vector& r, bool probing, sat::proof_hint*& ph) override {} + void get_antecedents(literal l, sat::ext_justification_idx idx, literal_vector& r, bool probing) override {} void asserted(literal l) override {} sat::check_result check() override; diff --git a/src/sat/smt/bv_solver.cpp b/src/sat/smt/bv_solver.cpp index 631f954b1..8ef2c5cd5 100644 --- a/src/sat/smt/bv_solver.cpp +++ b/src/sat/smt/bv_solver.cpp @@ -306,7 +306,7 @@ 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; } - void solver::get_antecedents(literal l, sat::ext_justification_idx idx, literal_vector& r, bool probing, sat::proof_hint*& ph) { + 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";); switch (c.m_kind) { @@ -395,7 +395,6 @@ namespace bv { sat::literal leq1(s().num_vars() + 1, false); sat::literal leq2(s().num_vars() + 2, false); expr_ref eq1(m), eq2(m); - sat::proof_hint* ph = nullptr; if (c.m_kind == bv_justification::kind_t::bv2int) { eq1 = m.mk_eq(c.a->get_expr(), c.b->get_expr()); eq2 = m.mk_eq(c.a->get_expr(), c.c->get_expr()); @@ -417,24 +416,24 @@ namespace bv { lits.push_back(c.m_consequent); break; case bv_justification::kind_t::ne2bit: - get_antecedents(c.m_consequent, c.to_index(), lits, true, ph); + get_antecedents(c.m_consequent, c.to_index(), lits, true); lits.push_back(c.m_consequent); break; case bv_justification::kind_t::bit2eq: - get_antecedents(leq1, c.to_index(), lits, true, ph); + get_antecedents(leq1, c.to_index(), lits, true); for (auto& lit : lits) lit.neg(); lits.push_back(leq1); break; case bv_justification::kind_t::bit2ne: - get_antecedents(c.m_consequent, c.to_index(), lits, true, ph); + get_antecedents(c.m_consequent, c.to_index(), lits, true); for (auto& lit : lits) lit.neg(); lits.push_back(c.m_consequent); break; case bv_justification::kind_t::bv2int: - get_antecedents(leq1, c.to_index(), lits, true, ph); - get_antecedents(leq2, c.to_index(), lits, true, ph); + get_antecedents(leq1, c.to_index(), lits, true); + get_antecedents(leq2, c.to_index(), lits, true); for (auto& lit : lits) lit.neg(); lits.push_back(leq1); diff --git a/src/sat/smt/bv_solver.h b/src/sat/smt/bv_solver.h index 313679443..2c8fb4ae9 100644 --- a/src/sat/smt/bv_solver.h +++ b/src/sat/smt/bv_solver.h @@ -335,7 +335,7 @@ namespace bv { double get_reward(literal l, sat::ext_constraint_idx idx, sat::literal_occs_fun& occs) const override; 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, sat::proof_hint*& ph) override; + void get_antecedents(literal l, sat::ext_justification_idx idx, literal_vector & r, bool probing) override; void asserted(literal l) override; sat::check_result check() override; void push_core() override; diff --git a/src/sat/smt/dt_solver.cpp b/src/sat/smt/dt_solver.cpp index 80846ec58..a87f8770b 100644 --- a/src/sat/smt/dt_solver.cpp +++ b/src/sat/smt/dt_solver.cpp @@ -755,7 +755,7 @@ namespace dt { SASSERT(m_find.get_num_vars() == get_num_vars()); } - void solver::get_antecedents(literal l, sat::ext_justification_idx idx, literal_vector& r, bool probing, sat::proof_hint*& ph) { + void solver::get_antecedents(literal l, sat::ext_justification_idx idx, literal_vector& r, bool probing) { auto& jst = euf::th_explain::from_index(idx); ctx.get_antecedents(l, jst, r, probing); } diff --git a/src/sat/smt/dt_solver.h b/src/sat/smt/dt_solver.h index 136e40eac..4e2524f6b 100644 --- a/src/sat/smt/dt_solver.h +++ b/src/sat/smt/dt_solver.h @@ -140,7 +140,7 @@ namespace dt { ~solver() override; bool is_external(bool_var v) override { return false; } - void get_antecedents(literal l, sat::ext_justification_idx idx, literal_vector& r, bool probing, sat::proof_hint*& ph) override; + void get_antecedents(literal l, sat::ext_justification_idx idx, literal_vector& r, bool probing) override; void asserted(literal l) override; sat::check_result check() override; diff --git a/src/sat/smt/euf_solver.cpp b/src/sat/smt/euf_solver.cpp index cde3ef2e0..f0d40a13f 100644 --- a/src/sat/smt/euf_solver.cpp +++ b/src/sat/smt/euf_solver.cpp @@ -222,19 +222,19 @@ namespace euf { sub-hints. */ - void solver::get_antecedents(literal l, ext_justification_idx idx, literal_vector& r, bool probing, sat::proof_hint*& ph) { + void solver::get_antecedents(literal l, ext_justification_idx idx, literal_vector& r, bool probing) { m_egraph.begin_explain(); m_explain.reset(); if (use_drat() && !probing) push(restore_size_trail(m_explain_cc, m_explain_cc.size())); auto* ext = sat::constraint_base::to_extension(idx); th_proof_hint* hint = nullptr; - sat::proof_hint* shint = nullptr; bool has_theory = false; + bool has_nested_theory = false; if (ext == this) get_antecedents(l, constraint::from_idx(idx), r, probing); else { - ext->get_antecedents(l, idx, r, probing, shint); + ext->get_antecedents(l, idx, r, probing); has_theory = true; } for (unsigned qhead = 0; qhead < m_explain.size(); ++qhead) { @@ -246,12 +246,13 @@ namespace euf { auto* ext = sat::constraint_base::to_extension(idx); SASSERT(ext != this); sat::literal lit = sat::null_literal; - ext->get_antecedents(lit, idx, r, probing, shint); + ext->get_antecedents(lit, idx, r, probing); has_theory = true; + has_nested_theory = true; } } m_egraph.end_explain(); - if (use_drat() && !probing) { + if (use_drat() && !probing) { if (!has_theory) hint = mk_hint(l, r); else { diff --git a/src/sat/smt/euf_solver.h b/src/sat/smt/euf_solver.h index cedfcf2da..5e38768ee 100644 --- a/src/sat/smt/euf_solver.h +++ b/src/sat/smt/euf_solver.h @@ -338,7 +338,7 @@ namespace euf { bool set_root(literal l, literal r) override; void flush_roots() override; - void get_antecedents(literal l, ext_justification_idx idx, literal_vector& r, bool probing, sat::proof_hint*& ph) override; + void get_antecedents(literal l, ext_justification_idx idx, literal_vector& r, bool probing) override; void get_antecedents(literal l, th_explain& jst, literal_vector& r, bool probing); void add_antecedent(bool probing, enode* a, enode* b); void add_diseq_antecedent(ptr_vector& ex, cc_justification* cc, enode* a, enode* b); diff --git a/src/sat/smt/fpa_solver.h b/src/sat/smt/fpa_solver.h index 537ae0895..38abb399d 100644 --- a/src/sat/smt/fpa_solver.h +++ b/src/sat/smt/fpa_solver.h @@ -71,7 +71,7 @@ namespace fpa { void finalize_model(model& mdl) override; bool unit_propagate() override; - void get_antecedents(sat::literal l, sat::ext_justification_idx idx, sat::literal_vector& r, bool probing, sat::proof_hint*& ph) override { UNREACHABLE(); } + void get_antecedents(sat::literal l, sat::ext_justification_idx idx, sat::literal_vector& r, bool probing) override { UNREACHABLE(); } sat::check_result check() override; euf::th_solver* clone(euf::solver& ctx) override { return alloc(solver, ctx); } diff --git a/src/sat/smt/pb_solver.cpp b/src/sat/smt/pb_solver.cpp index 2a29f07d5..1c762cb3f 100644 --- a/src/sat/smt/pb_solver.cpp +++ b/src/sat/smt/pb_solver.cpp @@ -722,8 +722,7 @@ namespace pb { auto* ext = sat::constraint_base::to_extension(cindex); if (ext != this) { m_lemma.reset(); - sat::proof_hint* ph = nullptr; - ext->get_antecedents(consequent, idx, m_lemma, false, ph); + ext->get_antecedents(consequent, idx, m_lemma, false); for (literal l : m_lemma) process_antecedent(~l, offset); break; } @@ -1053,8 +1052,7 @@ namespace pb { auto* ext = sat::constraint_base::to_extension(index); if (ext != this) { m_lemma.reset(); - sat::proof_hint* ph = nullptr; - ext->get_antecedents(consequent, index, m_lemma, false, ph); + ext->get_antecedents(consequent, index, m_lemma, false); for (literal l : m_lemma) process_antecedent(~l, 1); break; @@ -1690,7 +1688,7 @@ namespace pb { // ---------------------------- // constraint generic methods - void solver::get_antecedents(literal l, sat::ext_justification_idx idx, literal_vector & r, bool probing, sat::proof_hint*& ph) { + void solver::get_antecedents(literal l, sat::ext_justification_idx idx, literal_vector & r, bool probing) { get_antecedents(l, index2constraint(idx), r, probing); } diff --git a/src/sat/smt/pb_solver.h b/src/sat/smt/pb_solver.h index 9f9e6835c..09c0e47e0 100644 --- a/src/sat/smt/pb_solver.h +++ b/src/sat/smt/pb_solver.h @@ -377,7 +377,7 @@ namespace pb { bool propagated(literal l, sat::ext_constraint_idx idx) override; bool unit_propagate() override { return false; } lbool resolve_conflict() override; - void get_antecedents(literal l, sat::ext_justification_idx idx, literal_vector & r, bool probing, sat::proof_hint*& ph) override; + void get_antecedents(literal l, sat::ext_justification_idx idx, literal_vector & r, bool probing) override; void asserted(literal l) override; sat::check_result check() override; void push() override; diff --git a/src/sat/smt/q_solver.cpp b/src/sat/smt/q_solver.cpp index 7bddcbd9f..7fd7be97e 100644 --- a/src/sat/smt/q_solver.cpp +++ b/src/sat/smt/q_solver.cpp @@ -353,7 +353,7 @@ namespace q { return !m.is_and(arg) && !m.is_or(arg) && !m.is_iff(arg) && !m.is_implies(arg); } - void solver::get_antecedents(sat::literal l, sat::ext_justification_idx idx, sat::literal_vector& r, bool probing, sat::proof_hint*& ph) { + void solver::get_antecedents(sat::literal l, sat::ext_justification_idx idx, sat::literal_vector& r, bool probing) { m_ematch.get_antecedents(l, idx, r, probing); } diff --git a/src/sat/smt/q_solver.h b/src/sat/smt/q_solver.h index f199db610..3a95a00be 100644 --- a/src/sat/smt/q_solver.h +++ b/src/sat/smt/q_solver.h @@ -83,7 +83,7 @@ namespace q { solver(euf::solver& ctx, family_id fid); bool is_external(sat::bool_var v) override { return false; } - void get_antecedents(sat::literal l, sat::ext_justification_idx idx, sat::literal_vector& r, bool probing, sat::proof_hint*& ph) override; + void get_antecedents(sat::literal l, sat::ext_justification_idx idx, sat::literal_vector& r, bool probing) override; void asserted(sat::literal l) override; sat::check_result check() override; diff --git a/src/sat/smt/recfun_solver.cpp b/src/sat/smt/recfun_solver.cpp index ebb1ec7c1..c88138d3f 100644 --- a/src/sat/smt/recfun_solver.cpp +++ b/src/sat/smt/recfun_solver.cpp @@ -180,7 +180,7 @@ namespace recfun { add_clause(clause); } - void solver::get_antecedents(sat::literal l, sat::ext_justification_idx idx, sat::literal_vector& r, bool probing, sat::proof_hint*& ph) { + void solver::get_antecedents(sat::literal l, sat::ext_justification_idx idx, sat::literal_vector& r, bool probing) { UNREACHABLE(); } diff --git a/src/sat/smt/recfun_solver.h b/src/sat/smt/recfun_solver.h index 463aee6d6..4e41a35a9 100644 --- a/src/sat/smt/recfun_solver.h +++ b/src/sat/smt/recfun_solver.h @@ -92,7 +92,7 @@ namespace recfun { solver(euf::solver& ctx); ~solver() override; bool is_external(sat::bool_var v) override { return false; } - void get_antecedents(sat::literal l, sat::ext_justification_idx idx, sat::literal_vector& r, bool probing, sat::proof_hint*& ph) override; + void get_antecedents(sat::literal l, sat::ext_justification_idx idx, sat::literal_vector& r, bool probing) override; void asserted(sat::literal l) override; sat::check_result check() override; std::ostream& display(std::ostream& out) const override; diff --git a/src/sat/smt/user_solver.cpp b/src/sat/smt/user_solver.cpp index 34fd26c77..5c98a6fac 100644 --- a/src/sat/smt/user_solver.cpp +++ b/src/sat/smt/user_solver.cpp @@ -201,7 +201,7 @@ namespace user_solver { return sat::justification::mk_ext_justification(s().scope_lvl(), constraint->to_index()); } - void solver::get_antecedents(sat::literal l, sat::ext_justification_idx idx, sat::literal_vector & r, bool probing, sat::proof_hint*& ph) { + void solver::get_antecedents(sat::literal l, sat::ext_justification_idx idx, sat::literal_vector & r, bool probing) { auto& j = justification::from_index(idx); auto const& prop = m_prop[j.m_propagation_index]; for (unsigned id : prop.m_ids) diff --git a/src/sat/smt/user_solver.h b/src/sat/smt/user_solver.h index c996d1878..28528b9a1 100644 --- a/src/sat/smt/user_solver.h +++ b/src/sat/smt/user_solver.h @@ -152,7 +152,7 @@ namespace user_solver { void push_core() override; void pop_core(unsigned n) override; bool unit_propagate() override; - void get_antecedents(sat::literal l, sat::ext_justification_idx idx, sat::literal_vector & r, bool probing, sat::proof_hint*& ph) override; + void get_antecedents(sat::literal l, sat::ext_justification_idx idx, sat::literal_vector & r, bool probing) override; void collect_statistics(statistics& st) const override; sat::literal internalize(expr* e, bool sign, bool root, bool learned) override; void internalize(expr* e, bool redundant) override; diff --git a/src/sat/smt/xor_solver.cpp b/src/sat/smt/xor_solver.cpp index 941cd21d4..27354eac2 100644 --- a/src/sat/smt/xor_solver.cpp +++ b/src/sat/smt/xor_solver.cpp @@ -37,7 +37,7 @@ namespace xr { } void solver::get_antecedents(sat::literal l, sat::ext_justification_idx idx, - sat::literal_vector & r, bool probing, sat::proof_hint*& ph) { + sat::literal_vector & r, bool probing) { } diff --git a/src/sat/smt/xor_solver.h b/src/sat/smt/xor_solver.h index 0748e1e9b..3da30c580 100644 --- a/src/sat/smt/xor_solver.h +++ b/src/sat/smt/xor_solver.h @@ -30,7 +30,7 @@ namespace xr { void asserted(sat::literal l) override; bool unit_propagate() override; - void get_antecedents(sat::literal l, sat::ext_justification_idx idx, sat::literal_vector & r, bool probing, sat::proof_hint*& ph) override; + void get_antecedents(sat::literal l, sat::ext_justification_idx idx, sat::literal_vector & r, bool probing) override; void pre_simplify() override; void simplify() override;