some improvements to the sharing mechanism/interface

4 files changed, 74 insertions, 12 deletions

diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h
index 7314b6552..d8757926a 100644
--- a/src/theory/uf/equality_engine.h
+++ b/src/theory/uf/equality_engine.h
@@ -632,6 +632,11 @@ public:
   TNode getRepresentative(TNode t) const;
 
   /**
+   * Add all the terms where the given term appears in (directly or implicitly).
+   */
+  void getUseListTerms(TNode t, std::set<TNode>& output);
+
+  /**
    * Returns true if the two nodes are in the same class.
    */
   bool areEqual(TNode t1, TNode t2) const;
@@ -663,6 +668,11 @@ public:
   bool isTriggerTerm(TNode t) const;
 
   /**
+   * Returns the representative trigger term (isTriggerTerm(t)) should be true.
+   */
+  TNode getTriggerTermRepresentative(TNode t) const;
+
+  /**
    * Adds a notify trigger for equality t1 = t2, i.e. when t1 = t2 the notify will be called with
    * trigger.
    */
diff --git a/src/theory/uf/equality_engine_impl.h b/src/theory/uf/equality_engine_impl.h
index 925410561..dd1bf0cbc 100644
--- a/src/theory/uf/equality_engine_impl.h
+++ b/src/theory/uf/equality_engine_impl.h
@@ -886,6 +886,14 @@ bool EqualityEngine<NotifyClass>::isTriggerTerm(TNode t) const {
   return d_nodeIndividualTrigger[classId] != +null_id;
 }
 
+
+template <typename NotifyClass>
+TNode EqualityEngine<NotifyClass>::getTriggerTermRepresentative(TNode t) const {
+  Assert(isTriggerTerm(t));
+  EqualityNodeId classId = getEqualityNode(t).getFind();
+  return d_nodes[d_nodeIndividualTrigger[classId]];
+}
+
 template <typename NotifyClass>
 void EqualityEngine<NotifyClass>::storeApplicationLookup(FunctionApplication& funNormalized, EqualityNodeId funId) {
   Assert(d_applicationLookup.find(funNormalized) == d_applicationLookup.end());
@@ -897,6 +905,33 @@ void EqualityEngine<NotifyClass>::storeApplicationLookup(FunctionApplication& fu
   Assert(d_applicationLookupsCount == d_applicationLookups.size());
 }
 
+template <typename NotifyClass>
+void EqualityEngine<NotifyClass>::getUseListTerms(TNode t, std::set<TNode>& output) {
+  if (hasTerm(t)) {
+    // Get the equivalence class
+    EqualityNodeId classId = getEqualityNode(t).getFind();
+    // Go through the equivalence class and get where t is used in
+    EqualityNodeId currentId = classId;
+    do {
+      // Get the current node
+      EqualityNode& currentNode = getEqualityNode(currentId);
+      // Go through the use-list
+      UseListNodeId currentUseId = currentNode.getUseList();
+      while (currentUseId != null_uselist_id) {
+        // Get the node of the use list
+        UseListNode& useNode = d_useListNodes[currentUseId];
+        // Get the function application
+        EqualityNodeId funId = useNode.getApplicationId();
+        output.insert(d_nodes[funId]);
+        // Go to the next one in the use list
+        currentUseId = useNode.getNext();
+      }
+      // Move to the next node
+      currentId = currentNode.getNext();
+    } while (currentId != classId);
+  }
+}
+
 } // Namespace uf
 } // Namespace theory
 } // Namespace CVC4
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index 7f5e11a64..f0694462d 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -396,12 +396,21 @@ void TheoryUF::ppStaticLearn(TNode n, NodeBuilder<>& learned) {
 }/* TheoryUF::ppStaticLearn() */
 
 EqualityStatus TheoryUF::getEqualityStatus(TNode a, TNode b) {
+
+  Node equality = a.eqNode(b);
+  Node rewrittenEquality = Rewriter::rewrite(equality);
+  if (rewrittenEquality.isConst()) {
+    if (!rewrittenEquality.getConst<bool>()) {
+      return EQUALITY_FALSE;
+    }
+  }
+
   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
+    // The terms are implied to be dis-equal
     return EQUALITY_FALSE;
   }
   // All other terms we interpret as dis-equal in the model
@@ -413,17 +422,19 @@ void TheoryUF::addSharedTerm(TNode t) {
   d_equalityEngine.addTriggerTerm(t);
 }
 
-void TheoryUF::computeCareGraph(CareGraph& careGraph) {
+void TheoryUF::computeCareGraph() {
 
   if (d_sharedTerms.size() > 0) {
 
-    std::vector<CarePair> currentPairs;
+    vector< pair<TNode, TNode> > 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];
@@ -462,24 +473,30 @@ void TheoryUF::computeCareGraph(CareGraph& careGraph) {
             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
+            // We don't need this one
             Debug("uf::sharing") << "TheoryUf::computeCareGraph(): equal" << std::endl;
             continue;
           }
 
+          if (!d_equalityEngine.isTriggerTerm(x) || !d_equalityEngine.isTriggerTerm(y)) {
+            // 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);
+
           // 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));
+          currentPairs.push_back(make_pair(x_shared, y_shared));
         }
 
         if (!somePairIsDisequal) {
-          careGraph.insert(careGraph.end(), currentPairs.begin(), currentPairs.end());
+          for (unsigned i = 0; i < currentPairs.size(); ++ i) {
+            addCarePair(currentPairs[i].first, currentPairs[i].second);
+          }
         }
       }
     }
diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h
index cb7674342..071883e1a 100644
--- a/src/theory/uf/theory_uf.h
+++ b/src/theory/uf/theory_uf.h
@@ -113,7 +113,7 @@ public:
   void presolve();
 
   void addSharedTerm(TNode n);
-  void computeCareGraph(CareGraph& careGraph);
+  void computeCareGraph();
 
   EqualityStatus getEqualityStatus(TNode a, TNode b);