diff options
author | lianah <lianahady@gmail.com> | 2014-10-23 11:05:21 -0700 |
---|---|---|
committer | lianah <lianahady@gmail.com> | 2014-10-23 11:05:21 -0700 |
commit | 1c8d1d7c5831baebc0a59a7dcf36f942504e5556 (patch) | |
tree | 421e8dcb885d1d3d47ead354184f6ab02dc3dff8 /src | |
parent | 28027d15202a0dea0c13f5b01188ec3f1c4f0c38 (diff) |
Fixed inefficiency in bit-vector rewrite rule.
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/bv/theory_bv_rewrite_rules.h | 7 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_rewrite_rules_normalization.h | 45 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_rewriter.cpp | 4 |
3 files changed, 52 insertions, 4 deletions
diff --git a/src/theory/bv/theory_bv_rewrite_rules.h b/src/theory/bv/theory_bv_rewrite_rules.h index bc9095f03..3cc1c323c 100644 --- a/src/theory/bv/theory_bv_rewrite_rules.h +++ b/src/theory/bv/theory_bv_rewrite_rules.h @@ -152,6 +152,7 @@ enum RewriteRuleId { NotOr, // not sure why this would help (not done) NotXor, // not sure why this would help (not done) FlattenAssocCommut, + FlattenAssocCommutNoDuplicates, PlusCombineLikeTerms, MultSimplify, MultDistribConst, @@ -270,7 +271,8 @@ inline std::ostream& operator << (std::ostream& out, RewriteRuleId ruleId) { case SignExtendEliminate : out << "SignExtendEliminate"; return out; case NotIdemp : out << "NotIdemp"; return out; case UleSelf: out << "UleSelf"; return out; - case FlattenAssocCommut: out << "FlattenAssocCommut"; return out; + case FlattenAssocCommut: out << "FlattenAssocCommut"; return out; + case FlattenAssocCommutNoDuplicates: out << "FlattenAssocCommutNoDuplicates"; return out; case PlusCombineLikeTerms: out << "PlusCombineLikeTerms"; return out; case MultSimplify: out << "MultSimplify"; return out; case MultDistribConst: out << "MultDistribConst"; return out; @@ -485,8 +487,9 @@ struct AllRewriteRules { RewriteRule<SubEliminate> rule82; RewriteRule<XorOne> rule83; RewriteRule<XorZero> rule84; - RewriteRule<MultPow2> rule87; RewriteRule<MultSlice> rule85; + RewriteRule<FlattenAssocCommutNoDuplicates> rule86; + RewriteRule<MultPow2> rule87; RewriteRule<ExtractMultLeadingBit> rule88; RewriteRule<NegIdemp> rule91; RewriteRule<UdivPow2> rule92; diff --git a/src/theory/bv/theory_bv_rewrite_rules_normalization.h b/src/theory/bv/theory_bv_rewrite_rules_normalization.h index 21b59fa8c..bc1b92dce 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_normalization.h +++ b/src/theory/bv/theory_bv_rewrite_rules_normalization.h @@ -996,6 +996,51 @@ Node RewriteRule<AndSimplify>::apply(TNode node) { } template<> inline +bool RewriteRule<FlattenAssocCommutNoDuplicates>::applies(TNode node) { + Kind kind = node.getKind(); + if (kind != kind::BITVECTOR_OR && + kind != kind::BITVECTOR_AND) + return false; + TNode::iterator child_it = node.begin(); + for(; child_it != node.end(); ++child_it) { + if ((*child_it).getKind() == kind) { + return true; + } + } + return false; +} + +template<> inline +Node RewriteRule<FlattenAssocCommutNoDuplicates>::apply(TNode node) { + Debug("bv-rewrite") << "RewriteRule<FlattenAssocCommut>(" << node << ")" << std::endl; + std::vector<Node> processingStack; + processingStack.push_back(node); + __gnu_cxx::hash_set<TNode, TNodeHashFunction> processed; + std::vector<Node> children; + Kind kind = node.getKind(); + + while (! processingStack.empty()) { + TNode current = processingStack.back(); + processingStack.pop_back(); + if (processed.count(current)) + continue; + + processed.insert(current); + + // flatten expression + if (current.getKind() == kind) { + for (unsigned i = 0; i < current.getNumChildren(); ++i) { + processingStack.push_back(current[i]); + } + } else { + children.push_back(current); + } + } + return utils::mkSortedNode(kind, children); +} + + +template<> inline bool RewriteRule<OrSimplify>::applies(TNode node) { return (node.getKind() == kind::BITVECTOR_OR); } diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp index 306a3bd97..dc91c338b 100644 --- a/src/theory/bv/theory_bv_rewriter.cpp +++ b/src/theory/bv/theory_bv_rewriter.cpp @@ -214,7 +214,7 @@ RewriteResponse TheoryBVRewriter::RewriteConcat(TNode node, bool prerewrite) { RewriteResponse TheoryBVRewriter::RewriteAnd(TNode node, bool prerewrite) { Node resultNode = node; resultNode = LinearRewriteStrategy - < RewriteRule<FlattenAssocCommut>, + < RewriteRule<FlattenAssocCommutNoDuplicates>, RewriteRule<AndSimplify> >::apply(node); @@ -234,7 +234,7 @@ RewriteResponse TheoryBVRewriter::RewriteAnd(TNode node, bool prerewrite) { RewriteResponse TheoryBVRewriter::RewriteOr(TNode node, bool prerewrite){ Node resultNode = node; resultNode = LinearRewriteStrategy - < RewriteRule<FlattenAssocCommut>, + < RewriteRule<FlattenAssocCommutNoDuplicates>, RewriteRule<OrSimplify> >::apply(node); |