1 files changed, 2 insertions, 17 deletions
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.