prep for fix

diff --git a/src/theory/sets/term_info.h b/src/theory/sets/term_info.h
index ea435d9b704da97e68bcade6baf5904cc464684a..2783faa796b8225b7f704f6505153e9269fa51c2 100644 (file)
--- a/src/theory/sets/term_info.h
+++ b/src/theory/sets/term_info.h
@@ -31,12 +31,16 @@ class TheorySetsTermInfo {
 public:
   CDTNodeList* elementsInThisSet;
   CDTNodeList* elementsNotInThisSet;
+  CDTNodeList* setsContainingThisElement;
+  CDTNodeList* setsNotContainingThisElement;
   CDTNodeList* parents;
 
   TheorySetsTermInfo(context::Context* c)
   {
     elementsInThisSet = new(true)CDTNodeList(c);
     elementsNotInThisSet = new(true)CDTNodeList(c);
+    setsContainingThisElement = new(true)CDTNodeList(c);
+    setsNotContainingThisElement = new(true)CDTNodeList(c);
     parents = new(true)CDTNodeList(c);
   }
 
@@ -45,11 +49,19 @@ public:
     else elementsNotInThisSet -> push_back(n);
   }
 
+  void addToSetList(TNode n, bool polarity) {
+    if(polarity) setsContainingThisElement -> push_back(n);
+    else setsNotContainingThisElement -> push_back(n);
+  }
+
   ~TheorySetsTermInfo() {
     elementsInThisSet -> deleteSelf();
     elementsNotInThisSet -> deleteSelf();
+    setsContainingThisElement -> deleteSelf();
+    setsNotContainingThisElement -> deleteSelf();
     parents -> deleteSelf();
   }
+
 };
 
 }/* CVC4::theory::sets namespace */

diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index 42d417fc3feaa261f60bfe546bddb5a78f32c8fb..883e0147ebf2531ff2954c27023ab85b98256846 100644 (file)
--- a/src/theory/sets/theory_sets_private.cpp
+++ b/src/theory/sets/theory_sets_private.cpp
@@ -60,10 +60,12 @@ void TheorySetsPrivate::check(Theory::Effort level) {
         if (!d_equalityEngine.hasTerm(atom[0])) {
           Assert(atom[0].isConst());
           d_equalityEngine.addTerm(atom[0]);
+          d_termInfoManager->addTerm(atom[0]);
         }
         if (!d_equalityEngine.hasTerm(atom[1])) {
           Assert(atom[1].isConst());
           d_equalityEngine.addTerm(atom[1]);
+          d_termInfoManager->addTerm(atom[1]);
         }
       }
     }
@@ -1063,6 +1065,64 @@ void TheorySetsPrivate::TermInfoManager::addTerm(TNode n) {
   }
 }
 
+void TheorySetsPrivate::TermInfoManager::pushToSettermPropagationQueue
+(TNode x, TNode S, bool polarity)
+{
+  Node cur_atom = MEMBER(x, S);
+
+  // propagation : empty set
+  if(polarity && S.getKind() == kind::EMPTYSET) {
+    Debug("sets-prop") << "[sets-prop]  something in empty set? conflict."
+                       << std::endl;
+    d_theory.learnLiteral(cur_atom, false, cur_atom);
+    return;
+  }// propagation: empty set
+
+  // propagation : children
+  if(S.getKind() == kind::UNION ||
+     S.getKind() == kind::INTERSECTION ||
+     S.getKind() == kind::SETMINUS ||
+     S.getKind() == kind::SET_SINGLETON) {
+    d_theory.d_settermPropagationQueue.push_back(std::make_pair(x, S));
+  }// propagation: children
+
+  // propagation : parents
+  const CDTNodeList* parentList = getParents(S);
+  for(typeof(parentList->begin()) k = parentList->begin();
+      k != parentList->end(); ++k) {
+    d_theory.d_settermPropagationQueue.push_back(std::make_pair(x, *k));
+  }// propagation : parents
+
+}
+
+void TheorySetsPrivate::TermInfoManager::pushToSettermPropagationQueue
+(TNode x, CDTNodeList* l, bool polarity)
+{
+  set<TNode> alreadyProcessed;
+
+  BOOST_FOREACH(TNode S, (*l) ) {
+    Debug("sets-prop") << "[sets-terminfo]  setterm todo: "
+                       << MEMBER(x, d_eqEngine->getRepresentative(S))
+                       << std::endl;
+
+    TNode repS = d_eqEngine->getRepresentative(S);
+    if(alreadyProcessed.find(repS) != alreadyProcessed.end()) {
+      continue;
+    } else {
+      alreadyProcessed.insert(repS);
+    }
+
+    d_eqEngine->addTerm(MEMBER(d_eqEngine->getRepresentative(x), repS));
+
+    for(eq::EqClassIterator j(d_eqEngine->getRepresentative(S), d_eqEngine);
+        !j.isFinished(); ++j) {
+
+      pushToSettermPropagationQueue(x, *j, polarity);
+
+    }//j loop
+  }
+}
+
 void TheorySetsPrivate::TermInfoManager::pushToSettermPropagationQueue
 (CDTNodeList* l, TNode S, bool polarity)
 {
@@ -1077,32 +1137,7 @@ void TheorySetsPrivate::TermInfoManager::pushToSettermPropagationQueue
     for(eq::EqClassIterator j(d_eqEngine->getRepresentative(S), d_eqEngine);
         !j.isFinished(); ++j) {
 
-      TNode S = (*j);
-      Node cur_atom = MEMBER(x, S);
-
-      // propagation : empty set
-      if(polarity && S.getKind() == kind::EMPTYSET) {
-        Debug("sets-prop") << "[sets-prop]  something in empty set? conflict."
-                           << std::endl;
-        d_theory.learnLiteral(cur_atom, false, cur_atom);
-        return;
-      }// propagation: empty set
-
-      // propagation : children
-      if(S.getKind() == kind::UNION ||
-         S.getKind() == kind::INTERSECTION ||
-         S.getKind() == kind::SETMINUS ||
-         S.getKind() == kind::SET_SINGLETON) {
-        d_theory.d_settermPropagationQueue.push_back(std::make_pair(x, S));
-      }// propagation: children
-
-      // propagation : parents
-      const CDTNodeList* parentList = getParents(S);
-      for(typeof(parentList->begin()) k = parentList->begin();
-          k != parentList->end(); ++k) {
-        d_theory.d_settermPropagationQueue.push_back(std::make_pair(x, *k));
-      }// propagation : parents
-
+      pushToSettermPropagationQueue(x, *j, polarity);
 
     }//j loop
 
@@ -1110,11 +1145,10 @@ void TheorySetsPrivate::TermInfoManager::pushToSettermPropagationQueue
 
 }
 
-void TheorySetsPrivate::TermInfoManager::mergeTerms(TNode a, TNode b) {
-  // merge b into a
 
-  if(!a.getType().isSet()) return;
 
+void TheorySetsPrivate::TermInfoManager::mergeTerms(TNode a, TNode b) {
+  // merge b into a
   Debug("sets-terminfo") << "[sets-terminfo] Merging (into) a = " << a
                          << ", b = " << b << std::endl;
   Debug("sets-terminfo") << "[sets-terminfo] reps"
@@ -1128,16 +1162,25 @@ void TheorySetsPrivate::TermInfoManager::mergeTerms(TNode a, TNode b) {
   Assert(ita != d_info.end());
   Assert(itb != d_info.end());
 
+  /* elements in this sets */
   pushToSettermPropagationQueue( (*ita).second->elementsInThisSet, b, true );
   pushToSettermPropagationQueue( (*ita).second->elementsNotInThisSet, b, false );
   pushToSettermPropagationQueue( (*itb).second->elementsNotInThisSet, a, false );
   pushToSettermPropagationQueue( (*itb).second->elementsInThisSet, a, true );
-
   mergeLists((*ita).second->elementsInThisSet,
              (*itb).second->elementsInThisSet);
-
   mergeLists((*ita).second->elementsNotInThisSet,
              (*itb).second->elementsNotInThisSet);
+
+  /* sets containing this element */
+  pushToSettermPropagationQueue( b, (*ita).second->setsContainingThisElement, true);
+  pushToSettermPropagationQueue( b, (*ita).second->setsNotContainingThisElement, false);
+  pushToSettermPropagationQueue( a, (*itb).second->setsNotContainingThisElement, false);
+  pushToSettermPropagationQueue( a, (*itb).second->setsContainingThisElement, true);
+  mergeLists( (*ita).second->setsContainingThisElement,
+              (*itb).second->setsContainingThisElement );
+  mergeLists( (*ita).second->setsNotContainingThisElement,
+              (*itb).second->setsNotContainingThisElement );
 }
 
 

diff --git a/src/theory/sets/theory_sets_private.h b/src/theory/sets/theory_sets_private.h
index a4c9fb726979156a708e55f061125a5cbe6789ba..7e9d609053081027f8921759311aba55a4a813bc 100644 (file)
--- a/src/theory/sets/theory_sets_private.h
+++ b/src/theory/sets/theory_sets_private.h
@@ -108,7 +108,9 @@ private:
     std::hash_map<TNode, TheorySetsTermInfo*, TNodeHashFunction> d_info;
 
     void mergeLists(CDTNodeList* la, const CDTNodeList* lb) const;
+    void pushToSettermPropagationQueue(TNode x, TNode S, bool polarity);
     void pushToSettermPropagationQueue(CDTNodeList* l, TNode S, bool polarity);
+    void pushToSettermPropagationQueue(TNode x, CDTNodeList* l, bool polarity);
   public:
     TermInfoManager(TheorySetsPrivate&,
                     context::Context* satContext,