From: trevor_hansen Date: Sat, 14 Aug 2010 01:56:11 +0000 (+0000) Subject: Should cause not runtime effects. X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=9ca8b1e335185cf9e4948f5c8713a2791aab0dc0;p=francis%2Fstp.git Should cause not runtime effects. Add a new multiplication variant that uses bounds discovered during constant bit propagation to more efficiently encode multiplications. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@982 e59a4935-1847-0410-ae03-e826735625c1 --- diff --git a/src/to-sat/BitBlaster.cpp b/src/to-sat/BitBlaster.cpp index b1b00e8..421140f 100644 --- a/src/to-sat/BitBlaster.cpp +++ b/src/to-sat/BitBlaster.cpp @@ -200,8 +200,9 @@ template 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. - return it->second; + // Constant bit propagation may have updated something. + //updateTerm(term,it->second,support); + return it->second; } BBNodeVec result; @@ -398,19 +399,10 @@ const BBNodeVec BitBlaster::BBTerm(const ASTNode& term, B assert(BVTypeCheck(term)); assert(term.Degree() == 2); - const ASTNode& t0 = term[0]; - const ASTNode& t1 = term[1]; - - const BBNodeVec& mpcd1 = BBTerm(t0, support); - const BBNodeVec& mpcd2 = BBTerm(t1, support); + const BBNodeVec& mpcd1 = BBTerm(term[0], support); + const BBNodeVec& mpcd2 = BBTerm(term[1], support); assert(mpcd1.size() == mpcd2.size()); - //Revereses the order of the nodes w/out the need for temporaries - if ((BVCONST != t0.GetKind()) && (BVCONST == t1.GetKind())) { - - result = BBMult(mpcd2, mpcd1, support,t1,t0); - } else { - result = BBMult(mpcd1, mpcd2, support,t0,t1); - } + result = BBMult(mpcd1, mpcd2, support,term); break; } case BVDIV: @@ -856,74 +848,177 @@ const bool debug_multiply = false; * */ bool const adder_variant1 = true; +template +BBNodeVec BitBlaster::buildAdditionNetworkResult(stack* products, set& support, + const int bitWidth) +{ + BBNodeVec results; + for (int i = 0; i < bitWidth; i++) + { + buildAdditionNetworkResult(products, support, bitWidth, i); + assert(products[i].size() == 1); + results.push_back(products[i].top()); + } + + assert(results.size() == ((unsigned)bitWidth)); + return results; +} + + // Use full adders to create an addition network that adds together each of the // partial products. template -BBNodeVec BitBlaster::buildAdditionNetworkResult(stack* products, - const int bitWidth) { - int adderCount = 0; +void BitBlaster::buildAdditionNetworkResult(stack* products, set& support, + const int bitWidth, const int i, const int minTrue = 0, const int maxTrue = ((unsigned)~0) >> 1 ) +{ - // I experimented with sorting the partial products to put the known values together. - // But it didn't help. + while (products[i].size() >= 2) { + BBNode c; - BBNodeVec result; + if (products[i].size() == 2) + c = nf->getFalse(); + else { + c = products[i].top(); + products[i].pop(); + } - for (int i = 0; i < bitWidth; i++) { - while (products[i].size() >= 2) { - BBNode c; + const BBNode a = products[i].top(); + products[i].pop(); + const BBNode b = products[i].top(); + products[i].pop(); - if (products[i].size() == 2) - c = nf->getFalse(); - else { - c = products[i].top(); - products[i].pop(); - } + BBNode carry, sum; - const BBNode a = products[i].top(); - products[i].pop(); - const BBNode b = products[i].top(); - products[i].pop(); - - BBNode carry, sum; - - if (adder_variant1) - { - carry = Majority(a, b, c); - sum = nf->CreateNode(XOR, a, b, c); - } - else - { - carry = nf->CreateNode(OR, nf->CreateNode(AND, a, b), nf->CreateNode(AND, b, c), nf->CreateNode(AND, - a, c)); - sum = nf->CreateNode(XOR, nf->CreateNode(XOR, c, b), a); - } - - adderCount++; - - if (debug_multiply) { - cerr << "Column " << i << endl; - cerr << "a" << a; - cerr << "b" << b; - cerr << "c" << c; - cerr << "Carry" << carry; - cerr << "Sum" << sum; - } + if (adder_variant1) + { + carry = Majority(a, b, c); + sum = nf->CreateNode(XOR, a, b, c); + } + else + { + carry = nf->CreateNode(OR, nf->CreateNode(AND, a, b), nf->CreateNode(AND, b, c), nf->CreateNode(AND, + a, c)); + sum = nf->CreateNode(XOR, nf->CreateNode(XOR, c, b), a); + } - // I experimented with making products[] a deque and accessing the front and back of the queue. - // As a stack is works considerably better. - products[i].push(sum); - if (i + 1 != bitWidth) - products[i + 1].push(carry); - } + if (debug_multiply) { + cerr << "Column " << i << endl; + cerr << "a" << a; + cerr << "b" << b; + cerr << "c" << c; + cerr << "Carry" << carry; + cerr << "Sum" << sum; + } + + // I experimented with making products[] a deque and accessing the front and back of the queue. + // As a stack is works considerably better. + products[i].push(sum); + + // If we know the carry must be less than 2. + // Constraint each of the carries to zero. + if (maxTrue < 2) + { + support.insert(nf->CreateNode(NOT, carry)); + } + else if (i + 1 != bitWidth) + products[i + 1].push(carry); + } - assert(1==products[i].size()); - result.push_back(products[i].top()); - } + assert(1==products[i].size()); +} - if (debug_multiply) - cerr << "adder count" << adderCount << endl; - assert(result.size() == ((unsigned)bitWidth)); - return result; + +const bool debug_bounds = true; + +// 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) +{ + bool statsFound = false; + simplifier::constantBitP::MultiplicationStats ms; + + const int bitWidth = n.GetValueWidth(); + + assert (NULL != cb); + assert (NULL != cb->msm); + { + simplifier::constantBitP::MultiplicationStatsMap::NodeToStats::const_iterator + it; + it = cb->msm->map.find(n); + if (it != cb->msm->map.end()) + { + //it->second->print(); + ms = it->second; + statsFound = true; + + assert(ms.x.getWidth() == ms.y.getWidth()); + assert(ms.r.getWidth() == ms.y.getWidth()); + assert(ms.r.getWidth() == (int)ms.bitWidth); + assert(ms.r.getWidth() == bitWidth); + } + } + + if (!statsFound) + return buildAdditionNetworkResult(products, toConjoinToTop, bitWidth); + + // If all of the partial products in the column must be zero, then replace + for (int i = 0; i < bitWidth; i++) + { + if (ms.columnH[i] == 0) + { + while (products[i].size() > 0) + { + BBNode c = products[i].top(); // DONT take a reference of the top(). + products[i].pop(); + toConjoinToTop.insert(nf->CreateNode(NOT, c)); + } + products[i].push(nf->getFalse()); + } + } + + BBNodeVec result; + + if (debug_bounds) + { + ms.print(); + } + + for (int i = 0; i < bitWidth; i++) + { + if (debug_bounds) + cerr << " " << products[i].size(); + if (statsFound) + { + cerr << "["<< ms.columnL[i] << ":"<< ms.columnH[i] << "]["<< ms.sumL[i] << ":" << ms.sumH[i] << "]"; + } + + if ((products[i].size() > ms.sumH[i]) && ms.sumH[i] < 6) + { + if (debug_bounds) + cerr << "S"; + // sorting network. + + int width = std::min(ms.sumH[i]+1, (signed)products[i].size()); + mult_SortingNetwork(toConjoinToTop, bitWidth, width, products, i, ms.sumL[i], ms.sumH[i]); + + } + else // addition network. + { + if (debug_bounds) + cerr << "A"; + + buildAdditionNetworkResult(products,toConjoinToTop,bitWidth,i, ms.sumL[i], ms.sumH[i]); + } + + assert(products[i].size() == 1); + result.push_back(products[i].top()); + } + + if (debug_bitblaster) + cerr << endl << endl; + + assert(result.size() == ((unsigned)bitWidth)); + return result; } template @@ -999,22 +1094,32 @@ void BitBlaster::mult_Booth(const BBNodeVec& x_i, const B template 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(); - assert(x.size() == y.size()); + // Make a table of partial products. + const int bitWidth = x.size(); + assert(x.size() == y.size()); + assert(bitWidth > 0); + for (int i = 0; i < bitWidth; i++) + { + assert(!x[i].IsNull()); + assert(!y[i].IsNull()); + } - for (int i =0 ; i < bitWidth; i++) - { - for (int j=0; j<= i; j++) - { - BBNode n = nf->CreateNode(AND, y[j], x[i-j]); - products[i].push(n); - } - } - // I experimented with sorting the partial products to put the known values together. - // But it didn't help. - } + for (int i = 0; i < bitWidth; i++) + { + for (int j = 0; j <= i; j++) + { + BBNode n = nf->CreateNode(AND, x[i - j], y[j]); + + if (n != nf->getFalse()) + products[i].push(n); + } + + if (0 == products[i].size()) + products[i].push(nf->getFalse()); + + } + } template BBNodeVec BitBlaster::mult_normal(const BBNodeVec& x, @@ -1042,35 +1147,47 @@ BBNodeVec BitBlaster::mult_normal(const BBNodeVec& x, return prod; } - template void - BitBlaster::mult_SortingNetwork(const BBNodeVec& x_i, const BBNodeVec& y_i, - BBNodeSet& support, const ASTNode& xN, const ASTNode& yN, stack * products, int i) + BitBlaster::mult_SortingNetwork( + BBNodeSet& support, const int bitWidth, const int width, stack * products, int i + , const int minTrue = 0, const int maxTrue = ((unsigned)~0) >> 1 ) { - const int width = products[i].size(); - const int bitWidth = xN.GetValueWidth(); - + assert(i sorted(width, nf->getFalse()); - for (int l = 0; l < width; l++) - { - vector oldSorted(sorted); - BBNode c = products[i].top(); - products[i].pop(); - sorted[0] = nf->CreateNode(OR, oldSorted[0], c); - - for (int j = 1; j <= std::min(l, width - 1); j++) - { - sorted[j] = nf->CreateNode(OR, nf->CreateNode(AND, oldSorted[j - 1], c), oldSorted[j]); - } - } + for (int l = 0; l < height; l++) + { + vector oldSorted(sorted); + BBNode c = products[i].top(); + products[i].pop(); + sorted[0] = nf->CreateNode(OR, oldSorted[0], c); + + for (int j = 1; j <= std::min(l,width-1); j++) + { + sorted[j] = nf->CreateNode(OR, nf->CreateNode(AND, + oldSorted[j - 1], c), oldSorted[j]); + } + } for (int k = 0; k < width; k++) assert(!sorted[k].IsNull()); assert(products[i].size() == 0); + for (int j = 0; j < minTrue; j++) + { + support.insert(sorted[j]); + sorted[j] = BBTrue; + } + + for (int j = width-1; j >= maxTrue; j--) + { + support.insert(nf->CreateNode(NOT,sorted[j])); + sorted[j] = BBFalse; + } + // Add to next up columns. if (i + 1 != bitWidth) { @@ -1097,52 +1214,108 @@ BBNodeVec BitBlaster::mult_normal(const BBNodeVec& x, } + // If a bit has a fixed value, then it should equal BBTrue or BBFalse in the input vectors. + template + void + BitBlaster::checkFixed(const BBNodeVec& v, const ASTNode& n) + { + if (cb == NULL) + return; + + if (cb->fixedMap->map->find(n) != cb->fixedMap->map->end()) + { + FixedBits* b = cb->fixedMap->map->find(n)->second; + for (int i = 0; i < b->getWidth(); i++) + { + if (b->isFixed(i)) + if (b->getValue(i)) + { + assert(v[i]== BBTrue); + } + else + { + if (v[i] != BBFalse) + { + const BBNodeAIG* v2 = reinterpret_cast (&(v[i])); + if (v2 != 0) + { + cerr << *b; + cerr << i << endl; + cerr << n; + //v2->print(); + } + } + + assert(v[i]== BBFalse); + } + } + } + } + + // ONLY SELECT ONE OF THESE! const bool multiplication_variant1 = false; // multiplication with repeat addition. const bool multiplication_variant2 = false; // multiplication with partial products. const bool multiplication_variant3 = true; // multiplication with booth recoding. const bool multiplication_variant4 = false; // multiplication via sorting networks. - +const bool multiplication_variant5 = false; // Using bounds. // Multiply two bitblasted numbers template -BBNodeVec BitBlaster::BBMult(const BBNodeVec& x, const BBNodeVec& y, - BBNodeSet& support, const ASTNode& xN, const ASTNode& yN) { +BBNodeVec BitBlaster::BBMult(const BBNodeVec& _x, const BBNodeVec& _y, + BBNodeSet& support, const ASTNode& n) { - const int bitWidth = x.size(); - if (multiplication_variant1) { - return mult_normal(x, y, support); - } + checkFixed(_x,n[0]); + checkFixed(_y,n[1]); - stack products[bitWidth]; + BBNodeVec x = _x; + BBNodeVec y = _y; - if (multiplication_variant2) { - mult_allPairs(x, y, support,products); - return buildAdditionNetworkResult(products,bitWidth); - } + if ((BVCONST != n[0].GetKind()) && (BVCONST == n[1].GetKind())) + { + x = _y; + y = _x; + } - if (multiplication_variant3) { - mult_Booth(x, y, support,xN,yN,products); - return buildAdditionNetworkResult(products,bitWidth); - } + const int bitWidth = x.size(); - if (multiplication_variant4) - { - mult_Booth(x, y, support,xN,yN,products); - for (int i = 0; i < bitWidth; i++) - { - if (products[i].size() < 6) - { - mult_SortingNetwork(x, y, support, xN, yN, products, i); - assert(products[i].size() == 1); - } - } - return buildAdditionNetworkResult(products, bitWidth); - } + if (multiplication_variant1) { + return mult_normal(x, y, support); + } + + stack products[bitWidth]; + + if (multiplication_variant2) { + mult_allPairs(x, y, support,products); + return buildAdditionNetworkResult(products,support, bitWidth); + } + if (multiplication_variant3) { + mult_Booth(_x, _y, support,n[0],n[1],products); + return buildAdditionNetworkResult(products,support,bitWidth); + } + + if (multiplication_variant4) + { + mult_Booth(_x, _y, support,n[0],n[1],products); + for (int i = 0; i < bitWidth; i++) + { + if (products[i].size() < 6) + { + mult_SortingNetwork(support,n.GetValueWidth(),n.GetValueWidth(),products,i); + assert(products[i].size() == 1); + } + } + return buildAdditionNetworkResult(products,support, bitWidth); + } + + if (multiplication_variant5) { + mult_allPairs(x, y, support,products); + return multWithBounds(n,products,support); + } - FatalError("sda44f"); + FatalError("sda44f"); } //====== diff --git a/src/to-sat/BitBlaster.h b/src/to-sat/BitBlaster.h index 210de9e..a791c5b 100644 --- a/src/to-sat/BitBlaster.h +++ b/src/to-sat/BitBlaster.h @@ -70,18 +70,27 @@ class BitBlaster { // Multiply. vector BBMult(const vector& x, const vector& y, - set& support, const ASTNode& xN, const ASTNode& yN); + 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); vector mult_normal(const vector& x, const vector& y, set& support); - void mult_SortingNetwork(const vector& x_i, const vector& y_i, - set& support, const ASTNode& xN, const ASTNode& yN, stack * products, int i); + vector multWithBounds(const ASTNode&n, stack* products, set& toConjoinToTop); - vector buildAdditionNetworkResult(stack* products, const int bitWidth); + + void + mult_SortingNetwork( + set& support, const int bitWidth, const int width, stack * products, int i, const int minTrue, const int maxTrue ); + + + void buildAdditionNetworkResult(stack* products, set& support, const int bitWidth, const int index, const int minTrue, const int maxTrue ); + vector buildAdditionNetworkResult(stack* products, set& support, int bitWidth); vector BBAndBit(const vector& y, BBNode b); + void + checkFixed(const vector& v, const ASTNode& n); + // AND each bit of vector y with single bit b and return the result. // (used in BBMult) //vector BBAndBit(const vector& y, ASTNode b);