diff options
author | lianah <lianahady@gmail.com> | 2013-05-07 16:03:56 -0400 |
---|---|---|
committer | lianah <lianahady@gmail.com> | 2013-05-07 16:04:03 -0400 |
commit | 861d976c5c4c3d2898d6148cabd2763a020aa7ba (patch) | |
tree | 89341cdcc9ca7717e8b3aec40d37b69c5cd2feb5 /src/theory/bv | |
parent | e138840f8dbe4eedf692ca81a99e6415737b573c (diff) |
fixed bv rewrite blow-up
Diffstat (limited to 'src/theory/bv')
-rw-r--r-- | src/theory/bv/theory_bv_rewriter.cpp | 137 |
1 files changed, 69 insertions, 68 deletions
diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp index 9c072444d..621ae25c0 100644 --- a/src/theory/bv/theory_bv_rewriter.cpp +++ b/src/theory/bv/theory_bv_rewriter.cpp @@ -70,7 +70,7 @@ RewriteResponse TheoryBVRewriter::postRewrite(TNode node) { return res; } -RewriteResponse TheoryBVRewriter::RewriteUlt(TNode node, bool preregister) { +RewriteResponse TheoryBVRewriter::RewriteUlt(TNode node, bool prerewrite) { // reduce common subexpressions on both sides Node resultNode = LinearRewriteStrategy < RewriteRule<EvalUlt>, @@ -82,7 +82,7 @@ RewriteResponse TheoryBVRewriter::RewriteUlt(TNode node, bool preregister) { return RewriteResponse(REWRITE_DONE, resultNode); } -RewriteResponse TheoryBVRewriter::RewriteSlt(TNode node, bool preregister){ +RewriteResponse TheoryBVRewriter::RewriteSlt(TNode node, bool prerewrite){ Node resultNode = LinearRewriteStrategy < RewriteRule < EvalSlt > >::apply(node); @@ -97,7 +97,7 @@ RewriteResponse TheoryBVRewriter::RewriteSlt(TNode node, bool preregister){ // return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); } -RewriteResponse TheoryBVRewriter::RewriteUle(TNode node, bool preregister){ +RewriteResponse TheoryBVRewriter::RewriteUle(TNode node, bool prerewrite){ Node resultNode = LinearRewriteStrategy < RewriteRule<EvalUle>, RewriteRule<UleMax>, @@ -109,7 +109,7 @@ RewriteResponse TheoryBVRewriter::RewriteUle(TNode node, bool preregister){ return RewriteResponse(resultNode == node ? REWRITE_DONE : REWRITE_AGAIN, resultNode); } -RewriteResponse TheoryBVRewriter::RewriteSle(TNode node, bool preregister){ +RewriteResponse TheoryBVRewriter::RewriteSle(TNode node, bool prerewrite){ Node resultNode = LinearRewriteStrategy < RewriteRule <EvalSle>, RewriteRule <SleEliminate> @@ -117,7 +117,7 @@ RewriteResponse TheoryBVRewriter::RewriteSle(TNode node, bool preregister){ return RewriteResponse(resultNode == node? REWRITE_DONE : REWRITE_AGAIN, resultNode); } -RewriteResponse TheoryBVRewriter::RewriteUgt(TNode node, bool preregister){ +RewriteResponse TheoryBVRewriter::RewriteUgt(TNode node, bool prerewrite){ Node resultNode = LinearRewriteStrategy < RewriteRule<UgtEliminate> >::apply(node); @@ -125,7 +125,7 @@ RewriteResponse TheoryBVRewriter::RewriteUgt(TNode node, bool preregister){ return RewriteResponse(REWRITE_AGAIN, resultNode); } -RewriteResponse TheoryBVRewriter::RewriteSgt(TNode node, bool preregister){ +RewriteResponse TheoryBVRewriter::RewriteSgt(TNode node, bool prerewrite){ Node resultNode = LinearRewriteStrategy < RewriteRule<SgtEliminate> //RewriteRule<SltEliminate> @@ -134,7 +134,7 @@ RewriteResponse TheoryBVRewriter::RewriteSgt(TNode node, bool preregister){ return RewriteResponse(REWRITE_AGAIN, resultNode); } -RewriteResponse TheoryBVRewriter::RewriteUge(TNode node, bool preregister){ +RewriteResponse TheoryBVRewriter::RewriteUge(TNode node, bool prerewrite){ Node resultNode = LinearRewriteStrategy < RewriteRule<UgeEliminate> >::apply(node); @@ -142,7 +142,7 @@ RewriteResponse TheoryBVRewriter::RewriteUge(TNode node, bool preregister){ return RewriteResponse(REWRITE_AGAIN, resultNode); } -RewriteResponse TheoryBVRewriter::RewriteSge(TNode node, bool preregister){ +RewriteResponse TheoryBVRewriter::RewriteSge(TNode node, bool prerewrite){ Node resultNode = LinearRewriteStrategy < RewriteRule<SgeEliminate> // RewriteRule<SleEliminate> @@ -151,7 +151,7 @@ RewriteResponse TheoryBVRewriter::RewriteSge(TNode node, bool preregister){ return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); } -RewriteResponse TheoryBVRewriter::RewriteNot(TNode node, bool preregister){ +RewriteResponse TheoryBVRewriter::RewriteNot(TNode node, bool prerewrite){ Node resultNode = node; if(RewriteRule<NotXor>::applies(node)) { @@ -166,7 +166,7 @@ RewriteResponse TheoryBVRewriter::RewriteNot(TNode node, bool preregister){ return RewriteResponse(REWRITE_DONE, resultNode); } -RewriteResponse TheoryBVRewriter::RewriteExtract(TNode node, bool preregister) { +RewriteResponse TheoryBVRewriter::RewriteExtract(TNode node, bool prerewrite) { Node resultNode = node; if (RewriteRule<ExtractConcat>::applies(node)) { @@ -206,7 +206,7 @@ RewriteResponse TheoryBVRewriter::RewriteExtract(TNode node, bool preregister) { } -RewriteResponse TheoryBVRewriter::RewriteConcat(TNode node, bool preregister) { +RewriteResponse TheoryBVRewriter::RewriteConcat(TNode node, bool prerewrite) { Node resultNode = LinearRewriteStrategy < RewriteRule<ConcatFlatten>, @@ -220,15 +220,18 @@ RewriteResponse TheoryBVRewriter::RewriteConcat(TNode node, bool preregister) { return RewriteResponse(REWRITE_DONE, resultNode); } -RewriteResponse TheoryBVRewriter::RewriteAnd(TNode node, bool preregister){ +RewriteResponse TheoryBVRewriter::RewriteAnd(TNode node, bool prerewrite) { Node resultNode = node; - if (!preregister) { + resultNode = LinearRewriteStrategy + < RewriteRule<FlattenAssocCommut>, + RewriteRule<AndSimplify> + >::apply(node); + + if (!prerewrite) { resultNode = LinearRewriteStrategy - < RewriteRule<FlattenAssocCommut>, - RewriteRule<AndSimplify>, - RewriteRule<BitwiseSlicing> + < RewriteRule<BitwiseSlicing> >::apply(node); - + if (resultNode.getKind() != node.getKind()) { return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); } @@ -237,39 +240,41 @@ RewriteResponse TheoryBVRewriter::RewriteAnd(TNode node, bool preregister){ return RewriteResponse(REWRITE_DONE, resultNode); } -RewriteResponse TheoryBVRewriter::RewriteOr(TNode node, bool preregister){ +RewriteResponse TheoryBVRewriter::RewriteOr(TNode node, bool prerewrite){ Node resultNode = node; - if (! preregister) { + resultNode = LinearRewriteStrategy + < RewriteRule<FlattenAssocCommut>, + RewriteRule<OrSimplify> + >::apply(node); + + if (!prerewrite) { resultNode = LinearRewriteStrategy - < RewriteRule<FlattenAssocCommut>, - RewriteRule<OrSimplify>, - RewriteRule<BitwiseSlicing> + < RewriteRule<BitwiseSlicing> >::apply(node); - + if (resultNode.getKind() != node.getKind()) { return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); } } + return RewriteResponse(REWRITE_DONE, resultNode); } -RewriteResponse TheoryBVRewriter::RewriteXor(TNode node, bool preregister) { +RewriteResponse TheoryBVRewriter::RewriteXor(TNode node, bool prerewrite) { Node resultNode = node; - if (! 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> + >::apply(node); + + if (!prerewrite) { 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<XorOne>, + RewriteRule <BitwiseSlicing> >::apply(node); - // this simplification introduces new terms and might require further - // rewriting - if (RewriteRule<XorOne>::applies(resultNode)) { - resultNode = RewriteRule<XorOne>::run<false> (resultNode); - return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); - } - if (resultNode.getKind() != node.getKind()) { return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); } @@ -278,7 +283,7 @@ RewriteResponse TheoryBVRewriter::RewriteXor(TNode node, bool preregister) { return RewriteResponse(REWRITE_DONE, resultNode); } -RewriteResponse TheoryBVRewriter::RewriteXnor(TNode node, bool preregister) { +RewriteResponse TheoryBVRewriter::RewriteXnor(TNode node, bool prerewrite) { Node resultNode = LinearRewriteStrategy < RewriteRule<XnorEliminate> >::apply(node); @@ -286,7 +291,7 @@ RewriteResponse TheoryBVRewriter::RewriteXnor(TNode node, bool preregister) { return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); } -RewriteResponse TheoryBVRewriter::RewriteNand(TNode node, bool preregister) { +RewriteResponse TheoryBVRewriter::RewriteNand(TNode node, bool prerewrite) { Node resultNode = LinearRewriteStrategy < RewriteRule<NandEliminate> >::apply(node); @@ -294,7 +299,7 @@ RewriteResponse TheoryBVRewriter::RewriteNand(TNode node, bool preregister) { return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); } -RewriteResponse TheoryBVRewriter::RewriteNor(TNode node, bool preregister) { +RewriteResponse TheoryBVRewriter::RewriteNor(TNode node, bool prerewrite) { Node resultNode = LinearRewriteStrategy < RewriteRule<NorEliminate> >::apply(node); @@ -302,7 +307,7 @@ RewriteResponse TheoryBVRewriter::RewriteNor(TNode node, bool preregister) { return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); } -RewriteResponse TheoryBVRewriter::RewriteComp(TNode node, bool preregister) { +RewriteResponse TheoryBVRewriter::RewriteComp(TNode node, bool prerewrite) { Node resultNode = LinearRewriteStrategy < RewriteRule<CompEliminate> >::apply(node); @@ -310,7 +315,7 @@ RewriteResponse TheoryBVRewriter::RewriteComp(TNode node, bool preregister) { return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); } -RewriteResponse TheoryBVRewriter::RewriteMult(TNode node, bool preregister) { +RewriteResponse TheoryBVRewriter::RewriteMult(TNode node, bool prerewrite) { Node resultNode = node; resultNode = LinearRewriteStrategy @@ -320,7 +325,7 @@ RewriteResponse TheoryBVRewriter::RewriteMult(TNode node, bool preregister) { >::apply(node); // only apply if every subterm was already rewritten - if (!preregister) { + if (!prerewrite) { // distributes multiplication by constant over +, - and unary - if(RewriteRule<MultDistribConst>::applies(resultNode)) { resultNode = RewriteRule<MultDistribConst>::run<false>(resultNode); @@ -335,23 +340,19 @@ RewriteResponse TheoryBVRewriter::RewriteMult(TNode node, bool preregister) { return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); } -RewriteResponse TheoryBVRewriter::RewritePlus(TNode node, bool preregister) { - if (preregister) { - return RewriteResponse(REWRITE_DONE, node); - } +RewriteResponse TheoryBVRewriter::RewritePlus(TNode node, bool prerewrite) { Node resultNode = LinearRewriteStrategy < RewriteRule<FlattenAssocCommut>, RewriteRule<PlusCombineLikeTerms> - // RewriteRule<PlusLiftConcat> >::apply(node); - if (resultNode == node) { + if (prerewrite || node == resultNode) { return RewriteResponse(REWRITE_DONE, resultNode); - } else { - return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); } + + return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); } -RewriteResponse TheoryBVRewriter::RewriteSub(TNode node, bool preregister){ +RewriteResponse TheoryBVRewriter::RewriteSub(TNode node, bool prerewrite){ // return RewriteResponse(REWRITE_DONE, node); Node resultNode = LinearRewriteStrategy < RewriteRule<SubEliminate> @@ -360,7 +361,7 @@ RewriteResponse TheoryBVRewriter::RewriteSub(TNode node, bool preregister){ return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); } -RewriteResponse TheoryBVRewriter::RewriteNeg(TNode node, bool preregister) { +RewriteResponse TheoryBVRewriter::RewriteNeg(TNode node, bool prerewrite) { Node resultNode = node; resultNode = LinearRewriteStrategy @@ -374,7 +375,7 @@ RewriteResponse TheoryBVRewriter::RewriteNeg(TNode node, bool preregister) { return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); } - if(!preregister) { + if(!prerewrite) { if (RewriteRule<NegMult>::applies(node)) { resultNode = RewriteRule<NegMult>::run<false>(node); return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); @@ -385,7 +386,7 @@ RewriteResponse TheoryBVRewriter::RewriteNeg(TNode node, bool preregister) { } -RewriteResponse TheoryBVRewriter::RewriteUdivTotal(TNode node, bool preregister){ +RewriteResponse TheoryBVRewriter::RewriteUdivTotal(TNode node, bool prerewrite){ Node resultNode = node; if(RewriteRule<UdivPow2>::applies(node)) { @@ -402,7 +403,7 @@ RewriteResponse TheoryBVRewriter::RewriteUdivTotal(TNode node, bool preregister) return RewriteResponse(REWRITE_DONE, resultNode); } -RewriteResponse TheoryBVRewriter::RewriteUremTotal(TNode node, bool preregister) { +RewriteResponse TheoryBVRewriter::RewriteUremTotal(TNode node, bool prerewrite) { Node resultNode = node; if(RewriteRule<UremPow2>::applies(node)) { @@ -418,7 +419,7 @@ RewriteResponse TheoryBVRewriter::RewriteUremTotal(TNode node, bool preregister) return RewriteResponse(REWRITE_DONE, resultNode); } -RewriteResponse TheoryBVRewriter::RewriteSmod(TNode node, bool preregister) { +RewriteResponse TheoryBVRewriter::RewriteSmod(TNode node, bool prerewrite) { Node resultNode = LinearRewriteStrategy < RewriteRule<SmodEliminate> >::apply(node); @@ -426,7 +427,7 @@ RewriteResponse TheoryBVRewriter::RewriteSmod(TNode node, bool preregister) { return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); } -RewriteResponse TheoryBVRewriter::RewriteSdiv(TNode node, bool preregister) { +RewriteResponse TheoryBVRewriter::RewriteSdiv(TNode node, bool prerewrite) { Node resultNode = LinearRewriteStrategy < RewriteRule<SdivEliminate> >::apply(node); @@ -434,14 +435,14 @@ RewriteResponse TheoryBVRewriter::RewriteSdiv(TNode node, bool preregister) { return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); } -RewriteResponse TheoryBVRewriter::RewriteSrem(TNode node, bool preregister) { +RewriteResponse TheoryBVRewriter::RewriteSrem(TNode node, bool prerewrite) { Node resultNode = LinearRewriteStrategy < RewriteRule<SremEliminate> >::apply(node); return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); } -RewriteResponse TheoryBVRewriter::RewriteShl(TNode node, bool preregister) { +RewriteResponse TheoryBVRewriter::RewriteShl(TNode node, bool prerewrite) { Node resultNode = node; if(RewriteRule<ShlByConst>::applies(node)) { resultNode = RewriteRule<ShlByConst>::run <false> (node); @@ -456,7 +457,7 @@ RewriteResponse TheoryBVRewriter::RewriteShl(TNode node, bool preregister) { return RewriteResponse(REWRITE_DONE, resultNode); } -RewriteResponse TheoryBVRewriter::RewriteLshr(TNode node, bool preregister) { +RewriteResponse TheoryBVRewriter::RewriteLshr(TNode node, bool prerewrite) { Node resultNode = node; if(RewriteRule<LshrByConst>::applies(node)) { resultNode = RewriteRule<LshrByConst>::run <false> (node); @@ -471,7 +472,7 @@ RewriteResponse TheoryBVRewriter::RewriteLshr(TNode node, bool preregister) { return RewriteResponse(REWRITE_DONE, resultNode); } -RewriteResponse TheoryBVRewriter::RewriteAshr(TNode node, bool preregister) { +RewriteResponse TheoryBVRewriter::RewriteAshr(TNode node, bool prerewrite) { Node resultNode = node; if(RewriteRule<AshrByConst>::applies(node)) { resultNode = RewriteRule<AshrByConst>::run <false> (node); @@ -487,7 +488,7 @@ RewriteResponse TheoryBVRewriter::RewriteAshr(TNode node, bool preregister) { } -RewriteResponse TheoryBVRewriter::RewriteRepeat(TNode node, bool preregister) { +RewriteResponse TheoryBVRewriter::RewriteRepeat(TNode node, bool prerewrite) { Node resultNode = LinearRewriteStrategy < RewriteRule<RepeatEliminate > >::apply(node); @@ -495,7 +496,7 @@ RewriteResponse TheoryBVRewriter::RewriteRepeat(TNode node, bool preregister) { return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); } -RewriteResponse TheoryBVRewriter::RewriteZeroExtend(TNode node, bool preregister){ +RewriteResponse TheoryBVRewriter::RewriteZeroExtend(TNode node, bool prerewrite){ Node resultNode = LinearRewriteStrategy < RewriteRule<ZeroExtendEliminate > >::apply(node); @@ -503,7 +504,7 @@ RewriteResponse TheoryBVRewriter::RewriteZeroExtend(TNode node, bool preregister return RewriteResponse(REWRITE_AGAIN, resultNode); } -RewriteResponse TheoryBVRewriter::RewriteSignExtend(TNode node, bool preregister) { +RewriteResponse TheoryBVRewriter::RewriteSignExtend(TNode node, bool prerewrite) { Node resultNode = LinearRewriteStrategy < RewriteRule<EvalSignExtend> >::apply(node); @@ -513,7 +514,7 @@ RewriteResponse TheoryBVRewriter::RewriteSignExtend(TNode node, bool preregister } -RewriteResponse TheoryBVRewriter::RewriteRotateRight(TNode node, bool preregister) { +RewriteResponse TheoryBVRewriter::RewriteRotateRight(TNode node, bool prerewrite) { Node resultNode = LinearRewriteStrategy < RewriteRule<RotateRightEliminate > >::apply(node); @@ -521,7 +522,7 @@ RewriteResponse TheoryBVRewriter::RewriteRotateRight(TNode node, bool preregiste return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); } -RewriteResponse TheoryBVRewriter::RewriteRotateLeft(TNode node, bool preregister){ +RewriteResponse TheoryBVRewriter::RewriteRotateLeft(TNode node, bool prerewrite){ Node resultNode = LinearRewriteStrategy < RewriteRule<RotateLeftEliminate > >::apply(node); @@ -529,8 +530,8 @@ RewriteResponse TheoryBVRewriter::RewriteRotateLeft(TNode node, bool preregister return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); } -RewriteResponse TheoryBVRewriter::RewriteEqual(TNode node, bool preregister) { - if (preregister) { +RewriteResponse TheoryBVRewriter::RewriteEqual(TNode node, bool prerewrite) { + if (prerewrite) { Node resultNode = LinearRewriteStrategy < RewriteRule<FailEq>, RewriteRule<SimplifyEq>, |