diff options
| author | lianah <lianahady@gmail.com> | 2013-04-30 15:52:40 -0400 |
|---|---|---|
| committer | lianah <lianahady@gmail.com> | 2013-04-30 15:54:24 -0400 |
| commit | a6cbb4dd9f8c8e5d53f0d4b77e177bfa4cc2fb92 (patch) | |
| tree | 6387d38e2034150522c44004278c09a2d3e6ff80 | |
| parent | 2ba4f51d43406c9475116abbab7f3ebea94679af (diff) | |
updated the author name
| -rw-r--r-- | src/theory/bv/theory_bv_rewrite_rules_normalization.h | 2 | ||||
| -rw-r--r-- | src/theory/bv/theory_bv_rewriter.cpp | 20 |
2 files changed, 11 insertions, 11 deletions
diff --git a/src/theory/bv/theory_bv_rewrite_rules_normalization.h b/src/theory/bv/theory_bv_rewrite_rules_normalization.h index 035bd4469..2da4dfa6a 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_normalization.h +++ b/src/theory/bv/theory_bv_rewrite_rules_normalization.h @@ -1120,7 +1120,7 @@ template<> inline Node RewriteRule<BitwiseSlicing>::apply(TNode node) { Debug("bv-rewrite") << "RewriteRule<BitwiseSlicing>(" << node << ")" << std::endl; // get the constant - bool found_constant = false; + bool found_constant CVC4_UNUSED = false ; TNode constant; std::vector<Node> other_children; for (unsigned i = 0; i < node.getNumChildren(); ++i) { diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp index 44c498947..0775cb1f8 100644 --- a/src/theory/bv/theory_bv_rewriter.cpp +++ b/src/theory/bv/theory_bv_rewriter.cpp @@ -177,10 +177,10 @@ RewriteResponse TheoryBVRewriter::RewriteExtract(TNode node, bool preregister) { return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); } - // if (RewriteRule<ExtractSignExtend>::applies(node)) { - // resultNode = RewriteRule<ExtractSignExtend>::run<false>(node); - // return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); - // } + if (RewriteRule<ExtractSignExtend>::applies(node)) { + resultNode = RewriteRule<ExtractSignExtend>::run<false>(node); + return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); + } if (RewriteRule<ExtractBitwise>::applies(node)) { resultNode = RewriteRule<ExtractBitwise>::run<false>(node); @@ -228,8 +228,8 @@ RewriteResponse TheoryBVRewriter::RewriteAnd(TNode node, bool preregister){ resultNode = LinearRewriteStrategy < RewriteRule<FlattenAssocCommut>, - RewriteRule<AndSimplify>//, - // RewriteRule<BitwiseSlicing> + RewriteRule<AndSimplify>, + RewriteRule<BitwiseSlicing> >::apply(node); if (resultNode.getKind() != node.getKind()) { @@ -244,8 +244,8 @@ RewriteResponse TheoryBVRewriter::RewriteOr(TNode node, bool preregister){ resultNode = LinearRewriteStrategy < RewriteRule<FlattenAssocCommut>, - RewriteRule<OrSimplify>//, - // RewriteRule<BitwiseSlicing> + RewriteRule<OrSimplify>, + RewriteRule<BitwiseSlicing> >::apply(node); if (resultNode.getKind() != node.getKind()) { @@ -261,8 +261,8 @@ RewriteResponse TheoryBVRewriter::RewriteXor(TNode node, bool preregister) { resultNode = LinearRewriteStrategy < RewriteRule<FlattenAssocCommut>, // flatten the expression RewriteRule<XorSimplify>, // simplify duplicates and constants - RewriteRule<XorZero>//, // checks if the constant part is zero and eliminates it - // RewriteRule<BitwiseSlicing> + RewriteRule<XorZero>, // checks if the constant part is zero and eliminates it + RewriteRule<BitwiseSlicing> >::apply(node); // this simplification introduces new terms and might require further |