From c1410887627654fad536492d52d3c80cd1082575 Mon Sep 17 00:00:00 2001 From: =?utf8?q?Dejan=20Jovanovi=C4=87?= Date: Thu, 14 Jun 2012 19:46:22 +0000 Subject: [PATCH] fixes for the hasTerm issues in the shared database under the decision heuristic --- src/theory/shared_terms_database.cpp | 18 +- src/theory/theory_engine.cpp | 2 + test/regress/regress0/aufbv/Makefile.am | 4 +- .../regress/regress0/aufbv/fuzz06.delta01.smt | 17 ++ test/regress/regress0/aufbv/fuzz06.smt | 154 ++++++++++++++++++ 5 files changed, 192 insertions(+), 3 deletions(-) create mode 100644 test/regress/regress0/aufbv/fuzz06.delta01.smt create mode 100644 test/regress/regress0/aufbv/fuzz06.smt diff --git a/src/theory/shared_terms_database.cpp b/src/theory/shared_terms_database.cpp index c1266ee6d..7abc7f1e5 100644 --- a/src/theory/shared_terms_database.cpp +++ b/src/theory/shared_terms_database.cpp @@ -173,11 +173,25 @@ void SharedTermsDatabase::markNotified(TNode term, Theory::Set theories) { } bool SharedTermsDatabase::areEqual(TNode a, TNode b) const { - return d_equalityEngine.areEqual(a,b); + if (d_equalityEngine.hasTerm(a) && d_equalityEngine.hasTerm(b)) { + return d_equalityEngine.areEqual(a,b); + } else { + Assert(d_equalityEngine.hasTerm(a) || a.isConst()); + Assert(d_equalityEngine.hasTerm(b) || b.isConst()); + // since one (or both) of them is a constant, and the other is in the equality engine, they are not same + return false; + } } bool SharedTermsDatabase::areDisequal(TNode a, TNode b) const { - return d_equalityEngine.areDisequal(a,b,false); + if (d_equalityEngine.hasTerm(a) && d_equalityEngine.hasTerm(b)) { + return d_equalityEngine.areDisequal(a,b,false); + } else { + Assert(d_equalityEngine.hasTerm(a) || a.isConst()); + Assert(d_equalityEngine.hasTerm(b) || b.isConst()); + // one (or both) are in the equality engine + return false; + } } void SharedTermsDatabase::assertEquality(TNode equality, bool polarity, TNode reason) diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 060d48230..557acae95 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -390,6 +390,8 @@ void TheoryEngine::combineTheories() { Debug("sharing") << "TheoryEngine::combineTheories(): checking " << carePair.a << " = " << carePair.b << " from " << carePair.theory << std::endl; + Assert(d_sharedTerms.isShared(carePair.a) || carePair.a.isConst()); + Assert(d_sharedTerms.isShared(carePair.b) || carePair.b.isConst()); Assert(!d_sharedTerms.areEqual(carePair.a, carePair.b), "Please don't care about stuff you were notified about"); Assert(!d_sharedTerms.areDisequal(carePair.a, carePair.b), "Please don't care about stuff you were notified about"); diff --git a/test/regress/regress0/aufbv/Makefile.am b/test/regress/regress0/aufbv/Makefile.am index cb533a371..3335fb0b8 100644 --- a/test/regress/regress0/aufbv/Makefile.am +++ b/test/regress/regress0/aufbv/Makefile.am @@ -29,7 +29,9 @@ TESTS = \ fuzz04.delta01.smt \ fuzz04.smt \ fuzz05.delta01.smt \ - fuzz05.smt + fuzz05.smt \ + fuzz06.delta01.smt \ + fuzz06.smt # failing # fuzz01.smt \ diff --git a/test/regress/regress0/aufbv/fuzz06.delta01.smt b/test/regress/regress0/aufbv/fuzz06.delta01.smt new file mode 100644 index 000000000..6e411c663 --- /dev/null +++ b/test/regress/regress0/aufbv/fuzz06.delta01.smt @@ -0,0 +1,17 @@ +(benchmark fuzzsmt +:logic QF_AUFBV +:extrafuns ((a5 Array[6:11])) +:extrafuns ((v2 BitVec[1])) +:status sat +:formula +(let (?n1 bv0[11]) +(let (?n2 (sign_extend[9] v2)) +(let (?n3 (extract[7:2] ?n2)) +(let (?n4 (select a5 ?n3)) +(flet ($n5 (= ?n1 ?n4)) +(let (?n6 bv0[6]) +(let (?n7 (select a5 ?n6)) +(flet ($n8 (bvule ?n7 ?n1)) +(flet ($n9 (implies $n5 $n8)) +$n9 +)))))))))) diff --git a/test/regress/regress0/aufbv/fuzz06.smt b/test/regress/regress0/aufbv/fuzz06.smt new file mode 100644 index 000000000..bc8b23357 --- /dev/null +++ b/test/regress/regress0/aufbv/fuzz06.smt @@ -0,0 +1,154 @@ +(benchmark fuzzsmt +:logic QF_AUFBV +:status sat +:extrafuns ((v0 BitVec[3])) +:extrafuns ((v1 BitVec[10])) +:extrafuns ((v2 BitVec[1])) +:extrafuns ((v3 BitVec[10])) +:extrafuns ((v4 BitVec[10])) +:extrafuns ((a5 Array[6:11])) +:formula +(let (?e6 bv5[3]) +(let (?e7 bv71[8]) +(let (?e8 (bvnot v2)) +(let (?e9 (bvsub (zero_extend[5] ?e6) ?e7)) +(let (?e10 (ite (bvugt v1 (zero_extend[9] v2)) bv1[1] bv0[1])) +(let (?e11 (bvxnor v3 (sign_extend[9] ?e8))) +(let (?e12 (rotate_left[2] ?e7)) +(let (?e13 (bvudiv v4 ?e11)) +(let (?e14 (bvor v0 (zero_extend[2] ?e10))) +(let (?e15 (store a5 (extract[6:1] ?e7) (sign_extend[10] v2))) +(let (?e16 (select ?e15 (zero_extend[3] ?e6))) +(let (?e17 (store ?e15 (extract[6:1] v1) (sign_extend[3] ?e9))) +(let (?e18 (select ?e17 (extract[7:2] ?e11))) +(let (?e19 (bvudiv (zero_extend[7] ?e14) ?e11)) +(let (?e20 (extract[7:3] ?e12)) +(let (?e21 (bvxor (zero_extend[9] ?e10) v3)) +(let (?e22 (bvudiv (zero_extend[7] v0) ?e13)) +(let (?e23 (bvneg ?e16)) +(let (?e24 (ite (bvuge (sign_extend[9] ?e8) ?e21) bv1[1] bv0[1])) +(let (?e25 (ite (= bv1[1] (extract[7:7] ?e18)) ?e14 (zero_extend[2] ?e24))) +(let (?e26 (bvand ?e23 (sign_extend[10] v2))) +(let (?e27 (bvmul ?e7 (sign_extend[3] ?e20))) +(let (?e28 (ite (distinct ?e6 (sign_extend[2] ?e8)) bv1[1] bv0[1])) +(let (?e29 (bvnand v1 ?e13)) +(let (?e30 (bvudiv (zero_extend[2] ?e8) ?e14)) +(let (?e31 (bvcomp ?e9 (zero_extend[7] ?e10))) +(let (?e32 (ite (bvsgt v0 ?e25) bv1[1] bv0[1])) +(let (?e33 (bvxor v4 ?e19)) +(flet ($e34 (bvuge (zero_extend[2] ?e24) ?e6)) +(flet ($e35 (bvuge (sign_extend[1] ?e13) ?e16)) +(flet ($e36 (bvult ?e22 (zero_extend[9] ?e32))) +(flet ($e37 (bvugt v3 v3)) +(flet ($e38 (bvsge (sign_extend[2] ?e27) ?e33)) +(flet ($e39 (bvule ?e23 (zero_extend[3] ?e12))) +(flet ($e40 (bvule (sign_extend[2] ?e27) ?e19)) +(flet ($e41 (bvuge ?e33 ?e19)) +(flet ($e42 (bvsle (zero_extend[9] ?e8) ?e21)) +(flet ($e43 (bvsle (sign_extend[2] ?e12) ?e11)) +(flet ($e44 (= v2 ?e24)) +(flet ($e45 (bvugt (zero_extend[3] ?e9) ?e18)) +(flet ($e46 (bvugt ?e11 (zero_extend[2] ?e27))) +(flet ($e47 (bvsge ?e18 ?e18)) +(flet ($e48 (bvsge ?e11 (sign_extend[9] ?e31))) +(flet ($e49 (bvslt v1 (zero_extend[9] v2))) +(flet ($e50 (bvult ?e26 (zero_extend[1] ?e11))) +(flet ($e51 (bvule (sign_extend[9] ?e31) v4)) +(flet ($e52 (bvsgt v4 (zero_extend[2] ?e9))) +(flet ($e53 (bvule v3 (sign_extend[7] v0))) +(flet ($e54 (bvuge ?e16 (sign_extend[8] ?e6))) +(flet ($e55 (bvugt ?e31 ?e10)) +(flet ($e56 (bvugt (zero_extend[1] ?e29) ?e18)) +(flet ($e57 (bvslt v4 (sign_extend[7] v0))) +(flet ($e58 (bvsle ?e13 (zero_extend[9] ?e31))) +(flet ($e59 (distinct (zero_extend[7] ?e6) ?e22)) +(flet ($e60 (bvule (zero_extend[5] ?e30) ?e9)) +(flet ($e61 (bvult (sign_extend[2] ?e9) v1)) +(flet ($e62 (bvult v1 ?e29)) +(flet ($e63 (bvsge (sign_extend[3] ?e20) ?e12)) +(flet ($e64 (bvslt ?e14 (sign_extend[2] ?e31))) +(flet ($e65 (bvult (zero_extend[3] ?e9) ?e18)) +(flet ($e66 (= (zero_extend[9] v2) v3)) +(flet ($e67 (bvuge ?e24 ?e31)) +(flet ($e68 (bvult ?e8 ?e10)) +(flet ($e69 (bvugt ?e9 ?e27)) +(flet ($e70 (= ?e13 (zero_extend[7] v0))) +(flet ($e71 (bvsle v4 ?e33)) +(flet ($e72 (bvule (sign_extend[7] ?e31) ?e12)) +(flet ($e73 (bvult ?e11 ?e29)) +(flet ($e74 (bvult ?e25 (sign_extend[2] ?e24))) +(flet ($e75 (= (sign_extend[2] ?e7) v3)) +(flet ($e76 (= (sign_extend[7] v0) ?e19)) +(flet ($e77 (bvslt (zero_extend[9] v2) ?e29)) +(flet ($e78 (bvsge ?e25 (sign_extend[2] ?e32))) +(flet ($e79 (bvsle (zero_extend[9] ?e32) ?e21)) +(flet ($e80 (bvult ?e11 ?e19)) +(flet ($e81 (bvugt ?e27 (zero_extend[5] ?e25))) +(flet ($e82 (distinct ?e13 (zero_extend[7] ?e14))) +(flet ($e83 (bvugt (zero_extend[3] ?e9) ?e26)) +(flet ($e84 (= ?e18 (sign_extend[8] ?e25))) +(flet ($e85 (bvsgt (sign_extend[4] ?e8) ?e20)) +(flet ($e86 (bvult (sign_extend[9] ?e28) ?e33)) +(flet ($e87 (iff $e74 $e56)) +(flet ($e88 (xor $e54 $e45)) +(flet ($e89 (or $e64 $e80)) +(flet ($e90 (if_then_else $e83 $e62 $e89)) +(flet ($e91 (implies $e67 $e71)) +(flet ($e92 (iff $e50 $e34)) +(flet ($e93 (not $e73)) +(flet ($e94 (implies $e58 $e91)) +(flet ($e95 (not $e40)) +(flet ($e96 (and $e55 $e75)) +(flet ($e97 (if_then_else $e46 $e63 $e36)) +(flet ($e98 (or $e70 $e38)) +(flet ($e99 (iff $e59 $e49)) +(flet ($e100 (and $e41 $e88)) +(flet ($e101 (not $e60)) +(flet ($e102 (and $e78 $e61)) +(flet ($e103 (if_then_else $e102 $e48 $e101)) +(flet ($e104 (and $e90 $e93)) +(flet ($e105 (implies $e52 $e47)) +(flet ($e106 (xor $e53 $e103)) +(flet ($e107 (and $e97 $e100)) +(flet ($e108 (xor $e81 $e69)) +(flet ($e109 (xor $e107 $e37)) +(flet ($e110 (not $e98)) +(flet ($e111 (not $e105)) +(flet ($e112 (implies $e43 $e76)) +(flet ($e113 (and $e68 $e42)) +(flet ($e114 (if_then_else $e112 $e57 $e44)) +(flet ($e115 (iff $e72 $e86)) +(flet ($e116 (or $e82 $e114)) +(flet ($e117 (xor $e116 $e104)) +(flet ($e118 (implies $e110 $e65)) +(flet ($e119 (if_then_else $e106 $e106 $e108)) +(flet ($e120 (not $e79)) +(flet ($e121 (if_then_else $e77 $e99 $e95)) +(flet ($e122 (xor $e87 $e94)) +(flet ($e123 (and $e117 $e120)) +(flet ($e124 (xor $e85 $e92)) +(flet ($e125 (or $e118 $e123)) +(flet ($e126 (and $e119 $e121)) +(flet ($e127 (iff $e109 $e124)) +(flet ($e128 (or $e96 $e125)) +(flet ($e129 (iff $e51 $e66)) +(flet ($e130 (implies $e127 $e39)) +(flet ($e131 (if_then_else $e126 $e130 $e130)) +(flet ($e132 (or $e128 $e128)) +(flet ($e133 (iff $e35 $e115)) +(flet ($e134 (iff $e122 $e133)) +(flet ($e135 (not $e111)) +(flet ($e136 (iff $e131 $e113)) +(flet ($e137 (if_then_else $e134 $e129 $e129)) +(flet ($e138 (implies $e132 $e84)) +(flet ($e139 (not $e136)) +(flet ($e140 (implies $e135 $e139)) +(flet ($e141 (implies $e138 $e140)) +(flet ($e142 (not $e137)) +(flet ($e143 (and $e142 $e141)) +(flet ($e144 (and $e143 (not (= ?e14 bv0[3])))) +(flet ($e145 (and $e144 (not (= ?e11 bv0[10])))) +(flet ($e146 (and $e145 (not (= ?e13 bv0[10])))) +$e146 +)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) + -- 2.30.2