diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2018-08-03 19:41:49 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-08-03 19:41:49 -0700 |
commit | aacd3dda388891bf2302555d0754f1e2a19368b7 (patch) | |
tree | c529db9445026e464ee05edbed3b076de5d3b212 /src/theory | |
parent | dafa75521c0b38d0095792f232fbb53f16318676 (diff) |
Add rewrite for nested BITVECTOR_ITE with cond_outer == cond_inner. (#2272)
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/bv/theory_bv_rewrite_rules.h | 9 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_rewrite_rules_simplification.h | 40 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_rewriter.cpp | 5 |
3 files changed, 45 insertions, 9 deletions
diff --git a/src/theory/bv/theory_bv_rewrite_rules.h b/src/theory/bv/theory_bv_rewrite_rules.h index 55614f4e6..d8f360492 100644 --- a/src/theory/bv/theory_bv_rewrite_rules.h +++ b/src/theory/bv/theory_bv_rewrite_rules.h @@ -105,8 +105,9 @@ enum RewriteRuleId /// simplification rules /// all of these rules decrease formula size BvIteConstCond, - BvIteChildren, + BvIteEqualChildren, BvIteConstChildren, + BvIteEqualCond, BvComp, ShlByConst, LshrByConst, @@ -245,8 +246,9 @@ inline std::ostream& operator << (std::ostream& out, RewriteRuleId ruleId) { case EvalRotateRight : out << "EvalRotateRight"; return out; case EvalNeg : out << "EvalNeg"; return out; case BvIteConstCond : out << "BvIteConstCond"; return out; - case BvIteChildren : out << "BvIteChildren"; return out; + case BvIteEqualChildren : out << "BvIteEqualChildren"; return out; case BvIteConstChildren : out << "BvIteConstChildren"; return out; + case BvIteEqualCond : out << "BvIteEqualCond"; return out; case BvComp : out << "BvComp"; return out; case ShlByConst : out << "ShlByConst"; return out; case LshrByConst : out << "LshrByConst"; return out; @@ -562,8 +564,9 @@ struct AllRewriteRules { RewriteRule<NormalizeEqPlusNeg> rule129; RewriteRule<BvComp> rule130; RewriteRule<BvIteConstCond> rule131; - RewriteRule<BvIteChildren> rule132; + RewriteRule<BvIteEqualChildren> rule132; RewriteRule<BvIteConstChildren> rule133; + RewriteRule<BvIteEqualCond> rule134; }; template<> inline diff --git a/src/theory/bv/theory_bv_rewrite_rules_simplification.h b/src/theory/bv/theory_bv_rewrite_rules_simplification.h index 1213c0f05..a59f6524a 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_simplification.h +++ b/src/theory/bv/theory_bv_rewrite_rules_simplification.h @@ -49,20 +49,20 @@ inline Node RewriteRule<BvIteConstCond>::apply(TNode node) } /** - * BvIteChildren + * BvIteEqualChildren * * BITVECTOR_ITE with term_then = term_else */ template <> -inline bool RewriteRule<BvIteChildren>::applies(TNode node) +inline bool RewriteRule<BvIteEqualChildren>::applies(TNode node) { return (node.getKind() == kind::BITVECTOR_ITE && node[1] == node[2]); } template <> -inline Node RewriteRule<BvIteChildren>::apply(TNode node) +inline Node RewriteRule<BvIteEqualChildren>::apply(TNode node) { - Debug("bv-rewrite") << "RewriteRule<BvIteChildren>(" << node << ")" + Debug("bv-rewrite") << "RewriteRule<BvIteEqualChildren>(" << node << ")" << std::endl; return node[1]; } @@ -94,6 +94,38 @@ inline Node RewriteRule<BvIteConstChildren>::apply(TNode node) } /** + * BvIteEqualCond + * + * Nested BITVECTOR_ITE with cond_outer == cond_inner + * + * c0 ? (c0 ? t0 : e0) : e1 -> c0 ? t0 : e1 + * c0 ? t0 : (c0 ? t1 : e1) -> c0 ? t0 : e1 + * c0 ? (c0 ? t0 : e0) : (c0 ? t1 : e1) -> c0 ? t0 : e1 + */ +template <> +inline bool RewriteRule<BvIteEqualCond>::applies(TNode node) +{ + return ( + node.getKind() == kind::BITVECTOR_ITE + && ((node[1].getKind() == kind::BITVECTOR_ITE && node[0] == node[1][0]) + || (node[2].getKind() == kind::BITVECTOR_ITE + && node[0] == node[2][0]))); +} + +template <> +inline Node RewriteRule<BvIteEqualCond>::apply(TNode node) +{ + Debug("bv-rewrite") << "RewriteRule<BvIteEqualCond>(" << node << ")" + << std::endl; + Node t0 = node[1].getKind() == kind::BITVECTOR_ITE && node[0] == node[1][0] + ? node[1][1] + : node[1]; + Node e1 = node[2].getKind() == kind::BITVECTOR_ITE && node[0] == node[2][0] + ? node[2][2] + : node[2]; + return NodeManager::currentNM()->mkNode(kind::BITVECTOR_ITE, node[0], t0, e1); +} +/** * BvComp * * BITVECTOR_COMP of children of size 1 with one constant child diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp index f0218bbc5..d63fe4009 100644 --- a/src/theory/bv/theory_bv_rewriter.cpp +++ b/src/theory/bv/theory_bv_rewriter.cpp @@ -171,8 +171,9 @@ RewriteResponse TheoryBVRewriter::RewriteITEBv(TNode node, bool prerewrite) Node resultNode = LinearRewriteStrategy<RewriteRule<EvalITEBv>, RewriteRule<BvIteConstCond>, - RewriteRule<BvIteChildren>, - RewriteRule<BvIteConstChildren> >::apply(node); + RewriteRule<BvIteEqualChildren>, + RewriteRule<BvIteConstChildren>, + RewriteRule<BvIteEqualCond>>::apply(node); return RewriteResponse(REWRITE_DONE, resultNode); } |