From: Aina Niemetz Date: Thu, 2 Aug 2018 18:52:32 +0000 (-0700) Subject: Add rewrites for BITVECTOR_ITE and BITVECTOR_COMP with const condition/child. (#2259) X-Git-Tag: cvc5-1.0.0~4827 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=db53123fe114732b647f87e6dd6ee756ca43c291;p=cvc5.git Add rewrites for BITVECTOR_ITE and BITVECTOR_COMP with const condition/child. (#2259) --- diff --git a/src/theory/bv/theory_bv_rewrite_rules.h b/src/theory/bv/theory_bv_rewrite_rules.h index 25f9eccbb..1eb815ef9 100644 --- a/src/theory/bv/theory_bv_rewrite_rules.h +++ b/src/theory/bv/theory_bv_rewrite_rules.h @@ -104,6 +104,8 @@ enum RewriteRuleId /// simplification rules /// all of these rules decrease formula size + BvIte, + BvComp, ShlByConst, LshrByConst, AshrByConst, @@ -240,6 +242,8 @@ inline std::ostream& operator << (std::ostream& out, RewriteRuleId ruleId) { case EvalRotateLeft : out << "EvalRotateLeft"; return out; case EvalRotateRight : out << "EvalRotateRight"; return out; case EvalNeg : out << "EvalNeg"; return out; + case BvIte : out << "BvIte"; return out; + case BvComp : out << "BvComp"; return out; case ShlByConst : out << "ShlByConst"; return out; case LshrByConst : out << "LshrByConst"; return out; case AshrByConst : out << "AshrByConst"; return out; @@ -474,6 +478,7 @@ struct AllRewriteRules { RewriteRule rule46; RewriteRule rule47; RewriteRule rule48; + RewriteRule rule49; RewriteRule rule50; RewriteRule rule51; RewriteRule rule52; @@ -552,6 +557,7 @@ struct AllRewriteRules { RewriteRule rule127; RewriteRule rule128; RewriteRule rule129; + RewriteRule rule130; }; 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 397385996..9649fec77 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_simplification.h +++ b/src/theory/bv/theory_bv_rewrite_rules_simplification.h @@ -29,6 +29,50 @@ namespace bv { // FIXME: this rules subsume the constant evaluation ones +/** + * BvIte + * + * BITVECTOR_ITE with constant condition + */ +template <> +inline bool RewriteRule::applies(TNode node) +{ + return (node.getKind() == kind::BITVECTOR_ITE && node[0].isConst()); +} + +template <> +inline Node RewriteRule::apply(TNode node) +{ + Debug("bv-rewrite") << "RewriteRule(" << node << ")" << std::endl; + return utils::isZero(node[0]) ? node[2] : node[1]; +} + +/** + * BvComp + * + * BITVECTOR_COMP of children of size 1 with one constant child + */ +template <> +inline bool RewriteRule::applies(TNode node) +{ + return (node.getKind() == kind::BITVECTOR_COMP + && utils::getSize(node[0]) == 1 + && (node[0].isConst() || node[1].isConst())); +} + +template <> +inline Node RewriteRule::apply(TNode node) +{ + Debug("bv-rewrite") << "RewriteRule(" << node << ")" << std::endl; + NodeManager* nm = NodeManager::currentNM(); + if (node[0].isConst()) + { + return utils::isZero(node[0]) ? nm->mkNode(kind::BITVECTOR_NOT, node[1]) + : Node(node[1]); + } + return utils::isZero(node[1]) ? nm->mkNode(kind::BITVECTOR_NOT, node[0]) + : Node(node[0]); +} /** * ShlByConst diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp index aca44aa37..6355da07d 100644 --- a/src/theory/bv/theory_bv_rewriter.cpp +++ b/src/theory/bv/theory_bv_rewriter.cpp @@ -166,12 +166,13 @@ RewriteResponse TheoryBVRewriter::RewriteSge(TNode node, bool prerewrite){ return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); } -RewriteResponse TheoryBVRewriter::RewriteITEBv(TNode node, bool prerewrite){ - Node resultNode = LinearRewriteStrategy - < RewriteRule < EvalITEBv > - >::apply(node); +RewriteResponse TheoryBVRewriter::RewriteITEBv(TNode node, bool prerewrite) +{ + Node resultNode = + LinearRewriteStrategy, RewriteRule >::apply( + node); - return RewriteResponse(REWRITE_DONE, resultNode); + return RewriteResponse(REWRITE_DONE, resultNode); } RewriteResponse TheoryBVRewriter::RewriteNot(TNode node, bool prerewrite){ @@ -329,12 +330,13 @@ RewriteResponse TheoryBVRewriter::RewriteNor(TNode node, bool prerewrite) { return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); } -RewriteResponse TheoryBVRewriter::RewriteComp(TNode node, bool prerewrite) { - Node resultNode = LinearRewriteStrategy - < RewriteRule < EvalComp > - >::apply(node); +RewriteResponse TheoryBVRewriter::RewriteComp(TNode node, bool prerewrite) +{ + Node resultNode = + LinearRewriteStrategy, RewriteRule >::apply( + node); - return RewriteResponse(REWRITE_DONE, resultNode); + return RewriteResponse(REWRITE_DONE, resultNode); } RewriteResponse TheoryBVRewriter::RewriteMult(TNode node, bool prerewrite) { diff --git a/src/theory/bv/theory_bv_utils.cpp b/src/theory/bv/theory_bv_utils.cpp index 7c5a68259..e42882a12 100644 --- a/src/theory/bv/theory_bv_utils.cpp +++ b/src/theory/bv/theory_bv_utils.cpp @@ -89,7 +89,9 @@ unsigned isPow2Const(TNode node, bool& isNeg) bool isBvConstTerm(TNode node) { - if (node.getNumChildren() == 0) { return node.isConst(); + if (node.getNumChildren() == 0) + { + return node.isConst(); } for (const TNode& n : node)