diff options
author | Clark Barrett <barrett@cs.nyu.edu> | 2012-05-11 14:00:27 +0000 |
---|---|---|
committer | Clark Barrett <barrett@cs.nyu.edu> | 2012-05-11 14:00:27 +0000 |
commit | 57790a14676596e8c6ed42ff7ecd8038ddbaf09b (patch) | |
tree | 7e4d5c81f197beab924092fb72cc945d48a47e69 /src/theory/booleans | |
parent | 5181426cd8def23d67b69227fff033ef12850e68 (diff) |
Added some ITE rewrites,
Added ITE simplifier - on by default only for QF_LIA benchmarks
Fixed one bug in arrays
Added negate() to node.h - it returns kind == NOT ? kind[0] : kind.notNode()
Diffstat (limited to 'src/theory/booleans')
-rw-r--r-- | src/theory/booleans/theory_bool_rewriter.cpp | 37 |
1 files changed, 29 insertions, 8 deletions
diff --git a/src/theory/booleans/theory_bool_rewriter.cpp b/src/theory/booleans/theory_bool_rewriter.cpp index 4f41d2fa5..a6b02d784 100644 --- a/src/theory/booleans/theory_bool_rewriter.cpp +++ b/src/theory/booleans/theory_bool_rewriter.cpp @@ -153,15 +153,36 @@ RewriteResponse TheoryBoolRewriter::preRewrite(TNode n) { // non-Boolean-valued ITEs should have been removed in place of // a variable // rewrite simple cases of ITE - if(n[0] == tt) { - // ITE true x y - return RewriteResponse(REWRITE_AGAIN, n[1]); - } else if(n[0] == ff) { - // ITE false x y - return RewriteResponse(REWRITE_AGAIN, n[2]); - } else if(n[1] == n[2]) { - // ITE c x x + if (n[0].isConst()) { + if (n[0] == tt) { + // ITE true x y + return RewriteResponse(REWRITE_AGAIN, n[1]); + } else { + Assert(n[0] == ff); + // ITE false x y + return RewriteResponse(REWRITE_AGAIN, n[2]); + } + } else if (n[1].isConst()) { + if (n[1] == tt && n[2] == ff) { + return RewriteResponse(REWRITE_AGAIN, n[0]); + } + else if (n[1] == ff && n[2] == tt) { + return RewriteResponse(REWRITE_AGAIN, n[0].notNode()); + } + } + if (n[1] == n[2]) { return RewriteResponse(REWRITE_AGAIN, n[1]); + // Curiously, this rewrite affects several benchmarks dramatically, including copy_array and some simple_startup - disable for now + // } else if (n[0].getKind() == kind::NOT) { + // return RewriteResponse(REWRITE_AGAIN, n[0][0].iteNode(n[2], n[1])); + } else if (n[0] == n[1]) { + return RewriteResponse(REWRITE_AGAIN, n[0].iteNode(tt, n[2])); + } else if (n[0] == n[2]) { + return RewriteResponse(REWRITE_AGAIN, n[0].iteNode(n[1], ff)); + } else if (n[1].getKind() == kind::NOT && n[1][0] == n[0]) { + return RewriteResponse(REWRITE_AGAIN, n[0].iteNode(ff, n[2])); + } else if (n[2].getKind() == kind::NOT && n[2][0] == n[0]) { + return RewriteResponse(REWRITE_AGAIN, n[0].iteNode(n[1], tt)); } break; } |