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

1 files changed, 19 insertions, 11 deletions

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;