From b01fa25f8122ff646f719407ef1878d16d36024f Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Fri, 2 Jul 2010 12:06:37 +0000 Subject: [PATCH] Rename the bitblaster class fron BitBlasterNew to BitBlaster. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@906 e59a4935-1847-0410-ae03-e826735625c1 --- src/to-sat/AIG/ToSATAIG.h | 2 +- .../{BitBlastNew.cpp => BitBlaster.cpp} | 52 +++++++++---------- src/to-sat/{BitBlastNew.h => BitBlaster.h} | 8 +-- src/to-sat/ToSAT.cpp | 4 +- 4 files changed, 33 insertions(+), 33 deletions(-) rename src/to-sat/{BitBlastNew.cpp => BitBlaster.cpp} (93%) rename src/to-sat/{BitBlastNew.h => BitBlaster.h} (97%) diff --git a/src/to-sat/AIG/ToSATAIG.h b/src/to-sat/AIG/ToSATAIG.h index 2fec480..b36ce40 100644 --- a/src/to-sat/AIG/ToSATAIG.h +++ b/src/to-sat/AIG/ToSATAIG.h @@ -16,7 +16,7 @@ #include "../AST/AST.h" #include "../AST/RunTimes.h" #include "../STPManager/STPManager.h" -#include "BitBlastNew.h" +#include "BitBlaster.h" #include "BBNodeManagerAIG.h" namespace BEEV diff --git a/src/to-sat/BitBlastNew.cpp b/src/to-sat/BitBlaster.cpp similarity index 93% rename from src/to-sat/BitBlastNew.cpp rename to src/to-sat/BitBlaster.cpp index 851ef40..38234eb 100644 --- a/src/to-sat/BitBlastNew.cpp +++ b/src/to-sat/BitBlaster.cpp @@ -9,7 +9,7 @@ #include #include -#include "BitBlastNew.h" +#include "BitBlaster.h" #include "AIG/BBNodeManagerAIG.h" #include "BBNodeManagerASTNode.h" @@ -87,7 +87,7 @@ void check(BBNodeVec& x, const ASTNode& n, BBNodeManagerT* nf) template -const BBNodeVec BitBlasterNew::BBTerm(const ASTNode& term, BBNodeSet& support) { +const BBNodeVec BitBlaster::BBTerm(const ASTNode& term, BBNodeSet& support) { typename BBNodeVecMap::iterator it = BBTermMemo.find(term); if (it != BBTermMemo.end()) { // already there. Just return it. @@ -406,7 +406,7 @@ const BBNodeVec BitBlasterNew::BBTerm(const ASTNode& term // bit blast a formula (boolean term). Result is one bit wide, template -const BBNode BitBlasterNew::BBForm(const ASTNode& form, BBNodeSet& support) { +const BBNode BitBlaster::BBForm(const ASTNode& form, BBNodeSet& support) { typename map::iterator it = BBFormMemo.find(form); if (it != BBFormMemo.end()) { // already there. Just return it. @@ -504,7 +504,7 @@ const BBNode BitBlasterNew::BBForm(const ASTNode& form, B // Bit blast a sum of two equal length BVs. // Update sum vector destructively with new sum. template -void BitBlasterNew::BBPlus2(BBNodeVec& sum, const BBNodeVec& y, BBNode cin) { +void BitBlaster::BBPlus2(BBNodeVec& sum, const BBNodeVec& y, BBNode cin) { const int n = sum.size(); assert(y.size() == (unsigned)n); @@ -518,7 +518,7 @@ void BitBlasterNew::BBPlus2(BBNodeVec& sum, const BBNodeV // Stores result - x in result, destructively template -void BitBlasterNew::BBSub(BBNodeVec& result, const BBNodeVec& y, +void BitBlaster::BBSub(BBNodeVec& result, const BBNodeVec& y, BBNodeSet& support) { BBNodeVec compsubtrahend = BBNeg(y); BBPlus2(result, compsubtrahend, nf->getTrue()); @@ -526,7 +526,7 @@ void BitBlasterNew::BBSub(BBNodeVec& result, const BBNode // Add one bit template -BBNodeVec BitBlasterNew::BBAddOneBit(const BBNodeVec& x, BBNode cin) { +BBNodeVec BitBlaster::BBAddOneBit(const BBNodeVec& x, BBNode cin) { BBNodeVec result; result.reserve(x.size()); const typename BBNodeVec::const_iterator itend = x.end(); @@ -540,14 +540,14 @@ BBNodeVec BitBlasterNew::BBAddOneBit(const BBNodeVec& x, // Increment bit-blasted vector and return result. template -BBNodeVec BitBlasterNew::BBInc(const BBNodeVec& x) { +BBNodeVec BitBlaster::BBInc(const BBNodeVec& x) { return BBAddOneBit(x, nf->getTrue()); } // Return formula for majority function of three bits. // Pass arguments by reference to reduce refcounting. template -BBNode BitBlasterNew::Majority(const BBNode& a, const BBNode& b, +BBNode BitBlaster::Majority(const BBNode& a, const BBNode& b, const BBNode& c) { // Checking explicitly for constant a, b and c could // be more efficient, because they are repeated in the logic. @@ -574,7 +574,7 @@ BBNode BitBlasterNew::Majority(const BBNode& a, const BBN // Bitwise complement template -BBNodeVec BitBlasterNew::BBNeg(const BBNodeVec& x) { +BBNodeVec BitBlaster::BBNeg(const BBNodeVec& x) { BBNodeVec result; result.reserve(x.size()); // Negate each bit. @@ -587,14 +587,14 @@ BBNodeVec BitBlasterNew::BBNeg(const BBNodeVec& x) { // Compute unary minus template -BBNodeVec BitBlasterNew::BBUminus(const BBNodeVec& x) { +BBNodeVec BitBlaster::BBUminus(const BBNodeVec& x) { BBNodeVec xneg = BBNeg(x); return BBInc(xneg); } // AND each bit of vector y with single bit b and return the result. template -BBNodeVec BitBlasterNew::BBAndBit(const BBNodeVec& y, BBNode b) { +BBNodeVec BitBlaster::BBAndBit(const BBNodeVec& y, BBNode b) { if (nf->getTrue() == b) { return y; } @@ -690,7 +690,7 @@ void pushP(stack *products, const int start, const BBNodeVec& y, const B const bool debug_multiply = false; template -BBNodeVec BitBlasterNew::pairWiseAdd(stack* products, +BBNodeVec BitBlaster::pairWiseAdd(stack* products, const int bitWidth) { const BBNode& BBFalse = nf->getFalse(); @@ -779,7 +779,7 @@ BBNodeVec buildAdditionNetworkResult(stack* products, } template -void BitBlasterNew::mult_Booth(const BBNodeVec& x_i, const BBNodeVec& y_i, BBNodeSet& support, const ASTNode& xN, const ASTNode& yN, stack * products) +void BitBlaster::mult_Booth(const BBNodeVec& x_i, const BBNodeVec& y_i, BBNodeSet& support, const ASTNode& xN, const ASTNode& yN, stack * products) { const int bitWidth = x_i.size(); assert(x_i.size() == y_i.size()); @@ -849,7 +849,7 @@ void BitBlasterNew::mult_Booth(const BBNodeVec& x_i, cons // I've copied this in from my the "trevor" branch r482. // I've not measured if this is better than the current variant. template -void BitBlasterNew::mult_allPairs(const BBNodeVec& x, const BBNodeVec& y, BBNodeSet& support, stack * products) +void BitBlaster::mult_allPairs(const BBNodeVec& x, const BBNodeVec& y, BBNodeSet& support, stack * products) { // Make a table of partial products. const int bitWidth = x.size(); @@ -869,7 +869,7 @@ void BitBlasterNew::mult_allPairs(const BBNodeVec& x, con } template -BBNodeVec BitBlasterNew::mult_normal(const BBNodeVec& x, +BBNodeVec BitBlaster::mult_normal(const BBNodeVec& x, const BBNodeVec& y, BBNodeSet& support) { BBNodeVec ycopy(y); const typename BBNodeVec::const_iterator xend = x.end(); @@ -901,7 +901,7 @@ const bool multiplication_variant3 = true; // multiplication with booth recoding // Multiply two bitblasted numbers template -BBNodeVec BitBlasterNew::BBMult(const BBNodeVec& x, const BBNodeVec& y, +BBNodeVec BitBlaster::BBMult(const BBNodeVec& x, const BBNodeVec& y, BBNodeSet& support, const ASTNode& xN, const ASTNode& yN) { if (multiplication_variant1) { @@ -940,7 +940,7 @@ const bool division_variant_2 = false; // q and r are "out" parameters. rwidth puts a bound on the // recursion depth. template -void BitBlasterNew::BBDivMod(const BBNodeVec &y, const BBNodeVec &x, +void BitBlaster::BBDivMod(const BBNodeVec &y, const BBNodeVec &x, BBNodeVec &q, BBNodeVec &r, unsigned int rwidth, BBNodeSet& support) { const unsigned int width = y.size(); const BBNodeVec zero = BBfill(width, nf->getFalse()); @@ -1048,7 +1048,7 @@ void BitBlasterNew::BBDivMod(const BBNodeVec &y, const BB // build ITE's (ITE cond then[i] else[i]) for each i. template -BBNodeVec BitBlasterNew::BBITE(const BBNode& cond, const BBNodeVec& thn, +BBNodeVec BitBlaster::BBITE(const BBNode& cond, const BBNodeVec& thn, const BBNodeVec& els) { // Fast exits. if (cond == nf->getTrue()) { @@ -1107,7 +1107,7 @@ BBNode BBBVLE_variant(const BBNodeVec& left, const BBNodeVec& right, bool is_sig // is true, else it's unsigned. All other comparison operators can be reduced // to this by swapping args or complementing the result bit. template -BBNode BitBlasterNew::BBBVLE(const BBNodeVec& left, const BBNodeVec& right, +BBNode BitBlaster::BBBVLE(const BBNodeVec& left, const BBNodeVec& right, bool is_signed, bool is_bvlt) { typename BBNodeVec::const_reverse_iterator lit = left.rbegin(); const typename BBNodeVec::const_reverse_iterator litend = left.rend(); @@ -1155,7 +1155,7 @@ BBNode BitBlasterNew::BBBVLE(const BBNodeVec& left, const // Left shift within fixed field inserting zeros at LSB. // Writes result into first argument. template -void BitBlasterNew::BBLShift(BBNodeVec& x, unsigned int shift) { +void BitBlaster::BBLShift(BBNodeVec& x, unsigned int shift) { // left shift x (destructively) within width. // loop backwards so that copy to self works correctly. (DON'T use STL insert!) for (int i =((int)x.size())-1; i >=0; i--) @@ -1170,7 +1170,7 @@ void BitBlasterNew::BBLShift(BBNodeVec& x, unsigned int s // Right shift within fixed field inserting zeros at MSB. // Writes result into first argument. template -void BitBlasterNew::BBRShift(BBNodeVec& x, unsigned int shift) { +void BitBlaster::BBRShift(BBNodeVec& x, unsigned int shift) { // right shift x (destructively) within width. const typename BBNodeVec::iterator xend = x.end(); typename BBNodeVec::iterator xit = x.begin(); @@ -1184,7 +1184,7 @@ void BitBlasterNew::BBRShift(BBNodeVec& x, unsigned int s // Return bit-blasted form for BVLE, BVGE, BVGT, SBLE, etc. template -BBNode BitBlasterNew::BBcompare(const ASTNode& form, BBNodeSet& support) { +BBNode BitBlaster::BBcompare(const ASTNode& form, BBNodeSet& support) { const BBNodeVec& left = BBTerm(form[0], support); const BBNodeVec& right = BBTerm(form[1], support); @@ -1230,13 +1230,13 @@ BBNode BitBlasterNew::BBcompare(const ASTNode& form, BBNo // return a vector with n copies of fillval template -BBNodeVec BitBlasterNew::BBfill(unsigned int width, BBNode fillval) { +BBNodeVec BitBlaster::BBfill(unsigned int width, BBNode fillval) { BBNodeVec zvec(width, fillval); return zvec; } template -BBNode BitBlasterNew::BBEQ(const BBNodeVec& left, const BBNodeVec& right) { +BBNode BitBlaster::BBEQ(const BBNodeVec& left, const BBNodeVec& right) { BBNodeVec andvec; andvec.reserve(left.size()); typename BBNodeVec::const_iterator lit = left.begin(); @@ -1260,8 +1260,8 @@ BBNode BitBlasterNew::BBEQ(const BBNodeVec& left, const B } // This creates all the specialisations of the class that are ever needed. -template class BitBlasterNew; -template class BitBlasterNew; +template class BitBlaster; +template class BitBlaster; #undef BBNodeVec #undef BBNodeVecMap diff --git a/src/to-sat/BitBlastNew.h b/src/to-sat/BitBlaster.h similarity index 97% rename from src/to-sat/BitBlastNew.h rename to src/to-sat/BitBlaster.h index 2059218..93e9e70 100644 --- a/src/to-sat/BitBlastNew.h +++ b/src/to-sat/BitBlaster.h @@ -20,10 +20,10 @@ namespace BEEV { class ASTNode; typedef std::vector ASTVec; -template class BitBlasterNew; +template class BitBlaster; template -class BitBlasterNew { +class BitBlaster { private: // Memo table for bit blasted terms. If a node has already been // bitblasted, it is mapped to a vector of Boolean formulas for @@ -120,12 +120,12 @@ public: * Public Member Functions * ****************************************************************/ - BitBlasterNew(STPMgr * bm) + BitBlaster(STPMgr * bm) { nf = new BBNodeManagerT(bm); } - ~BitBlasterNew() { + ~BitBlaster() { BBTermMemo.clear(); BBFormMemo.clear(); delete nf; diff --git a/src/to-sat/ToSAT.cpp b/src/to-sat/ToSAT.cpp index 288069c..9f0c952 100644 --- a/src/to-sat/ToSAT.cpp +++ b/src/to-sat/ToSAT.cpp @@ -7,7 +7,7 @@ * LICENSE: Please view LICENSE file in the home dir of this Program ********************************************************************/ #include "ToSAT.h" -#include "BitBlastNew.h" +#include "BitBlaster.h" #include "../printer/printers.h" #include #include @@ -345,7 +345,7 @@ namespace BEEV ASTNode BBFormula; { - BitBlasterNew BB(bm); + BitBlaster BB(bm); set set; BBFormula = BB.BBForm(input,set); assert(set.size() == 0); // doesn't yet work. -- 2.47.3