diff options
Diffstat (limited to 'src/theory')
| -rw-r--r-- | src/theory/booleans/theory_bool_rewriter.cpp | 40 |
1 files changed, 22 insertions, 18 deletions
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: { |