From 10cf10ae6e13347a4ba2e67d2212f0b9c29f1447 Mon Sep 17 00:00:00 2001 From: khooyp Date: Wed, 11 Jan 2012 22:53:39 +0000 Subject: [PATCH] Fix BitBlaster to not use the non-standard std::vector::data, for GCC-4.0 compatibility. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1502 e59a4935-1847-0410-ae03-e826735625c1 --- src/to-sat/BitBlaster.cpp | 62 +++++++++++++++++++-------------------- src/to-sat/BitBlaster.h | 16 +++++----- 2 files changed, 39 insertions(+), 39 deletions(-) diff --git a/src/to-sat/BitBlaster.cpp b/src/to-sat/BitBlaster.cpp index e7c2b94..fddf077 100644 --- a/src/to-sat/BitBlaster.cpp +++ b/src/to-sat/BitBlaster.cpp @@ -681,7 +681,7 @@ namespace BEEV products[i].push_back(results[j][i]); } - result = buildAdditionNetworkResult(products.data(), support, term); + result = buildAdditionNetworkResult(products, support, term); } break; } @@ -1201,7 +1201,7 @@ namespace BEEV // Multiply "multiplier" by y[start ... bitWidth]. template void - pushP(vector *products, const int start, const BBNodeVec& y, const BBNode& multiplier, BBNodeManagerT*nf) + pushP(vector >& products, const int start, const BBNodeVec& y, const BBNode& multiplier, BBNodeManagerT*nf) { const int bitWidth = y.size(); @@ -1232,7 +1232,7 @@ namespace BEEV template BBNodeVec - BitBlaster::buildAdditionNetworkResult(list* products, set& support, + BitBlaster::buildAdditionNetworkResult(vector >& products, set& support, const ASTNode& n) { const int bitWidth = n.GetValueWidth(); @@ -1353,7 +1353,7 @@ namespace BEEV // Make sure x and y are the parameters in the correct order. THIS ISNT COMMUTATIVE. template BBNodeVec - BitBlaster::multWithBounds(const ASTNode&n, list* products, + BitBlaster::multWithBounds(const ASTNode&n, vector >& products, BBNodeSet& toConjoinToTop) { const int bitWidth = n.GetValueWidth(); @@ -1414,7 +1414,7 @@ namespace BEEV template void BitBlaster::mult_Booth(const BBNodeVec& x_i, const BBNodeVec& y_i, BBNodeSet& support, - const ASTNode& xN, const ASTNode& yN, list * products, const ASTNode& n) + const ASTNode& xN, const ASTNode& yN, vector >& products, const ASTNode& n) { const int bitWidth = x_i.size(); assert(x_i.size() == y_i.size()); @@ -1464,20 +1464,20 @@ namespace BEEV { if (x[i] != BBTrue && x[i] != BBFalse) { - pushP(&t_products[0], i, y, x[i], nf); + pushP(t_products, i, y, x[i], nf); } // A bit can not be true or false, as well as one of these two. if (xt[i] == MINUS_ONE_MT) { - pushP(&t_products[0], i, notY, BBTrue, nf); + pushP(t_products, i, notY, BBTrue, nf); t_products[i].push_back(BBTrue); booth_recoded.insert(n); } else if (xt[i] == ONE_MT) { - pushP(&t_products[0], i, y, BBTrue, nf); + pushP(t_products, i, y, BBTrue, nf); } if (t_products[i].size() == 0) @@ -1495,7 +1495,7 @@ namespace BEEV template void BitBlaster::mult_allPairs(const BBNodeVec& x, const BBNodeVec& y, BBNodeSet& support, - list * products) + vector >& products) { // Make a table of partial products. const int bitWidth = x.size(); @@ -1747,19 +1747,19 @@ namespace BEEV else if (multiplication_variant == "2") { //cout << "v2"; - mult_allPairs(x, y, support, products.data()); - return buildAdditionNetworkResult(products.data(), support, n); + mult_allPairs(x, y, support, products); + return buildAdditionNetworkResult(products, support, n); } else if (multiplication_variant == "3") { - mult_Booth(_x, _y, support, n[0], n[1], products.data(), n); - return buildAdditionNetworkResult(products.data(), support, n); + mult_Booth(_x, _y, support, n[0], n[1], products, n); + return buildAdditionNetworkResult(products, support, n); } else if (multiplication_variant == "4") { //cerr << "v4"; - mult_Booth(_x, _y, support, n[0], n[1], products.data(), n); + mult_Booth(_x, _y, support, n[0], n[1], products, n); vector prior; for (int i = 0; i < bitWidth; i++) @@ -1769,39 +1769,39 @@ namespace BEEV prior = output; assert(products[i].size() == 1); } - return buildAdditionNetworkResult(products.data(), support, n); + return buildAdditionNetworkResult(products, support, n); } else if (multiplication_variant == "5") { if (!statsFound(n) || !multiplication_upper_bound) { - mult_Booth(_x, _y, support, n[0], n[1], products.data(), n); - return buildAdditionNetworkResult(products.data(), support, n); + mult_Booth(_x, _y, support, n[0], n[1], products, n); + return buildAdditionNetworkResult(products, support, n); } - mult_allPairs(x, y, support, products.data()); - return multWithBounds(n, products.data(), support); + mult_allPairs(x, y, support, products); + return multWithBounds(n, products, support); } else if (multiplication_variant == "6") { - mult_Booth(_x, _y, support,n[0],n[1],products.data(),n); - return v6(products.data(), support, n); + mult_Booth(_x, _y, support,n[0],n[1],products,n); + return v6(products, support, n); } else if (multiplication_variant == "7") { - mult_Booth(_x, _y, support, n[0], n[1], products.data(),n); - return v7(products.data(), support, n); + mult_Booth(_x, _y, support, n[0], n[1], products,n); + return v7(products, support, n); } else if (multiplication_variant == "8") { - mult_Booth(_x, _y, support, n[0], n[1], products.data(),n); - return v8(products.data(), support, n); + mult_Booth(_x, _y, support, n[0], n[1], products,n); + return v8(products, support, n); } else if (multiplication_variant == "9") { - mult_Booth(_x, _y, support, n[0], n[1], products.data(),n); - return v9(products.data(), support,n); + mult_Booth(_x, _y, support, n[0], n[1], products,n); + return v9(products, support,n); } else { @@ -1903,7 +1903,7 @@ namespace BEEV template BBNodeVec - BitBlaster::v6(list* products, set& support, const ASTNode&n) + BitBlaster::v6(vector >& products, set& support, const ASTNode&n) { const int bitWidth = n.GetValueWidth(); @@ -1926,7 +1926,7 @@ namespace BEEV // For instance, if there are 6 true in a column, then a carry will flow to column+1, and column+2. template BBNodeVec - BitBlaster::v9(list* products, set& support,const ASTNode&n) + BitBlaster::v9(vector >& products, set& support,const ASTNode&n) { const int bitWidth = n.GetValueWidth(); @@ -2000,7 +2000,7 @@ namespace BEEV template BBNodeVec - BitBlaster::v7(list* products, set& support, const ASTNode&n) + BitBlaster::v7(vector >& products, set& support, const ASTNode&n) { const int bitWidth = n.GetValueWidth(); @@ -2069,7 +2069,7 @@ namespace BEEV template BBNodeVec - BitBlaster::v8(list* products, set& support, const ASTNode&n) + BitBlaster::v8(vector >& products, set& support, const ASTNode&n) { const int bitWidth = n.GetValueWidth(); diff --git a/src/to-sat/BitBlaster.h b/src/to-sat/BitBlaster.h index 6b4c2f4..09b19c9 100644 --- a/src/to-sat/BitBlaster.h +++ b/src/to-sat/BitBlaster.h @@ -84,10 +84,10 @@ namespace BEEV vector BBMult(const vector& x, const vector& y, set& support, const ASTNode& n); void - mult_allPairs(const vector& x, const vector& y, set& support, list * products); + mult_allPairs(const vector& x, const vector& y, set& support, vector >& products); void mult_Booth(const vector& x_i, const vector& y_i, set& support, const BEEV::ASTNode& xN, - const BEEV::ASTNode& yN, list * products, const ASTNode&n); + const BEEV::ASTNode& yN, vector >& products, const ASTNode&n); vector mult_normal(const vector& x, const vector& y, set& support, const ASTNode&n); @@ -101,13 +101,13 @@ namespace BEEV sortingNetworkAdd(set& support, list& current, vector& currentSorted, vector& priorSorted); - vector v6(list* products, set& support, const ASTNode&n); - vector v7(list* products, set& support, const ASTNode&n); - vector v8(list* products, set& support, const ASTNode&n); - vector v9(list* products, set& support, const ASTNode&n); + vector v6(vector >& products, set& support, const ASTNode&n); + vector v7(vector >& products, set& support, const ASTNode&n); + vector v8(vector >& products, set& support, const ASTNode&n); + vector v9(vector >& products, set& support, const ASTNode&n); vector - multWithBounds(const ASTNode&n, list* products, set& toConjoinToTop); + multWithBounds(const ASTNode&n, vector >& products, set& toConjoinToTop); bool statsFound(const ASTNode& n); @@ -119,7 +119,7 @@ namespace BEEV buildAdditionNetworkResult(list& from, list& to, set& support, const bool top, const bool empty); vector - buildAdditionNetworkResult(list* products, set& support, const ASTNode& n); + buildAdditionNetworkResult(vector >& products, set& support, const ASTNode& n); vector BBAndBit(const vector& y, BBNode b); -- 2.47.3