From 4dac1ec234ee0d0885f058b4b35a7eeba2ca5007 Mon Sep 17 00:00:00 2001
From: Guy <katz911@gmail.com>
Date: Wed, 1 Jun 2016 17:46:24 -0700
Subject: Merge from proof branch

---
 src/proof/array_proof.h | 33 +++++++++++++++++++++++++++++++++
 1 file changed, 33 insertions(+)

(limited to 'src/proof/array_proof.h')

diff --git a/src/proof/array_proof.h b/src/proof/array_proof.h
index fb25c9433..076ba7381 100644
--- a/src/proof/array_proof.h
+++ b/src/proof/array_proof.h
@@ -30,6 +30,32 @@ 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,
@@ -41,6 +67,8 @@ 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
@@ -53,6 +81,10 @@ public:
   void setRowMergeTag(unsigned tag);
   void setRow1MergeTag(unsigned tag);
   void setExtMergeTag(unsigned tag);
+
+  unsigned getRowMergeTag() const;
+  unsigned getRow1MergeTag() const;
+  unsigned getExtMergeTag() const;
 };
 
 namespace theory {
@@ -91,6 +123,7 @@ 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);
 };
 
 
-- 
cgit v1.2.3