From: trevor_hansen Date: Tue, 3 Jan 2012 13:42:56 +0000 (+0000) Subject: Refactor. Replace stacks with lists. X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=c2453dc56bc65b2e30f42029a77f2ff8972800cd;p=francis%2Fstp.git Refactor. Replace stacks with lists. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1464 e59a4935-1847-0410-ae03-e826735625c1 --- diff --git a/src/to-sat/BitBlaster.cpp b/src/to-sat/BitBlaster.cpp index 93d124e..786197e 100644 --- a/src/to-sat/BitBlaster.cpp +++ b/src/to-sat/BitBlaster.cpp @@ -644,11 +644,11 @@ const BBNodeVec BitBlaster::BBTerm(const ASTNode& _term, results.push_back(BBTerm(term[i], support)); const int bitWidth = term[0].GetValueWidth(); - std::vector > products(bitWidth); + std::vector > products(bitWidth); for (int i=0; i < bitWidth;i++) { for (int j=0; j < results.size();j++) - products[i].push(results[j][i]); + products[i].push_back(results[j][i]); } result = buildAdditionNetworkResult(products.data(),support,bitWidth); @@ -1143,7 +1143,7 @@ const bool debug_multiply = false; template -BBNodeVec BitBlaster::buildAdditionNetworkResult(stack* products, set& support, +BBNodeVec BitBlaster::buildAdditionNetworkResult(list* products, set& support, const int bitWidth) { @@ -1155,7 +1155,7 @@ BBNodeVec BitBlaster::buildAdditionNetworkResult(stack::buildAdditionNetworkResult(stack -void BitBlaster::buildAdditionNetworkResult(stack* from_, stack* to, set& support, +void BitBlaster::buildAdditionNetworkResult(list* from_, list* to, set& support, const int bitWidth, const int i, const int minTrue, const int maxTrue ) { - stack& from = *from_; + list& from = *from_; while (from.size() >= 2) { @@ -1178,14 +1178,14 @@ void BitBlaster::buildAdditionNetworkResult(stack if (from.size() == 2) c = nf->getFalse(); else { - c = from.top(); - from.pop(); + c = from.back(); + from.pop_back(); } - const BBNode a = from.top(); - from.pop(); - const BBNode b = from.top(); - from.pop(); + const BBNode a = from.back(); + from.pop_back(); + const BBNode b = from.back(); + from.pop_back(); BBNode carry, sum; @@ -1222,7 +1222,7 @@ void BitBlaster::buildAdditionNetworkResult(stack { // I experimented with making products[] a deque and accessing the front and back of the queue. // As a stack is works considerably better. - from.push(sum); + from.push_back(sum); } if (conjoin_to_top && maxTrue ==1) { @@ -1230,11 +1230,11 @@ void BitBlaster::buildAdditionNetworkResult(stack } else if (i + 1 != bitWidth && carry != BBFalse) { - to->push(carry); + to->push_back(carry); } } if (0==from.size()) - from.push(BBFalse); + from.push_back(BBFalse); assert(1==from.size()); } @@ -1259,7 +1259,7 @@ const bool debug_bounds = false; // Make sure x and y are the parameters in the correct order. THIS ISNT COMMUTATIVE. template -BBNodeVec BitBlaster::multWithBounds(const ASTNode&n, stack* products, BBNodeSet& toConjoinToTop) +BBNodeVec BitBlaster::multWithBounds(const ASTNode&n, list* products, BBNodeSet& toConjoinToTop) { simplifier::constantBitP::MultiplicationStats ms; @@ -1293,11 +1293,11 @@ BBNodeVec BitBlaster::multWithBounds(const ASTNode&n, sta { while (products[i].size() > 0) { - BBNode c = products[i].top(); // DONT take a reference of the top(). - products[i].pop(); + BBNode c = products[i].back(); // DONT take a reference of the back(). + products[i].pop_back(); toConjoinToTop.insert(nf->CreateNode(NOT, c)); } - products[i].push(nf->getFalse()); + products[i].push_back(nf->getFalse()); } } @@ -1338,7 +1338,7 @@ BBNodeVec BitBlaster::multWithBounds(const ASTNode&n, sta } assert(products[i].size() == 1); - result.push_back(products[i].top()); + result.push_back(products[i].back()); } if (debug_bitblaster) @@ -1349,7 +1349,7 @@ BBNodeVec BitBlaster::multWithBounds(const ASTNode&n, sta } template -void BitBlaster::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, list * products) { const int bitWidth = x_i.size(); assert(x_i.size() == y_i.size()); @@ -1421,7 +1421,7 @@ void BitBlaster::mult_Booth(const BBNodeVec& x_i, const B sort(t_products[i].begin(), t_products[i].end()); for (int j=0; j < t_products[i].size();j++) - products[i].push(t_products[i][j]); + products[i].push_back(t_products[i][j]); } } @@ -1430,7 +1430,7 @@ void BitBlaster::mult_Booth(const BBNodeVec& x_i, const B // 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 BitBlaster::mult_allPairs(const BBNodeVec& x, const BBNodeVec& y, BBNodeSet& support, stack * products) +void BitBlaster::mult_allPairs(const BBNodeVec& x, const BBNodeVec& y, BBNodeSet& support, list * products) { // Make a table of partial products. const int bitWidth = x.size(); @@ -1450,11 +1450,11 @@ void BitBlaster::mult_allPairs(const BBNodeVec& x, const BBNode n = nf->CreateNode(AND, x[i - j], y[j]); if (n != nf->getFalse()) - products[i].push(n); + products[i].push_back(n); } if (0 == products[i].size()) - products[i].push(nf->getFalse()); + products[i].push_back(nf->getFalse()); } } @@ -1489,14 +1489,14 @@ BBNodeVec BitBlaster::mult_normal(const BBNodeVec& x, template void BitBlaster::mult_SortingNetwork( - BBNodeSet& support, stack& current, vector& currentSorted, vector& priorSorted, + BBNodeSet& support, list& current, vector& currentSorted, vector& priorSorted, const int minTrue, const int maxTrue ) { // Add the carry from the prior column. i.e. each second sorted formula. for (int k = 1; k < priorSorted.size(); k += 2) { - current.push(priorSorted[k]); + current.push_back(priorSorted[k]); } const int height = current.size(); @@ -1512,8 +1512,8 @@ BBNodeVec BitBlaster::mult_normal(const BBNodeVec& x, for (int l = 0; l < height; l++) { vector oldSorted(currentSorted); - BBNode c = current.top(); - current.pop(); + BBNode c = current.back(); + current.pop_back(); currentSorted[0] = nf->CreateNode(OR, oldSorted[0], c); for (int j = 1; j <= l; j++) @@ -1556,7 +1556,7 @@ BBNodeVec BitBlaster::mult_normal(const BBNodeVec& x, if (height % 2 == 1) resultNode = nf->CreateNode(OR, resultNode, currentSorted.at(height - 1)); - current.push(resultNode); + current.push_back(resultNode); } @@ -1604,6 +1604,9 @@ BBNodeVec BitBlaster::BBMult(const BBNodeVec& _x, const B BBNodeSet& support, const ASTNode& n) { + if (uf->isSet("print_on_mult","0")) + cerr << "--mult--"; + BBNodeVec x = _x; BBNodeVec y = _y; @@ -1614,7 +1617,7 @@ BBNodeVec BitBlaster::BBMult(const BBNodeVec& _x, const B } const int bitWidth = x.size(); - std::vector > products(bitWidth); + std::vector > products(bitWidth); if (multiplication_variant == "1") { //cerr << "v1"; diff --git a/src/to-sat/BitBlaster.h b/src/to-sat/BitBlaster.h index aab61c0..26d9652 100644 --- a/src/to-sat/BitBlaster.h +++ b/src/to-sat/BitBlaster.h @@ -15,6 +15,7 @@ #include #include "../STPManager/STPManager.h" //#include "../STPManager/UserDefinedFlags.h" +#include namespace simplifier { @@ -27,6 +28,8 @@ namespace simplifier namespace BEEV { + using std::list; + class Simplifier; class ASTNode; typedef std::vector ASTVec; @@ -71,22 +74,22 @@ class BitBlaster { // Multiply. vector BBMult(const vector& x, const vector& y, set& support, const ASTNode& n); - void mult_allPairs(const vector& x, const vector& y, set& support, stack * products); - void mult_Booth(const vector& x_i, const vector& y_i, set& support, const BEEV::ASTNode& xN, const BEEV::ASTNode& yN, stack * products); + void mult_allPairs(const vector& x, const vector& y, set& support, list * products); + void mult_Booth(const vector& x_i, const vector& y_i, set& support, const BEEV::ASTNode& xN, const BEEV::ASTNode& yN, list * products); vector mult_normal(const vector& x, const vector& y, set& support); - vector multWithBounds(const ASTNode&n, stack* products, set& toConjoinToTop); + vector multWithBounds(const ASTNode&n, list* products, set& toConjoinToTop); bool statsFound(const ASTNode& n); void mult_SortingNetwork( - set& support, stack& currentColumn, vector& currentSorted, vector& priorSorted, + set& support, list& currentColumn, vector& currentSorted, vector& priorSorted, const int minTrue = 0, const int maxTrue = ((unsigned)~0) >> 1 ); - void buildAdditionNetworkResult(stack* from, stack* to, set& support, const int bitWidth, const int index, const int minTrue = 0, const int maxTrue = ((unsigned)~0) >> 1 ); - vector buildAdditionNetworkResult(stack* products, set& support, int bitWidth); + void buildAdditionNetworkResult(list* from, list* to, set& support, const int bitWidth, const int index, const int minTrue = 0, const int maxTrue = ((unsigned)~0) >> 1 ); + vector buildAdditionNetworkResult(list* products, set& support, int bitWidth); vector BBAndBit(const vector& y, BBNode b);