From: trevor_hansen Date: Sat, 7 Jan 2012 12:24:39 +0000 (+0000) Subject: Improvement. Assert that multiplications that have no partial products true in a... X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=14cdaa497bb11ee9b3b5526821667657adfed012;p=francis%2Fstp.git Improvement. Assert that multiplications that have no partial products true in a sum are false at the top level. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1474 e59a4935-1847-0410-ae03-e826735625c1 --- diff --git a/src/to-sat/BitBlaster.cpp b/src/to-sat/BitBlaster.cpp index 786197e..b2a3be5 100644 --- a/src/to-sat/BitBlaster.cpp +++ b/src/to-sat/BitBlaster.cpp @@ -651,7 +651,7 @@ const BBNodeVec BitBlaster::BBTerm(const ASTNode& _term, products[i].push_back(results[j][i]); } - result = buildAdditionNetworkResult(products.data(),support,bitWidth); + result = buildAdditionNetworkResult(products.data(),support,bitWidth,term); } break; } @@ -1142,25 +1142,40 @@ const bool debug_multiply = false; * */ -template -BBNodeVec BitBlaster::buildAdditionNetworkResult(list* products, set& support, - const int bitWidth) -{ +template + BBNodeVec + BitBlaster::buildAdditionNetworkResult(list* products, set& support, + const int bitWidth, const ASTNode& n) + { - BBNodeVec results; - for (int i = 0; i < bitWidth; i++) - { - if (i+1 != bitWidth) - buildAdditionNetworkResult(&(products[i]), &(products[i+1]), support, bitWidth, i); - else - buildAdditionNetworkResult(&(products[i]), NULL, support, bitWidth, i); - assert(products[i].size() == 1); - results.push_back(products[i].back()); - } + // If we have details of the partial products which can be true, + int highestZero = -1; + simplifier::constantBitP::MultiplicationStats* ms = getMS(n, highestZero); + if (!multiplication_upper_bound) + ms = NULL; - assert(results.size() == ((unsigned)bitWidth)); - return results; -} + + BBNodeVec results; + for (int i = 0; i < bitWidth; i++) + { + int max_true; + + if (ms!=NULL && (ms->sumH[i] ==0)) + max_true = 0; + else + max_true = ((unsigned)~0) >> 1; + + if (i + 1 != bitWidth) + buildAdditionNetworkResult(&(products[i]), &(products[i + 1]), support, bitWidth, i,0, max_true); + else + buildAdditionNetworkResult(&(products[i]), NULL, support, bitWidth, i,0, max_true); + assert(products[i].size() == 1); + results.push_back(products[i].back()); + } + + assert(results.size() == ((unsigned)bitWidth)); + return results; + } // Use full adders to create an addition network that adds together each of the @@ -1187,6 +1202,19 @@ void BitBlaster::buildAdditionNetworkResult(list* const BBNode b = from.back(); from.pop_back(); + + // Nothing can be true. All must be false. + if (conjoin_to_top && maxTrue ==0) + { + if (BBFalse != a) + support.insert(nf->CreateNode(NOT, a)); + if (BBFalse != b) + support.insert(nf->CreateNode(NOT, b)); + if (BBFalse != c) + support.insert(nf->CreateNode(NOT, c)); + continue; + } + BBNode carry, sum; if (adder_variant) @@ -1202,7 +1230,6 @@ void BitBlaster::buildAdditionNetworkResult(list* } if (debug_multiply) { - cerr << "Column " << i << endl; cerr << "a" << a; cerr << "b" << b; cerr << "c" << c; @@ -1210,20 +1237,8 @@ void BitBlaster::buildAdditionNetworkResult(list* cerr << "Sum" << sum; } - // If we know the carry must be less than 2. - // Constraint each of the carries to zero. - if (conjoin_to_top && maxTrue ==0) - { - support.insert(nf->CreateNode(NOT, a)); - support.insert(nf->CreateNode(NOT, b)); - support.insert(nf->CreateNode(NOT, c)); - } - else - { - // 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_back(sum); - } + from.push_back(sum); + if (conjoin_to_top && maxTrue ==1) { support.insert(nf->CreateNode(NOT, carry)); @@ -1252,6 +1267,9 @@ const bool debug_bounds = false; if (NULL == cb->msm) return false; + if (booth_recoded.find(n) != booth_recoded.end()) // Sums are wrong for recoded. + return false; + simplifier::constantBitP::MultiplicationStatsMap::NodeToStats::const_iterator it; it = cb->msm->map.find(n); return (it != cb->msm->map.end()); @@ -1349,7 +1367,7 @@ BBNodeVec BitBlaster::multWithBounds(const ASTNode&n, lis } template -void BitBlaster::mult_Booth(const BBNodeVec& x_i, const BBNodeVec& y_i, BBNodeSet& support, const ASTNode& xN, const ASTNode& yN, list * products) +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 int bitWidth = x_i.size(); assert(x_i.size() == y_i.size()); @@ -1409,6 +1427,7 @@ void BitBlaster::mult_Booth(const BBNodeVec& x_i, const B { pushP(t_products,i,notY,BBTrue,nf); t_products[i].push_back(BBTrue); + booth_recoded.insert(n); } else if (xt[i] == ONE_MT) @@ -1459,30 +1478,92 @@ void BitBlaster::mult_allPairs(const BBNodeVec& x, const } } -template -BBNodeVec BitBlaster::mult_normal(const BBNodeVec& x, - const BBNodeVec& y, BBNodeSet& support) { - BBNodeVec ycopy(y); - const typename BBNodeVec::const_iterator xend = x.end(); - typename BBNodeVec::const_iterator xit = x.begin(); - // start prod with first partial product. - BBNodeVec prod = BBNodeVec(BBAndBit(y, *xit)); - // start loop at next bit. - for (xit++; xit < xend; xit++) { - // shift first - BBLShift(ycopy, 1); - - if (nf->getFalse() == *xit) { - // If this bit is zero, the partial product will - // be zero. No reason to add that in. - continue; - } - BBNodeVec pprod = BBAndBit(ycopy, *xit); - // accumulate in the product. - BBPlus2(prod, pprod, nf->getFalse()); - } - return prod; +template +MultiplicationStats* +BitBlaster::getMS(const ASTNode&n, int& highestZero) +{ + MultiplicationStats * ms; + highestZero = -1; + + if (statsFound(n)) + { + simplifier::constantBitP::MultiplicationStatsMap::NodeToStats::iterator it; + it = cb->msm->map.find(n); + if (it != cb->msm->map.end()) + { + ms = &(it->second); + + assert(ms->x.getWidth() == ms->y.getWidth()); + assert(ms->r.getWidth() == ms->y.getWidth()); + assert(ms->r.getWidth() == (int)ms->bitWidth); + } + + for (int i = 0; i < n.GetValueWidth(); i++) + if (ms->sumH[i] == 0) + highestZero = i; + + return ms; + } + + return NULL; +} + + + + +template +BBNodeVec +BitBlaster::mult_normal(const BBNodeVec& x, const BBNodeVec& y, BBNodeSet& support, + const ASTNode&n) +{ + const int bitWidth = n.GetValueWidth(); + + // If we have details of the partial products which can be true, + int highestZero = -1; + const simplifier::constantBitP::MultiplicationStats* ms = getMS(n, highestZero); + if (!multiplication_upper_bound) + ms = NULL; + + + BBNodeVec ycopy(y); + + // start prod with first partial product. + BBNodeVec prod = BBNodeVec(BBAndBit(y, *x.begin())); + // start loop at next bit. + + for (int i = 1; i < bitWidth; i++) + { + const BBNode& xit = x[i]; + + // shift first + BBLShift(ycopy, 1); + + if (nf->getFalse() == xit) + { + // If this bit is zero, the partial product will + // be zero. No reason to add that in. + continue; + } + + BBNodeVec pprod = BBAndBit(ycopy, xit); + + // Iterate through from the current location upwards, setting anything to zero that can be.. + if (ms != NULL && highestZero >= i) + { + for (int column = i; column <= highestZero; column++) + { + if (ms->sumH[column] == 0 && (nf->getFalse() != prod[column] )) + { + support.insert(nf->CreateNode(NOT, prod[column])); + prod[column] = BBFalse; + } + } + } + + BBPlus2(prod, pprod, nf->getFalse()); + } + return prod; } // assumes the prior column is sorted. @@ -1621,23 +1702,22 @@ BBNodeVec BitBlaster::BBMult(const BBNodeVec& _x, const B if (multiplication_variant == "1") { //cerr << "v1"; - return mult_normal(x, y, support); + return mult_normal(x, y, support,n); } else if (multiplication_variant == "2") { //cout << "v2"; mult_allPairs(x, y, support,products.data()); - return buildAdditionNetworkResult(products.data(),support, bitWidth); + return buildAdditionNetworkResult(products.data(),support, bitWidth,n); } else if (multiplication_variant == "3") { - //cout << "v3" << endl; - mult_Booth(_x, _y, support,n[0],n[1],products.data()); - return buildAdditionNetworkResult(products.data(),support,bitWidth); + mult_Booth(_x, _y, support,n[0],n[1],products.data(),n); + return buildAdditionNetworkResult(products.data(),support,bitWidth,n); } else if (multiplication_variant == "4") { //cerr << "v4"; - mult_Booth(_x, _y, support,n[0],n[1],products.data()); + mult_Booth(_x, _y, support,n[0],n[1],products.data(),n); vector prior; for (int i = 0; i < bitWidth; i++) @@ -1647,15 +1727,14 @@ BBNodeVec BitBlaster::BBMult(const BBNodeVec& _x, const B prior = output; assert(products[i].size() == 1); } - return buildAdditionNetworkResult(products.data(),support, bitWidth); + return buildAdditionNetworkResult(products.data(),support, bitWidth,n); } else if (multiplication_variant == "5") { - //cout << "v5"; if (!statsFound(n)) { - mult_Booth(_x, _y, support, n[0], n[1], products.data()); - return buildAdditionNetworkResult(products.data(), support, bitWidth); + mult_Booth(_x, _y, support, n[0], n[1], products.data(),n); + return buildAdditionNetworkResult(products.data(), support, bitWidth,n); } mult_allPairs(x, y, support, products.data()); diff --git a/src/to-sat/BitBlaster.h b/src/to-sat/BitBlaster.h index 26d9652..cbc429e 100644 --- a/src/to-sat/BitBlaster.h +++ b/src/to-sat/BitBlaster.h @@ -16,6 +16,7 @@ #include "../STPManager/STPManager.h" //#include "../STPManager/UserDefinedFlags.h" #include +#include "../simplifier/constantBitP/MultiplicationStats.h" namespace simplifier { @@ -29,6 +30,7 @@ namespace simplifier namespace BEEV { using std::list; + using simplifier::constantBitP::MultiplicationStats; class Simplifier; class ASTNode; @@ -75,8 +77,8 @@ class BitBlaster { 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); - 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); + 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); + vector mult_normal(const vector& x, const vector& y, set& support,const ASTNode&n); vector multWithBounds(const ASTNode&n, list* products, set& toConjoinToTop); bool @@ -89,10 +91,12 @@ class BitBlaster { const int minTrue = 0, const int maxTrue = ((unsigned)~0) >> 1 ); 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 buildAdditionNetworkResult(list* products, set& support, const int bitWidth, const ASTNode& n); vector BBAndBit(const vector& y, BBNode b); + MultiplicationStats* getMS(const ASTNode&n, int& highestZero); + void checkFixed(const vector& v, const ASTNode& n); @@ -171,10 +175,11 @@ class BitBlaster { const bool division_variant_3 ; const bool adder_variant; const bool bbbvle_variant; + const bool multiplication_upper_bound; - // This is a number 1->5 (currently). const string multiplication_variant; + ASTNodeSet booth_recoded; // Nodes that have been recoded. public: simplifier::constantBitP::ConstantBitPropagation* cb; @@ -193,8 +198,12 @@ public: division_variant_1("1" == _uf->get("division_variant_1","1")), division_variant_2("1" == _uf->get("division_variant_2","1")), division_variant_3("1" == _uf->get("division_variant_3","1")), + multiplication_variant(_uf->get("multiplication_variant","3")), + multiplication_upper_bound("1" == _uf->get("upper_multiplication_bound","0")), + adder_variant("1" == _uf->get("adder_variant","1")), + bbbvle_variant("1" == _uf->get("bbbvle_variant","1")) { nf = bnm;