diff options
| -rw-r--r-- | src/theory/booleans/theory_bool_rewriter.cpp | 47 | ||||
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress0/bool/issue6717-ite-rewrite.smt2 | 7 |
3 files changed, 34 insertions, 21 deletions
diff --git a/src/theory/booleans/theory_bool_rewriter.cpp b/src/theory/booleans/theory_bool_rewriter.cpp index a5c63522d..8f6d9d3b7 100644 --- a/src/theory/booleans/theory_bool_rewriter.cpp +++ b/src/theory/booleans/theory_bool_rewriter.cpp @@ -345,16 +345,6 @@ RewriteResponse TheoryBoolRewriter::preRewrite(TNode n) { << n << ": " << n[0].notNode() << std::endl; return RewriteResponse(REWRITE_AGAIN, makeNegation(n[0])); } - if (n[1] == tt || n[1] == ff) - { - // ITE C true y --> C v y - // ITE C false y --> ~C ^ y - Node resp = - n[1] == tt ? n[0].orNode(n[2]) : (n[0].negate()).andNode(n[2]); - Debug("bool-ite") << "TheoryBoolRewriter::preRewrite_ITE: n[1] const " - << n << ": " << resp << std::endl; - return RewriteResponse(REWRITE_AGAIN, resp); - } } if (n[0].getKind() == kind::NOT) @@ -364,17 +354,6 @@ RewriteResponse TheoryBoolRewriter::preRewrite(TNode n) { REWRITE_AGAIN, nodeManager->mkNode(kind::ITE, n[0][0], n[2], n[1])); } - if (n[2].isConst() && (n[2] == tt || n[2] == ff)) - { - // ITE C x true --> ~C v x - // ITE C x false --> C ^ x - Node resp = - n[2] == tt ? (n[0].negate()).orNode(n[1]) : n[0].andNode(n[1]); - Debug("bool-ite") << "TheoryBoolRewriter::preRewrite_ITE: n[2] const " - << n << ": " << resp << std::endl; - return RewriteResponse(REWRITE_AGAIN, resp); - } - int parityTmp; if ((parityTmp = equalityParity(n[1], n[2])) != 0) { Node resp = (parityTmp == 1) ? (Node)n[1] : n[0].eqNode(n[1]); @@ -424,6 +403,32 @@ RewriteResponse TheoryBoolRewriter::preRewrite(TNode n) { << parityTmp << " " << n << ": " << resp << std::endl; return RewriteResponse(REWRITE_AGAIN, resp); } + + // Rewrites for ITEs with a constant branch. These rewrites are applied + // after the parity rewrites above because they may simplify ITEs such as + // `(ite c c true)` to `(ite c true true)`. As a result, we avoid + // introducing an unnecessary conjunction/disjunction here. + if (n[1].isConst() && (n[1] == tt || n[1] == ff)) + { + // ITE C true y --> C v y + // ITE C false y --> ~C ^ y + Node resp = + n[1] == tt ? n[0].orNode(n[2]) : (n[0].negate()).andNode(n[2]); + Debug("bool-ite") << "TheoryBoolRewriter::preRewrite_ITE: n[1] const " + << n << ": " << resp << std::endl; + return RewriteResponse(REWRITE_AGAIN, resp); + } + else if (n[2].isConst() && (n[2] == tt || n[2] == ff)) + { + // ITE C x true --> ~C v x + // ITE C x false --> C ^ x + Node resp = + n[2] == tt ? (n[0].negate()).orNode(n[1]) : n[0].andNode(n[1]); + Debug("bool-ite") << "TheoryBoolRewriter::preRewrite_ITE: n[2] const " + << n << ": " << resp << std::endl; + return RewriteResponse(REWRITE_AGAIN, resp); + } + break; } default: diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 4ee8e513e..19c689b87 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -163,6 +163,7 @@ set(regress_0_tests regress0/auflia/fuzz05.smtv1.smt2 regress0/auflia/x2.smtv1.smt2 regress0/bool/issue1978.smt2 + regress0/bool/issue6717-ite-rewrite.smt2 regress0/boolean-prec.cvc regress0/boolean-terms-bug-array.smt2 regress0/boolean-terms-kernel1.smt2 diff --git a/test/regress/regress0/bool/issue6717-ite-rewrite.smt2 b/test/regress/regress0/bool/issue6717-ite-rewrite.smt2 new file mode 100644 index 000000000..3f78823df --- /dev/null +++ b/test/regress/regress0/bool/issue6717-ite-rewrite.smt2 @@ -0,0 +1,7 @@ +(set-logic ALL) +(declare-fun T () Bool) +(declare-fun v () String) +(assert (ite T T true)) +(assert (or T (and (str.prefixof v "") (exists ((x Int)) (= "t" (str.substr v 0 x)))))) +(set-info :status sat) +(check-sat) |