diff options
Diffstat (limited to 'src/theory/bv')
-rw-r--r-- | src/theory/bv/theory_bv.cpp | 4 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_rewrite_rules.h | 6 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_rewrite_rules_normalization.h | 78 |
3 files changed, 87 insertions, 1 deletions
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index 107cb9672..638715ae4 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -767,6 +767,10 @@ Node TheoryBV::ppRewrite(TNode t) } else if (RewriteRule<ZeroExtendEqConst>::applies(t)) { res = RewriteRule<ZeroExtendEqConst>::run<false>(t); } + else if (RewriteRule<NormalizeEqPlusNeg>::applies(t)) + { + res = RewriteRule<NormalizeEqPlusNeg>::run<false>(t); + } // if(t.getKind() == kind::EQUAL && // ((t[0].getKind() == kind::BITVECTOR_MULT && t[1].getKind() == diff --git a/src/theory/bv/theory_bv_rewrite_rules.h b/src/theory/bv/theory_bv_rewrite_rules.h index 1d2e7d9a3..c6fa42ab0 100644 --- a/src/theory/bv/theory_bv_rewrite_rules.h +++ b/src/theory/bv/theory_bv_rewrite_rules.h @@ -31,7 +31,8 @@ namespace CVC4 { namespace theory { namespace bv { -enum RewriteRuleId { +enum RewriteRuleId +{ /// core normalization rules EmptyRule, @@ -175,6 +176,7 @@ enum RewriteRuleId { OrSimplify, XorSimplify, BitwiseSlicing, + NormalizeEqPlusNeg, // rules to simplify bitblasting BBPlusNeg, UltPlusOne, @@ -321,6 +323,7 @@ inline std::ostream& operator << (std::ostream& out, RewriteRuleId ruleId) { case ConcatToMult: out << "ConcatToMult"; return out; case IsPowerOfTwo: out << "IsPowerOfTwo"; return out; case MultSltMult: out << "MultSltMult"; return out; + case NormalizeEqPlusNeg: out << "NormalizeEqPlusNeg"; return out; default: Unreachable(); } @@ -548,6 +551,7 @@ struct AllRewriteRules { RewriteRule<SignExtendUltConst> rule126; RewriteRule<ZeroExtendUltConst> rule127; RewriteRule<MultSltMult> rule128; + RewriteRule<NormalizeEqPlusNeg> rule129; }; template<> inline diff --git a/src/theory/bv/theory_bv_rewrite_rules_normalization.h b/src/theory/bv/theory_bv_rewrite_rules_normalization.h index c2f6620aa..a02bf305f 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_normalization.h +++ b/src/theory/bv/theory_bv_rewrite_rules_normalization.h @@ -1451,6 +1451,84 @@ inline Node RewriteRule<BitwiseSlicing>::apply(TNode node) return result; } +template <> +inline bool RewriteRule<NormalizeEqPlusNeg>::applies(TNode node) +{ + return node.getKind() == kind::EQUAL + && (node[0].getKind() == kind::BITVECTOR_PLUS + || node[1].getKind() == kind::BITVECTOR_PLUS); +} + +template <> +inline Node RewriteRule<NormalizeEqPlusNeg>::apply(TNode node) +{ + Debug("bv-rewrite") << "RewriteRule<NormalizeEqPlusNeg>(" << node << ")" + << std::endl; + + NodeBuilder<> nb_lhs(kind::BITVECTOR_PLUS); + NodeBuilder<> nb_rhs(kind::BITVECTOR_PLUS); + NodeManager *nm = NodeManager::currentNM(); + + if (node[0].getKind() == kind::BITVECTOR_PLUS) + { + for (const TNode &n : node[0]) + { + if (n.getKind() == kind::BITVECTOR_NEG) + nb_rhs << n[0]; + else + nb_lhs << n; + } + } + else + { + nb_lhs << node[0]; + } + + if (node[1].getKind() == kind::BITVECTOR_PLUS) + { + for (const TNode &n : node[1]) + { + if (n.getKind() == kind::BITVECTOR_NEG) + nb_lhs << n[0]; + else + nb_rhs << n; + } + } + else + { + nb_rhs << node[1]; + } + + Node zero = utils::mkZero(utils::getSize(node[0])); + + Node lhs, rhs; + if (nb_lhs.getNumChildren() == 0) + { + lhs = zero; + } + else if (nb_lhs.getNumChildren() == 1) + { + lhs = nb_lhs[0]; + } + else + { + lhs = nb_lhs.constructNode(); + } + if (nb_rhs.getNumChildren() == 0) + { + rhs = zero; + } + else if (nb_rhs.getNumChildren() == 1) + { + rhs = nb_rhs[0]; + } + else + { + rhs = nb_rhs.constructNode(); + } + return nm->mkNode(node.getKind(), lhs, rhs); +} + // template<> inline // bool RewriteRule<>::applies(TNode node) { // return (node.getKind() == kind::BITVECTOR_CONCAT); |