Removed the theory-specific merge reason types. Instead, added a mechanism for dynamically allocating these tags upon request.

3 files changed, 78 insertions, 134 deletions

diff --git a/src/proof/array_proof.cpp b/src/proof/array_proof.cpp
index 764028c6b..aa615f90e 100644
--- a/src/proof/array_proof.cpp
+++ b/src/proof/array_proof.cpp
@@ -23,6 +23,10 @@
 
 namespace CVC4 {
 
+unsigned ProofArray::d_reasonRow;
+unsigned ProofArray::d_reasonRow1;
+unsigned ProofArray::d_reasonExt;
+
 inline static Node eqNode(TNode n1, TNode n2) {
   return NodeManager::currentNM()->mkNode(n1.getType().isBoolean() ? kind::IFF : kind::EQUAL, n1, n2);
 }
@@ -79,6 +83,18 @@ inline static bool match(TNode n1, TNode n2) {
   return true;
 }
 
+void ProofArray::setRowMergeTag(unsigned tag) {
+  d_reasonRow = tag;
+}
+
+void ProofArray::setRow1MergeTag(unsigned tag) {
+  d_reasonRow1 = tag;
+}
+
+void ProofArray::setExtMergeTag(unsigned tag) {
+  d_reasonExt = tag;
+}
+
 void ProofArray::toStream(std::ostream& out) {
   Trace("pf::array") << "; Print Array proof..." << std::endl;
   //AJR : carry this further?
@@ -95,16 +111,16 @@ void ProofArray::toStreamLFSC(std::ostream& out, TheoryProof* tp, theory::eq::Eq
   Debug("pf::array") << "Printing array proof in LFSC DONE" << std::endl;
 }
 
-void ProofArray::registerSkolem(Node equality, Node skolem) {
-  d_nodeToSkolem[equality] = skolem;
-}
-
 Node ProofArray::toStreamRecLFSC(std::ostream& out,
                                  TheoryProof* tp,
                                  theory::eq::EqProof* pf,
                                  unsigned tb,
                                  const LetMap& map) {
 
+  Debug("gk::temp") << "d_reasonExt = " << d_reasonExt << std::endl;
+  Debug("gk::temp") << "d_reasonRow = " << d_reasonRow << std::endl;
+  Debug("gk::temp") << "d_reasonRow1 = " << d_reasonRow1 << std::endl;
+
   Debug("pf::array") << std::endl << std::endl << "toStreamRecLFSC called. tb = " << tb << " . proof:" << std::endl;
   pf->debug_print("pf::array");
   Debug("pf::array") << std::endl;
@@ -138,8 +154,8 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out,
         Debug("pf::array") << "Collecting congruence sequence" << std::endl;
         for (count = 0;
              i + count < pf->d_children.size() &&
-             pf->d_children[i + count]->d_id==theory::eq::MERGED_THROUGH_CONGRUENCE &&
-             pf->d_children[i + count]->d_node.isNull();
+               pf->d_children[i + count]->d_id==theory::eq::MERGED_THROUGH_CONGRUENCE &&
+               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");
@@ -235,7 +251,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 == theory::eq::MERGED_ARRAYS_EXT) {
+    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
@@ -275,8 +291,7 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out,
     return Node();
   }
 
-  switch(pf->d_id) {
-  case theory::eq::MERGED_THROUGH_CONGRUENCE: {
+  if (pf->d_id == theory::eq::MERGED_THROUGH_CONGRUENCE) {
     Debug("mgd") << "\nok, looking at congruence:\n";
     pf->debug_print("mgd");
     std::stack<const theory::eq::EqProof*> stk;
@@ -324,8 +339,8 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out,
     } else {
       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");
+        Debug("mgd") << "IN BAD CASE, our first subproof is\n";
+        pf2->d_children[0]->debug_print("mgd");
       }
       Assert(match(pf2->d_node, n1[1]));
       side = 1;
@@ -370,7 +385,7 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out,
         b2 << kind::PARTIAL_APPLY_UF;
         b2 << ProofManager::currentPM()->mkOp(n1[1-side].getOperator());
       }
-        b2.append(n1[1-side].begin(), n1[1-side].end());
+      b2.append(n1[1-side].begin(), n1[1-side].end());
     } else if (n1[1-side].getKind() == kind::PARTIAL_SELECT_0) {
       b2 << kind::PARTIAL_SELECT_1;
     } else {
@@ -464,13 +479,13 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out,
       b1.append(n1.begin(), n1.end());
       n1 = b1;
       Debug("mgd") << "New n1: " << n1 << std::endl;
-    // } else if (n1.getKind() == kind::PARTIAL_SELECT_0 && n1.getNumChildren() == 1) {
-    //   Debug("mgd") << "Finished a PARTIAL_SELECT_1. Updating.." << std::endl;
-    //   b1.clear(kind::PARTIAL_SELECT_1);
-    //   b1.append(n1.begin(), n1.end());
-    //   n1 = b1;
-    //   Debug("mgd") << "New n1: " << n1 << std::endl;
-    // } else
+      // } else if (n1.getKind() == kind::PARTIAL_SELECT_0 && n1.getNumChildren() == 1) {
+      //   Debug("mgd") << "Finished a PARTIAL_SELECT_1. Updating.." << std::endl;
+      //   b1.clear(kind::PARTIAL_SELECT_1);
+      //   b1.append(n1.begin(), n1.end());
+      //   n1 = b1;
+      //   Debug("mgd") << "New n1: " << n1 << std::endl;
+      // } else
     } else if(n1.getOperator().getType().getNumChildren() == n1.getNumChildren() + 1) {
       if(ProofManager::currentPM()->hasOp(n1.getOperator())) {
         b1.clear(ProofManager::currentPM()->lookupOp(n2.getOperator()).getConst<Kind>());
@@ -498,13 +513,13 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out,
       b2.append(n2.begin(), n2.end());
       n2 = b2;
       Debug("mgd") << "New n2: " << n2 << std::endl;
-    // } else if (n2.getKind() == kind::PARTIAL_SELECT_0 && n2.getNumChildren() == 1) {
-    //   Debug("mgd") << "Finished a PARTIAL_SELECT_1. Updating.." << std::endl;
-    //   b2.clear(kind::PARTIAL_SELECT_1);
-    //   b2.append(n2.begin(), n2.end());
-    //   n2 = b2;
-    //   Debug("mgd") << "New n2: " << n2 << std::endl;
-    // } else
+      // } else if (n2.getKind() == kind::PARTIAL_SELECT_0 && n2.getNumChildren() == 1) {
+      //   Debug("mgd") << "Finished a PARTIAL_SELECT_1. Updating.." << std::endl;
+      //   b2.clear(kind::PARTIAL_SELECT_1);
+      //   b2.append(n2.begin(), n2.end());
+      //   n2 = b2;
+      //   Debug("mgd") << "New n2: " << n2 << std::endl;
+      // } else
     } else if(n2.getOperator().getType().getNumChildren() == n2.getNumChildren() + 1) {
       if(ProofManager::currentPM()->hasOp(n2.getOperator())) {
         b2.clear(ProofManager::currentPM()->lookupOp(n2.getOperator()).getConst<Kind>());
@@ -521,23 +536,25 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out,
     return n;
   }
 
-  case theory::eq::MERGED_THROUGH_REFLEXIVITY:
+  else if (pf->d_id == theory::eq::MERGED_THROUGH_REFLEXIVITY) {
     Assert(!pf->d_node.isNull());
     Assert(pf->d_children.empty());
     out << "(refl _ ";
     tp->printTerm(NodeManager::currentNM()->toExpr(pf->d_node), out, map);
     out << ")";
     return eqNode(pf->d_node, pf->d_node);
+  }
 
-  case theory::eq::MERGED_THROUGH_EQUALITY:
+  else if (pf->d_id == theory::eq::MERGED_THROUGH_EQUALITY) {
     Assert(!pf->d_node.isNull());
     Assert(pf->d_children.empty());
     Debug("pf::array") << "ArrayProof::toStream: getLitName( " << pf->d_node.negate() << " ) = " <<
       ProofManager::getLitName(pf->d_node.negate()) << std::endl;
     out << ProofManager::getLitName(pf->d_node.negate());
     return pf->d_node;
+  }
 
-  case theory::eq::MERGED_THROUGH_TRANS: {
+  else if (pf->d_id == theory::eq::MERGED_THROUGH_TRANS) {
     bool firstNeg = false;
     bool secondNeg = false;
 
@@ -734,27 +751,27 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out,
         // Both elements of the transitivity rule are equalities/iffs
       {
         if(n1[0] == n2[0]) {
-            if(tb == 1) { Debug("mgdx") << "case 1\n"; }
-            n1 = eqNode(n1[1], n2[1]);
-            ss << (firstNeg ? "(negsymm _ _ _ " : "(symm _ _ _ ") << ss1.str() << ") " << ss2.str();
+          if(tb == 1) { Debug("mgdx") << "case 1\n"; }
+          n1 = eqNode(n1[1], n2[1]);
+          ss << (firstNeg ? "(negsymm _ _ _ " : "(symm _ _ _ ") << ss1.str() << ") " << ss2.str();
         } else if(n1[1] == n2[1]) {
           if(tb == 1) { Debug("mgdx") << "case 2\n"; }
           n1 = eqNode(n1[0], n2[0]);
           ss << ss1.str() << (secondNeg ? " (negsymm _ _ _ " : " (symm _ _ _ " ) << ss2.str() << ")";
         } else if(n1[0] == n2[1]) {
-            if(tb == 1) { Debug("mgdx") << "case 3\n"; }
-            if(!firstNeg && !secondNeg) {
-              n1 = eqNode(n2[0], n1[1]);
-              ss << ss2.str() << " " << ss1.str();
-            } else if (firstNeg) {
-              n1 = eqNode(n1[1], n2[0]);
-              ss << " (negsymm _ _ _ " << ss1.str() << ") (symm _ _ _ " << ss2.str() << ")";
-            } else {
-              Assert(secondNeg);
-              n1 = eqNode(n1[1], n2[0]);
-              ss << " (symm _ _ _ " << ss1.str() << ") (negsymm _ _ _ " << ss2.str() << ")";
-            }
-            if(tb == 1) { Debug("mgdx") << "++ proved " << n1 << "\n"; }
+          if(tb == 1) { Debug("mgdx") << "case 3\n"; }
+          if(!firstNeg && !secondNeg) {
+            n1 = eqNode(n2[0], n1[1]);
+            ss << ss2.str() << " " << ss1.str();
+          } else if (firstNeg) {
+            n1 = eqNode(n1[1], n2[0]);
+            ss << " (negsymm _ _ _ " << ss1.str() << ") (symm _ _ _ " << ss2.str() << ")";
+          } else {
+            Assert(secondNeg);
+            n1 = eqNode(n1[1], n2[0]);
+            ss << " (symm _ _ _ " << ss1.str() << ") (negsymm _ _ _ " << ss2.str() << ")";
+          }
+          if(tb == 1) { Debug("mgdx") << "++ proved " << n1 << "\n"; }
         } else if(n1[1] == n2[0]) {
           if(tb == 1) { Debug("mgdx") << "case 4\n"; }
           n1 = eqNode(n1[0], n2[1]);
@@ -811,7 +828,7 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out,
     return n1;
   }
 
-  case theory::eq::MERGED_ARRAYS_ROW: {
+  else if (pf->d_id == d_reasonRow) {
     Debug("mgd") << "row lemma: " << pf->d_node << std::endl;
     Assert(pf->d_node.getKind() == kind::EQUAL);
 
@@ -942,8 +959,8 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out,
 
 
       // if (subproof[0][1] == t3) {
-        Debug("pf::array") << "Dont need symmetry!" << std::endl;
-        out << ss.str();
+      Debug("pf::array") << "Dont need symmetry!" << std::endl;
+      out << ss.str();
       // } else {
       //   Debug("pf::array") << "Need symmetry!" << std::endl;
       //   out << "(negsymm _ _ _ " << ss.str() << ")";
@@ -957,7 +974,7 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out,
     }
   }
 
-  case theory::eq::MERGED_ARRAYS_ROW1: {
+  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;
@@ -992,7 +1009,7 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out,
     return ret;
   }
 
-  case theory::eq::MERGED_ARRAYS_EXT: {
+  else if (pf->d_id == d_reasonExt) {
     theory::eq::EqProof *child_proof;
 
     Assert(pf->d_node.getKind() == kind::NOT);
@@ -1021,7 +1038,7 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out,
     return pf->d_node;
   }
 
-  default:
+  else {
     Assert(!pf->d_node.isNull());
     Assert(pf->d_children.empty());
     Debug("mgd") << "theory proof: " << pf->d_node << " by rule " << int(pf->d_id) << std::endl;
diff --git a/src/proof/array_proof.h b/src/proof/array_proof.h
index 9b308dcd8..b3fe89f0b 100644
--- a/src/proof/array_proof.h
+++ b/src/proof/array_proof.h
@@ -35,7 +35,12 @@ private:
                               unsigned tb,
                               const LetMap& map);
 
-  std::hash_map<Node, Node, NodeHashFunction> d_nodeToSkolem;
+  /** Merge tag for ROW applications */
+  static unsigned d_reasonRow;
+  /** Merge tag for ROW1 applications */
+  static unsigned d_reasonRow1;
+  /** Merge tag for EXT applications */
+  static unsigned d_reasonExt;
 public:
   ProofArray(theory::eq::EqProof* pf) : d_proof(pf) {}
   //it is simply an equality engine proof
@@ -44,6 +49,10 @@ public:
   static 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);
 };
 
 namespace theory {
diff --git a/src/proof/uf_proof.cpp b/src/proof/uf_proof.cpp
index 6a6f8d906..e728e9e49 100644
--- a/src/proof/uf_proof.cpp
+++ b/src/proof/uf_proof.cpp
@@ -615,88 +615,6 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::E
     return n1;
   }
 
-  case theory::eq::MERGED_ARRAYS_ROW: {
-    Debug("pf::uf") << "eq::MERGED_ARRAYS_ROW encountered in UF_PROOF" << std::endl;
-    Unreachable();
-
-    Debug("pf::uf") << "row lemma: " << pf->d_node << std::endl;
-    Assert(pf->d_node.getKind() == kind::EQUAL);
-    TNode t1, t2, t3, t4;
-    Node ret;
-    if(pf->d_node[1].getKind() == kind::SELECT &&
-       pf->d_node[1][0].getKind() == kind::STORE &&
-       pf->d_node[0].getKind() == kind::SELECT &&
-       pf->d_node[0][0] == pf->d_node[1][0][0] &&
-       pf->d_node[0][1] == pf->d_node[1][1]) {
-      t2 = pf->d_node[1][0][1];
-      t3 = pf->d_node[1][1];
-      t1 = pf->d_node[0][0];
-      t4 = pf->d_node[1][0][2];
-      ret = pf->d_node[1].eqNode(pf->d_node[0]);
-      Debug("pf::uf") << "t1 " << t1 << "\nt2 " << t2 << "\nt3 " << t3 << "\nt4 " << t4 << "\n";
-    } else {
-      Assert(pf->d_node[0].getKind() == kind::SELECT &&
-             pf->d_node[0][0].getKind() == kind::STORE &&
-             pf->d_node[1].getKind() == kind::SELECT &&
-             pf->d_node[1][0] == pf->d_node[0][0][0] &&
-             pf->d_node[1][1] == pf->d_node[0][1]);
-      t2 = pf->d_node[0][0][1];
-      t3 = pf->d_node[0][1];
-      t1 = pf->d_node[1][0];
-      t4 = pf->d_node[0][0][2];
-      ret = pf->d_node;
-      Debug("pf::uf") << "t1 " << t1 << "\nt2 " << t2 << "\nt3 " << t3 << "\nt4 " << t4 << "\n";
-    }
-    out << "(row _ _ ";
-    tp->printTerm(t2.toExpr(), out, map);
-    out << " ";
-    tp->printTerm(t3.toExpr(), out, map);
-    out << " ";
-    tp->printTerm(t1.toExpr(), out, map);
-    out << " ";
-    tp->printTerm(t4.toExpr(), out, map);
-    out << " " << ProofManager::getLitName(t2.eqNode(t3)) << ")";
-    return ret;
-  }
-
-  case theory::eq::MERGED_ARRAYS_ROW1: {
-    Debug("pf::uf") << "eq::MERGED_ARRAYS_ROW1 encountered in UF_PROOF" << std::endl;
-    Unreachable();
-
-    Debug("pf::uf") << "row1 lemma: " << pf->d_node << std::endl;
-    Assert(pf->d_node.getKind() == kind::EQUAL);
-    TNode t1, t2, t3;
-    Node ret;
-    if(pf->d_node[1].getKind() == kind::SELECT &&
-       pf->d_node[1][0].getKind() == kind::STORE &&
-       pf->d_node[1][0][1] == pf->d_node[1][1] &&
-       pf->d_node[1][0][2] == pf->d_node[0]) {
-      t1 = pf->d_node[1][0][0];
-      t2 = pf->d_node[1][0][1];
-      t3 = pf->d_node[0];
-      ret = pf->d_node[1].eqNode(pf->d_node[0]);
-      Debug("pf::uf") << "t1 " << t1 << "\nt2 " << t2 << "\nt3 " << t3 << "\n";
-    } else {
-      Assert(pf->d_node[0].getKind() == kind::SELECT &&
-             pf->d_node[0][0].getKind() == kind::STORE &&
-             pf->d_node[0][0][1] == pf->d_node[0][1] &&
-             pf->d_node[0][0][2] == pf->d_node[1]);
-      t1 = pf->d_node[0][0][0];
-      t2 = pf->d_node[0][0][1];
-      t3 = pf->d_node[1];
-      ret = pf->d_node;
-      Debug("pf::uf") << "t1 " << t1 << "\nt2 " << t2 << "\nt3 " << t3 << "\n";
-    }
-    out << "(row1 _ _ ";
-    tp->printTerm(t1.toExpr(), out, map);
-    out << " ";
-    tp->printTerm(t2.toExpr(), out, map);
-    out << " ";
-    tp->printTerm(t3.toExpr(), out, map);
-    out << ")";
-    return ret;
-  }
-
   default:
     Assert(!pf->d_node.isNull());
     Assert(pf->d_children.empty());