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

3 files changed, 37 insertions, 36 deletions

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)
   {}
 };