sets stronger equality propagator

3 files changed, 60 insertions, 8 deletions

diff --git a/src/theory/sets/options b/src/theory/sets/options
index 7cb3eb677..ac040881a 100644
--- a/src/theory/sets/options
+++ b/src/theory/sets/options
@@ -14,4 +14,7 @@ option setsEagerLemmas --sets-eager-lemmas bool :default true
 option setsCare1 --sets-care1 bool :default false
  generate one lemma at a time for care graph
 
+option setsPropFull --sets-prop-full bool :default false
+ agressive propagation
+
 endmodule
diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index 4125fd193..bfcb477cb 100644
--- a/src/theory/sets/theory_sets_private.cpp
+++ b/src/theory/sets/theory_sets_private.cpp
@@ -483,9 +483,9 @@ void TheorySetsPrivate::dumpAssertionsHumanified() const
         FORIT(jt, (*kt).second.first) {
           TNode x = (*jt);
           if(x.isConst() || numbering.find(d_equalityEngine.getRepresentative(x)) == numbering.end()) {
-            Trace(tag) << x;
+            Trace(tag) << x << ", ";
           } else {
-            Trace(tag) << "x" << numbering[d_equalityEngine.getRepresentative(x)] << ", ";
+            Trace(tag) << "t" << numbering[d_equalityEngine.getRepresentative(x)] << ", ";
           }
         }
         Trace(tag) << std::endl;
@@ -495,9 +495,9 @@ void TheorySetsPrivate::dumpAssertionsHumanified() const
         FORIT(jt, (*kt).second.second) {
           TNode x = (*jt);
           if(x.isConst() || numbering.find(d_equalityEngine.getRepresentative(x)) == numbering.end()) {
-            Trace(tag) << x;
+            Trace(tag) << x << ", ";
           } else {
-            Trace(tag) << "x" << numbering[d_equalityEngine.getRepresentative(x)] << ", ";
+            Trace(tag) << "t" << numbering[d_equalityEngine.getRepresentative(x)] << ", ";
           }
         }
         Trace(tag) << std::endl;
@@ -515,6 +515,8 @@ void TheorySetsPrivate::computeCareGraph() {
     dumpAssertionsHumanified();
   }
 
+  CVC4_UNUSED unsigned edgesAddedCnt = 0;
+
   unsigned i_st = 0;
   if(options::setsCare1()) { i_st = d_ccg_i; }
   for (unsigned i = i_st; i < d_external.d_sharedTerms.size(); ++ i) {
@@ -546,6 +548,15 @@ void TheorySetsPrivate::computeCareGraph() {
         break;
       case EQUALITY_TRUE_IN_MODEL:
         d_external.addCarePair(a, b);
+        if(Trace.isOn("sharing")) {
+          ++edgesAddedCnt;
+        }
+	if(Debug.isOn("sets-care")) {
+	  Debug("sets-care") << "[sets-care] Requesting split between" << a << " and "
+			     << b << "." << std::endl << "[sets-care] " 
+			     << "  Both current have value "
+			     << d_external.d_valuation.getModelValue(a) << std::endl;
+	}
       case EQUALITY_FALSE_IN_MODEL:
         if(Trace.isOn("sets-care-performance-test")) {
           // TODO: delete these lines, only for performance testing for now
@@ -566,6 +577,7 @@ void TheorySetsPrivate::computeCareGraph() {
       }
     }
   }
+  Trace("sharing") << "TheorySetsPrivate::computeCareGraph(): size = " << edgesAddedCnt << std::endl;
 }
 
 EqualityStatus TheorySetsPrivate::getEqualityStatus(TNode a, TNode b) {
@@ -1075,8 +1087,42 @@ TheorySetsPrivate::~TheorySetsPrivate()
     Assert(d_scrutinize != NULL);
     delete d_scrutinize;
   }
-}
+}/* TheorySetsPrivate::~TheorySetsPrivate() */
+
+void TheorySetsPrivate::propagate(Theory::Effort effort) {
+  if(effort != Theory::EFFORT_FULL || !options::setsPropFull()) {
+    return;
+  }
+
+  // build a model
+  Trace("sets-prop-full") << "[sets-prop-full] propagate(FULL_EFFORT)" << std::endl;
+  dumpAssertionsHumanified();
+
+  const CDNodeSet& terms = (d_termInfoManager->d_terms);
+  for(typeof(terms.begin()) it = terms.begin(); it != terms.end(); ++it) {
+    Node node = (*it);
+    Kind k = node.getKind();
+    if(k == kind::UNION && node[0].getKind() == kind::SINGLETON ) {
+
+      if(holds(MEMBER(node[0][0], node[1]))) {
+        Trace("sets-prop-full") << "[sets-prop-full] " << MEMBER(node[0][0], node[1])
+                                << " => " << EQUAL(node[1], node) << std::endl;
+        learnLiteral(EQUAL(node[1], node), MEMBER(node[0][0], node[1]));
+      }
 
+    } else if(k == kind::UNION && node[1].getKind() == kind::SINGLETON ) {
+
+      if(holds(MEMBER(node[1][0], node[0]))) {
+        Trace("sets-prop-full") << "[sets-prop-full] " << MEMBER(node[1][0], node[0])
+                                << " => " << EQUAL(node[0], node) << std::endl;
+        learnLiteral(EQUAL(node[0], node), MEMBER(node[1][0], node[0]));
+      }
+
+    }
+  }
+
+  finishPropagation();
+}
 
 bool TheorySetsPrivate::propagate(TNode literal) {
   Debug("sets-prop") << " propagate(" << literal  << ")" << std::endl;
@@ -1094,13 +1140,14 @@ bool TheorySetsPrivate::propagate(TNode literal) {
   }
 
   return ok;
-}/* TheorySetsPropagate::propagate(TNode) */
+}/* TheorySetsPrivate::propagate(TNode) */
 
 
 void TheorySetsPrivate::setMasterEqualityEngine(eq::EqualityEngine* eq) {
   d_equalityEngine.setMasterEqualityEngine(eq);
 }
 
+
 void TheorySetsPrivate::conflict(TNode a, TNode b)
 {
   if (a.getKind() == kind::CONST_BOOLEAN) {
@@ -1139,6 +1186,7 @@ Node TheorySetsPrivate::explain(TNode literal)
   return mkAnd(assumptions);
 }
 
+
 void TheorySetsPrivate::preRegisterTerm(TNode node)
 {
   Debug("sets") << "TheorySetsPrivate::preRegisterTerm(" << node << ")"
diff --git a/src/theory/sets/theory_sets_private.h b/src/theory/sets/theory_sets_private.h
index 72c041d49..e5f160fda 100644
--- a/src/theory/sets/theory_sets_private.h
+++ b/src/theory/sets/theory_sets_private.h
@@ -66,7 +66,7 @@ public:
 
   void preRegisterTerm(TNode node);
 
-  void propagate(Theory::Effort) { /* we don't depend on this call */ }
+  void propagate(Theory::Effort);
 
 private:
   TheorySets& d_external;
@@ -112,8 +112,9 @@ private:
     TheorySetsPrivate& d_theory;
     context::Context* d_context;
     eq::EqualityEngine* d_eqEngine;
-
+  public:
     CDNodeSet d_terms;
+  private:
     std::hash_map<TNode, TheorySetsTermInfo*, TNodeHashFunction> d_info;
 
     void mergeLists(CDTNodeList* la, const CDTNodeList* lb) const;