diff options
author | Clark Barrett <barrett@cs.nyu.edu> | 2012-06-13 13:54:14 +0000 |
---|---|---|
committer | Clark Barrett <barrett@cs.nyu.edu> | 2012-06-13 13:54:14 +0000 |
commit | c6aecebe573aeed87ef0661b38af7c3cbc7d641f (patch) | |
tree | 46fe7984b604954b5ee1ce5145bb0624dd2f6e61 /src/theory/bv | |
parent | 3b5f3faa37bb4408946061a8a612015096e21a84 (diff) |
Fixes more problems in bv rewrites
Diffstat (limited to 'src/theory/bv')
-rw-r--r-- | src/theory/bv/theory_bv_rewrite_rules_normalization.h | 28 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_rewriter.cpp | 9 |
2 files changed, 25 insertions, 12 deletions
diff --git a/src/theory/bv/theory_bv_rewrite_rules_normalization.h b/src/theory/bv/theory_bv_rewrite_rules_normalization.h index f8399041d..896133e46 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_normalization.h +++ b/src/theory/bv/theory_bv_rewrite_rules_normalization.h @@ -134,11 +134,20 @@ Node RewriteRule<ExtractArith2>::apply(TNode node) { template<> inline bool RewriteRule<FlattenAssocCommut>::applies(TNode node) { - return (node.getKind() == kind::BITVECTOR_PLUS || - node.getKind() == kind::BITVECTOR_MULT || - node.getKind() == kind::BITVECTOR_OR || - node.getKind() == kind::BITVECTOR_XOR || - node.getKind() == kind::BITVECTOR_AND); + Kind kind = node.getKind(); + if (kind != kind::BITVECTOR_PLUS && + kind != kind::BITVECTOR_MULT && + kind != kind::BITVECTOR_OR && + kind != kind::BITVECTOR_XOR && + 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; } @@ -329,9 +338,12 @@ bool RewriteRule<MultSimplify>::applies(TNode node) { return true; } } - if ((*child_it).isConst() && - (*child_it).getConst<BitVector>() == BitVector(utils::getSize(node), (unsigned) 0)) { - return true; + if ((*child_it).isConst()) { + BitVector bv = (*child_it).getConst<BitVector>(); + if (bv == BitVector(utils::getSize(node), (unsigned) 0) || + bv == BitVector(utils::getSize(node), (unsigned) 1)) { + return true; + } } return false; } diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp index c2a5780a3..955acf707 100644 --- a/src/theory/bv/theory_bv_rewriter.cpp +++ b/src/theory/bv/theory_bv_rewriter.cpp @@ -319,13 +319,14 @@ RewriteResponse TheoryBVRewriter::RewriteMult(TNode node, bool preregister) { } RewriteResponse TheoryBVRewriter::RewritePlus(TNode node, bool preregister) { - Node resultNode = node; - - resultNode = LinearRewriteStrategy + if (preregister) { + return RewriteResponse(REWRITE_DONE, node); + } + Node resultNode = LinearRewriteStrategy < RewriteRule<FlattenAssocCommut>, RewriteRule<PlusCombineLikeTerms> // RewriteRule<PlusLiftConcat> - >::apply(resultNode); + >::apply(node); if (resultNode == node) { return RewriteResponse(REWRITE_DONE, resultNode); } else { |