1 files changed, 0 insertions, 33 deletions
diff --git a/src/proof/array_proof.h b/src/proof/array_proof.h
index 076ba7381..fb25c9433 100644
--- a/src/proof/array_proof.h
+++ b/src/proof/array_proof.h
@@ -30,32 +30,6 @@ namespace CVC4 {
 //proof object outputted by TheoryARRAY
 class ProofArray : public Proof {
 private:
-  class ArrayProofPrinter : public theory::eq::EqProof::PrettyPrinter {
-  public:
-    ArrayProofPrinter() : d_row(0), d_row1(0), d_ext(0) {
-    }
-
-    std::string printTag(unsigned tag) {
-      if (tag == theory::eq::MERGED_THROUGH_CONGRUENCE) return "Congruence";
-      if (tag == theory::eq::MERGED_THROUGH_EQUALITY) return "Pure Equality";
-      if (tag == theory::eq::MERGED_THROUGH_REFLEXIVITY) return "Reflexivity";
-      if (tag == theory::eq::MERGED_THROUGH_CONSTANTS) return "Constants";
-      if (tag == theory::eq::MERGED_THROUGH_TRANS) return "Transitivity";
-
-      if (tag == d_row) return "Read Over Write";
-      if (tag == d_row1) return "Read Over Write (1)";
-      if (tag == d_ext) return "Extensionality";
-
-      std::ostringstream result;
-      result << tag;
-      return result.str();
-    }
-
-    unsigned d_row;
-    unsigned d_row1;
-    unsigned d_ext;
-  };
-
   Node toStreamRecLFSC(std::ostream& out, TheoryProof* tp,
                        theory::eq::EqProof* pf,
                        unsigned tb,
@@ -67,8 +41,6 @@ private:
   unsigned d_reasonRow1;
   /** Merge tag for EXT applications */
   unsigned d_reasonExt;
-
-  ArrayProofPrinter d_proofPrinter;
 public:
   ProofArray(theory::eq::EqProof* pf) : d_proof(pf) {}
   //it is simply an equality engine proof
@@ -81,10 +53,6 @@ public:
   void setRowMergeTag(unsigned tag);
   void setRow1MergeTag(unsigned tag);
   void setExtMergeTag(unsigned tag);
-
-  unsigned getRowMergeTag() const;
-  unsigned getRow1MergeTag() const;
-  unsigned getExtMergeTag() const;
 };
 
 namespace theory {
@@ -123,7 +91,6 @@ public:
   virtual void printSortDeclarations(std::ostream& os, std::ostream& paren);
   virtual void printTermDeclarations(std::ostream& os, std::ostream& paren);
   virtual void printDeferredDeclarations(std::ostream& os, std::ostream& paren);
-  virtual void printAliasingDeclarations(std::ostream& os, std::ostream& paren);
 };