Sharing work

5 files changed, 380 insertions, 58 deletions

diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h
index 18a525f2d..13b8898d5 100644
--- a/src/theory/uf/equality_engine.h
+++ b/src/theory/uf/equality_engine.h
@@ -141,7 +141,11 @@ public:
    * Creates a new node, which is in a list of it's own.
    */
   EqualityNode(EqualityNodeId nodeId = null_id)
-  : d_size(1), d_findId(nodeId), d_nextId(nodeId), d_useList(null_uselist_id) {}
+  : d_size(1), 
+    d_findId(nodeId), 
+    d_nextId(nodeId), 
+    d_useList(null_uselist_id)
+  {}
 
   /**
    * Retuerns the uselist.
@@ -266,6 +270,12 @@ public:
 
 private:
 
+  /** The context we are using */
+  context::Context* d_context;
+
+  /** Whether to notify or not (temporarily disabled on equality checks) */
+  bool d_performNotify;
+
   /** The class to notify when a representative changes for a term */
   NotifyClass d_notify;
 
@@ -455,6 +465,21 @@ 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;
+
+  /**
    * Adds the trigger with triggerId to the beginning of the trigger list of the node with id nodeId.
    */
   void addTriggerToList(EqualityNodeId nodeId, TriggerId triggerId);
@@ -503,6 +528,11 @@ private:
    */
   void debugPrintGraph() const;
 
+  /** The true node */
+  Node d_true;
+  /** The false node */
+  Node d_false;
+
 public:
 
   /**
@@ -511,15 +541,20 @@ public:
    */
   EqualityEngine(NotifyClass& notify, context::Context* context, std::string name)
   : ContextNotifyObj(context),
+    d_context(context),
+    d_performNotify(true),
     d_notify(notify),
     d_nodesCount(context, 0),
     d_assertedEqualitiesCount(context, 0),
     d_equalityTriggersCount(context, 0),
+    d_individualTriggersSize(context, 0),
     d_stats(name)
   {
     Debug("equality") << "EqualityEdge::EqualityEngine(): id_null = " << +null_id << std::endl;
     Debug("equality") << "EqualityEdge::EqualityEngine(): edge_null = " << +null_edge << std::endl;
     Debug("equality") << "EqualityEdge::EqualityEngine(): trigger_null = " << +null_trigger << std::endl;
+    d_true = NodeManager::currentNM()->mkConst<bool>(true);
+    d_false = NodeManager::currentNM()->mkConst<bool>(false);
   }
 
   /**
@@ -561,6 +596,11 @@ public:
   void addEquality(TNode t1, TNode t2, TNode reason);
 
   /**
+   * Adds an dis-equality t1 != t2 to the database.
+   */
+  void addDisequality(TNode t1, TNode t2, TNode reason);
+
+  /**
    * Returns the representative of the term t.
    */
   TNode getRepresentative(TNode t) const;
@@ -578,11 +618,38 @@ public:
   void getExplanation(TNode t1, TNode t2, std::vector<TNode>& equalities) const;
 
   /**
+   * Add term to the trigger terms. The notify class will get notified when two 
+   * trigger terms become equal. Thihs will only happen on trigger term 
+   * representatives.
+   */
+  void addTriggerTerm(TNode t);
+
+  /**
+   * Returns true if t is a trigger term or equal to some other trigger term.
+   */
+  bool isTriggerTerm(TNode t) const;
+
+  /**
    * Adds a notify trigger for equality t1 = t2, i.e. when t1 = t2 the notify will be called with
-   * (t1 = t2).
+   * trigger.
    */
   void addTriggerEquality(TNode t1, TNode t2, TNode trigger);
 
+  /**
+   * Adds a notify trigger for dis-equality t1 != t2, i.e. when t1 != t2 the notify will be called with
+   * trigger.
+   */
+  void addTriggerDisequality(TNode t1, TNode t2, TNode trigger);
+
+  /**
+   * Check whether the two terms are equal.
+   */
+  bool areEqual(TNode t1, TNode t2);
+
+  /**
+   * Check whether the two term are dis-equal.
+   */
+  bool areDisequal(TNode t1, TNode t2);
 };
 
 } // Namespace uf
diff --git a/src/theory/uf/equality_engine_impl.h b/src/theory/uf/equality_engine_impl.h
index b31d04a32..77c8e80b4 100644
--- a/src/theory/uf/equality_engine_impl.h
+++ b/src/theory/uf/equality_engine_impl.h
@@ -91,6 +91,8 @@ EqualityNodeId EqualityEngine<NotifyClass>::newNode(TNode node, bool isApplicati
   d_nodeTriggers.push_back(+null_trigger);
   // Add it to the equality graph
   d_equalityGraph.push_back(+null_edge);
+  // Mark the no-individual trigger
+  d_nodeIndividualTrigger.push_back(+null_id);
   // Add the equality node to the nodes
   d_equalityNodes.push_back(EqualityNode(newId));
 
@@ -176,15 +178,27 @@ void EqualityEngine<NotifyClass>::addEquality(TNode t1, TNode t2, TNode reason)
   Debug("equality") << "EqualityEngine::addEquality(" << t1 << "," << t2 << ")" << std::endl;
 
   // Add the terms if they are not already in the database
-  EqualityNodeId t1Id = getNodeId(t1);
-  EqualityNodeId t2Id = getNodeId(t2);
+  addTerm(t1);
+  addTerm(t2);
 
   // Add to the queue and propagate
+  EqualityNodeId t1Id = getNodeId(t1);
+  EqualityNodeId t2Id = getNodeId(t2);
   enqueue(MergeCandidate(t1Id, t2Id, MERGED_THROUGH_EQUALITY, reason));
   propagate();
 }
 
 template <typename NotifyClass>
+void EqualityEngine<NotifyClass>::addDisequality(TNode t1, TNode t2, TNode reason) {
+
+  Debug("equality") << "EqualityEngine::addDisequality(" << t1 << "," << t2 << ")" << std::endl;
+
+  Node equality = t1.eqNode(t2);
+  addEquality(equality, d_false, reason);
+}
+
+
+template <typename NotifyClass>
 TNode EqualityEngine<NotifyClass>::getRepresentative(TNode t) const {
 
   Debug("equality") << "EqualityEngine::getRepresentative(" << t << ")" << std::endl;
@@ -304,6 +318,24 @@ void EqualityEngine<NotifyClass>::merge(EqualityNode& class1, EqualityNode& clas
 
   // Now merge the lists
   class1.merge<true>(class2);
+
+  // Notfiy the triggers
+  EqualityNodeId class1triggerId = d_nodeIndividualTrigger[class1Id];
+  EqualityNodeId class2triggerId = d_nodeIndividualTrigger[class2Id];
+  if (class2triggerId != +null_id) {
+    if (class1triggerId == +null_id) {
+      // If class1 is not an individual trigger, but class2 is, mark it
+      d_nodeIndividualTrigger[class1Id] = class2triggerId;
+      // Add it to the list for backtracking
+      d_individualTriggers.push_back(class1Id);
+      d_individualTriggersSize = d_individualTriggersSize + 1;  
+    } else {
+      // Notify when done
+      if (d_performNotify) {
+        d_notify.notify(d_nodes[class1triggerId], d_nodes[class2triggerId]); 
+      }
+    }	
+  }
 }
 
 template <typename NotifyClass>
@@ -437,11 +469,19 @@ void EqualityEngine<NotifyClass>::backtrack() {
     d_equalityEdges.resize(2 * d_assertedEqualitiesCount);
   }
 
+  if (d_individualTriggers.size() > d_individualTriggersSize) {
+    // 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;
+    }
+    d_individualTriggers.resize(d_individualTriggersSize);
+  }
+  
   if (d_equalityTriggers.size() > d_equalityTriggersCount) {
     // Unlink the triggers from the lists
     for (int i = d_equalityTriggers.size() - 1, i_end = d_equalityTriggersCount; i >= i_end; -- i) {
-    	const Trigger& trigger = d_equalityTriggers[i];
-    	d_nodeTriggers[trigger.classId] = trigger.nextTrigger;
+      const Trigger& trigger = d_equalityTriggers[i];
+      d_nodeTriggers[trigger.classId] = trigger.nextTrigger;
     }
     // Get rid of the triggers 
     d_equalityTriggers.resize(d_equalityTriggersCount);
@@ -470,6 +510,7 @@ void EqualityEngine<NotifyClass>::backtrack() {
     d_nodes.resize(d_nodesCount);
     d_applications.resize(d_nodesCount);
     d_nodeTriggers.resize(d_nodesCount);
+    d_nodeIndividualTrigger.resize(d_nodesCount);
     d_equalityGraph.resize(d_nodesCount);
     d_equalityNodes.resize(d_nodesCount);
   }
@@ -614,6 +655,13 @@ void EqualityEngine<NotifyClass>::getExplanation(EqualityNodeId t1Id, EqualityNo
 }
 
 template <typename NotifyClass>
+void EqualityEngine<NotifyClass>::addTriggerDisequality(TNode t1, TNode t2, TNode trigger) {
+  Node equality = t1.eqNode(t2);
+  addTerm(equality);
+  addTriggerEquality(equality, d_false, trigger);
+}
+
+template <typename NotifyClass>
 void EqualityEngine<NotifyClass>::addTriggerEquality(TNode t1, TNode t2, TNode trigger) {
 
   Debug("equality") << "EqualityEngine::addTrigger(" << t1 << ", " << t2 << ", " << trigger << ")" << std::endl;
@@ -651,7 +699,9 @@ void EqualityEngine<NotifyClass>::addTriggerEquality(TNode t1, TNode t2, TNode t
   // If the trigger is already on, we propagate
   if (t1classId == t2classId) {
     Debug("equality") << "EqualityEngine::addTrigger(" << t1 << "," << t2 << "): triggered at setup time" << std::endl;
-    d_notify.notifyEquality(trigger); // Don't care about the return value
+    if (d_performNotify) {
+      d_notify.notify(trigger); // Don't care about the return value
+    }
   }
 
   Debug("equality") << "EqualityEngine::addTrigger(" << t1 << "," << t2 << ") => (" << t1NewTriggerId << ", " << t2NewTriggerId << ")" << std::endl;
@@ -690,31 +740,30 @@ void EqualityEngine<NotifyClass>::propagate() {
     Assert(node1.getFind() == t1classId);
     Assert(node2.getFind() == t2classId);
 
+    // Add the actuall equality to the equality graph
+    addGraphEdge(current.t1Id, current.t2Id, current.type, current.reason);
+
+    // One more equality added
+    d_assertedEqualitiesCount = d_assertedEqualitiesCount + 1;
+
     // Depending on the merge preference (such as size), merge them
     std::vector<TriggerId> triggers;
     if (node2.getSize() > node1.getSize()) {
       Debug("equality") << "EqualityEngine::propagate(): merging " << d_nodes[current.t1Id]<< " into " << d_nodes[current.t2Id] << std::endl;
-      merge(node2, node1, triggers);
       d_assertedEqualities.push_back(Equality(t2classId, t1classId));
+      merge(node2, node1, triggers);
     } else {
       Debug("equality") << "EqualityEngine::propagate(): merging " << d_nodes[current.t2Id] << " into " << d_nodes[current.t1Id] << std::endl;
-      merge(node1, node2, triggers);
       d_assertedEqualities.push_back(Equality(t1classId, t2classId));
+      merge(node1, node2, triggers);
     }
 
-    // Add the actuall equality to the equality graph
-    addGraphEdge(current.t1Id, current.t2Id, current.type, current.reason);
-
-    // One more equality added
-    d_assertedEqualitiesCount = d_assertedEqualitiesCount + 1;
-
-    Assert(2*d_assertedEqualities.size() == d_equalityEdges.size());
-    Assert(d_assertedEqualities.size() == d_assertedEqualitiesCount);
-
     // Notify the triggers
-    for (size_t trigger = 0, trigger_end = triggers.size(); trigger < trigger_end && !done; ++ trigger) {
-      // Notify the trigger and exit if it fails
-      done = !d_notify.notifyEquality(d_equalityTriggersOriginal[triggers[trigger]]);
+    if (d_performNotify) {
+      for (size_t trigger = 0, trigger_end = triggers.size(); trigger < trigger_end && !done; ++ trigger) {
+        // Notify the trigger and exit if it fails
+        done = !d_notify.notify(d_equalityTriggersOriginal[triggers[trigger]]);
+      }
     }
   }
 }
@@ -736,6 +785,108 @@ void EqualityEngine<NotifyClass>::debugPrintGraph() const {
   }
 }
 
+class ScopedBool {
+  bool& watch;
+  bool oldValue;
+public:
+  ScopedBool(bool& watch, bool newValue)
+  : watch(watch), oldValue(watch) {
+    watch = newValue;
+  }
+  ~ScopedBool() {
+    watch = oldValue;
+  }
+};
+
+template <typename NotifyClass>
+bool EqualityEngine<NotifyClass>::areEqual(TNode t1, TNode t2)
+{
+  // Don't notify during this check
+  ScopedBool turnOfNotify(d_performNotify, false);
+
+  // Push the context, so that we can remove the terms later
+  d_context->push();
+
+  // Add the terms
+  addTerm(t1);
+  addTerm(t2);
+  bool equal = getEqualityNode(t1).getFind() == getEqualityNode(t2).getFind();
+
+  // Pop the context (triggers new term removal)
+  d_context->pop();
+
+  // Return whether the two terms are equal
+  return equal;
+}
+
+template <typename NotifyClass>
+bool EqualityEngine<NotifyClass>::areDisequal(TNode t1, TNode t2)
+{
+  // Don't notify during this check
+  ScopedBool turnOfNotify(d_performNotify, false);
+
+  // Push the context, so that we can remove the terms later
+  d_context->push();
+
+  // Add the terms
+  addTerm(t1);
+  addTerm(t2);
+
+  // Check (t1 = t2) = false
+  Node equality1 = t1.eqNode(t2);
+  addTerm(equality1);
+  if (getEqualityNode(equality1).getFind() == getEqualityNode(d_false).getFind()) {
+    return true;
+  }
+
+  // Check (t2 = t1) = false
+  Node equality2 = t2.eqNode(t1);
+  addTerm(equality2);
+  if (getEqualityNode(equality2).getFind() == getEqualityNode(d_false).getFind()) {
+    return true;
+  }
+
+  // Pop the context (triggers new term removal)
+  d_context->pop();
+
+  // Return whether the terms are disequal
+  return false;
+}
+
+template <typename NotifyClass>
+void EqualityEngine<NotifyClass>::addTriggerTerm(TNode t) 
+{
+  Debug("equality::internal") << "EqualityEngine::addTriggerTerm(" << t << ")" << std::endl;
+
+  // Add the term if it's not already there
+  addTerm(t);
+
+  // Get the node id
+  EqualityNodeId eqNodeId = getNodeId(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
+    if (d_performNotify) {
+      d_notify.notify(t, d_nodes[d_nodeIndividualTrigger[classId]]); 
+    }
+  } else {
+    // 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;
+  }
+}
+
+template <typename NotifyClass>
+bool  EqualityEngine<NotifyClass>::isTriggerTerm(TNode t) const {
+  if (!hasTerm(t)) return false;
+  EqualityNodeId classId = getEqualityNode(t).getFind();
+  return d_nodeIndividualTrigger[classId] != +null_id;
+}
+
 } // Namespace uf
 } // Namespace theory
 } // Namespace CVC4
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index 84fad2f19..3c28e9d9d 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -50,34 +50,38 @@ Node mkAnd(const std::vector<TNode>& conjunctions) {
 
 void TheoryUF::check(Effort level) {
 
-  while (!done() && !d_conflict) {
+  while (!done() && !d_conflict) 
+  {
     // Get all the assertions
-    TNode assertion = get();
-    Debug("uf") << "TheoryUF::check(): processing " << assertion << std::endl;
+    Assertion assertion = get();
+    TNode fact = assertion.assertion;
 
-    // Fo the work
-    switch (assertion.getKind()) {
+    Debug("uf") << "TheoryUF::check(): processing " << fact << std::endl;
+
+    // If the assertion doesn't have a literal, it's a shared equality, so we set it up
+    if (!assertion.isPreregistered) {
+      Debug("uf") << "TheoryUF::check(): shared equality, setting up " << fact << std::endl;
+      if (fact.getKind() == kind::NOT) {
+        preRegisterTerm(fact[0]);
+      } else {
+        preRegisterTerm(fact);
+      }
+    }
+
+    // Do the work
+    switch (fact.getKind()) {
     case kind::EQUAL:
-      d_equalityEngine.addEquality(assertion[0], assertion[1], assertion);
+      d_equalityEngine.addEquality(fact[0], fact[1], fact);
       break;
     case kind::APPLY_UF:
-      d_equalityEngine.addEquality(assertion, d_true, assertion);
+      d_equalityEngine.addEquality(fact, d_true, fact);
       break;
     case kind::NOT:
-      if (assertion[0].getKind() == kind::APPLY_UF) {
-        d_equalityEngine.addEquality(assertion[0], d_false, assertion);
+      if (fact[0].getKind() == kind::APPLY_UF) {
+        d_equalityEngine.addEquality(fact[0], d_false, fact);
       } else {
-        // Disequality check
-        TNode equality = assertion[0];
-        if (d_equalityEngine.getRepresentative(equality[0]) == d_equalityEngine.getRepresentative(equality[1])) {
-          std::vector<TNode> assumptions;
-          assumptions.push_back(assertion);
-          explain(equality, assumptions);
-          d_conflictNode = mkAnd(assumptions);
-          d_conflict = true;
-        }
         // Assert the dis-equality
-        d_equalityEngine.addEquality(assertion[0], d_false, assertion);
+        d_equalityEngine.addDisequality(fact[0][0], fact[0][1], fact);
       }
       break;
     default:
@@ -138,9 +142,7 @@ void TheoryUF::preRegisterTerm(TNode node) {
     d_equalityEngine.addTerm(node[1]);
     // Add the trigger for equality
     d_equalityEngine.addTriggerEquality(node[0], node[1], node);
-	// Add the disequality terms and triggers
-	d_equalityEngine.addTerm(node);
-	d_equalityEngine.addTriggerEquality(node, d_false, node.notNode());
+    d_equalityEngine.addTriggerDisequality(node[0], node[1], node.notNode());
     break;
   case kind::APPLY_UF:
     // Function applications/predicates
@@ -151,6 +153,8 @@ void TheoryUF::preRegisterTerm(TNode node) {
       d_equalityEngine.addTriggerEquality(node, d_true, node);
       d_equalityEngine.addTriggerEquality(node, d_false, node.notNode());
     }
+    // Remember the function and predicate terms
+    d_functionsTerms.push_back(node);
     break;
   default:
     // Variables etc
@@ -359,3 +363,94 @@ void TheoryUF::staticLearning(TNode n, NodeBuilder<>& learned) {
     d_symb.assertFormula(n);
   }
 }
+
+EqualityStatus TheoryUF::getEqualityStatus(TNode a, TNode b) {
+  if (d_equalityEngine.areEqual(a, b)) {
+    // The terms are implied to be equal
+    return EQUALITY_TRUE;
+  }
+  if (d_equalityEngine.areDisequal(a, b)) {
+    // The rems are implied to be dis-equal
+    return EQUALITY_FALSE;
+  }
+  // All other terms we interpret as dis-equal in the model
+  return EQUALITY_FALSE_IN_MODEL;
+}
+
+void TheoryUF::addSharedTerm(TNode t) {
+  Debug("uf::sharing") << "TheoryUF::addSharedTerm(" << t << ")" << std::endl;
+  d_equalityEngine.addTriggerTerm(t);
+}
+
+void TheoryUF::computeCareGraph(CareGraph& careGraph) {
+
+  if (d_sharedTerms.size() > 0) {
+
+    std::vector<CarePair> currentPairs;
+
+    // Go through the function terms and see if there are any to split on
+    unsigned functionTerms = d_functionsTerms.size();
+    for (unsigned i = 0; i < functionTerms; ++ i) {
+      TNode f1 = d_functionsTerms[i];
+      Node op = f1.getOperator();
+      for (unsigned j = i + 1; j < functionTerms; ++ j) {
+
+        TNode f2 = d_functionsTerms[j];
+
+        // If the operators are not the same, we can skip this pair
+        if (f2.getOperator() != op) {
+          continue;
+        }
+
+        Debug("uf::sharing") << "TheoryUf::computeCareGraph(): checking function " << f1 << " and " << f2 << std::endl;
+
+        // If the terms are already known to be equal, we are also in good shape
+        if (d_equalityEngine.areEqual(f1, f2)) {
+          Debug("uf::sharing") << "TheoryUf::computeCareGraph(): equal, skipping" << std::endl;
+          continue;
+        }
+
+        // We have two functions f(x1, ..., xn) and f(y1, ..., yn) no known to be equal
+        // We split on the argument pairs that are are not known, unless there is some
+        // argument pair that is already dis-equal.
+        bool somePairIsDisequal = false;
+        currentPairs.clear();
+        for (unsigned k = 0; k < f1.getNumChildren(); ++ k) {
+
+          TNode x = f1[k];
+          TNode y = f2[k];
+
+          Debug("uf::sharing") << "TheoryUf::computeCareGraph(): checking arguments " << x << " and " << y << std::endl;
+
+          EqualityStatus eqStatusUf = getEqualityStatus(x, y);
+
+          if (eqStatusUf == EQUALITY_FALSE) {
+            // Mark that there is a dis-equal pair and break
+            somePairIsDisequal = true;
+            Debug("uf::sharing") << "TheoryUf::computeCareGraph(): disequal, disregarding all" << std::endl;
+            break;
+          }
+
+	    	  if (!d_equalityEngine.isTriggerTerm(x) || !d_equalityEngine.isTriggerTerm(y)) {
+	    	    // Not connected to shared terms, we don't care
+	    	    continue;
+	    	  }
+
+          if (eqStatusUf == EQUALITY_TRUE) {
+            // We don't neeed this one
+            Debug("uf::sharing") << "TheoryUf::computeCareGraph(): equal" << std::endl;
+            continue;
+          }
+
+          // Otherwise, we need to figure it out
+          Debug("uf::sharing") << "TheoryUf::computeCareGraph(): adding to care-graph" << std::endl;
+          currentPairs.push_back(CarePair(x, y, THEORY_UF));
+        }
+
+        if (!somePairIsDisequal) {
+          careGraph.insert(careGraph.end(), currentPairs.begin(), currentPairs.end());
+        }
+      }
+    }
+  }
+}
diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h
index f8e17b1de..769caba5c 100644
--- a/src/theory/uf/theory_uf.h
+++ b/src/theory/uf/theory_uf.h
@@ -44,10 +44,16 @@ public:
   public:
     NotifyClass(TheoryUF& uf): d_uf(uf) {}
 
-    bool notifyEquality(TNode reason) {
-      Debug("uf") << "NotifyClass::notifyEquality(" << reason << ")" << std::endl;
+    bool notify(TNode propagation) {
+      Debug("uf") << "NotifyClass::notify(" << propagation << ")" << std::endl;
       // Just forward to uf
-      return d_uf.propagate(reason);
+      return d_uf.propagate(propagation);
+    }
+    
+    void notify(TNode t1, TNode t2) {
+      Debug("uf") << "NotifyClass::notify(" << t1 << ", " << t2 << ")" << std::endl;
+      Node equality = Rewriter::rewriteEquality(theory::THEORY_UF, t1.eqNode(t2));
+      d_uf.propagate(equality);
     }
   };
 
@@ -59,9 +65,6 @@ private:
   /** Equaltity engine */
   EqualityEngine<NotifyClass> d_equalityEngine;
 
-  /** All the literals known to be true */
-  context::CDSet<TNode, TNodeHashFunction> d_knownFacts;
-
   /** Are we in conflict */
   context::CDO<bool> d_conflict;
 
@@ -79,11 +82,13 @@ private:
   void explain(TNode literal, std::vector<TNode>& assumptions);
 
   /** Literals to propagate */
-  context::CDList<TNode> d_literalsToPropagate;
+  context::CDList<Node> d_literalsToPropagate;
 
   /** Index of the next literal to propagate */
   context::CDO<unsigned> d_literalsToPropagateIndex;
 
+  /** All the function terms that the theory has seen */
+  context::CDList<TNode> d_functionsTerms;
 
   /** True node for predicates = true */
   Node d_true;
@@ -101,10 +106,10 @@ public:
     Theory(THEORY_UF, c, u, out, valuation),
     d_notify(*this),
     d_equalityEngine(d_notify, c, "theory::uf::TheoryUF"),
-    d_knownFacts(c),
     d_conflict(c, false),
     d_literalsToPropagate(c),
-    d_literalsToPropagateIndex(c, 0)
+    d_literalsToPropagateIndex(c, 0),
+    d_functionsTerms(c)
   {
     // The kinds we are treating as function application in congruence
     d_equalityEngine.addFunctionKind(kind::APPLY_UF);
@@ -126,6 +131,11 @@ public:
   void staticLearning(TNode in, NodeBuilder<>& learned);
   void presolve();
 
+  void addSharedTerm(TNode n);
+  void computeCareGraph(CareGraph& careGraph);
+
+  EqualityStatus getEqualityStatus(TNode a, TNode b);
+
   std::string identify() const {
     return "THEORY_UF";
   }
diff --git a/src/theory/uf/theory_uf_rewriter.h b/src/theory/uf/theory_uf_rewriter.h
index e1aba2c95..be4906ab6 100644
--- a/src/theory/uf/theory_uf_rewriter.h
+++ b/src/theory/uf/theory_uf_rewriter.h
@@ -39,12 +39,7 @@ public:
       }
       if (node[0] > node[1]) {
         Node newNode = NodeManager::currentNM()->mkNode(node.getKind(), node[1], node[0]);
-        // If we've switched theories, we need to rewrite again (TODO: THIS IS HACK, once theories accept eq, change)
-        if (Theory::theoryOf(newNode[0]) != Theory::theoryOf(newNode[1])) {
-          return RewriteResponse(REWRITE_AGAIN_FULL, newNode);
-        } else {
-          return RewriteResponse(REWRITE_DONE, newNode);
-        }
+        return RewriteResponse(REWRITE_DONE, newNode);
       }
     }
     return RewriteResponse(REWRITE_DONE, node);
@@ -59,6 +54,10 @@ public:
     return RewriteResponse(REWRITE_DONE, node);
   }
 
+  static Node rewriteEquality(TNode equality) {
+    return postRewrite(equality).node;
+  }
+
   static inline void init() {}
   static inline void shutdown() {}