some improvements to the sharing mechanism/interface

8 files changed, 159 insertions, 33 deletions

diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp
index 0404bda3b..6460533e2 100644
--- a/src/theory/theory.cpp
+++ b/src/theory/theory.cpp
@@ -49,7 +49,7 @@ void Theory::addSharedTermInternal(TNode n) {
   addSharedTerm(n);
 }
 
-void Theory::computeCareGraph(CareGraph& careGraph) {
+void Theory::computeCareGraph() {
   Debug("sharing") << "Theory::computeCareGraph<" << getId() << ">()" << std::endl;
   for (unsigned i = 0; i < d_sharedTerms.size(); ++ i) {
     TNode a = d_sharedTerms[i];
@@ -67,7 +67,7 @@ void Theory::computeCareGraph(CareGraph& careGraph) {
   	break;
       default:
   	// Let's split on it
-  	careGraph.push_back(CarePair(a, b, getId()));
+  	addCarePair(a, b);
   	break;
       }
     }  
diff --git a/src/theory/theory.h b/src/theory/theory.h
index c84d10ca1..a8d34eab3 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -31,6 +31,7 @@
 #include "context/cdlist.h"
 #include "context/cdo.h"
 #include "util/options.h"
+#include "util/stats.h"
 #include "util/dump.h"
 
 #include <string>
@@ -71,19 +72,36 @@ struct Assertion {
 };
 
 /**
- * A pair of terms a theory cares about.
+ * A (oredered) pair of terms a theory cares about.
  */
 struct CarePair {
+
   TNode a, b;
   TheoryId theory;
+
+public:
+
   CarePair(TNode a, TNode b, TheoryId theory) 
-  : a(a), b(b), theory(theory) {}
+  : a(a < b ? a : b), b(a < b ? b : a), theory(theory) {}
+
+  bool operator == (const CarePair& other) const {
+    return (theory == other.theory) && (a == other.a) && (b == other.b);
+  }
+
+  bool operator < (const CarePair& other) const {
+    if (theory < other.theory) return true;
+    if (theory > other.theory) return false;
+    if (a < other.a) return true;
+    if (a > other.a) return false;
+    return b < other.b;
+  }
+
 };
 
 /**
  * A set of care pairs.
  */
-typedef std::vector<CarePair> CareGraph;
+typedef std::set<CarePair> CareGraph;
 
 /**
  * Base class for T-solvers.  Abstract DPLL(T).
@@ -141,9 +159,39 @@ private:
    */
   context::CDO<unsigned> d_sharedTermsIndex;
 
+  /**
+   * The care graph the theory will use during combination.
+   */
+  CareGraph* d_careGraph;
+
+  // === STATISTICS ===
+  /** time spent in theory combination */
+  TimerStat d_computeCareGraphTime;
+
+  static std::string statName(TheoryId id, const char* statName) {
+    std::stringstream ss;
+    ss << "theory<" << id << ">::" << statName;
+    return ss.str();
+  }
+
 protected:
 
   /**
+   * The only method to add suff to the care graph.
+   */
+  void addCarePair(TNode t1, TNode t2) {
+    if (d_careGraph) {
+      d_careGraph->insert(CarePair(t1, t2, d_id));
+    }
+  }
+
+  /**
+   * The function should compute the care graph over the shared terms.
+   * The default function returns all the pairs among the shared variables.
+   */
+  virtual void computeCareGraph();
+
+  /**
    * A list of shared terms that the theory has.
    */
   context::CDList<TNode> d_sharedTerms;
@@ -159,10 +207,13 @@ protected:
     d_facts(context),
     d_factsHead(context, 0),
     d_sharedTermsIndex(context, 0),
+    d_careGraph(0),
+    d_computeCareGraphTime(statName(id, "computeCareGraphTime")),
     d_sharedTerms(context),
     d_out(&out),
     d_valuation(valuation)
   {
+    StatisticsRegistry::registerStat(&d_computeCareGraphTime);
   }
 
   /**
@@ -213,14 +264,13 @@ protected:
 
   void printFacts(std::ostream& os) const;
 
-
 public:
 
   /**
    * Return the ID of the theory responsible for the given type.
    */
   static inline TheoryId theoryOf(TypeNode typeNode) {
-    Trace("theory") << "theoryOf(" << typeNode << ")" << std::endl;
+    Trace("theory::internal") << "theoryOf(" << typeNode << ")" << std::endl;
     TheoryId id;
     while (typeNode.isPredicateSubtype()) {
       typeNode = typeNode.getSubtypeBaseType();
@@ -289,6 +339,7 @@ public:
    * destructor.
    */
   virtual ~Theory() {
+    StatisticsRegistry::unregisterStat(&d_computeCareGraphTime);
   }
 
   /**
@@ -378,10 +429,15 @@ public:
   virtual void addSharedTerm(TNode n) { }
 
   /**
-   * The function should compute the care graph over the shared terms.
-   * The default function returns all the pairs among the shared variables.
+   * Return the current theory care graph. Theories should overload computeCareGraph to do
+   * the actual computation, and use addCarePair to add pairs to the care graph.
    */
-  virtual void computeCareGraph(CareGraph& careGraph);
+  void getCareGraph(CareGraph& careGraph) {
+    TimerStat::CodeTimer computeCareGraphTime(d_computeCareGraphTime);
+    d_careGraph = &careGraph;
+    computeCareGraph();
+    d_careGraph = NULL;
+  }
 
   /**
    * Return the status of two terms in the current context. Should be implemented in 
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index ebfc797a1..a3ff4d90b 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -56,6 +56,7 @@ TheoryEngine::TheoryEngine(context::Context* context,
   d_propagatedLiteralsIndex(context, 0),
   d_decisionRequests(context),
   d_decisionRequestsIndex(context, 0),
+  d_combineTheoriesTime("TheoryEngine::combineTheoriesTime"),
   d_preRegistrationVisitor(this, context),
   d_sharedTermsVisitor(d_sharedTerms)
 {
@@ -64,6 +65,7 @@ TheoryEngine::TheoryEngine(context::Context* context,
     d_theoryOut[theoryId] = NULL;
   }
   Rewriter::init();
+  StatisticsRegistry::registerStat(&d_combineTheoriesTime);
 }
 
 TheoryEngine::~TheoryEngine() {
@@ -75,6 +77,8 @@ TheoryEngine::~TheoryEngine() {
       delete d_theoryOut[theoryId];
     }
   }
+
+  StatisticsRegistry::unregisterStat(&d_combineTheoriesTime);
 }
 
 void TheoryEngine::preRegister(TNode preprocessed) {
@@ -235,29 +239,30 @@ void TheoryEngine::combineTheories() {
 
   Debug("sharing") << "TheoryEngine::combineTheories()" << std::endl;
 
+  TimerStat::CodeTimer combineTheoriesTimer(d_combineTheoriesTime);
+
   CareGraph careGraph;
 #ifdef CVC4_FOR_EACH_THEORY_STATEMENT
 #undef CVC4_FOR_EACH_THEORY_STATEMENT
 #endif
 #define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \
   if (theory::TheoryTraits<THEORY>::isParametric && isActive(THEORY)) { \
-     CareGraph theoryGraph; \
-     reinterpret_cast<theory::TheoryTraits<THEORY>::theory_class*>(theoryOf(THEORY))->computeCareGraph(theoryGraph); \
-     careGraph.insert(careGraph.end(), theoryGraph.begin(), theoryGraph.end()); \
+     reinterpret_cast<theory::TheoryTraits<THEORY>::theory_class*>(theoryOf(THEORY))->getCareGraph(careGraph); \
   }
 
   CVC4_FOR_EACH_THEORY;
 
   // Now add splitters for the ones we are interested in
-  for (unsigned i = 0; i < careGraph.size(); ++ i) {
-    const CarePair& carePair = careGraph[i];
+  CareGraph::const_iterator care_it = careGraph.begin();
+  CareGraph::const_iterator care_it_end = careGraph.end();
+  for (; care_it != care_it_end; ++ care_it) {
+    const CarePair& carePair = *care_it;
 
     Debug("sharing") << "TheoryEngine::combineTheories(): checking " << carePair.a << " = " << carePair.b << " from " << carePair.theory << std::endl;
 
     Node equality = carePair.a.eqNode(carePair.b);
     Node normalizedEquality = Rewriter::rewrite(equality);
-	bool isTrivial = normalizedEquality.getKind() == kind::CONST_BOOLEAN;
-
+    bool isTrivial = normalizedEquality.getKind() == kind::CONST_BOOLEAN;
 
     // If the node has a literal, it has been asserted so we should just check it
     bool value;
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index a8aa62d35..5712b1502 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -194,28 +194,28 @@ class TheoryEngine {
     }
 
     void conflict(TNode conflictNode) throw(AssertionException) {
-      Trace("theory") << "EngineOutputChannel<" << d_theory << ">::conflict(" << conflictNode << ")" << std::endl;
+      Trace("theory::conflict") << "EngineOutputChannel<" << d_theory << ">::conflict(" << conflictNode << ")" << std::endl;
       ++ d_statistics.conflicts;
       d_engine->d_outputChannelUsed = true;
       d_engine->conflict(conflictNode, d_theory);
     }
 
     void propagate(TNode literal) throw(AssertionException) {
-      Trace("theory") << "EngineOutputChannel<" << d_theory << ">::propagate(" << literal << ")" << std::endl;
+      Trace("theory::propagate") << "EngineOutputChannel<" << d_theory << ">::propagate(" << literal << ")" << std::endl;
       ++ d_statistics.propagations;
       d_engine->d_outputChannelUsed = true;
       d_engine->propagate(literal, d_theory);
     }
 
     void propagateAsDecision(TNode literal) throw(AssertionException) {
-      Trace("theory") << "EngineOutputChannel<" << d_theory << ">::propagateAsDecision(" << literal << ")" << std::endl;
+      Trace("theory::propagate") << "EngineOutputChannel<" << d_theory << ">::propagateAsDecision(" << literal << ")" << std::endl;
       ++ d_statistics.propagationsAsDecisions;
       d_engine->d_outputChannelUsed = true;
       d_engine->propagateAsDecision(literal, d_theory);
     }
 
     theory::LemmaStatus lemma(TNode lemma, bool removable = false) throw(TypeCheckingExceptionPrivate, AssertionException) {
-      Trace("theory") << "EngineOutputChannel<" << d_theory << ">::lemma(" << lemma << ")" << std::endl;
+      Trace("theory::lemma") << "EngineOutputChannel<" << d_theory << ">::lemma(" << lemma << ")" << std::endl;
       ++ d_statistics.lemmas;
       d_engine->d_outputChannelUsed = true;
       return d_engine->lemma(lemma, false, removable);
@@ -419,6 +419,9 @@ class TheoryEngine {
     return theory::LemmaStatus(finalForm, d_userContext->getLevel());
   }
 
+  /** Time spent in theory combination */
+  TimerStat d_combineTheoriesTime;
+
 public:
 
   /** Constructs a theory engine */
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);