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

4 files changed, 70 insertions, 31 deletions

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,