summaryrefslogtreecommitdiff
path: root/src/theory/bv
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/bv')
-rw-r--r--src/theory/bv/theory_bv_rewriter.cpp137
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>,
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback