diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2018-08-03 18:09:07 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-08-03 18:09:07 -0700 |
commit | dafa75521c0b38d0095792f232fbb53f16318676 (patch) | |
tree | d7fea8a3a25d8337e3fc52941a6dfc624d44058a /src | |
parent | 23eef2bd8083600babd8498ec779d681620e97df (diff) |
Add rewrite for BITVECTOR_ITE with const children. (#2271)
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/bv/theory_bv_rewrite_rules.h | 3 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_rewrite_rules_simplification.h | 26 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_rewriter.cpp | 4 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_utils.cpp | 6 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_utils.h | 3 |
5 files changed, 40 insertions, 2 deletions
diff --git a/src/theory/bv/theory_bv_rewrite_rules.h b/src/theory/bv/theory_bv_rewrite_rules.h index 0ce9e6d5a..55614f4e6 100644 --- a/src/theory/bv/theory_bv_rewrite_rules.h +++ b/src/theory/bv/theory_bv_rewrite_rules.h @@ -106,6 +106,7 @@ enum RewriteRuleId /// all of these rules decrease formula size BvIteConstCond, BvIteChildren, + BvIteConstChildren, BvComp, ShlByConst, LshrByConst, @@ -245,6 +246,7 @@ inline std::ostream& operator << (std::ostream& out, RewriteRuleId ruleId) { case EvalNeg : out << "EvalNeg"; return out; case BvIteConstCond : out << "BvIteConstCond"; return out; case BvIteChildren : out << "BvIteChildren"; return out; + case BvIteConstChildren : out << "BvIteConstChildren"; return out; case BvComp : out << "BvComp"; return out; case ShlByConst : out << "ShlByConst"; return out; case LshrByConst : out << "LshrByConst"; return out; @@ -561,6 +563,7 @@ struct AllRewriteRules { RewriteRule<BvComp> rule130; RewriteRule<BvIteConstCond> rule131; RewriteRule<BvIteChildren> rule132; + RewriteRule<BvIteConstChildren> rule133; }; 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 6f9480489..1213c0f05 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_simplification.h +++ b/src/theory/bv/theory_bv_rewrite_rules_simplification.h @@ -68,6 +68,32 @@ inline Node RewriteRule<BvIteChildren>::apply(TNode node) } /** + * BvIteConstChildren + * + * BITVECTOR_ITE with constant children of size one + */ +template <> +inline bool RewriteRule<BvIteConstChildren>::applies(TNode node) +{ + return (node.getKind() == kind::BITVECTOR_ITE + && utils::getSize(node[1]) == 1 + && node[1].isConst() && node[2].isConst()); +} + +template <> +inline Node RewriteRule<BvIteConstChildren>::apply(TNode node) +{ + Debug("bv-rewrite") << "RewriteRule<BvIteConstChildren>(" << node << ")" + << std::endl; + if (utils::isOne(node[1]) && utils::isZero(node[2])) + { + return node[0]; + } + Assert(utils::isZero(node[1]) && utils::isOne(node[2])); + return NodeManager::currentNM()->mkNode(kind::BITVECTOR_NOT, node[0]); +} + +/** * 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 06ff8e77f..f0218bbc5 100644 --- a/src/theory/bv/theory_bv_rewriter.cpp +++ b/src/theory/bv/theory_bv_rewriter.cpp @@ -171,8 +171,8 @@ RewriteResponse TheoryBVRewriter::RewriteITEBv(TNode node, bool prerewrite) Node resultNode = LinearRewriteStrategy<RewriteRule<EvalITEBv>, RewriteRule<BvIteConstCond>, - RewriteRule<BvIteChildren> >::apply(node); - + RewriteRule<BvIteChildren>, + RewriteRule<BvIteConstChildren> >::apply(node); return RewriteResponse(REWRITE_DONE, resultNode); } diff --git a/src/theory/bv/theory_bv_utils.cpp b/src/theory/bv/theory_bv_utils.cpp index e42882a12..470f9ac7f 100644 --- a/src/theory/bv/theory_bv_utils.cpp +++ b/src/theory/bv/theory_bv_utils.cpp @@ -63,6 +63,12 @@ bool isZero(TNode node) return node == mkZero(getSize(node)); } +bool isOne(TNode node) +{ + if (!node.isConst()) return false; + return node == mkOne(getSize(node)); +} + unsigned isPow2Const(TNode node, bool& isNeg) { if (node.getKind() != kind::CONST_BITVECTOR) diff --git a/src/theory/bv/theory_bv_utils.h b/src/theory/bv/theory_bv_utils.h index e4bf90462..9fccf92a7 100644 --- a/src/theory/bv/theory_bv_utils.h +++ b/src/theory/bv/theory_bv_utils.h @@ -55,6 +55,9 @@ unsigned getSignExtendAmount(TNode node); /* Returns true if given node represents a zero bit-vector. */ bool isZero(TNode node); +/* Returns true if given node represents a one bit-vector. */ +bool isOne(TNode node); + /* If node is a constant of the form 2^c or -2^c, then this function returns * c+1. Otherwise, this function returns 0. The flag isNeg is updated to * indicate whether node is negative. */ |