Cleaning up ProofArray class. (#1208)

3 files changed, 71 insertions, 90 deletions

diff --git a/src/proof/array_proof.cpp b/src/proof/array_proof.cpp
index e5b7e64e5..fab9a896d 100644
--- a/src/proof/array_proof.cpp
+++ b/src/proof/array_proof.cpp
@@ -16,14 +16,49 @@
 **/
 
 #include "proof/array_proof.h"
+
+#include <stack>
+
 #include "proof/proof_manager.h"
 #include "proof/simplify_boolean_node.h"
 #include "proof/theory_proof.h"
 #include "theory/arrays/theory_arrays.h"
-#include <stack>
 
 namespace CVC4 {
 
+namespace {
+
+class ArrayProofPrinter : public theory::eq::EqProof::PrettyPrinter {
+ public:
+  ArrayProofPrinter(unsigned row, unsigned row1, unsigned ext)
+      : d_row(row), d_row1(row1), d_ext(ext) {}
+
+  std::string printTag(unsigned tag) override;
+
+ private:
+  const unsigned d_row;
+  const unsigned d_row1;
+  const unsigned d_ext;
+};  // class ArrayProofPrinter
+
+std::string ArrayProofPrinter::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();
+}
+
+}  // namespace
+
 inline static Node eqNode(TNode n1, TNode n2) {
   return NodeManager::currentNM()->mkNode(kind::EQUAL, n1, n2);
 }
@@ -80,32 +115,9 @@ inline static bool match(TNode n1, TNode n2) {
   return true;
 }
 
-void ProofArray::setRowMergeTag(unsigned tag) {
-  d_reasonRow = tag;
-  d_proofPrinter.d_row = tag;
-}
-
-void ProofArray::setRow1MergeTag(unsigned tag) {
-  d_reasonRow1 = tag;
-  d_proofPrinter.d_row1 = tag;
-}
-
-void ProofArray::setExtMergeTag(unsigned tag) {
-  d_reasonExt = tag;
-  d_proofPrinter.d_ext = tag;
-}
-
-unsigned ProofArray::getRowMergeTag() const {
-  return d_reasonRow;
-}
-
-unsigned ProofArray::getRow1MergeTag() const {
-  return d_reasonRow1;
-}
-
-unsigned ProofArray::getExtMergeTag() const {
-  return d_reasonExt;
-}
+ProofArray::ProofArray(theory::eq::EqProof* pf, unsigned row, unsigned row1,
+                       unsigned ext)
+    : d_proof(pf), d_reasonRow(row), d_reasonRow1(row1), d_reasonExt(ext) {}
 
 void ProofArray::toStream(std::ostream& out) {
   ProofLetMap map;
@@ -118,11 +130,13 @@ void ProofArray::toStream(std::ostream& out, const ProofLetMap& map) {
   Debug("pf::array") << "; Print Array proof done!" << std::endl;
 }
 
-void ProofArray::toStreamLFSC(std::ostream& out, TheoryProof* tp, theory::eq::EqProof* pf, const ProofLetMap& map) {
+void ProofArray::toStreamLFSC(std::ostream& out, TheoryProof* tp,
+                              theory::eq::EqProof* pf, const ProofLetMap& map) {
   Debug("pf::array") << "Printing array proof in LFSC : " << std::endl;
-  pf->debug_print("pf::array", 0, &d_proofPrinter);
+  ArrayProofPrinter proofPrinter(d_reasonRow, d_reasonRow1, d_reasonExt);
+  pf->debug_print("pf::array", 0, &proofPrinter);
   Debug("pf::array") << std::endl;
-  toStreamRecLFSC( out, tp, pf, 0, map );
+  toStreamRecLFSC(out, tp, pf, 0, map);
   Debug("pf::array") << "Printing array proof in LFSC DONE" << std::endl;
 }
 
@@ -133,7 +147,8 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out,
                                  const ProofLetMap& map) {
 
   Debug("pf::array") << std::endl << std::endl << "toStreamRecLFSC called. tb = " << tb << " . proof:" << std::endl;
-  pf->debug_print("pf::array", 0, &d_proofPrinter);
+  ArrayProofPrinter proofPrinter(d_reasonRow, d_reasonRow1, d_reasonExt);
+  pf->debug_print("pf::array", 0, &proofPrinter);
   Debug("pf::array") << std::endl;
 
   if(tb == 0) {
@@ -172,8 +187,8 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out,
                pf->d_children[i + count]->d_node.isNull();
              ++count) {
           Debug("pf::array") << "Found a congruence: " << std::endl;
-          pf->d_children[i+count]->debug_print("pf::array", 0, &d_proofPrinter);
-          congruenceClosures.push_back(pf->d_children[i+count]);
+          pf->d_children[i + count]->debug_print("pf::array", 0, &proofPrinter);
+          congruenceClosures.push_back(pf->d_children[i + count]);
         }
 
         Debug("pf::array") << "Total number of congruences found: " << congruenceClosures.size() << std::endl;
@@ -319,7 +334,7 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out,
 
   if (pf->d_id == theory::eq::MERGED_THROUGH_CONGRUENCE) {
     Debug("mgd") << "\nok, looking at congruence:\n";
-    pf->debug_print("mgd", 0, &d_proofPrinter);
+    pf->debug_print("mgd", 0, &proofPrinter);
     std::stack<const theory::eq::EqProof*> stk;
     for(const theory::eq::EqProof* pf2 = pf; pf2->d_id == theory::eq::MERGED_THROUGH_CONGRUENCE; pf2 = pf2->d_children[0]) {
       Debug("mgd") << "Looking at pf2 with d_node: " << pf2->d_node << std::endl;
@@ -351,7 +366,7 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out,
 
 
     Debug("mgd") << "\nok, in FIRST cong[" << stk.size() << "]" << "\n";
-    pf2->debug_print("mgd", 0, &d_proofPrinter);
+    pf2->debug_print("mgd", 0, &proofPrinter);
     // Temp
     Debug("mgd") << "n1 is a proof for: " << pf2->d_children[0]->d_node << ". It is: " << n1 << std::endl;
     Debug("mgd") << "n2 is a proof for: " << pf2->d_children[1]->d_node << ". It is: " << n2 << std::endl;
@@ -368,7 +383,7 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out,
       Debug("mgd") << "SIDE IS 1\n";
       if(!match(pf2->d_node, n1[1])) {
         Debug("mgd") << "IN BAD CASE, our first subproof is\n";
-        pf2->d_children[0]->debug_print("mgd", 0, &d_proofPrinter);
+        pf2->d_children[0]->debug_print("mgd", 0, &proofPrinter);
       }
       Assert(match(pf2->d_node, n1[1]));
       side = 1;
@@ -605,7 +620,7 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out,
     Assert(pf->d_children.size() >= 2);
     std::stringstream ss;
     Debug("mgd") << "\ndoing trans proof[[\n";
-    pf->debug_print("mgd", 0, &d_proofPrinter);
+    pf->debug_print("mgd", 0, &proofPrinter);
     Debug("mgd") << "\n";
 
     pf->d_children[0]->d_node = simplifyBooleanNode(pf->d_children[0]->d_node);
@@ -832,7 +847,7 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out,
           Warning() << "\n\ntrans proof failure at step " << i << "\n\n";
           Warning() << "0 proves " << n1 << "\n";
           Warning() << "1 proves " << n2 << "\n\n";
-          pf->debug_print("mgdx", 0, &d_proofPrinter);
+          pf->debug_print("mgdx", 0, &proofPrinter);
           //toStreamRec(Warning.getStream(), pf, 0);
           Warning() << "\n\n";
           Unreachable();
diff --git a/src/proof/array_proof.h b/src/proof/array_proof.h
index 9a2eef9e7..f40f13ea6 100644
--- a/src/proof/array_proof.h
+++ b/src/proof/array_proof.h
@@ -29,65 +29,33 @@
 
 namespace CVC4 {
 
-//proof object outputted by TheoryARRAY
+// 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;
-  };
+ public:
+  ProofArray(theory::eq::EqProof* pf, unsigned row, unsigned row1,
+             unsigned ext);
 
+  void registerSkolem(Node equality, Node skolem);
+
+  void toStream(std::ostream& out);
+  void toStream(std::ostream& out, const ProofLetMap& map);
+  void toStreamLFSC(std::ostream& out, TheoryProof* tp, theory::eq::EqProof* pf,
+                    const ProofLetMap& map);
+
+ private:
   Node toStreamRecLFSC(std::ostream& out, TheoryProof* tp,
-                       theory::eq::EqProof* pf,
-                       unsigned tb,
+                       theory::eq::EqProof* pf, unsigned tb,
                        const ProofLetMap& map);
 
+  // it is simply an equality engine proof
+  theory::eq::EqProof* d_proof;
+
   /** Merge tag for ROW applications */
   unsigned d_reasonRow;
   /** Merge tag for ROW1 applications */
   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
-  theory::eq::EqProof *d_proof;
-  void toStream(std::ostream& out);
-  void toStream(std::ostream& out, const ProofLetMap& map);
-  void toStreamLFSC(std::ostream& out, TheoryProof* tp, theory::eq::EqProof* pf, const ProofLetMap& map);
-
-  void registerSkolem(Node equality, Node skolem);
-
-  void setRowMergeTag(unsigned tag);
-  void setRow1MergeTag(unsigned tag);
-  void setExtMergeTag(unsigned tag);
-
-  unsigned getRowMergeTag() const;
-  unsigned getRow1MergeTag() const;
-  unsigned getExtMergeTag() const;
 };
 
 namespace theory {
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index 2f5a9a14f..a17f506de 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -2247,10 +2247,8 @@ void TheoryArrays::conflict(TNode a, TNode b) {
 
     if (d_proofsEnabled) {
       proof->debug_print("pf::array");
-      proof_array = new ProofArray( proof );
-      proof_array->setRowMergeTag(d_reasonRow);
-      proof_array->setRow1MergeTag(d_reasonRow1);
-      proof_array->setExtMergeTag(d_reasonExt);
+      proof_array = new ProofArray(proof, /*row=*/d_reasonRow,
+                                   /*row1=*/d_reasonRow1, /*ext=*/d_reasonExt);
     }
 
     d_out->conflict(d_conflictNode, proof_array);