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

10 files changed, 185 insertions, 201 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());
diff --git a/src/theory/arrays/array_proof_reconstruction.cpp b/src/theory/arrays/array_proof_reconstruction.cpp
index b2e8c3ab3..c8a6716f5 100644
--- a/src/theory/arrays/array_proof_reconstruction.cpp
+++ b/src/theory/arrays/array_proof_reconstruction.cpp
@@ -1,10 +1,10 @@
 /*********************                                                        */
 /*! \file array_proof_reconstruction.h
- ** \verbatim
- **
- ** \brief Array-specific proof construction logic to be used during the
- ** equality engine's path reconstruction
- **/
+** \verbatim
+**
+** \brief Array-specific proof construction logic to be used during the
+** equality engine's path reconstruction
+**/
 
 #include "theory/arrays/array_proof_reconstruction.h"
 
@@ -16,16 +16,26 @@ ArrayProofReconstruction::ArrayProofReconstruction(const eq::EqualityEngine* equ
   : d_equalityEngine(equalityEngine) {
 }
 
-void ArrayProofReconstruction::notify(eq::MergeReasonType reasonType, Node reason, Node a, Node b,
+void ArrayProofReconstruction::setRowMergeTag(unsigned tag) {
+  d_reasonRow = tag;
+}
+
+void ArrayProofReconstruction::setRow1MergeTag(unsigned tag) {
+  d_reasonRow1 = tag;
+}
+
+void ArrayProofReconstruction::setExtMergeTag(unsigned tag) {
+  d_reasonExt = tag;
+}
+
+void ArrayProofReconstruction::notify(unsigned reasonType, Node reason, Node a, Node b,
                                       std::vector<TNode>& equalities, eq::EqProof* proof) const {
 
   Debug("pf::array") << "ArrayProofReconstruction::notify( "
                      << reason << ", " << a << ", " << b << std::endl;
 
 
-  switch (reasonType) {
-
-  case eq::MERGED_ARRAYS_EXT: {
+  if (reasonType == d_reasonExt) {
     if (proof) {
       // Todo: here we assume that a=b is an assertion. We should probably call explain()
       // recursively, to explain this.
@@ -33,10 +43,9 @@ void ArrayProofReconstruction::notify(eq::MergeReasonType reasonType, Node reaso
       childProof->d_node = reason;
       proof->d_children.push_back(childProof);
     }
-    break;
   }
 
-  case eq::MERGED_ARRAYS_ROW: {
+  else if (reasonType == d_reasonRow) {
     // ROW rules mean that (i==k) OR ((a[i]:=t)[k] == a[k])
     // The equality here will be either (i == k) because ((a[i]:=t)[k] != a[k]),
     // or ((a[i]:=t)[k] == a[k]) because (i != k).
@@ -103,16 +112,11 @@ void ArrayProofReconstruction::notify(eq::MergeReasonType reasonType, Node reaso
         proof->d_children.push_back(childProof);
       }
     }
-    break;
-  }
 
-  case eq::MERGED_ARRAYS_ROW1: {
-    // No special handling required at this time
-    break;
   }
 
-  default:
-    break;
+  else if (reasonType == d_reasonRow1) {
+    // No special handling required at this time
   }
 }
 
diff --git a/src/theory/arrays/array_proof_reconstruction.h b/src/theory/arrays/array_proof_reconstruction.h
index 8afc0d3f7..6502b0e6b 100644
--- a/src/theory/arrays/array_proof_reconstruction.h
+++ b/src/theory/arrays/array_proof_reconstruction.h
@@ -26,10 +26,21 @@ class ArrayProofReconstruction : public eq::PathReconstructionNotify {
 public:
   ArrayProofReconstruction(const eq::EqualityEngine* equalityEngine);
 
-  void notify(eq::MergeReasonType reasonType, Node reason, Node a, Node b,
+  void notify(unsigned reasonType, Node reason, Node a, Node b,
               std::vector<TNode>& equalities, eq::EqProof* proof) const;
 
+  void setRowMergeTag(unsigned tag);
+  void setRow1MergeTag(unsigned tag);
+  void setExtMergeTag(unsigned tag);
+
 private:
+  /** Merge tag for ROW applications */
+  unsigned d_reasonRow;
+  /** Merge tag for ROW1 applications */
+  unsigned d_reasonRow1;
+  /** Merge tag for EXT applications */
+  unsigned d_reasonExt;
+
   const eq::EqualityEngine* d_equalityEngine;
 }; /* class ArrayProofReconstruction */
 
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index 37854ee90..8d97eb89d 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -129,9 +129,17 @@ TheoryArrays::TheoryArrays(context::Context* c, context::UserContext* u,
     d_equalityEngine.addFunctionKind(kind::ARR_TABLE_FUN);
   }
 
-  d_equalityEngine.addPathReconstructionTrigger(eq::MERGED_ARRAYS_ROW, &d_proofReconstruction);
-  d_equalityEngine.addPathReconstructionTrigger(eq::MERGED_ARRAYS_ROW1, &d_proofReconstruction);
-  d_equalityEngine.addPathReconstructionTrigger(eq::MERGED_ARRAYS_EXT, &d_proofReconstruction);
+  d_reasonRow = d_equalityEngine.getFreshMergeReasonType();
+  d_reasonRow1 = d_equalityEngine.getFreshMergeReasonType();
+  d_reasonExt = d_equalityEngine.getFreshMergeReasonType();
+
+  d_proofReconstruction.setRowMergeTag(d_reasonRow);
+  d_proofReconstruction.setRow1MergeTag(d_reasonRow1);
+  d_proofReconstruction.setExtMergeTag(d_reasonExt);
+
+  d_equalityEngine.addPathReconstructionTrigger(d_reasonRow, &d_proofReconstruction);
+  d_equalityEngine.addPathReconstructionTrigger(d_reasonRow1, &d_proofReconstruction);
+  d_equalityEngine.addPathReconstructionTrigger(d_reasonExt, &d_proofReconstruction);
 }
 
 TheoryArrays::~TheoryArrays() {
@@ -665,7 +673,7 @@ void TheoryArrays::preRegisterTermInternal(TNode node)
           if (ni != node) {
             preRegisterTermInternal(ni);
           }
-          d_equalityEngine.assertEquality(ni.eqNode(s[2]), true, d_true, eq::MERGED_ARRAYS_ROW1);
+          d_equalityEngine.assertEquality(ni.eqNode(s[2]), true, d_true, d_reasonRow1);
           Assert(++it == stores->end());
         }
       }
@@ -751,7 +759,7 @@ void TheoryArrays::preRegisterTermInternal(TNode node)
       }
 
       // Apply RIntro1 Rule
-      d_equalityEngine.assertEquality(ni.eqNode(v), true, d_true, eq::MERGED_ARRAYS_ROW1);
+      d_equalityEngine.assertEquality(ni.eqNode(v), true, d_true, d_reasonRow1);
     }
 
     d_infoMap.addStore(node, node);
@@ -1367,7 +1375,7 @@ void TheoryArrays::check(Effort e) {
                                  << "\teq = " << eq << std::endl
                                  << "\treason = " << fact << std::endl;
 
-              d_equalityEngine.assertEquality(eq, false, fact, eq::MERGED_ARRAYS_EXT);
+              d_equalityEngine.assertEquality(eq, false, fact, d_reasonExt);
               ++d_numProp;
             }
 
@@ -1669,7 +1677,7 @@ void TheoryArrays::checkRIntro1(TNode a, TNode b)
     d_infoMap.setRIntro1Applied(s);
     Node ni = nm->mkNode(kind::SELECT, s, s[1]);
     preRegisterTermInternal(ni);
-    d_equalityEngine.assertEquality(ni.eqNode(s[2]), true, d_true, eq::MERGED_ARRAYS_ROW1);
+    d_equalityEngine.assertEquality(ni.eqNode(s[2]), true, d_true, d_reasonRow1);
   }
 }
 
@@ -1976,7 +1984,7 @@ void TheoryArrays::propagate(RowLemmaType lem)
       if (!bjExists) {
         preRegisterTermInternal(bj);
       }
-      d_equalityEngine.assertEquality(aj_eq_bj, true, reason, eq::MERGED_ARRAYS_ROW);
+      d_equalityEngine.assertEquality(aj_eq_bj, true, reason, d_reasonRow);
       ++d_numProp;
       return;
     }
@@ -1986,7 +1994,7 @@ void TheoryArrays::propagate(RowLemmaType lem)
       Node i_eq_j = i.eqNode(j);
       Node reason = nm->mkNode(kind::OR, i_eq_j, aj_eq_bj);
       d_permRef.push_back(reason);
-      d_equalityEngine.assertEquality(i_eq_j, true, reason, eq::MERGED_ARRAYS_ROW);
+      d_equalityEngine.assertEquality(i_eq_j, true, reason, d_reasonRow);
       ++d_numProp;
       return;
     }
@@ -2230,15 +2238,22 @@ void TheoryArrays::conflict(TNode a, TNode b) {
   }
 
   if (!d_inCheckModel) {
-    if (proof) { proof->debug_print("pf::array"); }
-    ProofArray* proof_array = d_proofsEnabled ? new ProofArray( proof ) : NULL;
+    ProofArray* proof_array = NULL;
+
+    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);
+    }
+
     d_out->conflict(d_conflictNode, proof_array);
   }
 
   d_conflict = true;
 }
 
-
 }/* CVC4::theory::arrays namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h
index 6d2bb9e73..14e5a622a 100644
--- a/src/theory/arrays/theory_arrays.h
+++ b/src/theory/arrays/theory_arrays.h
@@ -125,6 +125,15 @@ class TheoryArrays : public Theory {
   /** conflicts in setModelVal */
   IntStat d_numSetModelValConflicts;
 
+  // Merge reason types
+
+  /** Merge tag for ROW applications */
+  unsigned d_reasonRow;
+  /** Merge tag for ROW1 applications */
+  unsigned d_reasonRow1;
+  /** Merge tag for EXT applications */
+  unsigned d_reasonExt;
+
  public:
 
   TheoryArrays(context::Context* c, context::UserContext* u, OutputChannel& out,
diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp
index d4a1e5ca4..20d0d85a8 100644
--- a/src/theory/uf/equality_engine.cpp
+++ b/src/theory/uf/equality_engine.cpp
@@ -93,6 +93,8 @@ void EqualityEngine::init() {
 
   d_trueId = getNodeId(d_true);
   d_falseId = getNodeId(d_false);
+
+  d_freshMergeReasonType = eq::NUMBER_OF_MERGE_REASONS;
 }
 
 EqualityEngine::~EqualityEngine() throw(AssertionException) {
@@ -389,7 +391,7 @@ const EqualityNode& EqualityEngine::getEqualityNode(EqualityNodeId nodeId) const
   return d_equalityNodes[nodeId];
 }
 
-void EqualityEngine::assertEqualityInternal(TNode t1, TNode t2, TNode reason, MergeReasonType pid) {
+void EqualityEngine::assertEqualityInternal(TNode t1, TNode t2, TNode reason, unsigned pid) {
 
   Debug("equality") << d_name << "::eq::addEqualityInternal(" << t1 << "," << t2 << "), pid = " << pid << std::endl;
 
@@ -407,7 +409,7 @@ void EqualityEngine::assertEqualityInternal(TNode t1, TNode t2, TNode reason, Me
   enqueue(MergeCandidate(t1Id, t2Id, pid, reason));
 }
 
-void EqualityEngine::assertPredicate(TNode t, bool polarity, TNode reason, MergeReasonType pid) {
+void EqualityEngine::assertPredicate(TNode t, bool polarity, TNode reason, unsigned pid) {
   Debug("equality") << d_name << "::eq::addPredicate(" << t << "," << (polarity ? "true" : "false") << ")" << std::endl;
   Assert(t.getKind() != kind::EQUAL, "Use assertEquality instead");
   assertEqualityInternal(t, polarity ? d_true : d_false, reason, pid);
@@ -420,7 +422,7 @@ void EqualityEngine::mergePredicates(TNode p, TNode q, TNode reason) {
   propagate();
 }
 
-void EqualityEngine::assertEquality(TNode eq, bool polarity, TNode reason, MergeReasonType pid) {
+void EqualityEngine::assertEquality(TNode eq, bool polarity, TNode reason, unsigned pid) {
   Debug("equality") << d_name << "::eq::addEquality(" << eq << "," << (polarity ? "true" : "false") << ")" << std::endl;
   if (polarity) {
     // If two terms are already equal, don't assert anything
@@ -888,7 +890,7 @@ void EqualityEngine::backtrack() {
 
 }
 
-void EqualityEngine::addGraphEdge(EqualityNodeId t1, EqualityNodeId t2, MergeReasonType type, TNode reason) {
+void EqualityEngine::addGraphEdge(EqualityNodeId t1, EqualityNodeId t2, unsigned type, TNode reason) {
   Debug("equality") << d_name << "::eq::addGraphEdge(" << d_nodes[t1] << "," << d_nodes[t2] << "," << reason << ")" << std::endl;
   EqualityEdgeId edge = d_equalityEdges.size();
   d_equalityEdges.push_back(EqualityEdge(t2, d_equalityGraph[t1], type, reason));
@@ -1089,7 +1091,7 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st
             // The current node
             currentNode = bfsQueue[currentIndex].nodeId;
             EqualityNodeId edgeNode = d_equalityEdges[currentEdge].getNodeId();
-            MergeReasonType reasonType = d_equalityEdges[currentEdge].getReasonType();
+            unsigned reasonType = d_equalityEdges[currentEdge].getReasonType();
             Node reason = d_equalityEdges[currentEdge].getReason();
 
             Debug("equality") << d_name << "::eq::getExplanation(): currentEdge = " << currentEdge << ", currentNode = " << currentNode << std::endl;
@@ -1711,12 +1713,16 @@ size_t EqualityEngine::getSize(TNode t) {
 }
 
 
-void EqualityEngine::addPathReconstructionTrigger(MergeReasonType trigger, const PathReconstructionNotify* notify) {
+void EqualityEngine::addPathReconstructionTrigger(unsigned trigger, const PathReconstructionNotify* notify) {
   // Currently we can only inform one callback per trigger
   Assert(d_pathReconstructionTriggers.find(trigger) == d_pathReconstructionTriggers.end());
   d_pathReconstructionTriggers[trigger] = notify;
 }
 
+unsigned EqualityEngine::getFreshMergeReasonType() {
+  return d_freshMergeReasonType++;
+}
+
 void EqualityEngine::addTriggerTerm(TNode t, TheoryId tag)
 {
   Debug("equality::trigger") << d_name << "::eq::addTriggerTerm(" << t << ", " << tag << ")" << std::endl;
@@ -2221,7 +2227,6 @@ void EqProof::debug_print( const char * c, unsigned tb ) const{
   Debug( c ) << ")" << std::endl;
 }
 
-
 } // Namespace uf
 } // Namespace theory
 } // Namespace CVC4
diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h
index 97abfccf1..7bc645c24 100644
--- a/src/theory/uf/equality_engine.h
+++ b/src/theory/uf/equality_engine.h
@@ -149,7 +149,7 @@ public:
 
   virtual ~PathReconstructionNotify() {}
 
-  virtual void notify(MergeReasonType reasonType, Node reason, Node a, Node b,
+  virtual void notify(unsigned reasonType, Node reason, Node a, Node b,
                       std::vector<TNode>& equalities, EqProof* proof) const = 0;
 };
 
@@ -231,7 +231,7 @@ private:
   KindMap d_congruenceKindsInterpreted;
 
   /** Objects that need to be notified during equality path reconstruction */
-  std::map<MergeReasonType, const PathReconstructionNotify*> d_pathReconstructionTriggers;
+  std::map<unsigned, const PathReconstructionNotify*> d_pathReconstructionTriggers;
 
   /** Map from nodes to their ids */
   __gnu_cxx::hash_map<TNode, EqualityNodeId, TNodeHashFunction> d_nodeIds;
@@ -274,6 +274,9 @@ private:
   /** Memory for the use-list nodes */
   std::vector<UseListNode> d_useListNodes;
 
+  /** A fresh merge reason type to return upon request */
+  unsigned d_freshMergeReasonType;
+
   /**
    * We keep a list of asserted equalities. Not among original terms, but
    * among the class representatives.
@@ -304,7 +307,7 @@ private:
     // The next edge
     EqualityEdgeId d_nextId;
     // Type of reason for this equality
-    MergeReasonType d_mergeType;
+    unsigned d_mergeType;
     // Reason of this equality
     TNode d_reason;
 
@@ -313,7 +316,7 @@ private:
     EqualityEdge():
       d_nodeId(null_edge), d_nextId(null_edge), d_mergeType(MERGED_THROUGH_CONGRUENCE) {}
 
-    EqualityEdge(EqualityNodeId nodeId, EqualityNodeId nextId, MergeReasonType type, TNode reason):
+    EqualityEdge(EqualityNodeId nodeId, EqualityNodeId nextId, unsigned type, TNode reason):
       d_nodeId(nodeId), d_nextId(nextId), d_mergeType(type), d_reason(reason) {}
 
     /** Returns the id of the next edge */
@@ -323,7 +326,7 @@ private:
     EqualityNodeId getNodeId() const { return d_nodeId; }
 
     /** The reason of this edge */
-    MergeReasonType getReasonType() const { return d_mergeType; }
+    unsigned getReasonType() const { return d_mergeType; }
 
     /** The reason of this edge */
     TNode getReason() const { return d_reason; }
@@ -348,7 +351,7 @@ private:
   std::vector<EqualityEdgeId> d_equalityGraph;
 
   /** Add an edge to the equality graph */
-  void addGraphEdge(EqualityNodeId t1, EqualityNodeId t2, MergeReasonType type, TNode reason);
+  void addGraphEdge(EqualityNodeId t1, EqualityNodeId t2, unsigned type, TNode reason);
 
   /** Returns the equality node of the given node */
   EqualityNode& getEqualityNode(TNode node);
@@ -520,7 +523,7 @@ private:
   /**
    * Adds an equality of terms t1 and t2 to the database.
    */
-  void assertEqualityInternal(TNode t1, TNode t2, TNode reason, MergeReasonType pid = MERGED_THROUGH_EQUALITY);
+  void assertEqualityInternal(TNode t1, TNode t2, TNode reason, unsigned pid = MERGED_THROUGH_EQUALITY);
 
   /**
    * Adds a trigger equality to the database with the trigger node and polarity for notification.
@@ -744,7 +747,7 @@ public:
    *                 asserting the negated predicate
    * @param reason the reason to keep for building explanations
    */
-  void assertPredicate(TNode p, bool polarity, TNode reason, MergeReasonType pid = MERGED_THROUGH_EQUALITY);
+  void assertPredicate(TNode p, bool polarity, TNode reason, unsigned pid = MERGED_THROUGH_EQUALITY);
 
   /**
    * Adds predicate p and q and makes them equal.
@@ -759,7 +762,7 @@ public:
    *                 asserting the negated equality
    * @param reason the reason to keep for building explanations
    */
-  void assertEquality(TNode eq, bool polarity, TNode reason, MergeReasonType pid = MERGED_THROUGH_EQUALITY);
+  void assertEquality(TNode eq, bool polarity, TNode reason, unsigned pid = MERGED_THROUGH_EQUALITY);
 
   /**
    * Returns the current representative of the term t.
@@ -851,7 +854,12 @@ public:
   /**
    * Marks an object for merge type based notification during equality path reconstruction.
    */
-  void addPathReconstructionTrigger(MergeReasonType trigger, const PathReconstructionNotify* notify);
+  void addPathReconstructionTrigger(unsigned trigger, const PathReconstructionNotify* notify);
+
+  /**
+   * Returns a fresh merge reason type tag for the client to use.
+   */
+  unsigned getFreshMergeReasonType();
 };
 
 /**
@@ -895,7 +903,7 @@ class EqProof
 {
 public:
   EqProof() : d_id(MERGED_THROUGH_REFLEXIVITY){}
-  MergeReasonType d_id;
+  unsigned d_id;
   Node d_node;
   std::vector< EqProof * > d_children;
   void debug_print( const char * c, unsigned tb = 0 ) const;
diff --git a/src/theory/uf/equality_engine_types.h b/src/theory/uf/equality_engine_types.h
index 0c2c3e354..5bf9db436 100644
--- a/src/theory/uf/equality_engine_types.h
+++ b/src/theory/uf/equality_engine_types.h
@@ -67,14 +67,11 @@ enum MergeReasonType {
   MERGED_THROUGH_REFLEXIVITY,
   /** Equality was merged to false, due to both sides of equality being a constant */
   MERGED_THROUGH_CONSTANTS,
-
   /** (for proofs only) Equality was merged due to transitivity */
   MERGED_THROUGH_TRANS,
 
-  /** Theory specific proof rules */
-  MERGED_ARRAYS_ROW,
-  MERGED_ARRAYS_ROW1,
-  MERGED_ARRAYS_EXT
+  /** Reason types beyond this constant are theory specific reasons */
+  NUMBER_OF_MERGE_REASONS
 };
 
 inline std::ostream& operator << (std::ostream& out, MergeReasonType reason) {
@@ -91,20 +88,11 @@ inline std::ostream& operator << (std::ostream& out, MergeReasonType reason) {
   case MERGED_THROUGH_CONSTANTS:
     out << "constants disequal";
     break;
-  // (for proofs only)
   case MERGED_THROUGH_TRANS:
     out << "transitivity";
     break;
-  case MERGED_ARRAYS_ROW:
-    out << "arrays ROW";
-    break;
-  case MERGED_ARRAYS_ROW1:
-    out << "arrays ROW1";
-    break;
-  case MERGED_ARRAYS_EXT:
-    out << "arrays EXT";
-    break;
-default:
+
+  default:
     out << "[theory]";
     break;
   }
@@ -117,9 +105,9 @@ default:
  */
 struct MergeCandidate {
   EqualityNodeId t1Id, t2Id;
-  MergeReasonType type;
+  unsigned type;
   TNode reason;
-  MergeCandidate(EqualityNodeId x, EqualityNodeId y, MergeReasonType type, TNode reason)
+  MergeCandidate(EqualityNodeId x, EqualityNodeId y, unsigned type, TNode reason)
   : t1Id(x), t2Id(y), type(type), reason(reason)
   {}
 };