fix a sharing issues with sets

4 files changed, 61 insertions, 27 deletions

diff --git a/src/theory/sets/kinds b/src/theory/sets/kinds
index 68941489f..e46f3a4f8 100644
--- a/src/theory/sets/kinds
+++ b/src/theory/sets/kinds
@@ -8,6 +8,7 @@ theory THEORY_SETS ::CVC4::theory::sets::TheorySets "theory/sets/theory_sets.h"
 typechecker "theory/sets/theory_sets_type_rules.h"
 rewriter ::CVC4::theory::sets::TheorySetsRewriter "theory/sets/theory_sets_rewriter.h"
 
+properties parametric
 properties check propagate #presolve postsolve
 
 # Theory content goes here.
diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index bd5324d2c..e5167dd6d 100644
--- a/src/theory/sets/theory_sets_private.cpp
+++ b/src/theory/sets/theory_sets_private.cpp
@@ -435,38 +435,36 @@ void TheorySetsPrivate::collectModelInfo(TheoryModel* m, bool fullModel)
   // Computer terms appearing assertions and shared terms
   d_external.computeRelevantTerms(terms);
 
+  // compute for each setterm elements that it contains
+  SettermElementsMap settermElementsMap;
+  TNode true_atom = NodeManager::currentNM()->mkConst<bool>(true);
+  TNode false_atom = NodeManager::currentNM()->mkConst<bool>(false);
+  for(eq::EqClassIterator it_eqclasses(true_atom, &d_equalityEngine);
+      ! it_eqclasses.isFinished() ; ++it_eqclasses) {
+    TNode n = (*it_eqclasses);
+    if(n.getKind() == kind::MEMBER) {
+      Assert(d_equalityEngine.areEqual(n, true_atom));
+      TNode x = d_equalityEngine.getRepresentative(n[0]);
+      TNode S = d_equalityEngine.getRepresentative(n[1]);
+      settermElementsMap[S].insert(x);
+    }
+  }
+
   // Assert equalities and disequalities to the model
   m->assertEqualityEngine(&d_equalityEngine, &terms);
 
-  // Loop over all collect set-terms for which we generate models
+  // Loop over terms to collect set-terms for which we generate models
   set<Node> settermsModEq;
-  SettermElementsMap settermElementsMap;
   BOOST_FOREACH(TNode term, terms) {
     TNode n = term.getKind() == kind::NOT ? term[0] : term;
 
     Debug("sets-model-details") << "[sets-model-details]  >   " << n << std::endl;
 
-    if(n.getKind() == kind::EQUAL) {
-      // nothing to do
-    } else if(n.getKind() == kind::MEMBER) {
-
-      TNode true_atom = NodeManager::currentNM()->mkConst<bool>(true);
-
-      if(d_equalityEngine.areEqual(n, true_atom)) {
-        TNode x = d_equalityEngine.getRepresentative(n[0]);
-        TNode S = d_equalityEngine.getRepresentative(n[1]);
-
-        settermElementsMap[S].insert(x);
-      }
-
-    } else if(n.getType().isSet()) {
-
+    if(n.getType().isSet()) {
       n = d_equalityEngine.getRepresentative(n);
-
       if( !n.isConst() ) {
         settermsModEq.insert(n);
       }
-
     }
 
   }
@@ -477,7 +475,6 @@ void TheorySetsPrivate::collectModelInfo(TheoryModel* m, bool fullModel)
     }
   }
 
-  // settermElementsMap processing
   BOOST_FOREACH( SettermElementsMap::value_type &it, settermElementsMap ) {
     BOOST_FOREACH( TNode element, it.second /* elements */ ) {
       Debug("sets-model-details") << "[sets-model-details]  >   " <<
diff --git a/src/theory/sets/theory_sets_rewriter.cpp b/src/theory/sets/theory_sets_rewriter.cpp
index db67576d8..82b79cbd6 100644
--- a/src/theory/sets/theory_sets_rewriter.cpp
+++ b/src/theory/sets/theory_sets_rewriter.cpp
@@ -44,8 +44,9 @@ bool checkConstantMembership(TNode elementTerm, TNode setTerm)
 // static
 RewriteResponse TheorySetsRewriter::postRewrite(TNode node) {
   NodeManager* nm = NodeManager::currentNM();
+  Kind kind = node.getKind();
 
-  switch(node.getKind()) {
+  switch(kind) {
 
   case kind::MEMBER: {
     if(!node[0].isConst() || !node[1].isConst())
@@ -54,7 +55,7 @@ RewriteResponse TheorySetsRewriter::postRewrite(TNode node) {
     // both are constants
     bool isMember = checkConstantMembership(node[0], node[1]);
     return RewriteResponse(REWRITE_DONE, nm->mkConst(isMember));
-  }
+  }//kind::MEMBER
 
   case kind::SUBSET: {
     // rewrite (A subset-or-equal B) as (A union B = B)
@@ -85,24 +86,59 @@ RewriteResponse TheorySetsRewriter::postRewrite(TNode node) {
       return RewriteResponse(REWRITE_DONE, newNode);
     }
     break;
-  }
+  }//kind::IFF
+
+  case kind::SETMINUS: {
+    if(node[0] == node[1]) {
+      Node newNode = nm->mkConst(EmptySet(nm->toType(node[0].getType())));
+      Trace("sets-postrewrite") << "Sets::postRewrite returning " << newNode << std::endl;
+      return RewriteResponse(REWRITE_DONE, newNode);
+    } else if(node[0].getKind() == kind::EMPTYSET ||
+              node[1].getKind() == kind::EMPTYSET) {
+      Trace("sets-postrewrite") << "Sets::postRewrite returning " << node[0] << std::endl;
+      return RewriteResponse(REWRITE_DONE, node[0]);
+    } else if (node[0] > node[1]) {
+      Node newNode = nm->mkNode(node.getKind(), node[1], node[0]);
+      Trace("sets-postrewrite") << "Sets::postRewrite returning " << newNode << std::endl;
+      return RewriteResponse(REWRITE_DONE, newNode);
+    }
+    break;
+  }//kind::INTERSECION
 
-  case kind::UNION:
   case kind::INTERSECTION: {
     if(node[0] == node[1]) {
       Trace("sets-postrewrite") << "Sets::postRewrite returning " << node[0] << std::endl;
       return RewriteResponse(REWRITE_DONE, node[0]);
+    } else if(node[0].getKind() == kind::EMPTYSET) {
+      return RewriteResponse(REWRITE_DONE, node[0]);
+    } else if(node[1].getKind() == kind::EMPTYSET) {
+      return RewriteResponse(REWRITE_DONE, node[1]);
     } else if (node[0] > node[1]) {
       Node newNode = nm->mkNode(node.getKind(), node[1], node[0]);
       Trace("sets-postrewrite") << "Sets::postRewrite returning " << newNode << std::endl;
       return RewriteResponse(REWRITE_DONE, newNode);
     }
     break;
-  }
+  }//kind::INTERSECION
 
-  default:
+  case kind::UNION: {
+    if(node[0] == node[1]) {
+      Trace("sets-postrewrite") << "Sets::postRewrite returning " << node[0] << std::endl;
+      return RewriteResponse(REWRITE_DONE, node[0]);
+    } else if(node[0].getKind() == kind::EMPTYSET) {
+      return RewriteResponse(REWRITE_DONE, node[1]);
+    } else if(node[1].getKind() == kind::EMPTYSET) {
+      return RewriteResponse(REWRITE_DONE, node[0]);
+    } else if (node[0] > node[1]) {
+      Node newNode = nm->mkNode(node.getKind(), node[1], node[0]);
+      Trace("sets-postrewrite") << "Sets::postRewrite returning " << newNode << std::endl;
+      return RewriteResponse(REWRITE_DONE, newNode);
+    }
     break;
+  }//kind::UNION
 
+  default:
+    break;
   }//switch(node.getKind())
 
   // This default implementation
diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp
index 4f753187f..8ec25dffd 100644
--- a/src/theory/theory_model.cpp
+++ b/src/theory/theory_model.cpp
@@ -779,7 +779,7 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel)
           << "n: " << n << endl
           << "getValue(n): " << tm->getValue(n) << endl
           << "rep: " << rep << endl;
-        Assert(tm->getValue(*eqc_i) == rep);
+        Assert(tm->getValue(*eqc_i) == rep, "run with -d check-model::rep-checking for details");
       }
     }
   }