fixes for the hasTerm issues in the shared database under the decision heuristic

diff --git a/src/theory/shared_terms_database.cpp b/src/theory/shared_terms_database.cpp
index c1266ee6dd577e914f861b1361623ef46cc7d919..7abc7f1e5c1871a48b310790ce5894d4937f0c3e 100644 (file)
--- 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 060d48230a4f2607586f5f299296b52b73ce6478..557acae9554a7ecb5fba2a7c5847b5bc988df83b 100644 (file)
--- 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 cb533a371e27b1c1ce66aa4f1525b5c8453fb4a7..3335fb0b87c36334bf011c1a7e95eaf9f5405617 100644 (file)
--- 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 (file)
index 0000000..6e411c6
--- /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 (file)
index 0000000..bc8b233
--- /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
+))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
+