fix a sharing issues with sets

diff --git a/src/theory/sets/kinds b/src/theory/sets/kinds
index 68941489f4bf8c7ae2c7ff70f9a081cc81468fdc..e46f3a4f81be3b2aa9956ca0f037ea849f8e5718 100644 (file)
--- 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 bd5324d2c2965df2002727ad710ec750cf0022b0..e5167dd6d5126448014f8d6223304ccbe6812745 100644 (file)
--- 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 db67576d84658b36540bf33fb357af1fadd2de6e..82b79cbd656ed1554a0ab213b2d3956c984adbbb 100644 (file)
--- 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 4f753187ffbeef6ddebf8210489599ebbc26e647..8ec25dffd8cf1abadf80bef7cc9a0766599bf1dd 100644 (file)
--- 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");
       }
     }
   }

diff --git a/test/regress/regress0/sets/sets-testlemma-ints.smt2 b/test/regress/regress0/sets/sets-testlemma-ints.smt2
index 23bde47fd62e158ce7ad9b9bb48c4daaabd3c737..c8277be71499a20456246b4fe2951b554e1c6aec 100644 (file)
--- a/test/regress/regress0/sets/sets-testlemma-ints.smt2
+++ b/test/regress/regress0/sets/sets-testlemma-ints.smt2
@@ -5,4 +5,3 @@
 (declare-fun y () (Set Int))
 (assert (= x y))
 (check-sat)
-(get-model)

diff --git a/test/regress/regress0/sets/sets-testlemma-reals.smt2 b/test/regress/regress0/sets/sets-testlemma-reals.smt2
index 97ac5841ae71110f3d2e8ef5dc963621783258db..16e7780b4f882d7704c0c1e434e39c27d9c6b98d 100644 (file)
--- a/test/regress/regress0/sets/sets-testlemma-reals.smt2
+++ b/test/regress/regress0/sets/sets-testlemma-reals.smt2
@@ -5,4 +5,3 @@
 (declare-fun y () (Set Real))
 (assert (not (= x y)))
 (check-sat)
-(get-model)