mv default care graph function inside the theory implementation

4 files changed, 53 insertions, 14 deletions

diff --git a/src/theory/sets/theory_sets.cpp b/src/theory/sets/theory_sets.cpp
index c230b9ac5..5d5e1f9ee 100644
--- a/src/theory/sets/theory_sets.cpp
+++ b/src/theory/sets/theory_sets.cpp
@@ -34,10 +34,6 @@ TheorySets::~TheorySets() {
   delete d_internal;
 }
 
-void TheorySets::setMasterEqualityEngine(eq::EqualityEngine* eq) {
-  d_internal->setMasterEqualityEngine(eq);
-}
-
 void TheorySets::addSharedTerm(TNode n) {
   d_internal->addSharedTerm(n);
 }
@@ -50,8 +46,8 @@ void TheorySets::collectModelInfo(TheoryModel* m, bool fullModel) {
   d_internal->collectModelInfo(m, fullModel);
 }
 
-void TheorySets::propagate(Effort e) {
-  d_internal->propagate(e);
+void TheorySets::computeCareGraph() {
+  d_internal->computeCareGraph();
 }
 
 Node TheorySets::explain(TNode node) {
@@ -59,7 +55,15 @@ Node TheorySets::explain(TNode node) {
 }
 
 void TheorySets::preRegisterTerm(TNode node) {
-  return d_internal->preRegisterTerm(node);
+  d_internal->preRegisterTerm(node);
+}
+
+void TheorySets::propagate(Effort e) {
+  d_internal->propagate(e);
+}
+
+void TheorySets::setMasterEqualityEngine(eq::EqualityEngine* eq) {
+  d_internal->setMasterEqualityEngine(eq);
 }
 
 }/* CVC4::theory::sets namespace */
diff --git a/src/theory/sets/theory_sets.h b/src/theory/sets/theory_sets.h
index 6ff41d5f5..84d91de72 100644
--- a/src/theory/sets/theory_sets.h
+++ b/src/theory/sets/theory_sets.h
@@ -48,14 +48,14 @@ public:
 
   ~TheorySets();
 
-  void setMasterEqualityEngine(eq::EqualityEngine* eq);
-  
   void addSharedTerm(TNode);
 
   void check(Effort);
 
   void collectModelInfo(TheoryModel*, bool fullModel);
 
+  void computeCareGraph();
+
   Node explain(TNode);
 
   std::string identify() const { return "THEORY_SETS"; }
@@ -64,6 +64,8 @@ public:
 
   void propagate(Effort);
 
+  void setMasterEqualityEngine(eq::EqualityEngine* eq);
+
 };/* class TheorySets */
 
 }/* CVC4::theory::sets namespace */
diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index c06f1bd5e..0a7ecd14e 100644
--- a/src/theory/sets/theory_sets_private.cpp
+++ b/src/theory/sets/theory_sets_private.cpp
@@ -408,6 +408,42 @@ void TheorySetsPrivate::learnLiteral(TNode atom, bool polarity, Node reason) {
 }/*TheorySetsPrivate::learnLiteral(...)*/
 
 
+/************************ Sharing ************************/
+/************************ Sharing ************************/
+/************************ Sharing ************************/
+
+void TheorySetsPrivate::addSharedTerm(TNode n) {
+  Debug("sets") << "[sets] ThoerySetsPrivate::addSharedTerm( " << n << ")" << std::endl;
+  d_equalityEngine.addTriggerTerm(n, THEORY_SETS);
+}
+
+
+void TheorySetsPrivate::computeCareGraph() {
+  Debug("sharing") << "Theory::computeCareGraph<" << d_external.identify() << ">()" << endl;
+  for (unsigned i = 0; i < d_external.d_sharedTerms.size(); ++ i) {
+    TNode a = d_external.d_sharedTerms[i];
+    TypeNode aType = a.getType();
+    for (unsigned j = i + 1; j < d_external.d_sharedTerms.size(); ++ j) {
+      TNode b = d_external.d_sharedTerms[j];
+      if (b.getType() != aType) {
+        // We don't care about the terms of different types
+        continue;
+      }
+      switch (d_external.d_valuation.getEqualityStatus(a, b)) {
+      case EQUALITY_TRUE_AND_PROPAGATED:
+      case EQUALITY_FALSE_AND_PROPAGATED:
+        // If we know about it, we should have propagated it, so we can skip
+        break;
+      default:
+        // Let's split on it
+        d_external.addCarePair(a, b);
+        break;
+      }
+    }
+  }
+}
+
+
 /******************** Model generation ********************/
 /******************** Model generation ********************/
 /******************** Model generation ********************/
@@ -886,11 +922,6 @@ void TheorySetsPrivate::setMasterEqualityEngine(eq::EqualityEngine* eq) {
   d_equalityEngine.setMasterEqualityEngine(eq);
 }
 
-void TheorySetsPrivate::addSharedTerm(TNode n) {
-  Debug("sets") << "[sets] ThoerySetsPrivate::addSharedTerm( " << n << ")" << std::endl;
-  d_equalityEngine.addTriggerTerm(n, THEORY_SETS);
-}
-
 void TheorySetsPrivate::conflict(TNode a, TNode b)
 {
   if (a.getKind() == kind::CONST_BOOLEAN) {
diff --git a/src/theory/sets/theory_sets_private.h b/src/theory/sets/theory_sets_private.h
index 90dec7c0b..e5d7beb2c 100644
--- a/src/theory/sets/theory_sets_private.h
+++ b/src/theory/sets/theory_sets_private.h
@@ -56,6 +56,8 @@ public:
 
   void collectModelInfo(TheoryModel*, bool fullModel);
 
+  void computeCareGraph();
+
   Node explain(TNode);
 
   void preRegisterTerm(TNode node);