rename antecedent utilities for clarity

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/sat/smt/arith_solver.cpp

@@ -1460,7 +1460,7 @@ namespace arith {
 
     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);
+        ctx.get_th_antecedents(l, jst, r, probing);
     }
 
     bool solver::include_func_interp(func_decl* f) const {

src/sat/smt/bv_solver.cpp

@@ -308,7 +308,7 @@ namespace bv {
         case bv_justification::kind_t::eq2bit:
             SASSERT(s().value(c.m_antecedent) == l_true);
             r.push_back(c.m_antecedent);
-            ctx.add_antecedent(probing, var2enode(c.m_v1), var2enode(c.m_v2));
+            ctx.add_eq_antecedent(probing, var2enode(c.m_v1), var2enode(c.m_v2));
             break;
         case bv_justification::kind_t::ne2bit: {
             r.push_back(c.m_antecedent);
@@ -376,8 +376,8 @@ namespace bv {
             break;
         }
         case bv_justification::kind_t::bv2int: {
-            ctx.add_antecedent(probing, c.a, c.b);
+            ctx.add_eq_antecedent(probing, c.a, c.b);
-            ctx.add_antecedent(probing, c.a, c.c);
+            ctx.add_eq_antecedent(probing, c.a, c.c);
             break;
         }
         }

src/sat/smt/dt_solver.cpp

@@ -757,7 +757,7 @@ namespace dt {
 
     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);
+        ctx.get_th_antecedents(l, jst, r, probing);
     }
 
     void solver::add_value(euf::enode* n, model& mdl, expr_ref_vector& values) {

src/sat/smt/euf_proof.cpp

@@ -197,7 +197,6 @@ namespace euf {
                 if (!literal2expr(lits[i])) 
                     IF_VERBOSE(0, verbose_stream() << lits[i] << "\n"; display(verbose_stream()));
                 
-
                 SASSERT(literal2expr(lits[i]));
                 m_proof_literals.push_back(lits[i]);
             }
@@ -260,10 +259,7 @@ namespace euf {
             auto const& [a, b] = s.m_proof_deqs[i];
             args.push_back(m.mk_not(m.mk_eq(a, b)));
         }
-        for (auto * arg : args)
+        return m.mk_app(m_name, args.size(), args.data(), proof);
-            sorts.push_back(arg->get_sort());
-        func_decl* f = m.mk_func_decl(m_name, sorts.size(), sorts.data(), proof);
-        return m.mk_app(f, args);
     }
 
     void solver::set_tmp_bool_var(bool_var b, expr* e) {
@@ -298,7 +294,7 @@ namespace euf {
     }
 
     void solver::on_clause(unsigned n, literal const* lits, sat::status st) {
-        TRACE("euf", tout << "on-clause " << n << "\n");
+        TRACE("euf_verbose", tout << "on-clause " << n << "\n");
         on_lemma(n, lits, st);
         on_proof(n, lits, st);
         on_check(n, lits, st);
@@ -417,7 +413,7 @@ namespace euf {
         if (proof_hint)
             return display_expr(out << " ", proof_hint);
         else
-          return out;
+            return out;
     }
 
     app_ref solver::status2proof_hint(sat::status st) {

src/sat/smt/euf_solver.cpp

@@ -239,7 +239,7 @@ namespace euf {
         th_proof_hint* hint = nullptr;
 
         if (ext == this)
-            get_antecedents(l, constraint::from_idx(idx), r, probing);
+            get_euf_antecedents(l, constraint::from_idx(idx), r, probing);
         else 
             ext->get_antecedents(l, idx, r, probing);
 
@@ -260,8 +260,11 @@ namespace euf {
             if (create_hint) {
                 if (is_literal(e))
                     m_hint_lits.push_back(get_literal(e));
-                else
+                else {
-                    m_hint_eqs.push_back(th_explain::from_index(get_justification(e)).eq_consequent());
+                    auto const& eq = th_explain::from_index(get_justification(e)).eq_consequent();
+                    TRACE("euf", tout << "consequent " << bpp(eq.first) << " " << bpp(eq.second) << "\n"; );
+                    m_hint_eqs.push_back(eq);
+                }
             }
         }
         m_egraph.end_explain();
@@ -292,17 +295,17 @@ namespace euf {
             set_tmp_bool_var(v, nullptr);
     }
 
-    void solver::get_antecedents(literal l, th_explain& jst, literal_vector& r, bool probing) {
+    void solver::get_th_antecedents(literal l, th_explain& jst, literal_vector& r, bool probing) {
         for (auto lit : euf::th_explain::lits(jst))
             r.push_back(lit);
         for (auto eq : euf::th_explain::eqs(jst))
-            add_antecedent(probing, eq.first, eq.second);
+            add_eq_antecedent(probing, eq.first, eq.second);
         
         if (!probing && use_drat()) 
             log_justification(l, jst);
     }
 
-    void solver::add_antecedent(bool probing, enode* a, enode* b) {
+    void solver::add_eq_antecedent(bool probing, enode* a, enode* b) {
         cc_justification* cc = (!probing && use_drat()) ? &m_explain_cc : nullptr;
         m_egraph.explain_eq<size_t>(m_explain, cc, a, b);
     }
@@ -321,7 +324,7 @@ namespace euf {
         return true;
     }
 
-    void solver::get_antecedents(literal l, constraint& j, literal_vector& r, bool probing) {
+    void solver::get_euf_antecedents(literal l, constraint& j, literal_vector& r, bool probing) {
         expr* e = nullptr;
         euf::enode* n = nullptr;
         cc_justification* cc = nullptr;
@@ -357,6 +360,7 @@ namespace euf {
                 lbool val = ante->value();
                 SASSERT(val != l_undef);
                 literal ante_lit(v, val == l_false);
+                TRACE("euf", tout << "explain " << bpp(n) << " by " << bpp(ante) << "\n");
                 m_explain.push_back(to_ptr(ante_lit));
             }
             break;

src/sat/smt/euf_solver.h

@@ -220,7 +220,7 @@ namespace euf {
         void propagate_literal(enode* n, enode* ante);
         void propagate_th_eqs();
         bool is_self_propagated(th_eq const& e);
-        void get_antecedents(literal l, constraint& j, literal_vector& r, bool probing);
+        void get_euf_antecedents(literal l, constraint& j, literal_vector& r, bool probing);
         void new_diseq(enode* a, enode* b, literal lit);
         bool merge_shared_bools();
 
@@ -365,8 +365,8 @@ namespace euf {
         void flush_roots() 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 get_th_antecedents(literal l, th_explain& jst, literal_vector& r, bool probing);
-        void add_antecedent(bool probing, enode* a, enode* b);
+        void add_eq_antecedent(bool probing, enode* a, enode* b);
         void add_diseq_antecedent(ptr_vector<size_t>& ex, cc_justification* cc, enode* a, enode* b);
         void add_explain(size_t* p) { m_explain.push_back(p); }
         void reset_explain() { m_explain.reset(); }

src/sat/smt/user_solver.cpp

@@ -221,7 +221,7 @@ namespace user_solver {
         for (unsigned id : prop.m_ids)
             r.append(m_id2justification[id]);
         for (auto const& p : prop.m_eqs)
-            ctx.add_antecedent(probing, expr2enode(p.first), expr2enode(p.second));
+            ctx.add_eq_antecedent(probing, expr2enode(p.first), expr2enode(p.second));
     }
 
     /*