Removes old proof code (#4964)

This deletes much of the old proof code. Basically everything but the minimal necessary infra-structure for producing unsat cores. That includes dependency tracking in preprocessing, the prop engine proof and the unsat core computation code in the old proof manager. These should also go once we fully integrate into master the new proof infrastructure.

It also cleans interfaces that were using old-proof-code-specific constructs (such as LemmaProofRecipe). When possible or when it made sense standalone local proof production code was kept, but deactivated (such is in the equality engine and in the arithmetic solver).

7 files changed, 99 insertions, 254 deletions

diff --git a/src/theory/uf/eq_proof.cpp b/src/theory/uf/eq_proof.cpp
index 513cf2f39..d7b615ffa 100644
--- a/src/theory/uf/eq_proof.cpp
+++ b/src/theory/uf/eq_proof.cpp
@@ -21,33 +21,20 @@ namespace CVC4 {
 namespace theory {
 namespace eq {
 
-void EqProof::debug_print(const char* c,
-                          unsigned tb,
-                          PrettyPrinter* prettyPrinter) const
+void EqProof::debug_print(const char* c, unsigned tb) const
 {
   std::stringstream ss;
-  debug_print(ss, tb, prettyPrinter);
+  debug_print(ss, tb);
   Debug(c) << ss.str();
 }
 
-void EqProof::debug_print(std::ostream& os,
-                          unsigned tb,
-                          PrettyPrinter* prettyPrinter) const
+void EqProof::debug_print(std::ostream& os, unsigned tb) const
 {
   for (unsigned i = 0; i < tb; i++)
   {
     os << "  ";
   }
-
-  if (prettyPrinter)
-  {
-    os << prettyPrinter->printTag(d_id);
-  }
-  else
-  {
-    os << static_cast<MergeReasonType>(d_id);
-  }
-  os << "(";
+  os << d_id << "(";
   if (d_children.empty() && d_node.isNull())
   {
     os << ")";
@@ -66,7 +53,7 @@ void EqProof::debug_print(std::ostream& os,
   for (unsigned i = 0; i < size; ++i)
   {
     os << std::endl;
-    d_children[i]->debug_print(os, tb + 1, prettyPrinter);
+    d_children[i]->debug_print(os, tb + 1);
     if (i < size - 1)
     {
       for (unsigned j = 0; j < tb + 1; ++j)
@@ -850,8 +837,7 @@ Node EqProof::addToProof(
                           << ", returning " << it->second << "\n";
     return it->second;
   }
-  Trace("eqproof-conv") << "EqProof::addToProof: adding step for "
-                        << static_cast<MergeReasonType>(d_id)
+  Trace("eqproof-conv") << "EqProof::addToProof: adding step for " << d_id
                         << " with conclusion " << d_node << "\n";
   // Assumption
   if (d_id == MERGED_THROUGH_EQUALITY)
@@ -976,12 +962,10 @@ Node EqProof::addToProof(
   {
     Assert(!d_node.isNull() && d_node.getKind() == kind::EQUAL
            && d_node[1].isConst())
-        << ". Conclusion " << d_node << " from "
-        << static_cast<MergeReasonType>(d_id)
+        << ". Conclusion " << d_node << " from " << d_id
         << " was expected to be (= (f t1 ... tn) c)\n";
     Assert(!assumptions.count(d_node))
-        << "Conclusion " << d_node << " from "
-        << static_cast<MergeReasonType>(d_id) << " is an assumption\n";
+        << "Conclusion " << d_node << " from " << d_id << " is an assumption\n";
     // The step has the form
     //  [(= t1 c1)] ... [(= tn cn)]
     //  ------------------------
diff --git a/src/theory/uf/eq_proof.h b/src/theory/uf/eq_proof.h
index 492252baa..72368c8c9 100644
--- a/src/theory/uf/eq_proof.h
+++ b/src/theory/uf/eq_proof.h
@@ -35,36 +35,21 @@ namespace eq {
 class EqProof
 {
  public:
-  /** A custom pretty printer used for custom rules being those in
-   * MergeReasonType. */
-  class PrettyPrinter
-  {
-   public:
-    virtual ~PrettyPrinter() {}
-    virtual std::string printTag(unsigned tag) = 0;
-  };
-
   EqProof() : d_id(MERGED_THROUGH_REFLEXIVITY) {}
   /** The proof rule for concluding d_node */
-  unsigned d_id;
+  MergeReasonType d_id;
   /** The conclusion of this EqProof */
   Node d_node;
   /** The proofs of the premises for deriving d_node with d_id */
   std::vector<std::shared_ptr<EqProof>> d_children;
   /**
-   * Debug print this proof on debug trace c with tabulation tb and pretty
-   * printer prettyPrinter.
+   * Debug print this proof on debug trace c with tabulation tb.
    */
-  void debug_print(const char* c,
-                   unsigned tb = 0,
-                   PrettyPrinter* prettyPrinter = nullptr) const;
+  void debug_print(const char* c, unsigned tb = 0) const;
   /**
-   * Debug print this proof on output stream os with tabulation tb and pretty
-   * printer prettyPrinter.
+   * Debug print this proof on output stream os with tabulation tb.
    */
-  void debug_print(std::ostream& os,
-                   unsigned tb = 0,
-                   PrettyPrinter* prettyPrinter = nullptr) const;
+  void debug_print(std::ostream& os, unsigned tb = 0) const;
 
   /** Add to proof
    *
diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp
index dd142edf4..c97c99776 100644
--- a/src/theory/uf/equality_engine.cpp
+++ b/src/theory/uf/equality_engine.cpp
@@ -103,8 +103,6 @@ void EqualityEngine::init() {
 
   d_trueId = getNodeId(d_true);
   d_falseId = getNodeId(d_false);
-
-  d_freshMergeReasonType = eq::NUMBER_OF_MERGE_REASONS;
 }
 
 EqualityEngine::~EqualityEngine() {
@@ -1100,7 +1098,7 @@ void EqualityEngine::explainEquality(TNode t1, TNode t2, bool polarity,
     getExplanation(t1Id, t2Id, equalities, cache, eqp);
   } else {
     if (eqp) {
-      eqp->d_id = eq::MERGED_THROUGH_TRANS;
+      eqp->d_id = MERGED_THROUGH_TRANS;
       eqp->d_node = d_nodes[t1Id].eqNode(d_nodes[t2Id]).notNode();
     }
 
@@ -1137,12 +1135,13 @@ void EqualityEngine::explainEquality(TNode t1, TNode t2, bool polarity,
           Debug("pf::ee") << "Child proof is:" << std::endl;
           eqpc->debug_print("pf::ee", 1);
         }
-        if (eqpc->d_id == eq::MERGED_THROUGH_TRANS) {
+        if (eqpc->d_id == MERGED_THROUGH_TRANS)
+        {
           std::vector<std::shared_ptr<EqProof>> orderedChildren;
           bool nullCongruenceFound = false;
           for (const auto& child : eqpc->d_children)
           {
-            if (child->d_id == eq::MERGED_THROUGH_CONGRUENCE
+            if (child->d_id == MERGED_THROUGH_CONGRUENCE
                 && child->d_node.isNull())
             {
               nullCongruenceFound = true;
@@ -1382,35 +1381,24 @@ void EqualityEngine::getExplanation(
 #endif
 
   // If the nodes are the same, we're done
-  if (t1Id == t2Id){
-    if( eqp ) {
-      if (options::proofNew())
-      {
-        // ignore equalities between function symbols, i.e. internal nullary
-        // non-constant nodes.
-        //
-        // Note that this is robust for HOL because in that case function
-        // symbols are not internal nodes
-        if (d_isInternal[t1Id] && d_nodes[t1Id].getNumChildren() == 0
-            && !d_isConstant[t1Id])
-        {
-          eqp->d_node = Node::null();
-        }
-        else
-        {
-          Assert(d_nodes[t1Id].getKind() != kind::BUILTIN);
-          eqp->d_node = d_nodes[t1Id].eqNode(d_nodes[t1Id]);
-        }
-      }
-      else if ((d_nodes[t1Id].getKind() == kind::BUILTIN)
-               && (d_nodes[t1Id].getConst<Kind>() == kind::SELECT))
+  if (t1Id == t2Id)
+  {
+    if (eqp)
+    {
+      // ignore equalities between function symbols, i.e. internal nullary
+      // non-constant nodes.
+      //
+      // Note that this is robust for HOL because in that case function
+      // symbols are not internal nodes
+      if (d_isInternal[t1Id] && d_nodes[t1Id].getNumChildren() == 0
+          && !d_isConstant[t1Id])
       {
-        std::vector<Node> no_children;
-        eqp->d_node = NodeManager::currentNM()->mkNode(kind::PARTIAL_SELECT_0, no_children);
+        eqp->d_node = Node::null();
       }
       else
       {
-        eqp->d_node = ProofManager::currentPM()->mkOp(d_nodes[t1Id]);
+        Assert(d_nodes[t1Id].getKind() != kind::BUILTIN);
+        eqp->d_node = d_nodes[t1Id].eqNode(d_nodes[t1Id]);
       }
     }
     return;
@@ -1466,7 +1454,8 @@ void EqualityEngine::getExplanation(
             // The current node
             currentNode = bfsQueue[currentIndex].d_nodeId;
             EqualityNodeId edgeNode = d_equalityEdges[currentEdge].getNodeId();
-            unsigned reasonType = d_equalityEdges[currentEdge].getReasonType();
+            MergeReasonType reasonType = static_cast<MergeReasonType>(
+                d_equalityEdges[currentEdge].getReasonType());
             Node reason = d_equalityEdges[currentEdge].getReason();
 
             Debug("equality")
@@ -1482,8 +1471,9 @@ void EqualityEngine::getExplanation(
                 << edge.getNodeId() << "} " << d_nodes[edge.getNodeId()] << ")"
                 << std::endl;
             Debug("equality")
-                << d_name << "                       reason type = "
-                << static_cast<MergeReasonType>(reasonType) << std::endl;
+                << d_name
+                << "                       reason type = " << reasonType
+                << "\n";
 
             std::shared_ptr<EqProof> eqpc;;
             // Make child proof if a proof is being constructed
@@ -1518,63 +1508,21 @@ void EqualityEngine::getExplanation(
               {
                 eqpc->d_children.push_back(eqpc1);
                 eqpc->d_children.push_back(eqpc2);
-                if (options::proofNew())
+                // build conclusion if ids correspond to non-internal nodes or
+                // if non-internal nodes can be retrieved from them (in the
+                // case of n-ary applications), otherwise leave conclusion as
+                // null. This is only done for congruence kinds, since
+                // congruence is not used otherwise.
+                Kind k = d_nodes[currentNode].getKind();
+                if (d_congruenceKinds[k])
                 {
-                  // build conclusion if ids correspond to non-internal nodes or
-                  // if non-internal nodes can be retrieved from them (in the
-                  // case of n-ary applications), otherwise leave conclusion as
-                  // null. This is only done for congruence kinds, since
-                  // congruence is not used otherwise.
-                  Kind k = d_nodes[currentNode].getKind();
-                  if (d_congruenceKinds[k])
-                  {
-                    buildEqConclusion(currentNode, edgeNode, eqpc.get());
-                  }
-                  else
-                  {
-                    Assert(k == kind::EQUAL)
-                        << "not an internal node " << d_nodes[currentNode]
-                        << " with non-congruence with " << k << "\n";
-                  }
-                }
-                else if (d_nodes[currentNode].getKind() == kind::EQUAL)
-                {
-                  //leave node null for now
-                  eqpc->d_node = Node::null();
+                  buildEqConclusion(currentNode, edgeNode, eqpc.get());
                 }
                 else
                 {
-                  if (d_nodes[f1.d_a].getKind() == kind::APPLY_UF
-                      || d_nodes[f1.d_a].getKind() == kind::SELECT
-                      || d_nodes[f1.d_a].getKind() == kind::STORE)
-                  {
-                    eqpc->d_node = d_nodes[f1.d_a];
-                  }
-                  else
-                  {
-                    if (d_nodes[f1.d_a].getKind() == kind::BUILTIN
-                        && d_nodes[f1.d_a].getConst<Kind>() == kind::SELECT)
-                    {
-                      eqpc->d_node = NodeManager::currentNM()->mkNode(
-                          kind::PARTIAL_SELECT_1, d_nodes[f1.d_b]);
-                      // The first child is a PARTIAL_SELECT_0.
-                      // Give it a child so that we know what kind of (read) it is, when we dump to LFSC.
-                      Assert(eqpc->d_children[0]->d_node.getKind()
-                             == kind::PARTIAL_SELECT_0);
-                      Assert(eqpc->d_children[0]->d_children.size() == 0);
-
-                      eqpc->d_children[0]->d_node =
-                          NodeManager::currentNM()->mkNode(
-                              kind::PARTIAL_SELECT_0, d_nodes[f1.d_b]);
-                    }
-                    else
-                    {
-                      eqpc->d_node = NodeManager::currentNM()->mkNode(
-                          kind::PARTIAL_APPLY_UF,
-                          ProofManager::currentPM()->mkOp(d_nodes[f1.d_a]),
-                          d_nodes[f1.d_b]);
-                    }
-                  }
+                  Assert(k == kind::EQUAL)
+                      << "not an internal node " << d_nodes[currentNode]
+                      << " with non-congruence with " << k << "\n";
                 }
               }
               Debug("equality") << pop;
@@ -1608,7 +1556,7 @@ void EqualityEngine::getExplanation(
 
               // Get the node we interpreted
               TNode interpreted;
-              if (eqpc && options::proofNew())
+              if (eqpc)
               {
                 // build the conclusion f(c1, ..., cn) = c
                 if (d_nodes[currentNode].isConst())
@@ -1661,24 +1609,19 @@ void EqualityEngine::getExplanation(
               Debug("equality") << d_name << "::eq::getExplanation(): adding: "
                                 << reason << std::endl;
               Debug("equality")
-                  << d_name << "::eq::getExplanation(): reason type = "
-                  << static_cast<MergeReasonType>(reasonType) << std::endl;
+                  << d_name
+                  << "::eq::getExplanation(): reason type = " << reasonType
+                  << "\n";
               Node a = d_nodes[currentNode];
               Node b = d_nodes[d_equalityEdges[currentEdge].getNodeId()];
 
               if (eqpc) {
-                //apply proof reconstruction processing (when eqpc is non-null)
-                if (d_pathReconstructionTriggers.find(reasonType) != d_pathReconstructionTriggers.end()) {
-                  d_pathReconstructionTriggers.find(reasonType)
-                      ->second->notify(reasonType, reason, a, b, equalities,
-                                       eqpc.get());
-                }
                 if (reasonType == MERGED_THROUGH_EQUALITY) {
                   // in the new proof infrastructure we can assume that "theory
                   // assumptions", which are a consequence of theory reasoning
                   // on other assumptions, are externally justified. In this
                   // case we can use (= a b) directly as the conclusion here.
-                  eqpc->d_node = !options::proofNew() ? reason : b.eqNode(a);
+                  eqpc->d_node = b.eqNode(a);
                 } else {
                   // The LFSC translator prefers (not (= a b)) over (= (= a b) false)
 
@@ -1722,20 +1665,12 @@ void EqualityEngine::getExplanation(
             } else {
               eqp->d_id = MERGED_THROUGH_TRANS;
               eqp->d_children.insert( eqp->d_children.end(), eqp_trans.begin(), eqp_trans.end() );
-              if (options::proofNew())
-              {
-                // build conclusion in case of equality between non-internal
-                // nodes or of n-ary congruence kinds, otherwise leave as
-                // null. The latter is necessary for the overall handling of
-                // congruence proofs involving n-ary kinds, see
-                // EqProof::reduceNestedCongruence for more details.
-                buildEqConclusion(t1Id, t2Id, eqp);
-              }
-              else
-              {
-                eqp->d_node = NodeManager::currentNM()->mkNode(
-                    kind::EQUAL, d_nodes[t1Id], d_nodes[t2Id]);
-              }
+              // build conclusion in case of equality between non-internal
+              // nodes or of n-ary congruence kinds, otherwise leave as
+              // null. The latter is necessary for the overall handling of
+              // congruence proofs involving n-ary kinds, see
+              // EqProof::reduceNestedCongruence for more details.
+              buildEqConclusion(t1Id, t2Id, eqp);
             }
             if (Debug.isOn("pf::ee"))
             {
@@ -2218,18 +2153,6 @@ size_t EqualityEngine::getSize(TNode t) {
   return getEqualityNode(getEqualityNode(t).getFind()).getSize();
 }
 
-
-void EqualityEngine::addPathReconstructionTrigger(unsigned trigger, const PathReconstructionNotify* notify) {
-  // Currently we can only inform one callback per trigger
-  Assert(d_pathReconstructionTriggers.find(trigger)
-         == d_pathReconstructionTriggers.end());
-  d_pathReconstructionTriggers[trigger] = notify;
-}
-
-unsigned EqualityEngine::getFreshMergeReasonType() {
-  return d_freshMergeReasonType++;
-}
-
 std::string EqualityEngine::identify() const { return d_name; }
 
 void EqualityEngine::addTriggerTerm(TNode t, TheoryId tag)
diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h
index 19a10eba8..f8444965f 100644
--- a/src/theory/uf/equality_engine.h
+++ b/src/theory/uf/equality_engine.h
@@ -43,26 +43,10 @@ namespace CVC4 {
 namespace theory {
 namespace eq {
 
-
-class EqProof;
 class EqClassesIterator;
 class EqClassIterator;
 
 /**
- * An interface for equality engine notifications during equality path reconstruction.
- * Can be used to add theory-specific logic for, e.g., proof construction.
- */
-class PathReconstructionNotify {
-public:
-
-  virtual ~PathReconstructionNotify() {}
-
-  virtual void notify(unsigned reasonType, Node reason, Node a, Node b,
-                      std::vector<TNode>& equalities,
-                      EqProof* proof) const = 0;
-};
-
-/**
  * Class for keeping an incremental congruence closure over a set of terms. It provides
  * notifications via an EqualityEngineNotify object.
  */
@@ -152,9 +136,6 @@ private:
   /** The map of kinds with operators to be considered external (for higher-order) */
   KindMap d_congruenceKindsExtOperators;
 
-  /** Objects that need to be notified during equality path reconstruction */
-  std::map<unsigned, const PathReconstructionNotify*> d_pathReconstructionTriggers;
-
   /** Map from nodes to their ids */
   std::unordered_map<TNode, EqualityNodeId, TNodeHashFunction> d_nodeIds;
 
@@ -196,9 +177,6 @@ private:
   /** Memory for the use-list nodes */
   std::vector<UseListNode> d_useListNodes;
 
-  /** A fresh merge reason type to return upon request */
-  unsigned d_freshMergeReasonType;
-
   /**
    * We keep a list of asserted equalities. Not among original terms, but
    * among the class representatives.
@@ -861,16 +839,6 @@ private:
    */
   bool consistent() const { return !d_done; }
 
-  /**
-   * Marks an object for merge type based notification during equality path reconstruction.
-   */
-  void addPathReconstructionTrigger(unsigned trigger, const PathReconstructionNotify* notify);
-
-  /**
-   * Returns a fresh merge reason type tag for the client to use.
-   */
-  unsigned getFreshMergeReasonType();
-
   /** Identify this equality engine (for debugging, etc..) */
   std::string identify() const;
 };
diff --git a/src/theory/uf/equality_engine_types.h b/src/theory/uf/equality_engine_types.h
index 14cd80436..cceffa51d 100644
--- a/src/theory/uf/equality_engine_types.h
+++ b/src/theory/uf/equality_engine_types.h
@@ -63,20 +63,26 @@ static const EqualityEdgeId null_edge = (EqualityEdgeId)(-1);
  * or a merge of an equality to false due to both sides being
  * (different) constants.
  */
-enum MergeReasonType {
-  /** Terms were merged due to application of congruence closure */
+enum MergeReasonType
+{
+  /** Terms were merged due to congruence */
   MERGED_THROUGH_CONGRUENCE,
-  /** Terms were merged due to application of pure equality */
+  /** Terms were merged due to an assumption */
   MERGED_THROUGH_EQUALITY,
-  /** Equality was merged to true, due to both sides of equality being in the same class */
+  /** Terms were merged due to reflexivity */
   MERGED_THROUGH_REFLEXIVITY,
-  /** Equality was merged to false, due to both sides of equality being a constant */
+  /** Terms were merged due to theory reasoning */
   MERGED_THROUGH_CONSTANTS,
-  /** (for proofs only) Equality was merged due to transitivity */
+  /** Terms were merged due to transitivity */
   MERGED_THROUGH_TRANS,
-
-  /** Reason types beyond this constant are theory specific reasons */
-  NUMBER_OF_MERGE_REASONS
+  // TEMPORARY RULES WHILE WE DON'T MIGRATE TO PROOF_NEW
+
+  /** Terms were merged due to arrays read-over-write */
+  MERGED_THROUGH_ROW,
+  /** Terms were merged due to arrays read-over-write (1) */
+  MERGED_THROUGH_ROW1,
+  /** Terms were merged due to extensionality */
+  MERGED_THROUGH_EXT,
 };
 
 inline std::ostream& operator << (std::ostream& out, MergeReasonType reason) {
@@ -90,13 +96,13 @@ inline std::ostream& operator << (std::ostream& out, MergeReasonType reason) {
   case MERGED_THROUGH_REFLEXIVITY:
     out << "reflexivity";
     break;
-  case MERGED_THROUGH_CONSTANTS:
-    out << "constants disequal";
-    break;
+  case MERGED_THROUGH_CONSTANTS: out << "theory constants"; break;
   case MERGED_THROUGH_TRANS:
     out << "transitivity";
     break;
-
+  case MERGED_THROUGH_ROW: out << "read-over-write"; break;
+  case MERGED_THROUGH_ROW1: out << "read-over-write (1)"; break;
+  case MERGED_THROUGH_EXT: out << "extensionality"; break;
   default:
     out << "[theory]";
     break;
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index f94cc36af..3d90637e2 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -25,9 +25,6 @@
 #include "options/smt_options.h"
 #include "options/theory_options.h"
 #include "options/uf_options.h"
-#include "proof/proof_manager.h"
-#include "proof/theory_proof.h"
-#include "proof/uf_proof.h"
 #include "theory/theory_model.h"
 #include "theory/type_enumerator.h"
 #include "theory/uf/cardinality_extension.h"
@@ -288,39 +285,30 @@ bool TheoryUF::propagateLit(TNode literal)
   return ok;
 }/* TheoryUF::propagate(TNode) */
 
-void TheoryUF::explain(TNode literal, std::vector<TNode>& assumptions, eq::EqProof* pf) {
+void TheoryUF::explain(TNode literal, Node& exp)
+{
+  Debug("uf") << "TheoryUF::explain(" << literal << ")" << std::endl;
+  std::vector<TNode> assumptions;
   // Do the work
   bool polarity = literal.getKind() != kind::NOT;
   TNode atom = polarity ? literal : literal[0];
-  if (atom.getKind() == kind::EQUAL) {
+  if (atom.getKind() == kind::EQUAL)
+  {
     d_equalityEngine->explainEquality(
-        atom[0], atom[1], polarity, assumptions, pf);
-  } else {
-    d_equalityEngine->explainPredicate(atom, polarity, assumptions, pf);
-  }
-  if( pf ){
-    Debug("pf::uf") << std::endl;
-    pf->debug_print("pf::uf");
+        atom[0], atom[1], polarity, assumptions, nullptr);
   }
-
-  Debug("pf::uf") << "UF: explain( " << literal << " ):" << std::endl << "\t";
-  for (unsigned i = 0; i < assumptions.size(); ++i) {
-    Debug("pf::uf") << assumptions[i] << " ";
+  else
+  {
+    d_equalityEngine->explainPredicate(atom, polarity, assumptions, nullptr);
   }
-  Debug("pf::uf") << std::endl;
+  exp = mkAnd(assumptions);
 }
 
 TrustNode TheoryUF::explain(TNode literal)
 {
-  Node exp = explain(literal, NULL);
-  return TrustNode::mkTrustPropExp(literal, exp, nullptr);
-}
-
-Node TheoryUF::explain(TNode literal, eq::EqProof* pf) {
-  Debug("uf") << "TheoryUF::explain(" << literal << ")" << std::endl;
-  std::vector<TNode> assumptions;
-  explain(literal, assumptions, pf);
-  return mkAnd(assumptions);
+  Node explanation;
+  explain(literal, explanation);
+  return TrustNode::mkTrustPropExp(literal, explanation, nullptr);
 }
 
 bool TheoryUF::collectModelValues(TheoryModel* m, const std::set<Node>& termSet)
@@ -662,12 +650,11 @@ void TheoryUF::computeCareGraph() {
                        << std::endl;
 }/* TheoryUF::computeCareGraph() */
 
-void TheoryUF::conflict(TNode a, TNode b) {
-  std::shared_ptr<eq::EqProof> pf =
-      d_proofsEnabled ? std::make_shared<eq::EqProof>() : nullptr;
-  Node conf = explain(a.eqNode(b), pf.get());
-  std::unique_ptr<ProofUF> puf(d_proofsEnabled ? new ProofUF(pf) : nullptr);
-  d_out->conflict(conf, std::move(puf));
+void TheoryUF::conflict(TNode a, TNode b)
+{
+  Node conf;
+  explain(a.eqNode(b), conf);
+  d_out->conflict(conf);
   d_state.notifyInConflict();
 }
 
diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h
index 2bfd7e16c..41f2ba9d5 100644
--- a/src/theory/uf/theory_uf.h
+++ b/src/theory/uf/theory_uf.h
@@ -112,17 +112,6 @@ private:
    */
   bool propagateLit(TNode literal);
 
-  /**
-   * Explain why this literal is true by adding assumptions
-   * with proof (if "pf" is non-NULL).
-   */
-  void explain(TNode literal, std::vector<TNode>& assumptions, eq::EqProof* pf);
-
-  /**
-   * Explain a literal, with proof (if "pf" is non-NULL).
-   */
-  Node explain(TNode literal, eq::EqProof* pf);
-
   /** All the function terms that the theory has seen */
   context::CDList<TNode> d_functionsTerms;
 
@@ -202,6 +191,9 @@ private:
   CardinalityExtension* getCardinalityExtension() const { return d_thss.get(); }
 
  private:
+  /** Explain why this literal is true by building an explanation */
+  void explain(TNode literal, Node& exp);
+
   bool areCareDisequal(TNode x, TNode y);
   void addCarePairs(const TNodeTrie* t1,
                     const TNodeTrie* t2,