From f6700c7fd27b5f822cdaa68d85fb385df6c65dfa Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Fri, 25 Jun 2010 08:22:50 +0000 Subject: [PATCH] Speedups. * Cache the max, one and zero values inside the Create__Const() functions. * Return a reference from the [] operator to reduce unncessary copies. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@886 e59a4935-1847-0410-ae03-e826735625c1 --- src/AST/ASTNode.h | 2 +- src/STPManager/STPManager.cpp | 56 ++++++++++++++++++++++++++++++----- src/STPManager/STPManager.h | 5 ++++ src/simplifier/simplifier.cpp | 23 +++++++++----- 4 files changed, 69 insertions(+), 17 deletions(-) diff --git a/src/AST/ASTNode.h b/src/AST/ASTNode.h index 013247d..75d1b22 100644 --- a/src/AST/ASTNode.h +++ b/src/AST/ASTNode.h @@ -301,7 +301,7 @@ namespace BEEV ; // Get indexth childNode. - const ASTNode operator[](size_t index) const + const ASTNode& operator[](size_t index) const { return GetChildren()[index]; } diff --git a/src/STPManager/STPManager.cpp b/src/STPManager/STPManager.cpp index 1947efb..207e9e9 100644 --- a/src/STPManager/STPManager.cpp +++ b/src/STPManager/STPManager.cpp @@ -285,16 +285,43 @@ namespace BEEV ASTNode STPMgr::CreateZeroConst(unsigned width) { - CBV z = CONSTANTBV::BitVector_Create(width, true); - return CreateBVConst(z, width); + assert(width > 0); + if (zeroes.size() == 0) + { + zeroes.push_back(ASTNode()); // null + for (int i =1; i < 65;i++) + zeroes.push_back(CreateZeroConst(i)); + } + + if (width < zeroes.size()) + return zeroes[width]; + else + { + CBV z = CONSTANTBV::BitVector_Create(width, true); + return CreateBVConst(z, width); + } } + ASTNode STPMgr::CreateOneConst(unsigned width) { - CBV o = CONSTANTBV::BitVector_Create(width, true); - CONSTANTBV::BitVector_increment(o); + assert(width > 0); + if (ones.size() == 0) + { + ones.push_back(ASTNode()); // null + for (int i =1; i < 65;i++) + ones.push_back(CreateOneConst(i)); + } + + if (width < ones.size()) + return ones[width]; + else + { + CBV o = CONSTANTBV::BitVector_Create(width, true); + CONSTANTBV::BitVector_increment(o); - return CreateBVConst(o, width); + return CreateBVConst(o, width); + } } ASTNode STPMgr::CreateTwoConst(unsigned width) @@ -308,10 +335,23 @@ namespace BEEV ASTNode STPMgr::CreateMaxConst(unsigned width) { - CBV max = CONSTANTBV::BitVector_Create(width, false); - CONSTANTBV::BitVector_Fill(max); + assert(width > 0); + if (max.size() == 0) + { + max.push_back(ASTNode()); // null + for (int i =1; i < 65;i++) + max.push_back(CreateMaxConst(i)); + } + + if (width < max.size()) + return max[width]; + else + { + CBV max = CONSTANTBV::BitVector_Create(width, false); + CONSTANTBV::BitVector_Fill(max); - return CreateBVConst(max, width); + return CreateBVConst(max, width); + } } //To ensure unique BVConst nodes, lookup the node in unique-table diff --git a/src/STPManager/STPManager.h b/src/STPManager/STPManager.h index 78b394b..c7dc7ec 100644 --- a/src/STPManager/STPManager.h +++ b/src/STPManager/STPManager.h @@ -127,6 +127,11 @@ namespace BEEV // Called by ASTNode constructors to uniqueify ASTBVConst ASTBVConst *LookupOrCreateBVConst(ASTBVConst& s); + // Cache of zero/one/max BVConsts of different widths. + ASTVec zeroes; + ASTVec ones; + ASTVec max; + public: /**************************************************************** diff --git a/src/simplifier/simplifier.cpp b/src/simplifier/simplifier.cpp index f406029..ca235c3 100644 --- a/src/simplifier/simplifier.cpp +++ b/src/simplifier/simplifier.cpp @@ -1640,9 +1640,11 @@ namespace BEEV if (simplify_upfront) { - if (k != BVCONST && k != SYMBOL) // const and symbols need to be created specially. + assert(k != BVCONST); + if (k != SYMBOL) // const and symbols need to be created specially. { ASTVec v; + v.reserve(actualInputterm.Degree()); for (unsigned i = 0; i < actualInputterm.Degree(); i++) if (inputterm[i].GetType() == BITVECTOR_TYPE) v.push_back(SimplifyTerm(inputterm[i], VarConstMap)); @@ -1651,10 +1653,14 @@ namespace BEEV else v.push_back(inputterm[i]); - // TODO: Should check if the children arrays are different and only - // create then. - output = nf->CreateTerm(k, inputValueWidth, v); - output.SetIndexWidth(actualInputterm.GetIndexWidth()); + assert(v.size() > 0); + if (v != actualInputterm.GetChildren()) // short-cut. + { + output = nf->CreateTerm(k, inputValueWidth, v); + output.SetIndexWidth(actualInputterm.GetIndexWidth()); + } + else + output = actualInputterm; if (inputterm != output) { UpdateSimplifyMap(inputterm, output, false, VarConstMap); @@ -2011,7 +2017,8 @@ namespace BEEV //indices for BVEXTRACT ASTNode i = inputterm[1]; ASTNode j = inputterm[2]; - ASTNode zero = _bm->CreateBVConst(32, 0); + ASTNode zero = _bm->CreateZeroConst(32); + //recall that the indices of BVEXTRACT are always 32 bits //long. therefore doing a GetBVUnsigned is ok. unsigned int i_val = i.GetUnsignedConst(); @@ -2160,7 +2167,7 @@ namespace BEEV // } break; } case ITE: { - ASTNode t0 = a0[0]; + const ASTNode& t0 = a0[0]; ASTNode t1 = SimplifyTerm(nf->CreateTerm(BVEXTRACT, a_len, a0[1], i, j), @@ -2526,7 +2533,7 @@ namespace BEEV { ASTNode zero = _bm->CreateZeroConst(shift); ASTNode hi = _bm->CreateBVConst(32, width - shift -1); - ASTNode low = _bm->CreateBVConst(32, 0); + ASTNode low = _bm->CreateZeroConst(32); ASTNode extract = nf->CreateTerm(BVEXTRACT, width - shift, a, hi, low); -- 2.47.3