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

3 files changed, 89 insertions, 4 deletions

diff --git a/test/regress/regress0/sets/Makefile.am b/test/regress/regress0/sets/Makefile.am
index 6d718553d..7f1f07461 100644
--- 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
index 000000000..907e074fe
--- /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
index 000000000..65f55f3a6
--- /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)