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).

4 files changed, 54 insertions, 405 deletions

diff --git a/src/theory/arrays/array_proof_reconstruction.cpp b/src/theory/arrays/array_proof_reconstruction.cpp
deleted file mode 100644
index abc4857e8..000000000
--- a/src/theory/arrays/array_proof_reconstruction.cpp
+++ /dev/null
@@ -1,199 +0,0 @@
-/*********************                                                        */
-/*! \file array_proof_reconstruction.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Guy Katz, Tim King
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
- ** All rights reserved.  See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** [[ Add lengthier description here ]]
-
- ** \todo document this file
-
-**/
-
-#include "theory/arrays/array_proof_reconstruction.h"
-
-#include <memory>
-
-namespace CVC4 {
-namespace theory {
-namespace arrays {
-
-ArrayProofReconstruction::ArrayProofReconstruction(const eq::EqualityEngine* equalityEngine)
-  : d_equalityEngine(equalityEngine) {
-}
-
-void ArrayProofReconstruction::setRowMergeTag(unsigned tag) {
-  d_reasonRow = tag;
-}
-
-void ArrayProofReconstruction::setRow1MergeTag(unsigned tag) {
-  d_reasonRow1 = tag;
-}
-
-void ArrayProofReconstruction::setExtMergeTag(unsigned tag) {
-  d_reasonExt = tag;
-}
-
-void ArrayProofReconstruction::notify(
-    unsigned reasonType, Node reason, Node a, Node b,
-    std::vector<TNode>& equalities, eq::EqProof* proof) const {
-  Debug("pf::array") << "ArrayProofReconstruction::notify( "
-                     << reason << ", " << a << ", " << b << std::endl;
-
-
-  if (reasonType == d_reasonExt) {
-    if (proof) {
-      // Todo: here we assume that a=b is an assertion. We should probably call
-      // explain() recursively, to explain this.
-      std::shared_ptr<eq::EqProof> childProof = std::make_shared<eq::EqProof>();
-      childProof->d_node = reason;
-      proof->d_children.push_back(childProof);
-    }
-  }
-
-  else if (reasonType == d_reasonRow) {
-    // ROW rules mean that (i==k) OR ((a[i]:=t)[k] == a[k])
-    // The equality here will be either (i == k) because ((a[i]:=t)[k] != a[k]),
-    // or ((a[i]:=t)[k] == a[k]) because (i != k).
-
-    if (proof) {
-      if (a.getKind() == kind::SELECT) {
-        // This is the case of ((a[i]:=t)[k] == a[k]) because (i != k).
-
-        // The edge is ((a[i]:=t)[k], a[k]), or (a[k], (a[i]:=t)[k]). This flag should be
-        // false in the first case and true in the second case.
-        bool currentNodeIsUnchangedArray;
-
-        Assert(a.getNumChildren() == 2);
-        Assert(b.getNumChildren() == 2);
-
-        if (a[0].getKind() == kind::VARIABLE || a[0].getKind() == kind::SKOLEM) {
-          currentNodeIsUnchangedArray = true;
-        } else if (b[0].getKind() == kind::VARIABLE || b[0].getKind() == kind::SKOLEM) {
-          currentNodeIsUnchangedArray = false;
-        } else {
-          Assert(a[0].getKind() == kind::STORE);
-          Assert(b[0].getKind() == kind::STORE);
-
-          if (a[0][0] == b[0]) {
-            currentNodeIsUnchangedArray = false;
-          } else if (b[0][0] == a[0]) {
-            currentNodeIsUnchangedArray = true;
-          } else {
-            Unreachable();
-          }
-        }
-
-        Node indexOne = currentNodeIsUnchangedArray ? a[1] : a[0][1];
-        Node indexTwo = currentNodeIsUnchangedArray ? b[0][1] : b[1];
-
-        // Some assertions to ensure that the theory of arrays behaves as expected
-        Assert(a[1] == b[1]);
-        if (currentNodeIsUnchangedArray) {
-          Assert(a[0] == b[0][0]);
-        } else {
-          Assert(a[0][0] == b[0]);
-        }
-
-        Debug("pf::ee") << "Getting explanation for ROW guard: "
-                        << indexOne << " != " << indexTwo << std::endl;
-
-        std::shared_ptr<eq::EqProof> childProof =
-            std::make_shared<eq::EqProof>();
-        d_equalityEngine->explainEquality(indexOne, indexTwo, false, equalities,
-                                          childProof.get());
-
-        // It could be that the guard condition is a constant disequality. In
-        // this case, we need to change it to a different format.
-        bool haveNegChild = false;
-        for (unsigned i = 0; i < childProof->d_children.size(); ++i) {
-          if (childProof->d_children[i]->d_node.getKind() == kind::NOT)
-            haveNegChild = true;
-        }
-
-        if ((childProof->d_children.size() != 0) &&
-            (childProof->d_id == theory::eq::MERGED_THROUGH_CONSTANTS || !haveNegChild)) {
-          // The proof has two children, explaining why each index is a (different) constant.
-          Assert(childProof->d_children.size() == 2);
-
-          Node constantOne, constantTwo;
-          // Each subproof explains why one of the indices is constant.
-
-          if (childProof->d_children[0]->d_id == theory::eq::MERGED_THROUGH_REFLEXIVITY) {
-            constantOne = childProof->d_children[0]->d_node;
-          } else {
-            Assert(childProof->d_children[0]->d_node.getKind() == kind::EQUAL);
-            if ((childProof->d_children[0]->d_node[0] == indexOne) ||
-                (childProof->d_children[0]->d_node[0] == indexTwo)) {
-              constantOne = childProof->d_children[0]->d_node[1];
-            } else {
-              constantOne = childProof->d_children[0]->d_node[0];
-            }
-          }
-
-          if (childProof->d_children[1]->d_id == theory::eq::MERGED_THROUGH_REFLEXIVITY) {
-            constantTwo = childProof->d_children[1]->d_node;
-          } else {
-            Assert(childProof->d_children[1]->d_node.getKind() == kind::EQUAL);
-            if ((childProof->d_children[1]->d_node[0] == indexOne) ||
-                (childProof->d_children[1]->d_node[0] == indexTwo)) {
-              constantTwo = childProof->d_children[1]->d_node[1];
-            } else {
-              constantTwo = childProof->d_children[1]->d_node[0];
-            }
-          }
-
-          std::shared_ptr<eq::EqProof> constantDisequalityProof =
-              std::make_shared<eq::EqProof>();
-          constantDisequalityProof->d_id = theory::eq::MERGED_THROUGH_CONSTANTS;
-          constantDisequalityProof->d_node =
-            NodeManager::currentNM()->mkNode(kind::EQUAL, constantOne, constantTwo).negate();
-
-          // Middle is where we need to insert the new disequality
-          std::vector<std::shared_ptr<eq::EqProof>>::iterator middle =
-              childProof->d_children.begin();
-          ++middle;
-
-          childProof->d_children.insert(middle, constantDisequalityProof);
-
-          childProof->d_id = theory::eq::MERGED_THROUGH_TRANS;
-          childProof->d_node =
-            NodeManager::currentNM()->mkNode(kind::EQUAL, indexOne, indexTwo).negate();
-        }
-
-        proof->d_children.push_back(childProof);
-      } else {
-        // This is the case of (i == k) because ((a[i]:=t)[k] != a[k]),
-
-        Node indexOne = a;
-        Node indexTwo = b;
-
-        Debug("pf::ee") << "The two indices are: " << indexOne << ", " << indexTwo << std::endl
-                        << "The reason for the edge is: " << reason << std::endl;
-
-        Assert(reason.getNumChildren() == 2);
-        Debug("pf::ee") << "Getting explanation for ROW guard: " << reason[1] << std::endl;
-
-        std::shared_ptr<eq::EqProof> childProof =
-            std::make_shared<eq::EqProof>();
-        d_equalityEngine->explainEquality(reason[1][0], reason[1][1], false,
-                                          equalities, childProof.get());
-        proof->d_children.push_back(childProof);
-      }
-    }
-
-  }
-
-  else if (reasonType == d_reasonRow1) {
-    // No special handling required at this time
-  }
-}
-
-}/* CVC4::theory::arrays namespace */
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
diff --git a/src/theory/arrays/array_proof_reconstruction.h b/src/theory/arrays/array_proof_reconstruction.h
deleted file mode 100644
index a73b5dd08..000000000
--- a/src/theory/arrays/array_proof_reconstruction.h
+++ /dev/null
@@ -1,59 +0,0 @@
-/*********************                                                        */
-/*! \file array_proof_reconstruction.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Paul Meng, Mathias Preiner, Tim King
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
- ** All rights reserved.  See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief Array-specific proof construction logic to be used during the
- ** equality engine's path reconstruction
- **/
-
-#include "cvc4_private.h"
-
-#ifndef CVC4__THEORY__ARRAYS__ARRAY_PROOF_RECONSTRUCTION_H
-#define CVC4__THEORY__ARRAYS__ARRAY_PROOF_RECONSTRUCTION_H
-
-#include "theory/uf/equality_engine.h"
-
-namespace CVC4 {
-namespace theory {
-namespace arrays {
-
-/**
- * A callback class to be invoked whenever the equality engine traverses
- * an "array-owned" edge during path reconstruction.
- */
-
-class ArrayProofReconstruction : public eq::PathReconstructionNotify {
-public:
-  ArrayProofReconstruction(const eq::EqualityEngine* equalityEngine);
-
-  void notify(unsigned reasonType, Node reason, Node a, Node b,
-              std::vector<TNode>& equalities,
-              eq::EqProof* proof) const override;
-
-  void setRowMergeTag(unsigned tag);
-  void setRow1MergeTag(unsigned tag);
-  void setExtMergeTag(unsigned tag);
-
-private:
-  /** Merge tag for ROW applications */
-  unsigned d_reasonRow;
-  /** Merge tag for ROW1 applications */
-  unsigned d_reasonRow1;
-  /** Merge tag for EXT applications */
-  unsigned d_reasonExt;
-
-  const eq::EqualityEngine* d_equalityEngine;
-}; /* class ArrayProofReconstruction */
-
-}/* CVC4::theory::arrays namespace */
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
-
-#endif /* CVC4__THEORY__ARRAYS__ARRAY_PROOF_RECONSTRUCTION_H */
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index 3adcd4f49..603dc9639 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -23,9 +23,6 @@
 #include "expr/node_algorithm.h"
 #include "options/arrays_options.h"
 #include "options/smt_options.h"
-#include "proof/array_proof.h"
-#include "proof/proof_manager.h"
-#include "proof/theory_proof.h"
 #include "smt/command.h"
 #include "smt/logic_exception.h"
 #include "smt/smt_statistics_registry.h"
@@ -111,7 +108,6 @@ TheoryArrays::TheoryArrays(context::Context* c,
       d_readTableContext(new context::Context()),
       d_arrayMerges(c),
       d_inCheckModel(false),
-      d_proofReconstruction(nullptr),
       d_dstrat(new TheoryArraysDecisionStrategy(this)),
       d_dstratInit(false)
 {
@@ -183,22 +179,6 @@ void TheoryArrays::finishInit()
   {
     d_equalityEngine->addFunctionKind(kind::ARR_TABLE_FUN);
   }
-
-  d_proofReconstruction.reset(new ArrayProofReconstruction(d_equalityEngine));
-  d_reasonRow = d_equalityEngine->getFreshMergeReasonType();
-  d_reasonRow1 = d_equalityEngine->getFreshMergeReasonType();
-  d_reasonExt = d_equalityEngine->getFreshMergeReasonType();
-
-  d_proofReconstruction->setRowMergeTag(d_reasonRow);
-  d_proofReconstruction->setRow1MergeTag(d_reasonRow1);
-  d_proofReconstruction->setExtMergeTag(d_reasonExt);
-
-  d_equalityEngine->addPathReconstructionTrigger(d_reasonRow,
-                                                 d_proofReconstruction.get());
-  d_equalityEngine->addPathReconstructionTrigger(d_reasonRow1,
-                                                 d_proofReconstruction.get());
-  d_equalityEngine->addPathReconstructionTrigger(d_reasonExt,
-                                                 d_proofReconstruction.get());
 }
 
 /////////////////////////////////////////////////////////////////////////////
@@ -440,37 +420,6 @@ bool TheoryArrays::propagateLit(TNode literal)
 }/* TheoryArrays::propagate(TNode) */
 
 
-void TheoryArrays::explain(TNode literal, std::vector<TNode>& assumptions,
-                           eq::EqProof* proof) {
-  // Do the work
-  bool polarity = literal.getKind() != kind::NOT;
-  TNode atom = polarity ? literal : literal[0];
-  //eq::EqProof * eqp = new eq::EqProof;
-  // eq::EqProof * eqp = NULL;
-  if (atom.getKind() == kind::EQUAL) {
-    d_equalityEngine->explainEquality(
-        atom[0], atom[1], polarity, assumptions, proof);
-  } else {
-    d_equalityEngine->explainPredicate(atom, polarity, assumptions, proof);
-  }
-  if (Debug.isOn("pf::array"))
-  {
-    if (proof)
-    {
-      Debug("pf::array") << " Proof is : " << std::endl;
-      proof->debug_print("pf::array");
-    }
-
-    Debug("pf::array") << "Array: explain( " << literal << " ):" << std::endl
-                       << "\t";
-    for (unsigned i = 0; i < assumptions.size(); ++i)
-    {
-      Debug("pf::array") << assumptions[i] << " ";
-    }
-    Debug("pf::array") << std::endl;
-  }
-}
-
 TNode TheoryArrays::weakEquivGetRep(TNode node) {
   TNode pointer;
   while (true) {
@@ -795,7 +744,8 @@ void TheoryArrays::preRegisterTermInternal(TNode node)
     }
 
     // Apply RIntro1 Rule
-    d_equalityEngine->assertEquality(ni.eqNode(v), true, d_true, d_reasonRow1);
+    d_equalityEngine->assertEquality(
+        ni.eqNode(v), true, d_true, theory::eq::MERGED_THROUGH_ROW1);
 
     d_infoMap.addStore(node, node);
     d_infoMap.addInStore(a, node);
@@ -864,19 +814,32 @@ void TheoryArrays::preRegisterTerm(TNode node)
   }
 }
 
-TrustNode TheoryArrays::explain(TNode literal)
+void TheoryArrays::explain(TNode literal, Node& explanation)
 {
-  Node explanation = explain(literal, NULL);
-  return TrustNode::mkTrustPropExp(literal, explanation, nullptr);
-}
-
-Node TheoryArrays::explain(TNode literal, eq::EqProof* proof) {
   ++d_numExplain;
   Debug("arrays") << spaces(getSatContext()->getLevel())
                   << "TheoryArrays::explain(" << literal << ")" << std::endl;
   std::vector<TNode> assumptions;
-  explain(literal, assumptions, proof);
-  return mkAnd(assumptions);
+  // Do the work
+  bool polarity = literal.getKind() != kind::NOT;
+  TNode atom = polarity ? literal : literal[0];
+  if (atom.getKind() == kind::EQUAL)
+  {
+    d_equalityEngine->explainEquality(
+        atom[0], atom[1], polarity, assumptions, nullptr);
+  }
+  else
+  {
+    d_equalityEngine->explainPredicate(atom, polarity, assumptions, nullptr);
+  }
+  explanation = mkAnd(assumptions);
+}
+
+TrustNode TheoryArrays::explain(TNode literal)
+{
+  Node explanation;
+  explain(literal, explanation);
+  return TrustNode::mkTrustPropExp(literal, explanation, nullptr);
 }
 
 /////////////////////////////////////////////////////////////////////////////
@@ -1329,49 +1292,20 @@ void TheoryArrays::check(Effort e) {
 
             TNode k;
             // k is the skolem for this disequality.
-            if (!d_proofsEnabled) {
-              Debug("pf::array") << "Check: kind::NOT: array theory making a skolem" << std::endl;
-
-              // If not in replay mode, generate a fresh skolem variable
-              k = getSkolem(fact,
-                            "array_ext_index",
-                            indexType,
-                            "an extensional lemma index variable from the theory of arrays",
-                            false);
-
-              // Register this skolem for the proof replay phase
-              PROOF(ProofManager::getSkolemizationManager()->registerSkolem(fact, k));
-            } else {
-              if (!ProofManager::getSkolemizationManager()->hasSkolem(fact)) {
-                // In the solution pass we didn't need this skolem. Therefore, we don't need it
-                // in this reply pass, either.
-                break;
-              }
-
-              // Reuse the same skolem as in the solution pass
-              k = ProofManager::getSkolemizationManager()->getSkolem(fact);
-              Debug("pf::array") << "Skolem = " << k << std::endl;
-            }
-
+            Debug("pf::array")
+                << "Check: kind::NOT: array theory making a skolem"
+                << std::endl;
+            k = getSkolem(
+                fact,
+                "array_ext_index",
+                indexType,
+                "an extensional lemma index variable from the theory of arrays",
+                false);
             Node ak = nm->mkNode(kind::SELECT, fact[0][0], k);
             Node bk = nm->mkNode(kind::SELECT, fact[0][1], k);
             Node eq = ak.eqNode(bk);
             Node lemma = fact[0].orNode(eq.notNode());
 
-            // In solve mode we don't care if ak and bk are registered. If they aren't, they'll be registered
-            // when we output the lemma. However, in replay need the lemma to be propagated, and so we
-            // preregister manually.
-            if (d_proofsEnabled) {
-              if (!d_equalityEngine->hasTerm(ak))
-              {
-                preRegisterTermInternal(ak);
-              }
-              if (!d_equalityEngine->hasTerm(bk))
-              {
-                preRegisterTermInternal(bk);
-              }
-            }
-
             if (options::arraysPropagate() > 0 && d_equalityEngine->hasTerm(ak)
                 && d_equalityEngine->hasTerm(bk))
             {
@@ -1381,17 +1315,16 @@ void TheoryArrays::check(Effort e) {
                                  << "\teq = " << eq << std::endl
                                  << "\treason = " << fact << std::endl;
 
-              d_equalityEngine->assertEquality(eq, false, fact, d_reasonExt);
+              d_equalityEngine->assertEquality(
+                  eq, false, fact, theory::eq::MERGED_THROUGH_EXT);
               ++d_numProp;
             }
 
-            if (!d_proofsEnabled) {
-              // If this is the solution pass, generate the lemma. Otherwise, don't generate it -
-              // as this is the lemma that we're reproving...
-              Trace("arrays-lem")<<"Arrays::addExtLemma " << lemma <<"\n";
-              d_out->lemma(lemma);
-              ++d_numExt;
-            }
+            // If this is the solution pass, generate the lemma. Otherwise,
+            // don't generate it - as this is the lemma that we're reproving...
+            Trace("arrays-lem") << "Arrays::addExtLemma " << lemma << "\n";
+            d_out->lemma(lemma);
+            ++d_numExt;
           } else {
             Debug("pf::array") << "Check: kind::NOT: array theory NOT making a skolem" << std::endl;
             d_modelConstraints.push_back(fact);
@@ -1480,7 +1413,7 @@ void TheoryArrays::check(Effort e) {
           lemma = mkAnd(conjunctions, true);
           // LSH FIXME: which kind of arrays lemma is this
           Trace("arrays-lem") << "Arrays::addExtLemma " << lemma <<"\n";
-          d_out->lemma(lemma, RULE_INVALID, LemmaProperty::SEND_ATOMS);
+          d_out->lemma(lemma, LemmaProperty::SEND_ATOMS);
           d_readTableContext->pop();
           Trace("arrays") << spaces(getSatContext()->getLevel()) << "Arrays::check(): done" << endl;
           return;
@@ -1908,7 +1841,8 @@ void TheoryArrays::propagate(RowLemmaType lem)
       if (!bjExists) {
         preRegisterTermInternal(bj);
       }
-      d_equalityEngine->assertEquality(aj_eq_bj, true, reason, d_reasonRow);
+      d_equalityEngine->assertEquality(
+          aj_eq_bj, true, reason, theory::eq::MERGED_THROUGH_ROW);
       ++d_numProp;
       return;
     }
@@ -1919,7 +1853,8 @@ void TheoryArrays::propagate(RowLemmaType lem)
           (aj.isConst() && bj.isConst()) ? d_true : aj.eqNode(bj).notNode();
       Node i_eq_j = i.eqNode(j);
       d_permRef.push_back(reason);
-      d_equalityEngine->assertEquality(i_eq_j, true, reason, d_reasonRow);
+      d_equalityEngine->assertEquality(
+          i_eq_j, true, reason, theory::eq::MERGED_THROUGH_ROW);
       ++d_numProp;
       return;
     }
@@ -1971,19 +1906,18 @@ void TheoryArrays::queueRowLemma(RowLemmaType lem)
       && !d_equalityEngine->areDisequal(i, j, false))
   {
     Node i_eq_j;
-    if (!d_proofsEnabled) {
-      i_eq_j = d_valuation.ensureLiteral(i.eqNode(j)); // TODO: think about this
-    } else {
-      i_eq_j = i.eqNode(j);
-    }
-
+    i_eq_j = d_valuation.ensureLiteral(i.eqNode(j));  // TODO: think about this
+#if 0
+    i_eq_j = i.eqNode(j);
+#endif
     getOutputChannel().requirePhase(i_eq_j, true);
     d_decisionRequests.push(i_eq_j);
   }
 
   // TODO: maybe add triggers here
 
-  if ((options::arraysEagerLemmas() || bothExist) && !d_proofsEnabled) {
+  if (options::arraysEagerLemmas() || bothExist)
+  {
     // Make sure that any terms introduced by rewriting are appropriately stored in the equality database
     Node aj2 = Rewriter::rewrite(aj);
     if (aj != aj2) {
@@ -2162,23 +2096,11 @@ bool TheoryArrays::dischargeLemmas()
 
 void TheoryArrays::conflict(TNode a, TNode b) {
   Debug("pf::array") << "TheoryArrays::Conflict called" << std::endl;
-  std::shared_ptr<eq::EqProof> proof = d_proofsEnabled ?
-      std::make_shared<eq::EqProof>() : nullptr;
 
-  d_conflictNode = explain(a.eqNode(b), proof.get());
+  explain(a.eqNode(b), d_conflictNode);
 
   if (!d_inCheckModel) {
-    std::unique_ptr<ProofArray> proof_array;
-
-    if (d_proofsEnabled) {
-      proof->debug_print("pf::array");
-      proof_array.reset(new ProofArray(proof,
-                                       /*row=*/d_reasonRow,
-                                       /*row1=*/d_reasonRow1,
-                                       /*ext=*/d_reasonExt));
-    }
-
-    d_out->conflict(d_conflictNode, std::move(proof_array));
+    d_out->conflict(d_conflictNode);
   }
 
   d_conflict = true;
diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h
index 9044b9950..8fdbde0ab 100644
--- a/src/theory/arrays/theory_arrays.h
+++ b/src/theory/arrays/theory_arrays.h
@@ -26,7 +26,6 @@
 #include "context/cdhashset.h"
 #include "context/cdqueue.h"
 #include "theory/arrays/array_info.h"
-#include "theory/arrays/array_proof_reconstruction.h"
 #include "theory/arrays/theory_arrays_rewriter.h"
 #include "theory/theory.h"
 #include "theory/uf/equality_engine.h"
@@ -129,15 +128,6 @@ class TheoryArrays : public Theory {
   /** conflicts in setModelVal */
   IntStat d_numSetModelValConflicts;
 
-  // Merge reason types
-
-  /** Merge tag for ROW applications */
-  unsigned d_reasonRow;
-  /** Merge tag for ROW1 applications */
-  unsigned d_reasonRow1;
-  /** Merge tag for EXT applications */
-  unsigned d_reasonExt;
-
  public:
   TheoryArrays(context::Context* c,
                context::UserContext* u,
@@ -215,9 +205,8 @@ class TheoryArrays : public Theory {
   /** Should be called to propagate the literal.  */
   bool propagateLit(TNode literal);
 
-  /** Explain why this literal is true by adding assumptions */
-  void explain(TNode literal, std::vector<TNode>& assumptions,
-               eq::EqProof* proof);
+  /** Explain why this literal is true by building an explanation */
+  void explain(TNode literal, Node& exp);
 
   /** For debugging only- checks invariants about when things are preregistered*/
   context::CDHashSet<Node, NodeHashFunction > d_isPreRegistered;
@@ -227,7 +216,6 @@ class TheoryArrays : public Theory {
 
  public:
   void preRegisterTerm(TNode n) override;
-  Node explain(TNode n, eq::EqProof* proof);
   TrustNode explain(TNode n) override;
 
   /////////////////////////////////////////////////////////////////////////////
@@ -446,9 +434,6 @@ class TheoryArrays : public Theory {
   bool d_inCheckModel;
   int d_topLevel;
 
-  /** An equality-engine callback for proof reconstruction */
-  std::unique_ptr<ArrayProofReconstruction> d_proofReconstruction;
-
   /**
    * The decision strategy for the theory of arrays, which calls the
    * getNextDecisionEngineRequest function below.