diff options
author | Clark Barrett <barrett@cs.nyu.edu> | 2013-03-13 20:37:57 -0400 |
---|---|---|
committer | Clark Barrett <barrett@cs.nyu.edu> | 2013-03-13 20:37:57 -0400 |
commit | c03a972a85d565f10953ee58ec809f1751063f8e (patch) | |
tree | af901613c5f58dbfc5e0272167e041d6650497c9 | |
parent | 63c1d547b7598e3dba35f865ba3749c15a105a6f (diff) |
Added a rewrite for iff:
x = c iff x = d ---> false
This fixes Andy's problem if unconstrained simplification is turned on.
-rw-r--r-- | src/theory/booleans/theory_bool_rewriter.cpp | 18 |
1 files changed, 18 insertions, 0 deletions
diff --git a/src/theory/booleans/theory_bool_rewriter.cpp b/src/theory/booleans/theory_bool_rewriter.cpp index 567a8dd70..2fa2e095a 100644 --- a/src/theory/booleans/theory_bool_rewriter.cpp +++ b/src/theory/booleans/theory_bool_rewriter.cpp @@ -118,6 +118,24 @@ 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); + } + } } break; } |