wip - remove stale skaffolding for retrieving sub-hints.

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; }

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);
-        m_ext->get_antecedents(consequent, idx, m_ext_antecedents, probing, ph);
     }
 
     bool solver::is_two_phase() const {

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);
     }

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 {}

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;
 

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(leq1, c.to_index(), lits, true);
-            get_antecedents(leq2, c.to_index(), lits, true, ph);
+            get_antecedents(leq2, c.to_index(), lits, true);
             for (auto& lit : lits)
                 lit.neg();
             lits.push_back(leq1);

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;

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);
     }

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;
 

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,8 +246,9 @@ 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();  

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<size_t>& ex, cc_justification* cc, enode* a, enode* 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); }

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);
-                    ext->get_antecedents(consequent, idx, m_lemma, false, ph);
                     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);
-                    ext->get_antecedents(consequent, index, m_lemma, false, ph);
                     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);
     }
 

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;

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);
     }
 

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;
 

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();
     }
 

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;

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)

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;

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) {
         
     }
     

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;