Merge pull request #28 from kbansal/sets

Sets translator, bug fixes

2 files changed, 178 insertions, 24 deletions

diff --git a/test/regress/regress0/sets/Makefile.am b/test/regress/regress0/sets/Makefile.am
index 7f1f07461..07006d6c3 100644
--- a/test/regress/regress0/sets/Makefile.am
+++ b/test/regress/regress0/sets/Makefile.am
@@ -19,49 +19,46 @@ MAKEFLAGS = -k
 # If a test shouldn't be run in e.g. competition mode,
 # put it below in "TESTS +="
 TESTS =	\
-	union-1b-flip.smt2 \
-	sets-sharing.smt2 \
-	union-1a-flip.smt2 \
-	copy_check_heap_access_33_4.smt2 \
-	rec_copy_loop_check_heap_access_43_4.smt2 \
-	sets-testlemma.smt2 \
 	jan24/insert_invariant_37_2.smt2 \
 	jan24/deepmeas0.hs.fqout.cvc4.47.smt2 \
 	jan24/deepmeas0.hs.fqout.small.smt2 \
 	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 \
 	jan27/ListConcat.hs.fqout.177minimized.smt2 \
 	jan27/ListElem.hs.fqout.cvc4.38.smt2 \
-	feb3/ListElts.hs.fqout.cvc4.317.smt2 \
-	setel-eq.smt2 \
-	sets-new.smt2 \
+	jan28/TalkingAboutSets.hs.fqout.cvc4.3577.smt2 \
+	jan28/TalkingAboutSets.hs.fqout.3577minimized.smt2 \
 	jan30/UniqueZipper.hs.fqout.minimized10.smt2 \
 	jan30/UniqueZipper.hs.fqout.cvc4.10.smt2 \
 	jan30/UniqueZipper.hs.fqout.minimized1832.smt2 \
 	jan30/UniqueZipper.hs.fqout.cvc4.1832.smt2 \
-	emptyset.smt2 \
-	sets-union.smt2 \
-	error2.smt2 \
-	union-1b.smt2 \
-	union-1a.smt2 \
-	error1.smt2 \
-	jan28/TalkingAboutSets.hs.fqout.cvc4.3577.smt2 \
-	jan28/TalkingAboutSets.hs.fqout.3577minimized.smt2 \
-	sets-sample.smt2 \
-	eqtest.smt2 \
+	feb3/ListElts.hs.fqout.cvc4.317.smt2 \
 	mar2014/lemmabug-ListElts317minimized.smt2 \
 	mar2014/sharing-preregister.smt2 \
 	mar2014/small.smt2 \
 	mar2014/smaller.smt2 \
 	mar2014/UniqueZipper.hs.1030minimized2.cvc4.smt2 \
 	mar2014/UniqueZipper.hs.1030minimized.cvc4.smt2 \
+	copy_check_heap_access_33_4.smt2 \
 	emptyset.smt2 \
-	error2.smt2
+	error1.smt2 \
+	error2.smt2 \
+	eqtest.smt2 \
+	rec_copy_loop_check_heap_access_43_4.smt2 \
+	sets-disequal.smt2 \
+	sets-equal.smt2 \
+	sets-inter.smt2 \
+	sets-sample.smt2 \
+	sets-sharing.smt2 \
+	sets-testlemma.smt2 \
+	sets-union.smt2 \
+	sharingbug.smt2 \
+	union-1a-flip.smt2 \
+	union-1a.smt2 \
+	union-1b-flip.smt2 \
+	union-1b.smt2 \
+	union-2.smt2
 
 EXTRA_DIST = $(TESTS)
 
diff --git a/test/regress/regress0/sets/sharingbug.smt2 b/test/regress/regress0/sets/sharingbug.smt2
new file mode 100644
index 000000000..b2b61f739
--- /dev/null
+++ b/test/regress/regress0/sets/sharingbug.smt2
@@ -0,0 +1,157 @@
+(set-info :source |fuzzsmt|)
+(set-info :smt-lib-version 2.0)
+(set-info :category "random")
+(set-info :status sat)
+(set-logic QF_UFLIA_SETS)
+(define-sort Element () Int)
+(declare-fun f0 ( Int Int Int) Int)
+(declare-fun f1 ( (Set Element)) (Set Element))
+(declare-fun p0 ( Int Int Int) Bool)
+(declare-fun p1 ( (Set Element)) Bool)
+(declare-fun v0 () Int)
+(declare-fun v1 () (Set Element))
+(declare-fun v2 () (Set Element))
+(declare-fun v3 () (Set Element))
+(assert (let ((e4 1))
+(let ((e5 (- v0)))
+(let ((e6 (* v0 (- e4))))
+(let ((e7 (ite (p0 v0 e5 v0) 1 0)))
+(let ((e8 (- e6 e7)))
+(let ((e9 (+ e5 v0)))
+(let ((e10 (ite (p0 e7 e7 e5) 1 0)))
+(let ((e11 (+ e8 e10)))
+(let ((e12 (* (- e4) e7)))
+(let ((e13 (- e10)))
+(let ((e14 (f0 e5 e7 e6)))
+(let ((e15 (in v0 v1)))
+(let ((e16 (in e12 v2)))
+(let ((e17 (in e14 v1)))
+(let ((e18 (f1 v3)))
+(let ((e19 (f1 v2)))
+(let ((e20 (f1 v1)))
+(let ((e21 (>= v0 e9)))
+(let ((e22 (> e6 e6)))
+(let ((e23 (> e5 e12)))
+(let ((e24 (distinct e8 e11)))
+(let ((e25 (= e10 e10)))
+(let ((e26 (> e13 e13)))
+(let ((e27 (distinct e14 e10)))
+(let ((e28 (> e11 e5)))
+(let ((e29 (>= e14 e6)))
+(let ((e30 (< e14 e14)))
+(let ((e31 (< e7 e12)))
+(let ((e32 (<= e11 e12)))
+(let ((e33 (< e14 e11)))
+(let ((e34 (<= e7 e9)))
+(let ((e35 (distinct e12 e5)))
+(let ((e36 (= e14 e6)))
+(let ((e37 (< v0 e8)))
+(let ((e38 (< e13 e14)))
+(let ((e39 (>= e6 e13)))
+(let ((e40 (< e12 e13)))
+(let ((e41 (< v0 e14)))
+(let ((e42 (< v0 e11)))
+(let ((e43 (p0 e13 e7 e8)))
+(let ((e44 (ite e17 e19 e19)))
+(let ((e45 (ite e34 v1 v1)))
+(let ((e46 (ite e28 v1 e44)))
+(let ((e47 (ite e24 e44 e20)))
+(let ((e48 (ite e39 e18 v3)))
+(let ((e49 (ite e35 v2 v3)))
+(let ((e50 (ite e38 e18 e20)))
+(let ((e51 (ite e22 v2 e44)))
+(let ((e52 (ite e17 e20 e18)))
+(let ((e53 (ite e35 e52 e19)))
+(let ((e54 (ite e38 e49 e20)))
+(let ((e55 (ite e15 e20 e45)))
+(let ((e56 (ite e37 v1 v3)))
+(let ((e57 (ite e41 e50 v1)))
+(let ((e58 (ite e28 v1 e54)))
+(let ((e59 (ite e27 e19 e53)))
+(let ((e60 (ite e16 e46 e44)))
+(let ((e61 (ite e29 e57 e52)))
+(let ((e62 (ite e21 e50 e53)))
+(let ((e63 (ite e32 e45 e19)))
+(let ((e64 (ite e42 v3 e57)))
+(let ((e65 (ite e33 e50 v3)))
+(let ((e66 (ite e43 e49 e20)))
+(let ((e67 (ite e22 v1 e63)))
+(let ((e68 (ite e40 e45 e19)))
+(let ((e69 (ite e30 e62 e58)))
+(let ((e70 (ite e24 e52 e58)))
+(let ((e71 (ite e31 e64 e67)))
+(let ((e72 (ite e30 e18 e20)))
+(let ((e73 (ite e25 e58 e44)))
+(let ((e74 (ite e36 e63 v3)))
+(let ((e75 (ite e43 e62 e73)))
+(let ((e76 (ite e26 e61 e55)))
+(let ((e77 (ite e23 e61 e71)))
+(let ((e78 (ite e40 e13 v0)))
+(let ((e79 (ite e23 e8 e13)))
+(let ((e80 (ite e24 e78 e6)))
+(let ((e81 (ite e39 e9 e80)))
+(let ((e82 (ite e31 e7 v0)))
+(let ((e83 (ite e43 e14 e6)))
+(let ((e84 (ite e38 e80 e81)))
+(let ((e85 (ite e32 e14 e10)))
+(let ((e86 (ite e29 e84 e78)))
+(let ((e87 (ite e27 e12 e8)))
+(let ((e88 (ite e31 e11 e6)))
+(let ((e89 (ite e33 e88 e85)))
+(let ((e90 (ite e36 e12 v0)))
+(let ((e91 (ite e23 e5 e7)))
+(let ((e92 (ite e34 e89 e80)))
+(let ((e93 (ite e15 e79 v0)))
+(let ((e94 (ite e21 e6 e7)))
+(let ((e95 (ite e26 v0 e91)))
+(let ((e96 (ite e28 e94 e87)))
+(let ((e97 (ite e32 e90 e78)))
+(let ((e98 (ite e42 e78 e83)))
+(let ((e99 (ite e40 e13 e82)))
+(let ((e100 (ite e25 e88 e90)))
+(let ((e101 (ite e26 e11 e81)))
+(let ((e102 (ite e17 e101 e81)))
+(let ((e103 (ite e30 v0 e80)))
+(let ((e104 (ite e28 e80 e79)))
+(let ((e105 (ite e27 e95 e101)))
+(let ((e106 (ite e22 e92 e94)))
+(let ((e107 (ite e16 e82 e94)))
+(let ((e108 (ite e41 e10 e78)))
+(let ((e109 (ite e37 e107 e84)))
+(let ((e110 (ite e35 e89 e92)))
+(let ((e111 (and e30 e37)))
+(let ((e112 (=> e21 e41)))
+(let ((e113 (ite e25 e33 e26)))
+(let ((e114 (and e34 e38)))
+(let ((e115 (=> e22 e43)))
+(let ((e116 (and e24 e35)))
+(let ((e117 (not e112)))
+(let ((e118 (=> e27 e116)))
+(let ((e119 (= e36 e15)))
+(let ((e120 (= e42 e42)))
+(let ((e121 (xor e29 e115)))
+(let ((e122 (xor e39 e16)))
+(let ((e123 (or e118 e32)))
+(let ((e124 (not e28)))
+(let ((e125 (=> e23 e40)))
+(let ((e126 (ite e17 e123 e111)))
+(let ((e127 (not e117)))
+(let ((e128 (not e31)))
+(let ((e129 (xor e121 e126)))
+(let ((e130 (or e125 e119)))
+(let ((e131 (=> e127 e114)))
+(let ((e132 (or e113 e128)))
+(let ((e133 (= e122 e124)))
+(let ((e134 (not e130)))
+(let ((e135 (or e133 e132)))
+(let ((e136 (= e129 e135)))
+(let ((e137 (=> e120 e120)))
+(let ((e138 (or e134 e137)))
+(let ((e139 (or e138 e138)))
+(let ((e140 (and e139 e131)))
+(let ((e141 (or e136 e136)))
+(let ((e142 (= e140 e141)))
+e142
+))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
+
+(check-sat)