sets: fix equality propagation

diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index 8c9441483b87c72c6cb8e49ab24bb3cb5f360f67..9b628ede2176b8c55feae338fc59ee8836723196 100644 (file)
--- a/src/theory/sets/theory_sets_private.cpp
+++ b/src/theory/sets/theory_sets_private.cpp
@@ -990,6 +990,7 @@ bool TheorySetsPrivate::NotifyClass::eqNotifyTriggerTermEquality(TheoryId tag, T
   if(value) {
     d_theory.d_termInfoManager->mergeTerms(t1, t2);
   }
+  d_theory.propagate( value ? EQUAL(t1, t2) : NOT(EQUAL(t1, t2)) );
   return true;
 }
 

diff --git a/test/regress/regress0/sets/Makefile.am b/test/regress/regress0/sets/Makefile.am
index 7f1f074614e6ea275a77b3dd7a40f79c8779b46a..07006d6c318646d45bd9b98d7df5c59a762b9650 100644 (file)
--- 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 (file)
index 0000000..b2b61f7
--- /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)