From: trevor_hansen Date: Wed, 27 Apr 2011 02:36:30 +0000 (+0000) Subject: Add extra simplifying rules. X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=352ce58bddb955145561f42b291ba9ed662d7e8f;p=francis%2Fstp.git Add extra simplifying rules. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1285 e59a4935-1847-0410-ae03-e826735625c1 --- diff --git a/src/AST/NodeFactory/SimplifyingNodeFactory.cpp b/src/AST/NodeFactory/SimplifyingNodeFactory.cpp index 0fad759..d7dd803 100644 --- a/src/AST/NodeFactory/SimplifyingNodeFactory.cpp +++ b/src/AST/NodeFactory/SimplifyingNodeFactory.cpp @@ -469,6 +469,25 @@ ASTNode SimplifyingNodeFactory::CreateSimpleEQ(const ASTVec& children) } + if (k1 == BEEV::BVCONST && k2 == BEEV::BVSX) + { + // Each of the bits in the extended part, and one into the un-extended part must be the same. + bool foundZero=false, foundOne=false; + const unsigned original_width = in2[0].GetValueWidth(); + const unsigned new_width = in2.GetValueWidth(); + for (int i = original_width-1; i < new_width;i++) + if (CONSTANTBV::BitVector_bit_test(in1.GetBVConst(),i)) + foundOne=true; + else + foundZero=true; + if (foundZero && foundOne) + return ASTFalse; + ASTNode lhs = NodeFactory::CreateTerm(BEEV::BVEXTRACT, original_width, in1, bm.CreateBVConst(32,original_width-1), bm.CreateZeroConst(32)); + ASTNode rhs = NodeFactory::CreateTerm(BEEV::BVEXTRACT, original_width, in2, bm.CreateBVConst(32,original_width-1), bm.CreateZeroConst(32)); + return NodeFactory::CreateNode(BEEV::EQ, lhs,rhs); + } + + //last resort is to CreateNode return hashing.CreateNode(BEEV::EQ, children); } @@ -791,8 +810,7 @@ ASTNode SimplifyingNodeFactory::CreateTerm(Kind kind, unsigned int width, { if (children[0].isConstant() && CONSTANTBV::BitVector_is_empty(children[0].GetBVConst())) result = bm.CreateZeroConst(width); - - if (children[0].isConstant() && CONSTANTBV::BitVector_is_full(children[0].GetBVConst())) + else if (children[0].isConstant() && CONSTANTBV::BitVector_is_full(children[0].GetBVConst())) result = bm.CreateMaxConst(width); else if (children[1].isConstant() && CONSTANTBV::BitVector_is_empty(children[1].GetBVConst())) result = children[0]; @@ -800,6 +818,8 @@ ASTNode SimplifyingNodeFactory::CreateTerm(Kind kind, unsigned int width, result = children[0]; else if (width == 1 && children[1].isConstant() && children[1] == bm.CreateOneConst(1)) result = children[0]; + else if (children[1].isConstant()) + result = BEEV::Simplifier::convertArithmeticKnownShiftAmount(kind, children, bm, &hashing); } @@ -831,6 +851,10 @@ ASTNode SimplifyingNodeFactory::CreateTerm(Kind kind, unsigned int width, if (children[0].isConstant() && CONSTANTBV::BitVector_is_empty(children[0].GetBVConst())) result = children[1]; + if (children[1].GetKind() == BEEV::BVNEG && children[0] == children[1][0]) + result = bm.CreateMaxConst(width); + if (children[0].GetKind() == BEEV::BVNEG && children[1] == children[0][0]) + result = bm.CreateMaxConst(width); } } break; diff --git a/src/simplifier/simplifier.cpp b/src/simplifier/simplifier.cpp index f0786cf..b29a770 100644 --- a/src/simplifier/simplifier.cpp +++ b/src/simplifier/simplifier.cpp @@ -1056,23 +1056,6 @@ namespace BEEV } } - if (k1 == BVCONST && k2 == BVSX) - { - // Each of the bits in the extended part, and one into the un-extended part must be the same. - bool foundZero=false, foundOne=false; - const unsigned original_width = in2[0].GetValueWidth(); - const unsigned new_width = in2.GetValueWidth(); - for (int i = original_width-1; i < new_width;i++) - if (CONSTANTBV::BitVector_bit_test(in1.GetBVConst(),i)) - foundOne=true; - else - foundZero=true; - if (foundZero && foundOne) - return ASTFalse; - ASTNode lhs = nf->CreateTerm(BVEXTRACT, original_width, in1, _bm->CreateBVConst(32,original_width-1), _bm->CreateZeroConst(32)); - ASTNode rhs = nf->CreateTerm(BVEXTRACT, original_width, in2, _bm->CreateBVConst(32,original_width-1), _bm->CreateZeroConst(32)); - return nf->CreateNode(EQ, lhs,rhs); - } //last resort is to CreateNode return nf->CreateNode(EQ, in1, in2); @@ -1746,6 +1729,28 @@ namespace BEEV return output; } + // If the shift is bigger than the bitwidth, replace by an extract. + ASTNode Simplifier::convertArithmeticKnownShiftAmount(const Kind k, const ASTVec& children, STPMgr& bm, NodeFactory *nf) + { + const ASTNode a =children[0]; + const ASTNode b =children[1]; + const int width = children[0].GetValueWidth(); + ASTNode output; + + assert(b.isConstant()); + assert(k == BVSRSHIFT); + const unsigned int shift = b.GetUnsignedConst(); + + if (CONSTANTBV::Set_Max(b.GetBVConst()) > 1 + log2(width) || (shift >= width)) + { + ASTNode top = bm.CreateBVConst(32,width-1); + return nf->CreateTerm(BVSX, width, nf->CreateTerm(BVEXTRACT,1, children[0], top,top ), bm.CreateBVConst(32,width)); + } + + return ASTNode(); + } + + // If the rhs of a left or right shift is known. Then replace it with a concat / extract. ASTNode Simplifier::convertKnownShiftAmount(const Kind k, const ASTVec& children, STPMgr& bm, NodeFactory *nf) { diff --git a/src/simplifier/simplifier.h b/src/simplifier/simplifier.h index 8a337ac..9002cff 100644 --- a/src/simplifier/simplifier.h +++ b/src/simplifier/simplifier.h @@ -61,7 +61,7 @@ namespace BEEV ASTNode pullUpBVSX(const ASTNode output); public: - + static ASTNode convertArithmeticKnownShiftAmount(const Kind k, const ASTVec& children, STPMgr& bm, NodeFactory *nf); static ASTNode convertKnownShiftAmount(const Kind k, const ASTVec& children, STPMgr& bm, NodeFactory *nf);