diff options
author | lianah <lianahady@gmail.com> | 2013-10-09 18:48:07 -0400 |
---|---|---|
committer | lianah <lianahady@gmail.com> | 2013-10-09 18:48:07 -0400 |
commit | 5ffddfd87d690b915d46685cf07e8399fba028b9 (patch) | |
tree | 9c270a639274b2ab53712db7dfe72b34393331b6 /src/theory | |
parent | 44485520fae92b34e4385d4d2c4774c9dd7d0dc0 (diff) |
fixed options::proof() segfault
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/bv/theory_bv_rewrite_rules.h | 3 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_rewrite_rules_normalization.h | 30 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_rewriter.cpp | 6 |
3 files changed, 39 insertions, 0 deletions
diff --git a/src/theory/bv/theory_bv_rewrite_rules.h b/src/theory/bv/theory_bv_rewrite_rules.h index 8426afb59..db48a1d05 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 { PlusCombineLikeTerms, MultSimplify, MultDistribConst, + MultDistribVariable, SolveEq, BitwiseEq, AndSimplify, @@ -265,6 +266,7 @@ inline std::ostream& operator << (std::ostream& out, RewriteRuleId ruleId) { case PlusCombineLikeTerms: out << "PlusCombineLikeTerms"; return out; case MultSimplify: out << "MultSimplify"; return out; case MultDistribConst: out << "MultDistribConst"; return out; + case MultDistribVariable: out << "MultDistribConst"; return out; case SolveEq : out << "SolveEq"; return out; case BitwiseEq : out << "BitwiseEq"; return out; case NegMult : out << "NegMult"; return out; @@ -498,6 +500,7 @@ struct AllRewriteRules { RewriteRule<SltZero> rule115; RewriteRule<BVToNatEliminate> rule116; RewriteRule<IntToBVEliminate> rule117; + RewriteRule<MultDistribVariable> rule118; }; 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 2da4dfa6a..bb5c94b1e 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_normalization.h +++ b/src/theory/bv/theory_bv_rewrite_rules_normalization.h @@ -432,6 +432,36 @@ Node RewriteRule<MultSimplify>::apply(TNode node) { } template<> inline +bool RewriteRule<MultDistribVariable>::applies(TNode node) { + if (node.getKind() != kind::BITVECTOR_MULT || + node.getNumChildren() != 2) { + return false; + } + Assert(!node[0].isConst()); + if (!node[1].getNumChildren() == 0) { + return false; + } + TNode factor = node[0]; + return (factor.getKind() == kind::BITVECTOR_PLUS || + factor.getKind() == kind::BITVECTOR_SUB); +} + +template<> inline +Node RewriteRule<MultDistribVariable>::apply(TNode node) { + Debug("bv-rewrite") << "RewriteRule<MultDistrib>(" << node << ")" << std::endl; + TNode var = node[1]; + TNode factor = node[0]; + + std::vector<Node> children; + for(unsigned i = 0; i < factor.getNumChildren(); ++i) { + children.push_back(utils::mkNode(kind::BITVECTOR_MULT, factor[i], var)); + } + + return utils::mkNode(factor.getKind(), children); +} + + +template<> inline bool RewriteRule<MultDistribConst>::applies(TNode node) { if (node.getKind() != kind::BITVECTOR_MULT || node.getNumChildren() != 2) { diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp index 2467ae3f1..76eb97b39 100644 --- a/src/theory/bv/theory_bv_rewriter.cpp +++ b/src/theory/bv/theory_bv_rewriter.cpp @@ -332,6 +332,12 @@ RewriteResponse TheoryBVRewriter::RewriteMult(TNode node, bool prerewrite) { // creating new terms that might simplify further return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); } + if(RewriteRule<MultDistribVariable>::applies(resultNode)) { + resultNode = RewriteRule<MultDistribVariable>::run<false>(resultNode); + // creating new terms that might simplify further + return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); + } + } if(resultNode == node) { |