sets: fix a bug in model building, another in handling set of sets

diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index 9d00cde7b82e115a7013764eec019c3e75097571..af96b50d06c410254fb63b045117b4a0f65a7d24 100644 (file)
--- a/src/theory/sets/theory_sets_private.cpp
+++ b/src/theory/sets/theory_sets_private.cpp
@@ -190,6 +190,29 @@ void TheorySetsPrivate::assertMemebership(TNode fact, TNode reason, bool learnt)
     return;
   }
 
+  /**
+   * Disequality propagation if element type is set
+   */
+  if(x.getType().isSet()) {
+    if(polarity) {
+      const CDTNodeList* l = d_termInfoManager->getNonMembers(S);
+      for(typeof(l->begin()) it = l->begin(); it != l->end(); ++it) {
+        TNode n = *it;
+        learnLiteral( /* atom = */ EQUAL(x, n),
+                      /* polarity = */ false,
+                      /* reason = */ AND( MEMBER(x, S), NOT( MEMBER(n, S)) ) );
+      }
+    } else {
+      const CDTNodeList* l = d_termInfoManager->getMembers(S);
+      for(typeof(l->begin()) it = l->begin(); it != l->end(); ++it) {
+        TNode n = *it;
+        learnLiteral( /* atom = */ EQUAL(x, n),
+                      /* polarity = */ false,
+                      /* reason = */ AND( NOT(MEMBER(x, S)), MEMBER(n, S)) );
+      }
+    }
+  }
+
   for(; !j.isFinished(); ++j) {
     TNode S = (*j);
     Node cur_atom = MEMBER(x, S);
@@ -227,7 +250,10 @@ void TheorySetsPrivate::doSettermPropagation(TNode x, TNode S)
   Debug("sets-prop") << "[sets-prop] doSettermPropagation("
                      << x << ", " << S << std::endl;
 
-  Assert(S.getType().isSet() && S.getType().getSetElementType() == x.getType());
+  Assert(S.getType().isSet() && S.getType().getSetElementType() == x.getType(),
+         ( std::string("types of S and x are ") + S.getType().toString() +
+           std::string(" and ") + x.getType().toString() +
+           std::string(" respectively") ).c_str()  );
 
   Node literal, left_literal, right_literal;
 
@@ -416,7 +442,8 @@ const TheorySetsPrivate::Elements& TheorySetsPrivate::getElements
         Unhandled();
       }
     } else {
-      Assert(k == kind::VARIABLE || k == kind::APPLY_UF);
+      Assert(k == kind::VARIABLE || k == kind::APPLY_UF || k == kind::SKOLEM,
+             (std::string("Expect variable or UF got ") + kindToString(k)).c_str() );
       /* assign emptyset, which is default */
     }
 
@@ -598,6 +625,7 @@ void TheorySetsPrivate::collectModelInfo(TheoryModel* m, bool fullModel)
   BOOST_FOREACH( TNode setterm, settermsModEq ) {
     Elements elements = getElements(setterm, settermElementsMap);
     Node shape = elementsToShape(elements, setterm.getType());
+    shape = theory::Rewriter::rewrite(shape);
     m->assertEquality(shape, setterm, true);
     m->assertRepresentative(shape);
   }
@@ -1042,6 +1070,14 @@ const CDTNodeList* TheorySetsPrivate::TermInfoManager::getParents(TNode x) {
   return d_info[x]->parents;
 }
 
+const CDTNodeList* TheorySetsPrivate::TermInfoManager::getMembers(TNode S) {
+  return d_info[S]->elementsInThisSet;
+}
+
+const CDTNodeList* TheorySetsPrivate::TermInfoManager::getNonMembers(TNode S) {
+  return d_info[S]->elementsNotInThisSet;
+}
+
 void TheorySetsPrivate::TermInfoManager::addTerm(TNode n) {
   unsigned numChild = n.getNumChildren();
 
@@ -1052,8 +1088,7 @@ void TheorySetsPrivate::TermInfoManager::addTerm(TNode n) {
 
   if(n.getKind() == kind::UNION ||
      n.getKind() == kind::INTERSECTION ||
-     n.getKind() == kind::SETMINUS ||
-     n.getKind() == kind::SET_SINGLETON) {
+     n.getKind() == kind::SETMINUS) {
 
     for(unsigned i = 0; i < numChild; ++i) {
       if(d_terms.contains(n[i])) {

diff --git a/src/theory/sets/theory_sets_private.h b/src/theory/sets/theory_sets_private.h
index 7e9d609053081027f8921759311aba55a4a813bc..9225bfbfd459b5d55e87851ec3f43951d1015d9e 100644 (file)
--- a/src/theory/sets/theory_sets_private.h
+++ b/src/theory/sets/theory_sets_private.h
@@ -118,6 +118,8 @@ private:
     ~TermInfoManager();
     void notifyMembership(TNode fact);
     const CDTNodeList* getParents(TNode x);
+    const CDTNodeList* getMembers(TNode S);
+    const CDTNodeList* getNonMembers(TNode S);
     void addTerm(TNode n);
     void mergeTerms(TNode a, TNode b);
   };

diff --git a/src/theory/sets/theory_sets_rewriter.cpp b/src/theory/sets/theory_sets_rewriter.cpp
index 328592abb63a8eaa7a7e08326442c4fe12dd99b8..bcfbc46ae8d61352d53dac09f9d91c2d8c3b3f7d 100644 (file)
--- a/src/theory/sets/theory_sets_rewriter.cpp
+++ b/src/theory/sets/theory_sets_rewriter.cpp
@@ -201,12 +201,13 @@ const Elements& collectConstantElements(TNode setterm, SettermElementsMap& sette
         break;
       case kind::SET_SINGLETON:
         Assert(setterm[0].isConst());
-        cur.insert(setterm[0]);
+        cur.insert(TheorySetsRewriter::preRewrite(setterm[0]).node);
         break;
       default:
         Unhandled();
       }
     }
+    Debug("sets-rewrite-constant") << "[sets-rewrite-constant] "<< setterm << " " << setterm.getId() << std::endl;
 
     it = settermElementsMap.insert(SettermElementsMap::value_type(setterm, cur)).first;
   }
@@ -246,7 +247,10 @@ RewriteResponse TheorySetsRewriter::preRewrite(TNode node) {
     //rewrite set to normal form
     SettermElementsMap setTermElementsMap;   // cache
     const Elements& elements = collectConstantElements(node, setTermElementsMap);
-    return RewriteResponse(REWRITE_DONE, elementsToNormalConstant(elements, node.getType()));
+    RewriteResponse response(REWRITE_DONE, elementsToNormalConstant(elements, node.getType()));
+    Debug("sets-rewrite-constant") << "[sets-rewrite-constant] Rewriting " << node << std::endl
+                                   << "[sets-rewrite-constant]        to " << response.node << std::endl;
+    return response;
   }
 
   return RewriteResponse(REWRITE_DONE, node);

diff --git a/src/theory/sets/theory_sets_rewriter.h b/src/theory/sets/theory_sets_rewriter.h
index 715817508b4b861c0f60032199ab060752278d69..6ce418e85c730258e48ee663aa52932563d79c00 100644 (file)
--- a/src/theory/sets/theory_sets_rewriter.h
+++ b/src/theory/sets/theory_sets_rewriter.h
@@ -83,7 +83,6 @@ public:
   static inline void shutdown() {
     // nothing to do
   }
-
 };/* class TheorySetsRewriter */
 
 }/* CVC4::theory::sets namespace */

diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp
index 203f116bb9bbdbeb4497f16bd91a1becec82e346..6c0018c054ba5ffdeadb149eb3e62d3b37d5c088 100644 (file)
--- a/src/theory/theory_model.cpp
+++ b/src/theory/theory_model.cpp
@@ -70,8 +70,8 @@ Node TheoryModel::getValue(TNode n) const {
     //normalize
     nn = Rewriter::rewrite(nn);
   }
-  Debug("model-getvalue") << "[model-getvalue] getValue( " << n << " ):  returning"
-                          << nn << std::endl;
+  Debug("model-getvalue") << "[model-getvalue] getValue( " << n << " ): " << std::endl
+                          << "[model-getvalue] returning " << nn << std::endl;
   return nn;
 }
 

diff --git a/test/regress/regress0/sets/Makefile.am b/test/regress/regress0/sets/Makefile.am
index 6d718553d1db93679cf3e710f155f8ea94a6e8db..7f1f074614e6ea275a77b3dd7a40f79c8779b46a 100644 (file)
--- a/test/regress/regress0/sets/Makefile.am
+++ b/test/regress/regress0/sets/Makefile.am
@@ -31,6 +31,7 @@ TESTS =       \
        jan24/remove_check_free_31_6.smt2 \
        sets-inter.smt2 \
        sets-equal.smt2 \
+       sets-disequal.smt2 \
        union-2.smt2 \
        jan27/deepmeas0.hs.fqout.cvc4.41.smt2 \
        jan27/ListConcat.hs.fqout.cvc4.177.smt2 \
@@ -69,10 +70,10 @@ EXTRA_DIST = $(TESTS)
 #TESTS += \
 #      error.cvc
 #endif
-#
-# and make sure to distribute it
-#EXTRA_DIST += \
-#      error.cvc
+
+# disabled tests, yet distribute
+EXTRA_DIST += \
+       setofsets-disequal.smt2
 
 # synonyms for "check"
 .PHONY: regress regress0 test

diff --git a/test/regress/regress0/sets/setofsets-disequal.smt2 b/test/regress/regress0/sets/setofsets-disequal.smt2
new file mode 100644 (file)
index 0000000..907e074
--- /dev/null
+++ b/test/regress/regress0/sets/setofsets-disequal.smt2
@@ -0,0 +1,64 @@
+; On a production build (as of 2014-05-16), takes several minutes
+; to finish (2967466 decisions).
+
+(set-logic QF_BV_SETS)
+(set-info :status unsat)
+
+(define-sort myset () (Set (Set (_ BitVec 1))))
+(declare-fun S () myset)
+
+; 0 elements
+(assert (not (= S (as emptyset myset))))
+
+; 1 element is S
+(assert (not (= S (setenum (as emptyset (Set (_ BitVec 1)))))))
+(assert (not (= S (setenum (setenum (_ bv0 1)) ))))
+(assert (not (= S (setenum (setenum (_ bv1 1)) ))))
+(assert (not (= S (setenum (union (setenum (_ bv0 1))
+                                  (setenum (_ bv1 1)))))))
+
+; 2 elements in S
+(assert (not (= S (union (setenum (as emptyset (Set (_ BitVec 1))))
+                         (setenum (setenum (_ bv0 1)))) )))
+(assert (not (= S (union (setenum (as emptyset (Set (_ BitVec 1))))
+                         (setenum (setenum (_ bv1 1)))))))
+(assert (not (= S (union (setenum (as emptyset (Set (_ BitVec 1))))
+                         (setenum (union (setenum (_ bv0 1))
+                                         (setenum (_ bv1 1))))))))
+(assert (not (= S (union (setenum (union (setenum (_ bv0 1))
+                                         (setenum (_ bv1 1))))
+                         (setenum (setenum (_ bv0 1)))) )))
+(assert (not (= S (union (setenum (setenum (_ bv0 1)))
+                         (setenum (setenum (_ bv1 1))))   )))
+(assert (not (= S (union (setenum (union (setenum (_ bv0 1))
+                                         (setenum (_ bv1 1))))
+                         (setenum (setenum (_ bv1 1)))))))
+
+; 3 elements in S
+(assert (not (= S (union (setenum (setenum (_ bv1 1)))
+                         (union (setenum (as emptyset (Set (_ BitVec 1))))
+                                (setenum (setenum (_ bv0 1)))))  )))
+(assert (not (= S (union (setenum (union (setenum (_ bv0 1))
+                                         (setenum (_ bv1 1))))
+                         (union (setenum (as emptyset (Set (_ BitVec 1))))
+                                (setenum (setenum (_ bv1 1)))))  )))
+(assert (not (= S (union (setenum (union (setenum (_ bv0 1))
+                                         (setenum (_ bv1 1))))
+                         (union (setenum (setenum (_ bv0 1)))
+                                (setenum (setenum (_ bv1 1)))))  )))
+(assert (not (= S (union (setenum (union (setenum (_ bv0 1))
+                                         (setenum (_ bv1 1))))
+                         (union (setenum (as emptyset (Set (_ BitVec 1))))
+                                (setenum (setenum (_ bv0 1)))))  )))
+
+; 4 elements in S
+(assert (not (= S (union (setenum (union (setenum (_ bv0 1))
+                                         (setenum (_ bv1 1))))
+                         (union (setenum (setenum (_ bv1 1)))
+                                (union (setenum (as emptyset (Set (_ BitVec 1))))
+                                       (setenum (setenum (_ bv0 1))))))  )))
+
+(check-sat)
+
+; if you delete any of the above assertions, you should get sat
+; (get-model)

diff --git a/test/regress/regress0/sets/sets-disequal.smt2 b/test/regress/regress0/sets/sets-disequal.smt2
new file mode 100644 (file)
index 0000000..65f55f3
--- /dev/null
+++ b/test/regress/regress0/sets/sets-disequal.smt2
@@ -0,0 +1,20 @@
+; COMMAND-LINE: --incremental
+; EXPECT: sat
+; EXPECT: sat
+; EXPECT: unsat
+; EXIT: 0
+(set-logic QF_BV_SETS)
+(declare-fun S1 () (Set (_ BitVec 1)))
+(declare-fun S2 () (Set (_ BitVec 1)))
+(declare-fun S3 () (Set (_ BitVec 1)))
+(declare-fun S4 () (Set (_ BitVec 1)))
+(assert (distinct S1 S2 S3 S4))
+(check-sat)
+;(get-model)
+(declare-fun S5 () (Set (_ BitVec 1)))
+(assert (not (= S5 S1)))
+(assert (not (= S5 S2)))
+(assert (not (= S5 S3)))
+(check-sat)
+(assert (not (= S5 S4)))
+(check-sat)