From 5b2fc4b690f9358dac09b057285c54a6df7c543e Mon Sep 17 00:00:00 2001 From: Kshitij Bansal Date: Fri, 6 Jun 2014 15:32:32 -0400 Subject: [PATCH] sets: fix equality propagation --- src/theory/sets/theory_sets_private.cpp | 1 + test/regress/regress0/sets/Makefile.am | 45 +++--- test/regress/regress0/sets/sharingbug.smt2 | 157 +++++++++++++++++++++ 3 files changed, 179 insertions(+), 24 deletions(-) create mode 100644 test/regress/regress0/sets/sharingbug.smt2 diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index 8c9441483..9b628ede2 100644 --- 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 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) -- 2.30.2