diff options
| author | Andres Notzli <andres.noetzli@gmail.com> | 2016-10-19 02:58:59 -0700 |
|---|---|---|
| committer | Andres Notzli <andres.noetzli@gmail.com> | 2016-10-19 02:58:59 -0700 |
| commit | eed6f3a1fee9cbfe68e15acb50a84cf2cab7bc2c (patch) | |
| tree | 6addb6865f825c2846a76329ccad8329f4a37f4f | |
| parent | 9da056f71c0c4a8ed5afd01c300e9c86cfcf5601 (diff) | |
Fix minor bug and typo in boolean rewriterfix_rewrite
One of the rewrites in the boolean rewriter had the condition `n[0] ==
tt && n[0] == ff`, which could never be true. Another rewrite covers the
same case but returns a `REWRITE_AGAIN` instead of a `REWRITE_DONE`.
This commit also fixes a minor typo.
| -rw-r--r-- | src/theory/booleans/theory_bool_rewriter.cpp | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/theory/booleans/theory_bool_rewriter.cpp b/src/theory/booleans/theory_bool_rewriter.cpp index cc9eb54b9..dc5f655aa 100644 --- a/src/theory/booleans/theory_bool_rewriter.cpp +++ b/src/theory/booleans/theory_bool_rewriter.cpp @@ -168,7 +168,7 @@ RewriteResponse TheoryBoolRewriter::preRewrite(TNode n) { } case kind::IMPLIES: { if (n[0] == ff || n[1] == tt) return RewriteResponse(REWRITE_DONE, tt); - if (n[0] == tt && n[0] == ff) return RewriteResponse(REWRITE_DONE, ff); + if (n[0] == tt && n[1] == ff) return RewriteResponse(REWRITE_DONE, ff); if (n[0] == tt) return RewriteResponse(REWRITE_AGAIN, n[1]); if (n[1] == ff) return RewriteResponse(REWRITE_AGAIN, makeNegation(n[0])); break; @@ -259,7 +259,7 @@ RewriteResponse TheoryBoolRewriter::preRewrite(TNode n) { // XOR true x return RewriteResponse(REWRITE_AGAIN, makeNegation(n[1])); } else if(n[1] == tt) { - // XCR x true + // XOR x true return RewriteResponse(REWRITE_AGAIN, makeNegation(n[0])); } else if(n[0] == ff) { // XOR false x |