From: lianah Date: Mon, 1 Apr 2013 19:23:46 +0000 (-0400) Subject: fixed TheoryBool rewriter bug X-Git-Tag: cvc5-1.0.0~7355 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=bf7f728381bb27163f3e056d698ba4da6316b9c8;p=cvc5.git fixed TheoryBool rewriter bug --- diff --git a/src/theory/booleans/theory_bool_rewriter.cpp b/src/theory/booleans/theory_bool_rewriter.cpp index 2fa2e095a..967126da1 100644 --- a/src/theory/booleans/theory_bool_rewriter.cpp +++ b/src/theory/booleans/theory_bool_rewriter.cpp @@ -118,25 +118,29 @@ RewriteResponse TheoryBoolRewriter::preRewrite(TNode n) { } else if(n[1].getKind() == kind::NOT && n[1][0] == n[0]) { // IFF x (NOT x) return RewriteResponse(REWRITE_DONE, ff); - } else if(n[0].getKind() == kind::EQUAL && n[1].getKind() == kind::EQUAL) { - TNode t,c; - if (n[0][0].isConst()) { - c = n[0][0]; - t = n[0][1]; - } - else if (n[0][1].isConst()) { - c = n[0][1]; - t = n[0][0]; - } - if (!c.isNull()) { - if (n[1][0] == t && n[1][1].isConst()) { - return RewriteResponse(REWRITE_DONE, n[1][1] == c ? tt : ff); - } - else if (n[1][1] == t && n[1][0].isConst()) { - return RewriteResponse(REWRITE_DONE, n[1][0] == c ? tt : ff); - } - } } + // This is wrong: it would rewrite c1 == x <=> c2 == x to false + // when this is sat for x = c3 where c3 is different from c1, and c2 + + // else if(n[0].getKind() == kind::EQUAL && n[1].getKind() == kind::EQUAL) { + // TNode t,c; + // if (n[0][0].isConst()) { + // c = n[0][0]; + // t = n[0][1]; + // } + // else if (n[0][1].isConst()) { + // c = n[0][1]; + // t = n[0][0]; + // } + // if (!c.isNull()) { + // if (n[1][0] == t && n[1][1].isConst()) { + // return RewriteResponse(REWRITE_DONE, n[1][1] == c ? tt : ff); + // } + // else if (n[1][1] == t && n[1][0].isConst()) { + // return RewriteResponse(REWRITE_DONE, n[1][0] == c ? tt : ff); + // } + // } + // } break; } case kind::XOR: { diff --git a/test/regress/regress0/incorrect1.smt b/test/regress/regress0/incorrect1.smt new file mode 100644 index 000000000..f1352334c --- /dev/null +++ b/test/regress/regress0/incorrect1.smt @@ -0,0 +1,57 @@ +(benchmark fuzzsmt +:logic QF_BV +:status unknown +:extrafuns ((v0 BitVec[10])) +:formula +(let (?e1 bv30369[16]) +(let (?e2 bv3[2]) +(let (?e3 (ite (bvule ?e1 ?e1) bv1[1] bv0[1])) +(let (?e4 (bvcomp (zero_extend[1] ?e3) ?e2)) +(let (?e5 (ite (bvsgt (sign_extend[15] ?e4) ?e1) bv1[1] bv0[1])) +(let (?e6 (bvsmod ?e1 ?e1)) +(let (?e7 (bvsdiv v0 v0)) +(flet ($e8 (bvult ?e2 ?e2)) +(flet ($e9 (bvsge ?e7 (zero_extend[9] ?e3))) +(flet ($e10 (bvugt (sign_extend[15] ?e4) ?e6)) +(flet ($e11 (bvsgt (sign_extend[15] ?e3) ?e6)) +(flet ($e12 (bvsgt v0 (sign_extend[9] ?e3))) +(flet ($e13 (bvsgt ?e4 ?e4)) +(flet ($e14 (bvsle ?e1 (zero_extend[14] ?e2))) +(flet ($e15 (bvslt (sign_extend[14] ?e2) ?e6)) +(flet ($e16 (bvslt (zero_extend[9] ?e3) ?e7)) +(flet ($e17 (= ?e6 (sign_extend[15] ?e3))) +(flet ($e18 (= (zero_extend[8] ?e2) v0)) +(flet ($e19 (bvsgt ?e2 (sign_extend[1] ?e3))) +(flet ($e20 (bvslt ?e3 ?e4)) +(flet ($e21 (bvslt ?e6 (zero_extend[15] ?e4))) +(flet ($e22 (distinct (zero_extend[9] ?e4) v0)) +(flet ($e23 (bvuge ?e1 (sign_extend[15] ?e5))) +(flet ($e24 (or $e12 $e19)) +(flet ($e25 (implies $e16 $e8)) +(flet ($e26 (and $e14 $e20)) +(flet ($e27 (not $e13)) +(flet ($e28 (not $e22)) +(flet ($e29 (xor $e11 $e23)) +(flet ($e30 (or $e29 $e15)) +(flet ($e31 (not $e26)) +(flet ($e32 (iff $e31 $e18)) +(flet ($e33 (and $e27 $e17)) +(flet ($e34 (xor $e21 $e10)) +(flet ($e35 (xor $e32 $e33)) +(flet ($e36 (and $e30 $e30)) +(flet ($e37 (xor $e9 $e9)) +(flet ($e38 (xor $e36 $e34)) +(flet ($e39 (or $e24 $e25)) +(flet ($e40 (iff $e38 $e28)) +(flet ($e41 (iff $e40 $e35)) +(flet ($e42 (not $e37)) +(flet ($e43 (and $e42 $e42)) +(flet ($e44 (iff $e43 $e41)) +(flet ($e45 (iff $e39 $e44)) +(flet ($e46 (and $e45 (not (= v0 bv0[10])))) +(flet ($e47 (and $e46 (not (= v0 (bvnot bv0[10]))))) +(flet ($e48 (and $e47 (not (= ?e1 bv0[16])))) +(flet ($e49 (and $e48 (not (= ?e1 (bvnot bv0[16]))))) +$e49 +)))))))))))))))))))))))))))))))))))))))))))))))))) +