From c4e08e8a41297efd759d086954d42825e20f54b0 Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Sun, 13 Nov 2011 12:52:09 +0000 Subject: [PATCH] Rewrite rule changes. Left shift by a constant now rewrites to multiplication (rather than extract/concat). Adds some new rewrite rules. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1415 e59a4935-1847-0410-ae03-e826735625c1 --- .../NodeFactory/SimplifyingNodeFactory.cpp | 12 +++++- src/simplifier/simplifier.cpp | 40 +++++++++++++------ 2 files changed, 37 insertions(+), 15 deletions(-) diff --git a/src/AST/NodeFactory/SimplifyingNodeFactory.cpp b/src/AST/NodeFactory/SimplifyingNodeFactory.cpp index 476a961..c288adc 100644 --- a/src/AST/NodeFactory/SimplifyingNodeFactory.cpp +++ b/src/AST/NodeFactory/SimplifyingNodeFactory.cpp @@ -930,6 +930,9 @@ ASTNode SimplifyingNodeFactory::CreateTerm(Kind kind, unsigned int width, result = bm.CreateZeroConst(width); else if (children[1].isConstant()) result = BEEV::Simplifier::convertKnownShiftAmount(kind, children, bm, &hashing); + else if(children[0].isConstant() && children[0] == bm.CreateOneConst(width) && width > 1) + result = NodeFactory::CreateTerm(BEEV::ITE,width, NodeFactory::CreateNode(BEEV::EQ, children[1], bm.CreateZeroConst(width)), children[0], bm.CreateZeroConst(width)); + } break; @@ -955,6 +958,8 @@ ASTNode SimplifyingNodeFactory::CreateTerm(Kind kind, unsigned int width, result = BEEV::Simplifier::convertArithmeticKnownShiftAmount(kind, children, bm, &hashing); else if (children[1].GetKind() == BEEV::BVUMINUS && children[0] == children[1][0]) result = NodeFactory::CreateTerm(BEEV::BVSRSHIFT,width, children[0], children[1][0]); + else if(children[0].isConstant() && !CONSTANTBV::BitVector_bit_test(children[0].GetBVConst(), width-1)) + result = NodeFactory::CreateTerm(BEEV::BVRIGHTSHIFT,width, children[0], children[1]); } break; @@ -1237,7 +1242,6 @@ ASTNode SimplifyingNodeFactory::CreateTerm(Kind kind, unsigned int width, result = BEEV::ArrayTransformer::TranslateSignedDivModRem(hashing.CreateTerm(kind, width, children),this,&bm); break; - case BEEV::BVDIV: if (children[1].isConstant() && children[1] == bm.CreateOneConst(width)) result = children[0]; @@ -1245,6 +1249,8 @@ ASTNode SimplifyingNodeFactory::CreateTerm(Kind kind, unsigned int width, result = bm.CreateOneConst(width); else if (bm.UserFlags.division_by_zero_returns_one_flag && children[0] == children[1]) result = bm.CreateOneConst(width); + else if (bm.UserFlags.division_by_zero_returns_one_flag && children[0].isConstant() && CONSTANTBV::BitVector_is_empty(children[0].GetBVConst())) + result = NodeFactory::CreateTerm(BEEV::ITE,width, NodeFactory::CreateNode(BEEV::EQ, children[1], bm.CreateZeroConst(width)), children[0], bm.CreateZeroConst(width)); break; @@ -1253,8 +1259,10 @@ ASTNode SimplifyingNodeFactory::CreateTerm(Kind kind, unsigned int width, result = children[0]; else if (children[0] == children[1] && bm.UserFlags.division_by_zero_returns_one_flag) result = bm.CreateOneConst(width); + else if (children[1].GetKind() == BEEV::BVUMINUS && children[0] == children[1][0] && bm.UserFlags.division_by_zero_returns_one_flag) + result = NodeFactory::CreateTerm(BEEV::SBVDIV,width, children[1], children[0]); else - result = BEEV::ArrayTransformer::TranslateSignedDivModRem(hashing.CreateTerm(kind, width, children),this,&bm); + result = BEEV::ArrayTransformer::TranslateSignedDivModRem(hashing.CreateTerm(kind, width, children),this,&bm); break; diff --git a/src/simplifier/simplifier.cpp b/src/simplifier/simplifier.cpp index 3e507b7..8d518a9 100644 --- a/src/simplifier/simplifier.cpp +++ b/src/simplifier/simplifier.cpp @@ -1754,7 +1754,7 @@ namespace BEEV } - // If the rhs of a left or right shift is known. Then replace it with a concat / extract. + // If the rhs of a left or right shift is known. ASTNode Simplifier::convertKnownShiftAmount(const Kind k, const ASTVec& children, STPMgr& bm, NodeFactory *nf) { const ASTNode a =children[0]; @@ -1787,17 +1787,16 @@ namespace BEEV { if (k == BVLEFTSHIFT) { - ASTNode zero = bm.CreateZeroConst(shift); - ASTNode hi = bm.CreateBVConst(32, width - shift -1); - ASTNode low = bm.CreateZeroConst(32); - ASTNode extract = - nf->CreateTerm(BVEXTRACT, width - shift, - a, hi, low); - BVTypeCheck(extract); + CBV cbv = CONSTANTBV::BitVector_Create(width,true); + CONSTANTBV::BitVector_Bit_On(cbv,shift); + ASTNode c = bm.CreateBVConst(cbv,width); + output = - nf->CreateTerm(BVCONCAT, width, - extract, zero); + nf->CreateTerm(BVMULT, width, + a, c); BVTypeCheck(output); + //cout << output; + //cout << a << b << endl; } else if (k == BVRIGHTSHIFT) { @@ -1819,8 +1818,6 @@ namespace BEEV return output; } - - //This function simplifies terms based on their kind ASTNode Simplifier::SimplifyTerm(const ASTNode& actualInputterm, @@ -2236,7 +2233,24 @@ namespace BEEV output = nf->CreateTerm(BVSUB, inputValueWidth, a0[1], a0[0]); break; } - case ITE: + case BVAND: + if (a0.Degree() == 2 && (a0[1].GetKind() == BVUMINUS) && a0[1][0] == a0[0]) + { + output = nf->CreateTerm(BVOR, inputValueWidth, a0[0], a0[1]); + } + break; + case BVOR: + if (a0.Degree() == 2 && (a0[1].GetKind() == BVUMINUS) && a0[1][0] == a0[0]) + { + output = nf->CreateTerm(BVAND, inputValueWidth, a0[0], a0[1]); + } + break; + case BVLEFTSHIFT: + if (a0[0].GetKind() == BVCONST) + output = nf->CreateTerm(BVLEFTSHIFT, inputValueWidth, nf->CreateTerm(BVUMINUS, inputValueWidth, a0[0]), + a0[1]); + break; + case ITE: { //BVUMINUS(ITE(c,t1,t2)) <==> ITE(c,BVUMINUS(t1),BVUMINUS(t2)) ASTNode c = a0[0]; -- 2.47.3