Made ProofArray's printing functions non-static, and consequently the data members...

diff --git a/src/proof/array_proof.cpp b/src/proof/array_proof.cpp
index 4a292fc9285eb5fcd47056c6484c8ed416c062c8..017a17cbe3419dc65ce69a3e7965e2f4398f0b50 100644 (file)
--- a/src/proof/array_proof.cpp
+++ b/src/proof/array_proof.cpp
@@ -23,10 +23,6 @@
 
 namespace CVC4 {
 
-unsigned ProofArray::s_reasonRow;
-unsigned ProofArray::s_reasonRow1;
-unsigned ProofArray::s_reasonExt;
-
 inline static Node eqNode(TNode n1, TNode n2) {
   return NodeManager::currentNM()->mkNode(n1.getType().isBoolean() ? kind::IFF : kind::EQUAL, n1, n2);
 }
@@ -84,15 +80,15 @@ inline static bool match(TNode n1, TNode n2) {
 }
 
 void ProofArray::setRowMergeTag(unsigned tag) {
-  s_reasonRow = tag;
+  d_reasonRow = tag;
 }
 
 void ProofArray::setRow1MergeTag(unsigned tag) {
-  s_reasonRow1 = tag;
+  d_reasonRow1 = tag;
 }
 
 void ProofArray::setExtMergeTag(unsigned tag) {
-  s_reasonExt = tag;
+  d_reasonExt = tag;
 }
 
 void ProofArray::toStream(std::ostream& out) {
@@ -247,7 +243,7 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out,
     if (n2[0].getNumChildren() > 0) { Debug("mgdx") << "\nn2[0]: " << n2[0][0] << std::endl; }
     if (n1.getNumChildren() > 1) { Debug("mgdx") << "n1[1]: " << n1[1] << std::endl; }
 
-    if (pf->d_children[neg]->d_id == s_reasonExt) {
+    if (pf->d_children[neg]->d_id == d_reasonExt) {
       // The negative node was created by an EXT rule; e.g. it is a[k]!=b[k], due to a!=b.
 
       //           (clausify_false (contra _ .gl2 (or_elim_1 _ _ .gl1 FIXME))))))) (\ .glemc6
@@ -824,7 +820,7 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out,
     return n1;
   }
 
-  else if (pf->d_id == s_reasonRow) {
+  else if (pf->d_id == d_reasonRow) {
     Debug("mgd") << "row lemma: " << pf->d_node << std::endl;
     Assert(pf->d_node.getKind() == kind::EQUAL);
 
@@ -970,7 +966,7 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out,
     }
   }
 
-  else if (pf->d_id == s_reasonRow1) {
+  else if (pf->d_id == d_reasonRow1) {
     Debug("mgd") << "row1 lemma: " << pf->d_node << std::endl;
     Assert(pf->d_node.getKind() == kind::EQUAL);
     TNode t1, t2, t3;
@@ -1005,7 +1001,7 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out,
     return ret;
   }
 
-  else if (pf->d_id == s_reasonExt) {
+  else if (pf->d_id == d_reasonExt) {
     theory::eq::EqProof *child_proof;
 
     Assert(pf->d_node.getKind() == kind::NOT);

diff --git a/src/proof/array_proof.h b/src/proof/array_proof.h
index af980bc439bab1060e55eb148d921806d34bf3e9..5792bd272710d5a6462056a3f100c20fec71b35d 100644 (file)
--- a/src/proof/array_proof.h
+++ b/src/proof/array_proof.h
@@ -30,29 +30,29 @@ namespace CVC4 {
 //proof object outputted by TheoryARRAY
 class ProofArray : public Proof {
 private:
-  static Node toStreamRecLFSC(std::ostream& out, TheoryProof* tp,
-                              theory::eq::EqProof* pf,
-                              unsigned tb,
-                              const LetMap& map);
+  Node toStreamRecLFSC(std::ostream& out, TheoryProof* tp,
+                       theory::eq::EqProof* pf,
+                       unsigned tb,
+                       const LetMap& map);
 
   /** Merge tag for ROW applications */
-  static unsigned s_reasonRow;
+  unsigned d_reasonRow;
   /** Merge tag for ROW1 applications */
-  static unsigned s_reasonRow1;
+  unsigned d_reasonRow1;
   /** Merge tag for EXT applications */
-  static unsigned s_reasonExt;
+  unsigned d_reasonExt;
 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);
-  static void toStreamLFSC(std::ostream& out, TheoryProof* tp, theory::eq::EqProof* pf, const LetMap& map);
+  void toStreamLFSC(std::ostream& out, TheoryProof* tp, theory::eq::EqProof* pf, const LetMap& map);
 
   void registerSkolem(Node equality, Node skolem);
 
-  static void setRowMergeTag(unsigned tag);
-  static void setRow1MergeTag(unsigned tag);
-  static void setExtMergeTag(unsigned tag);
+  void setRowMergeTag(unsigned tag);
+  void setRow1MergeTag(unsigned tag);
+  void setExtMergeTag(unsigned tag);
 };
 
 namespace theory {