Updating equality manager to handle tagged trigger terms. Notifications are pushed out for relationships between terms tagged with the same tag. No performance impact.

13 files changed, 292 insertions, 79 deletions

diff --git a/src/theory/arith/congruence_manager.cpp b/src/theory/arith/congruence_manager.cpp
index 39468e928..649e34134 100644
--- a/src/theory/arith/congruence_manager.cpp
+++ b/src/theory/arith/congruence_manager.cpp
@@ -300,7 +300,7 @@ void ArithCongruenceManager::equalsConstant(Constraint lb, Constraint ub){
 }
 
 void ArithCongruenceManager::addSharedTerm(Node x){
-  d_ee.addTriggerTerm(x);
+  d_ee.addTriggerTerm(x, THEORY_ARITH);
 }
 
 }/* CVC4::theory::arith namespace */
diff --git a/src/theory/arith/congruence_manager.h b/src/theory/arith/congruence_manager.h
index 18ecbeb9d..5e4616628 100644
--- a/src/theory/arith/congruence_manager.h
+++ b/src/theory/arith/congruence_manager.h
@@ -56,7 +56,7 @@ private:
       Unreachable();
     }
 
-    bool eqNotifyTriggerTermEquality(TNode t1, TNode t2, bool value) {
+    bool eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value) {
       Debug("arith::congruences") << "ArithCongruenceNotify::eqNotifyTriggerTermEquality(" << t1 << ", " << t2 << ", " << (value ? "true" : "false") << ")" << std::endl;
       if (value) {
         return d_acm.propagate(t1.eqNode(t2));
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index 3c48c7907..bcdb75845 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -420,7 +420,7 @@ void TheoryArrays::preRegisterTerm(TNode node)
   case kind::STORE: {
     // Invariant: array terms should be preregistered before being added to the equality engine
     Assert(!d_equalityEngine.hasTerm(node));
-    d_equalityEngine.addTriggerTerm(node);
+    d_equalityEngine.addTriggerTerm(node, THEORY_ARRAY);
 
     TNode a = node[0];
     //    TNode i = node[1];
@@ -446,7 +446,7 @@ void TheoryArrays::preRegisterTerm(TNode node)
   default:
     // Variables etc
     if (node.getType().isArray()) {
-      d_equalityEngine.addTriggerTerm(node);
+      d_equalityEngine.addTriggerTerm(node, THEORY_ARRAY);
       Assert(d_equalityEngine.getSize(node) == 1);
     }
     else {
@@ -504,7 +504,7 @@ Node TheoryArrays::explain(TNode literal)
 
 void TheoryArrays::addSharedTerm(TNode t) {
   Debug("arrays::sharing") << spaces(getSatContext()->getLevel()) << "TheoryArrays::addSharedTerm(" << t << ")" << std::endl;
-  d_equalityEngine.addTriggerTerm(t);
+  d_equalityEngine.addTriggerTerm(t, THEORY_ARRAY);
   if (t.getType().isArray()) {
     d_sharedArrays.insert(t,true);
   }
@@ -583,7 +583,7 @@ void TheoryArrays::computeCareGraph()
         TNode x = r1[1];
         TNode y = r2[1];
 
-        if (!d_equalityEngine.isTriggerTerm(x) || !d_equalityEngine.isTriggerTerm(y)) {
+        if (!d_equalityEngine.isTriggerTerm(x, THEORY_ARRAY) || !d_equalityEngine.isTriggerTerm(y, THEORY_ARRAY)) {
           Debug("arrays::sharing") << "TheoryArrays::computeCareGraph(): not connected to shared terms, skipping" << std::endl;
           continue;
         }
@@ -596,8 +596,8 @@ void TheoryArrays::computeCareGraph()
         }
 
         // Get representative trigger terms
-        TNode x_shared = d_equalityEngine.getTriggerTermRepresentative(x);
-        TNode y_shared = d_equalityEngine.getTriggerTermRepresentative(y);
+        TNode x_shared = d_equalityEngine.getTriggerTermRepresentative(x, THEORY_ARRAY);
+        TNode y_shared = d_equalityEngine.getTriggerTermRepresentative(y, THEORY_ARRAY);
 
         EqualityStatus eqStatusDomain = d_valuation.getEqualityStatus(x_shared, y_shared);
         switch (eqStatusDomain) {
diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h
index 146a2145b..639b03df8 100644
--- a/src/theory/arrays/theory_arrays.h
+++ b/src/theory/arrays/theory_arrays.h
@@ -241,7 +241,7 @@ class TheoryArrays : public Theory {
       Unreachable();
     }
 
-    bool eqNotifyTriggerTermEquality(TNode t1, TNode t2, bool value) {
+    bool eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value) {
       Debug("arrays") << spaces(d_arrays.getSatContext()->getLevel()) << "NotifyClass::eqNotifyTriggerTermEquality(" << t1 << ", " << t2 << ")" << std::endl;
       if (value) {
         if (t1.getType().isArray()) {
diff --git a/src/theory/bv/bv_subtheory.cpp b/src/theory/bv/bv_subtheory.cpp
index 502d59f8d..fa36236c9 100644
--- a/src/theory/bv/bv_subtheory.cpp
+++ b/src/theory/bv/bv_subtheory.cpp
@@ -233,7 +233,7 @@ bool EqualitySolver::NotifyClass::eqNotifyTriggerPredicate(TNode predicate, bool
   }
 }
 
-bool EqualitySolver::NotifyClass::eqNotifyTriggerTermEquality(TNode t1, TNode t2, bool value) {
+bool EqualitySolver::NotifyClass::eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value) {
   Debug("bitvector::equality") << "NotifyClass::eqNotifyTriggerTermMerge(" << t1 << ", " << t2 << std::endl;
   if (value) {
     return d_bv->storePropagation(t1.eqNode(t2), TheoryBV::SUB_EQUALITY);
diff --git a/src/theory/bv/bv_subtheory.h b/src/theory/bv/bv_subtheory.h
index db7bad30c..d508976ae 100644
--- a/src/theory/bv/bv_subtheory.h
+++ b/src/theory/bv/bv_subtheory.h
@@ -102,7 +102,7 @@ class EqualitySolver : public SubtheorySolver {
     NotifyClass(TheoryBV* bv): d_bv(bv) {}
     bool eqNotifyTriggerEquality(TNode equality, bool value);
     bool eqNotifyTriggerPredicate(TNode predicate, bool value);
-    bool eqNotifyTriggerTermEquality(TNode t1, TNode t2, bool value); 
+    bool eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value);
     bool eqNotifyConstantTermMerge(TNode t1, TNode t2);
 };
 
@@ -121,7 +121,7 @@ public:
   bool  addAssertions(const std::vector<TNode>& assertions, Theory::Effort e);
   void  explain(TNode literal, std::vector<TNode>& assumptions);
   void  addSharedTerm(TNode t) {
-    d_equalityEngine.addTriggerTerm(t);
+    d_equalityEngine.addTriggerTerm(t, THEORY_BV);
   }
   EqualityStatus getEqualityStatus(TNode a, TNode b) {
     if (d_equalityEngine.areEqual(a, b)) {
diff --git a/src/theory/shared_terms_database.cpp b/src/theory/shared_terms_database.cpp
index 235d6959c..90037b90b 100644
--- a/src/theory/shared_terms_database.cpp
+++ b/src/theory/shared_terms_database.cpp
@@ -58,7 +58,7 @@ void SharedTermsDatabase::addSharedTerm(TNode atom, TNode term, Theory::Set theo
     d_addedSharedTermsSize = d_addedSharedTermsSize + 1;
     d_termsToTheories[search_pair] = theories;
     if (!d_equalityEngine.hasTerm(term)) {
-      d_equalityEngine.addTriggerTerm(term);
+      d_equalityEngine.addTriggerTerm(term, THEORY_UF);
     }
   } else {
     Assert(theories != (*find).second);
diff --git a/src/theory/shared_terms_database.h b/src/theory/shared_terms_database.h
index b04f835e7..c044097ff 100644
--- a/src/theory/shared_terms_database.h
+++ b/src/theory/shared_terms_database.h
@@ -117,7 +117,7 @@ private:
       return true;
     }
 
-    bool eqNotifyTriggerTermEquality(TNode t1, TNode t2, bool value) {
+    bool eqNotifyTriggerTermEquality(theory::TheoryId tag, TNode t1, TNode t2, bool value) {
       if (value) {
         d_sharedTerms.mergeSharedTerms(t1, t2);
       }
diff --git a/src/theory/theory.h b/src/theory/theory.h
index 9ac07d849..36255d1d6 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -38,6 +38,8 @@
 #include <string>
 #include <iostream>
 
+#include <strings.h>
+
 namespace CVC4 {
 
 class TheoryEngine;
@@ -612,6 +614,34 @@ public:
   /** A set of all theories */
   static const Set AllTheories = (1 << theory::THEORY_LAST) - 1;
 
+  /** Pops a first theory off the set */
+  static inline TheoryId setPop(Set& set) {
+    uint32_t i = ffs(set); // Find First Set (bit)
+    if (i == 0) { return THEORY_LAST; }
+    TheoryId id = (TheoryId)(i-1);
+    set = setRemove(id, set);
+    return id;
+  }
+
+  /** Returns the size of a set of theories */
+  static inline size_t setSize(Set set) {
+    size_t count = 0;
+    while (setPop(set) != THEORY_LAST) {
+      ++ count;
+    }
+    return count;
+  }
+
+  /** Returns the index size of a set of theories */
+  static inline size_t setIndex(TheoryId id, Set set) {
+    Assert (setContains(id, set));
+    size_t count = 0;
+    while (setPop(set) != id) {
+      ++ count;
+    }
+    return count;
+  }
+
   /** Add the theory to the set. If no set specified, just returns a singleton set */
   static inline Set setInsert(TheoryId theory, Set set = 0) {
     return set | (1 << theory);
diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp
index f9220c7f3..2527893ff 100644
--- a/src/theory/uf/equality_engine.cpp
+++ b/src/theory/uf/equality_engine.cpp
@@ -62,8 +62,15 @@ void EqualityEngine::init() {
   d_false = NodeManager::currentNM()->mkConst<bool>(false);
   addTerm(d_true);
   addTerm(d_false);
+
+  d_triggerDatabaseAllocatedSize = 100000;
+  d_triggerDatabase = (char*) malloc(d_triggerDatabaseAllocatedSize);
 } 
 
+EqualityEngine::~EqualityEngine() throw(AssertionException) {
+  free(d_triggerDatabase);
+}
+
 
 EqualityEngine::EqualityEngine(context::Context* context, std::string name) 
 : ContextNotifyObj(context)
@@ -74,10 +81,11 @@ EqualityEngine::EqualityEngine(context::Context* context, std::string name)
 , d_nodesCount(context, 0)
 , d_assertedEqualitiesCount(context, 0)
 , d_equalityTriggersCount(context, 0)
-, d_individualTriggersSize(context, 0)
 , d_constantRepresentativesSize(context, 0)
 , d_constantsSize(context, 0)
 , d_stats(name)
+, d_triggerDatabaseSize(context, 0)
+, d_triggerTermSetUpdatesSize(context, 0)
 {
   init();
 }
@@ -91,10 +99,11 @@ EqualityEngine::EqualityEngine(EqualityEngineNotify& notify, context::Context* c
 , d_nodesCount(context, 0)
 , d_assertedEqualitiesCount(context, 0)
 , d_equalityTriggersCount(context, 0)
-, d_individualTriggersSize(context, 0)
 , d_constantRepresentativesSize(context, 0)
 , d_constantsSize(context, 0)
 , d_stats(name)
+, d_triggerDatabaseSize(context, 0)
+, d_triggerTermSetUpdatesSize(context, 0)
 {
   init();
 }
@@ -162,7 +171,7 @@ EqualityNodeId EqualityEngine::newNode(TNode node) {
   // Add it to the equality graph
   d_equalityGraph.push_back(+null_edge);
   // Mark the no-individual trigger
-  d_nodeIndividualTrigger.push_back(+null_id);
+  d_nodeIndividualTrigger.push_back(+null_set_id);
   // Mark non-constant by default
   d_constantRepresentative.push_back(node.isConst() ? newId : +null_id);
   // Add the equality node to the nodes
@@ -423,22 +432,67 @@ bool EqualityEngine::merge(EqualityNode& class1, EqualityNode& class2, std::vect
   }
 
   // Notify the trigger term merges
-  EqualityNodeId class2triggerId = d_nodeIndividualTrigger[class2Id];
-  if (class2triggerId != +null_id) {
-    EqualityNodeId class1triggerId = d_nodeIndividualTrigger[class1Id];
-    if (class1triggerId == +null_id) {
-      // If class1 is not an individual trigger, but class2 is, mark it
-      d_nodeIndividualTrigger[class1Id] = class2triggerId;
+  TriggerTermSetRef class2triggerRef = d_nodeIndividualTrigger[class2Id];
+  if (class2triggerRef != +null_set_id) {
+    TriggerTermSetRef class1triggerRef = d_nodeIndividualTrigger[class1Id];
+    if (class1triggerRef == +null_set_id) {
+      // If class1 doesn't have individual triggers, but class2 does, mark it
+      d_nodeIndividualTrigger[class1Id] = class2triggerRef;
       // Add it to the list for backtracking
-      d_individualTriggers.push_back(class1Id);
-      d_individualTriggersSize = d_individualTriggersSize + 1;  
+      d_triggerTermSetUpdates.push_back(TriggerSetUpdate(class1Id, +null_set_id));
+      d_triggerTermSetUpdatesSize = d_triggerTermSetUpdatesSize + 1;
     } else {
-      // Notify when done
-      if (d_performNotify) {
-        if (!d_notify.eqNotifyTriggerTermEquality(d_nodes[class1triggerId], d_nodes[class2triggerId], true)) {
-          return false;
+      // Get the triggers
+      TriggerTermSet& class1triggers = getTriggerTermSet(class1triggerRef);
+      TriggerTermSet& class2triggers = getTriggerTermSet(class2triggerRef);
+      
+      // Initialize the merged set
+      d_newSetTags = Theory::setUnion(class1triggers.tags, class2triggers.tags);
+      d_newSetTriggersSize = 0;
+      
+      int i1 = 0;
+      int i2 = 0;
+      Theory::Set tags1 = class1triggers.tags;
+      Theory::Set tags2 = class2triggers.tags;
+      TheoryId tag1 = Theory::setPop(tags1);
+      TheoryId tag2 = Theory::setPop(tags2);
+      
+      // Comparing the THEORY_LAST is OK because all other theories are
+      // smaller, and will therefore be preferred
+      while (tag1 != THEORY_LAST || tag2 != THEORY_LAST) 
+      {
+        if (tag1 < tag2) {
+          // copy tag1 
+          d_newSetTriggers[d_newSetTriggersSize++] = class1triggers.triggers[i1++];
+          tag1 = Theory::setPop(tags1);
+        } else if (tag1 > tag2) {
+          // copy tag2
+          d_newSetTriggers[d_newSetTriggersSize++] = class2triggers.triggers[i2++];
+          tag2 = Theory::setPop(tags2);
+        } else {
+          // copy tag1 
+          EqualityNodeId tag1id = d_newSetTriggers[d_newSetTriggersSize++] = class1triggers.triggers[i1++];
+          // since they are both tagged notify of merge
+          if (d_performNotify) {
+            EqualityNodeId tag2id = class2triggers.triggers[i2++];
+            if (!d_notify.eqNotifyTriggerTermEquality(tag1, d_nodes[tag1id], d_nodes[tag2id], true)) {
+              return false;
+            }
+          }
+          // Next tags
+          tag1 = Theory::setPop(tags1);
+          tag2 = Theory::setPop(tags2);
         }
-      }
+      }   
+      
+      // Add the new trigger set, if different from previous one
+      if (class1triggers.tags != class2triggers.tags) {
+        // Add it to the list for backtracking
+        d_triggerTermSetUpdates.push_back(TriggerSetUpdate(class1Id, class1triggerRef));
+        d_triggerTermSetUpdatesSize = d_triggerTermSetUpdatesSize + 1;
+        // Mark the the new set as a trigger 
+        d_nodeIndividualTrigger[class1Id] = newTriggerTermSet();
+      }  
     }	
   }
 
@@ -513,12 +567,13 @@ void EqualityEngine::backtrack() {
     d_equalityEdges.resize(2 * d_assertedEqualitiesCount);
   }
 
-  if (d_individualTriggers.size() > d_individualTriggersSize) {
+  if (d_triggerTermSetUpdates.size() > d_triggerTermSetUpdatesSize) {
     // Unset the individual triggers
-    for (int i = d_individualTriggers.size() - 1, i_end = d_individualTriggersSize; i >= i_end; -- i) {
-      d_nodeIndividualTrigger[d_individualTriggers[i]] = +null_id;
+    for (int i = d_triggerTermSetUpdates.size() - 1, i_end = d_triggerTermSetUpdatesSize; i >= i_end; -- i) {
+      const TriggerSetUpdate& update = d_triggerTermSetUpdates[i];
+      d_nodeIndividualTrigger[update.classId] = update.oldValue;
     }
-    d_individualTriggers.resize(d_individualTriggersSize);
+    d_triggerTermSetUpdates.resize(d_triggerTermSetUpdatesSize);
   }
   
   if (d_constantRepresentatives.size() > d_constantRepresentativesSize) {
@@ -935,9 +990,10 @@ size_t EqualityEngine::getSize(TNode t)
   return getEqualityNode(getEqualityNode(t).getFind()).getSize();
 }
 
-void EqualityEngine::addTriggerTerm(TNode t)
+void EqualityEngine::addTriggerTerm(TNode t, TheoryId tag)
 {
-  Debug("equality::internal") << "EqualityEngine::addTriggerTerm(" << t << ")" << std::endl;
+  Debug("equality::internal") << "EqualityEngine::addTriggerTerm(" << t << ", " << tag << ")" << std::endl;
+  Assert(tag != THEORY_LAST);
 
   // Add the term if it's not already there
   addTerm(t);
@@ -947,31 +1003,67 @@ void EqualityEngine::addTriggerTerm(TNode t)
   EqualityNode& eqNode = getEqualityNode(eqNodeId);
   EqualityNodeId classId = eqNode.getFind();
 
-  if (d_nodeIndividualTrigger[classId] != +null_id) {  
-    // No need to keep it, just propagate the existing individual triggers
+  // Possibly existing set of triggers
+  TriggerTermSetRef triggerSetRef = d_nodeIndividualTrigger[classId];
+  if (triggerSetRef != +null_set_id && getTriggerTermSet(triggerSetRef).hasTrigger(tag)) {
+    // If the term already is in the equivalence class that a tagged representative, just notify
     if (d_performNotify) {
-      d_notify.eqNotifyTriggerTermEquality(t, d_nodes[d_nodeIndividualTrigger[classId]], true);
+      EqualityNodeId triggerId = getTriggerTermSet(triggerSetRef).getTrigger(tag);
+      d_notify.eqNotifyTriggerTermEquality(tag, t, d_nodes[triggerId], true);
     }
   } else {
+
+    // Setup the data for the new set
+    if (triggerSetRef != null_set_id) {
+      // Get the existing set
+      TriggerTermSet& triggerSet = getTriggerTermSet(triggerSetRef);
+      // Initialize the new set for copy/insert
+      d_newSetTags = Theory::setInsert(tag, triggerSet.tags);
+      d_newSetTriggersSize = 0;
+      // Copy into to new one, and insert the new tag/id      
+      unsigned i = 0;
+      Theory::Set tags = d_newSetTags;
+      TheoryId current; 
+      while ((current = Theory::setPop(tags)) != THEORY_LAST) {
+        // Remove from the tags
+        tags = Theory::setRemove(current, tags);
+        // Insert the id into the triggers
+        d_newSetTriggers[d_newSetTriggersSize++] = 
+          current == tag ? eqNodeId : triggerSet.triggers[i++];
+      }
+    } else {
+      // Setup a singleton 
+      d_newSetTags = Theory::setInsert(tag);
+      d_newSetTriggers[0] = eqNodeId;
+      d_newSetTriggersSize = 1;
+    }
+
     // Add it to the list for backtracking
-    d_individualTriggers.push_back(classId);
-    d_individualTriggersSize = d_individualTriggersSize + 1; 
-    // Mark the class id as a trigger
-    d_nodeIndividualTrigger[classId] = eqNodeId;
+    d_triggerTermSetUpdates.push_back(TriggerSetUpdate(classId, triggerSetRef));
+    d_triggerTermSetUpdatesSize = d_triggerTermSetUpdatesSize + 1;
+    // Mark the the new set as a trigger 
+    d_nodeIndividualTrigger[classId] = newTriggerTermSet();
   }
 }
 
-bool EqualityEngine::isTriggerTerm(TNode t) const {
+bool EqualityEngine::isTriggerTerm(TNode t, TheoryId tag) const {
   if (!hasTerm(t)) return false;
   EqualityNodeId classId = getEqualityNode(t).getFind();
-  return d_nodeIndividualTrigger[classId] != +null_id;
+  TriggerTermSetRef triggerSetRef = d_nodeIndividualTrigger[classId];
+  return triggerSetRef != +null_set_id && getTriggerTermSet(triggerSetRef).hasTrigger(tag);
 }
 
 
-TNode EqualityEngine::getTriggerTermRepresentative(TNode t) const {
-  Assert(isTriggerTerm(t));
+TNode EqualityEngine::getTriggerTermRepresentative(TNode t, TheoryId tag) const {
+  Assert(isTriggerTerm(t, tag));
   EqualityNodeId classId = getEqualityNode(t).getFind();
-  return d_nodes[d_nodeIndividualTrigger[classId]];
+  const TriggerTermSet& triggerSet = getTriggerTermSet(d_nodeIndividualTrigger[classId]);
+  unsigned i = 0;
+  Theory::Set tags = triggerSet.tags;
+  while (Theory::setPop(tags) != tag) {
+    ++ i;
+  }
+  return d_nodes[triggerSet.triggers[i]];
 }
 
 void EqualityEngine::storeApplicationLookup(FunctionApplication& funNormalized, EqualityNodeId funId) {
@@ -1010,6 +1102,31 @@ void EqualityEngine::getUseListTerms(TNode t, std::set<TNode>& output) {
   }
 }
 
+EqualityEngine::TriggerTermSetRef EqualityEngine::newTriggerTermSet() {
+  // Size of the required set
+  size_t size = sizeof(TriggerTermSet) + d_newSetTriggersSize*sizeof(EqualityNodeId);
+  // Align the size
+  size = (size + 7) & ~((size_t)7);
+  // Reallocate if necessary
+  if (d_triggerDatabaseSize + size > d_triggerDatabaseAllocatedSize) {
+    d_triggerDatabaseAllocatedSize *= 2;
+    d_triggerDatabase = (char*) realloc(d_triggerDatabase, d_triggerDatabaseAllocatedSize);
+  }
+  // New reference
+  TriggerTermSetRef newTriggerSetRef = d_triggerDatabaseSize;
+  // Update the size
+  d_triggerDatabaseSize = d_triggerDatabaseSize + size;
+  // Copy the information
+  TriggerTermSet& newSet = getTriggerTermSet(newTriggerSetRef);
+  newSet.tags = d_newSetTags;
+  for (unsigned i = 0; i < d_newSetTriggersSize; ++i) {
+    newSet.triggers[i] = d_newSetTriggers[i];
+  }
+  // Return the new reference
+  return newTriggerSetRef;
+}
+
+
 } // Namespace uf
 } // Namespace theory
 } // Namespace CVC4
diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h
index 047e9de49..c59436aaf 100644
--- a/src/theory/uf/equality_engine.h
+++ b/src/theory/uf/equality_engine.h
@@ -32,6 +32,7 @@
 #include "util/output.h"
 #include "util/stats.h"
 #include "theory/rewriter.h"
+#include "theory/theory.h"
 
 namespace CVC4 {
 namespace theory {
@@ -244,11 +245,12 @@ public:
   /**
    * Notifies about the merge of two trigger terms.
    *
+   * @param tag the theory that both triggers were tagged with
    * @param t1 a term marked as trigger
    * @param t2 a term marked as trigger
    * @param value true if equal, false if dis-equal
    */
-  virtual bool eqNotifyTriggerTermEquality(TNode t1, TNode t2, bool value) = 0;
+  virtual bool eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value) = 0;
 
   /**
    * Notifies about the merge of two constant terms.
@@ -267,7 +269,7 @@ class EqualityEngineNotifyNone : public EqualityEngineNotify {
 public:
   bool eqNotifyTriggerEquality(TNode equality, bool value) { return true; }
   bool eqNotifyTriggerPredicate(TNode predicate, bool value) { return true; }
-  bool eqNotifyTriggerTermEquality(TNode t1, TNode t2, bool value) { return true; }
+  bool eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value) { return true; }
   bool eqNotifyConstantTermMerge(TNode t1, TNode t2) { return true; }
 };
 
@@ -557,21 +559,6 @@ private:
   std::vector<TriggerId> d_nodeTriggers;
 
   /**
-   * List of terms that are marked as individual triggers.
-   */
-  std::vector<EqualityNodeId> d_individualTriggers;
-
-  /**
-   * Size of the individual triggers list.
-   */
-  context::CDO<unsigned> d_individualTriggersSize;
-
-  /** 
-   * Map from ids to the individual trigger id representative. 
-   */
-  std::vector<EqualityNodeId> d_nodeIndividualTrigger;
-
-  /**
    * Map from ids to the id of the constant that is the representative.
    */
   std::vector<EqualityNodeId> d_constantRepresentative;
@@ -666,6 +653,81 @@ private:
    */
   void init();
 
+  /** Set of trigger terms */
+  struct TriggerTermSet {
+    /** Set of theories in this set */
+    Theory::Set tags;
+    /** The trigger terms */
+    EqualityNodeId triggers[0];
+    /** Returns the theory tags */
+    Theory::Set hasTrigger(TheoryId tag) const { return Theory::setContains(tag, tags); }
+    /** Returns a trigger by tag */
+    EqualityNodeId getTrigger(TheoryId tag) const {
+      return triggers[Theory::setIndex(tag, tags)];
+    }
+  };
+
+  /** Internal tags for creating a new set */
+  Theory::Set d_newSetTags;
+  
+  /** Internal triggers for creating a new set */
+  EqualityNodeId d_newSetTriggers[THEORY_LAST];
+  
+  /** Size of the internal triggers array */
+  unsigned d_newSetTriggersSize; 
+
+  /** The information about trigger terms is stored in this easily maintained memory. */
+  char* d_triggerDatabase;
+
+  /** Allocated size of the trigger term database */
+  size_t d_triggerDatabaseAllocatedSize ;
+
+  /** Reference for the trigger terms set */
+  typedef size_t TriggerTermSetRef;
+
+  /** Null reference */
+  static const TriggerTermSetRef null_set_id = (size_t)(-1);
+
+  /** Create new trigger term set based on the internally set information */
+  TriggerTermSetRef newTriggerTermSet();
+
+  /** Get the trigger set give a reference */
+  TriggerTermSet& getTriggerTermSet(TriggerTermSetRef ref) {
+    Assert(ref < d_triggerDatabaseSize);
+    return *(reinterpret_cast<TriggerTermSet*>(d_triggerDatabase + ref));
+  }
+
+  /** Get the trigger set give a reference */
+  const TriggerTermSet& getTriggerTermSet(TriggerTermSetRef ref) const {
+    Assert(ref < d_triggerDatabaseSize);
+    return *(reinterpret_cast<const TriggerTermSet*>(d_triggerDatabase + ref));
+  }
+
+  /** Used part of the trigger term database */
+  context::CDO<size_t> d_triggerDatabaseSize;
+
+  struct TriggerSetUpdate {
+    EqualityNodeId classId;
+    TriggerTermSetRef oldValue;
+    TriggerSetUpdate(EqualityNodeId classId = null_id, TriggerTermSetRef oldValue = null_set_id) 
+    : classId(classId), oldValue(oldValue) {}
+  };
+
+  /**
+   * List of trigger updates for backtracking.
+   */
+  std::vector<TriggerSetUpdate> d_triggerTermSetUpdates;
+
+  /**
+   * Size of the individual triggers list.
+   */
+  context::CDO<unsigned> d_triggerTermSetUpdatesSize;
+
+  /**
+   * Map from ids to the individual trigger set representatives.
+   */
+  std::vector<TriggerTermSetRef> d_nodeIndividualTrigger;
+
 public:
 
   /**
@@ -681,7 +743,7 @@ public:
   /**
    * Just a destructor.
    */
-  virtual ~EqualityEngine() throw(AssertionException) {}
+  virtual ~EqualityEngine() throw(AssertionException);
 
   /**
    * Adds a term to the term database.
@@ -764,25 +826,29 @@ public:
   void explainPredicate(TNode p, bool polarity, std::vector<TNode>& assertions);
 
   /**
-   * Add term to the trigger terms. The notify class will get notified 
-   * when two trigger terms become equal or dis-equal. The notification
-   * will not happen on all the terms, but only on the ones that are 
-   * represent the class.
+   * Add term to the set of trigger terms with a corresponding tag. The notify class will get
+   * notified when two trigger terms with the same tag become equal or dis-equal. The notification
+   * will not happen on all the terms, but only on the ones that are represent the class. Note that
+   * a term can be added more than once with different tags, and each tag apperance will merit
+   * it's own notification.
+   *
+   * @param t the trigger term
+   * @param tag tag for this trigger (do NOT use THEORY_LAST)
    */
-  void addTriggerTerm(TNode t);
+  void addTriggerTerm(TNode t, TheoryId theoryTag);
 
   /**
    * Returns true if t is a trigger term or in the same equivalence 
    * class as some other trigger term.
    */
-  bool isTriggerTerm(TNode t) const;
+  bool isTriggerTerm(TNode t, TheoryId theoryTag) const;
 
   /**
    * Returns the representative trigger term of the given term.
    *
    * @param t the term to check where isTriggerTerm(t) should be true
    */
-  TNode getTriggerTermRepresentative(TNode t) const;
+  TNode getTriggerTermRepresentative(TNode t, TheoryId theoryTag) const;
 
   /**
    * Adds a notify trigger for equality. When equality becomes true eqNotifyTriggerEquality
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index 7f173a0c4..0b9e1b3a7 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -345,7 +345,7 @@ EqualityStatus TheoryUF::getEqualityStatus(TNode a, TNode b) {
 
 void TheoryUF::addSharedTerm(TNode t) {
   Debug("uf::sharing") << "TheoryUF::addSharedTerm(" << t << ")" << std::endl;
-  d_equalityEngine.addTriggerTerm(t);
+  d_equalityEngine.addTriggerTerm(t, THEORY_UF);
 }
 
 void TheoryUF::computeCareGraph() {
@@ -405,14 +405,14 @@ void TheoryUF::computeCareGraph() {
             continue;
           }
 
-          if (!d_equalityEngine.isTriggerTerm(x) || !d_equalityEngine.isTriggerTerm(y)) {
+          if (!d_equalityEngine.isTriggerTerm(x, THEORY_UF) || !d_equalityEngine.isTriggerTerm(y, THEORY_UF)) {
             // Not connected to shared terms, we don't care
             continue;
           }
 
           // Get representative trigger terms
-          TNode x_shared = d_equalityEngine.getTriggerTermRepresentative(x);
-          TNode y_shared = d_equalityEngine.getTriggerTermRepresentative(y);
+          TNode x_shared = d_equalityEngine.getTriggerTermRepresentative(x, THEORY_UF);
+          TNode y_shared = d_equalityEngine.getTriggerTermRepresentative(y, THEORY_UF);
 
           EqualityStatus eqStatusDomain = d_valuation.getEqualityStatus(x_shared, y_shared);
           switch (eqStatusDomain) {
diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h
index 9017928b7..1dfcb86f0 100644
--- a/src/theory/uf/theory_uf.h
+++ b/src/theory/uf/theory_uf.h
@@ -63,8 +63,8 @@ public:
       }
     }
 
-    bool eqNotifyTriggerTermEquality(TNode t1, TNode t2, bool value) {
-      Debug("uf") << "NotifyClass::eqNotifyTriggerTermMerge(" << t1 << ", " << t2 << std::endl;
+    bool eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value) {
+      Debug("uf") << "NotifyClass::eqNotifyTriggerTermMerge(" << tag << ", " << t1 << ", " << t2 << std::endl;
       if (value) {
         return d_uf.propagate(t1.eqNode(t2));
       } else {