From f64efc8228a44e16d38e8d064e0c62af4e8d6482 Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Fri, 25 Mar 2011 13:34:55 +0000 Subject: [PATCH] Improvement. Convert left/right (NOT aritmetic), shifts by a known amount to a concatenation and extract in the simplifying node factory. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1238 e59a4935-1847-0410-ae03-e826735625c1 --- .../NodeFactory/SimplifyingNodeFactory.cpp | 35 ++---- src/simplifier/simplifier.cpp | 117 ++++++++++-------- src/simplifier/simplifier.h | 3 + 3 files changed, 81 insertions(+), 74 deletions(-) diff --git a/src/AST/NodeFactory/SimplifyingNodeFactory.cpp b/src/AST/NodeFactory/SimplifyingNodeFactory.cpp index b4d36da..3b56b9e 100644 --- a/src/AST/NodeFactory/SimplifyingNodeFactory.cpp +++ b/src/AST/NodeFactory/SimplifyingNodeFactory.cpp @@ -638,33 +638,22 @@ ASTNode SimplifyingNodeFactory::CreateTerm(Kind kind, unsigned int width, case BEEV::BVLEFTSHIFT: { - if (children[0].isConstant() && CONSTANTBV::BitVector_is_empty(children[0].GetBVConst())) - result = bm.CreateZeroConst(width); - else if (children[1].isConstant() && CONSTANTBV::Set_Max(children[1].GetBVConst()) > 1 + log2(width)) - result = bm.CreateZeroConst(width); - else if (children[1].isConstant() && children[1].GetUnsignedConst() >=width) - result = bm.CreateZeroConst(width); - else if (children[1].isConstant() && CONSTANTBV::BitVector_is_empty(children[1].GetBVConst())) - result = children[0]; - - + if (children[0].isConstant() && CONSTANTBV::BitVector_is_empty(children[0].GetBVConst())) + result = bm.CreateZeroConst(width); + else if (children[1].isConstant()) + result = BEEV::Simplifier::convertKnownShiftAmount(kind, children, bm, &hashing); } break; case BEEV::BVRIGHTSHIFT: - { - if (children[0] == children[1]) - result= bm.CreateZeroConst(width); - if (children[0].isConstant() && CONSTANTBV::BitVector_is_empty(children[0].GetBVConst())) - result = bm.CreateZeroConst(width); - else if (children[1].isConstant() && CONSTANTBV::Set_Max(children[1].GetBVConst()) > 1 + log2(width)) - result = bm.CreateZeroConst(width); - else if (children[1].isConstant() && children[1].GetUnsignedConst() >=width) - result = bm.CreateZeroConst(width); - else if (children[1].isConstant() && CONSTANTBV::BitVector_is_empty(children[1].GetBVConst())) - result = children[0]; - - } + { + if (children[0] == children[1]) + result= bm.CreateZeroConst(width); + if (children[0].isConstant() && CONSTANTBV::BitVector_is_empty(children[0].GetBVConst())) + result = bm.CreateZeroConst(width); + else if (children[1].isConstant()) + result = BEEV::Simplifier::convertKnownShiftAmount(kind, children, bm, &hashing); + } break; case BEEV::BVSRSHIFT: diff --git a/src/simplifier/simplifier.cpp b/src/simplifier/simplifier.cpp index 66fbded..ecc4c22 100644 --- a/src/simplifier/simplifier.cpp +++ b/src/simplifier/simplifier.cpp @@ -1709,6 +1709,71 @@ namespace BEEV return output; } + // 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) + { + const ASTNode a =children[0]; + const ASTNode b =children[1]; + const int width = children[0].GetValueWidth(); + ASTNode output; + + assert(b.isConstant()); + assert(k == BVLEFTSHIFT || BVRIGHTSHIFT ==k); + + if (CONSTANTBV::Set_Max(b.GetBVConst()) > 1 + log2(width)) + { + // Intended to remove shifts by very large amounts + // that don't fit into the unsigned. at thhe start + // of the "else" branch. + output = bm.CreateZeroConst(width); + } + else + { + const unsigned int shift = b.GetUnsignedConst(); + if (shift >= width) + { + output = bm.CreateZeroConst(width); + } + else if (shift == 0) + { + output = a; // unchanged. + } + else + { + 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); + output = + nf->CreateTerm(BVCONCAT, width, + extract, zero); + BVTypeCheck(output); + } + else if (k == BVRIGHTSHIFT) + { + ASTNode zero = bm.CreateZeroConst(shift); + ASTNode hi = bm.CreateBVConst(32, width -1); + ASTNode low = bm.CreateBVConst(32, shift); + ASTNode extract = + nf->CreateTerm(BVEXTRACT, width - shift, + a, hi, low); + BVTypeCheck(extract); + output = + nf->CreateTerm(BVCONCAT, width, zero, extract); + BVTypeCheck(output); + } + else + FatalError("herasdf"); + } + } + return output; +} + //This function simplifies terms based on their kind @@ -2742,57 +2807,7 @@ namespace BEEV const unsigned int width = a.GetValueWidth(); if (BVCONST == b.GetKind()) // known shift amount. { - if (CONSTANTBV::Set_Max(b.GetBVConst()) > 1 + log2(width)) - { - // Intended to remove shifts by very large amounts - // that don't fit into the unsigned. at thhe start - // of the "else" branch. - output = _bm->CreateZeroConst(width); - } - else - { - const unsigned int shift = b.GetUnsignedConst(); - if (shift >= width) - { - output = _bm->CreateZeroConst(width); - } - else if (shift == 0) - { - output = a; // unchanged. - } - else - { - 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); - output = - nf->CreateTerm(BVCONCAT, width, - extract, zero); - BVTypeCheck(output); - } - else if (k == BVRIGHTSHIFT) - { - ASTNode zero = _bm->CreateZeroConst(shift); - ASTNode hi = _bm->CreateBVConst(32, width -1); - ASTNode low = _bm->CreateBVConst(32, shift); - ASTNode extract = - nf->CreateTerm(BVEXTRACT, width - shift, - a, hi, low); - BVTypeCheck(extract); - output = - nf->CreateTerm(BVCONCAT, width, zero, extract); - BVTypeCheck(output); - } - else - FatalError("herasdf"); - } - } + output = convertKnownShiftAmount(k, inputterm.GetChildren(), *_bm, nf); } else if (a == _bm->CreateZeroConst(width)) { diff --git a/src/simplifier/simplifier.h b/src/simplifier/simplifier.h index 3aa9eb4..9c0343f 100644 --- a/src/simplifier/simplifier.h +++ b/src/simplifier/simplifier.h @@ -62,6 +62,9 @@ namespace BEEV public: + static ASTNode convertKnownShiftAmount(const Kind k, const ASTVec& children, STPMgr& bm, NodeFactory *nf); + + /**************************************************************** * Public Member Functions * ****************************************************************/ -- 2.47.3