diff options
author | Tim King <taking@cs.nyu.edu> | 2016-10-19 09:40:12 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2016-10-19 09:40:12 -0700 |
commit | 3e93fdba8102e4ad1399af78967fec3d0495722a (patch) | |
tree | 6addb6865f825c2846a76329ccad8329f4a37f4f | |
parent | 9da056f71c0c4a8ed5afd01c300e9c86cfcf5601 (diff) | |
parent | eed6f3a1fee9cbfe68e15acb50a84cf2cab7bc2c (diff) |
Merge pull request #97 from 4tXJ7f/fix_rewrite
Fix minor bug and typo in boolean rewriter
-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 |