From: trevor_hansen Date: Tue, 10 Jan 2012 03:03:23 +0000 (+0000) Subject: Adds an extra multiplication variant that's not enabled by default. X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=d6ffe885ca103f8a6c9d678f22a0f17ff9c36017;p=francis%2Fstp.git Adds an extra multiplication variant that's not enabled by default. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1484 e59a4935-1847-0410-ae03-e826735625c1 --- diff --git a/src/to-sat/BitBlaster.cpp b/src/to-sat/BitBlaster.cpp index c43ded2..147b101 100644 --- a/src/to-sat/BitBlaster.cpp +++ b/src/to-sat/BitBlaster.cpp @@ -998,10 +998,10 @@ namespace BEEV BitBlaster::BBPlus2(BBNodeVec& sum, const BBNodeVec& y, BBNode cin) { - const int n = sum.size(); - assert(y.size() == (unsigned)n); + const int bitWidth = sum.size(); + assert(y.size() == (unsigned)bitWidth); // Revision 320 avoided creating the nextcin, at I suspect unjustified cost. - for (int i = 0; i < n; i++) + for (int i = 0; i < bitWidth; i++) { BBNode nextcin = Majority(sum[i], y[i], cin); sum[i] = nf->CreateNode(XOR, sum[i], y[i], cin); @@ -1554,6 +1554,7 @@ namespace BEEV return NULL; } + // Each bit of 'x' is taken in turn and multiplied by a shifted y. template BBNodeVec BitBlaster::mult_normal(const BBNodeVec& x, const BBNodeVec& y, BBNodeSet& support, @@ -1569,11 +1570,9 @@ namespace BEEV BBNodeVec ycopy(y); - // start prod with first partial product. - BBNodeVec prod = BBNodeVec(BBAndBit(y, *x.begin())); - // start loop at next bit. + BBNodeVec prod = BBNodeVec(BBAndBit(y, *x.begin())); // start prod with first partial product. - for (int i = 1; i < bitWidth; i++) + for (int i = 1; i < bitWidth; i++) // start loop at next bit. { const BBNode& xit = x[i]; @@ -1735,14 +1734,14 @@ namespace BEEV y = _x; } - const int bitWidth = x.size(); + const int bitWidth = n.GetValueWidth(); + assert(x.size() == bitWidth); + assert(y.size() == bitWidth); - // Create one extra to avoid special cases. - std::vector > products(bitWidth+1); + std::vector > products(bitWidth+1); // Create one extra to avoid special cases. if (multiplication_variant == "1") { - //cerr << "v1"; return mult_normal(x, y, support, n); } else if (multiplication_variant == "2") @@ -1780,32 +1779,29 @@ namespace BEEV return buildAdditionNetworkResult(products.data(), support, n); } + mult_allPairs(x, y, support, products.data()); return multWithBounds(n, products.data(), support); } else if (multiplication_variant == "6") { mult_Booth(_x, _y, support,n[0],n[1],products.data(),n); - vector prior; - - for (int i = 0; i < bitWidth; i++) - { - vector output; - v6(support, products[i], output ,prior); - prior = output; - assert(products[i].size() == 1); - } - return buildAdditionNetworkResult(products.data(),support, n); + return v6(products.data(), support, n); } else if (multiplication_variant == "7") { mult_Booth(_x, _y, support, n[0], n[1], products.data(),n); - return v7(products.data(), support, bitWidth,n); + return v7(products.data(), support, n); } else if (multiplication_variant == "8") { mult_Booth(_x, _y, support, n[0], n[1], products.data(),n); - return v8(products.data(), support, bitWidth,n); + return v8(products.data(), 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); } else { @@ -1851,13 +1847,13 @@ namespace BEEV // assumes that the prior column is sorted. template void - BitBlaster::v6(BBNodeSet& support, list& current, vector& currentSorted, + BitBlaster::sortingNetworkAdd(BBNodeSet& support, list& current, vector& currentSorted, vector& priorSorted) { - int height = current.size(); + vector toSort; - // convert the stack to a vector. + // convert the list to a vector. while (current.size() != 0) { BBNode currentN = current.front(); @@ -1882,7 +1878,7 @@ namespace BEEV currentSorted = mergeSorted(sortedCarryIn, sorted); assert(currentSorted.size() == sortedCarryIn.size() + toSort.size()); - height = currentSorted.size(); + int height = currentSorted.size(); assert(current.size() == 0); @@ -1907,8 +1903,106 @@ namespace BEEV template BBNodeVec - BitBlaster::v7(list* products, set& support, const int bitWidth, const ASTNode&n) + BitBlaster::v6(list* products, set& support, const ASTNode&n) + { + const int bitWidth = n.GetValueWidth(); + + vector prior; + + for (int i = 0; i < bitWidth; i++) + { + vector output; + sortingNetworkAdd(support, products[i], output ,prior); + prior = output; + assert(products[i].size() == 1); + } + + // This converts the array of lists to a vector. + return buildAdditionNetworkResult(products ,support, n); + } + + + // Sorting network that delivers carries directly to the correct column. + // 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) + { + const int bitWidth = n.GetValueWidth(); + + vector< vector< BBNode> > toAdd(bitWidth); + + for (int column = 0; column < bitWidth; column++) + { + vector sorted; // The current column (sorted) gets put into here. + vector prior; // Prior is always empty in this.. + + const int size= products[column].size(); + sortingNetworkAdd(support, products[column], sorted ,prior); + + assert(products[column].size() == 1); + assert(sorted.size() == size); + + for (int k = 2; k <= sorted.size(); k++) + { + BBNode part; + if (k==sorted.size()) + part = sorted[k - 1]; + else + { + // We expect the 1's to be sorted first. + assert((sorted[k-1] != BBFalse) || (sorted[k] != BBTrue)); + part = nf->CreateNode(AND, nf->CreateNode(NOT, sorted[k]), sorted[k - 1]); + + if (part == BBFalse) + continue; // shortcut. + } + + int position =k; + int increment =1; + while (position != 0) + { + if (column+increment >= bitWidth) + break; + + position >>=1; + if ((position & 1) !=0) // bit is set. + toAdd[column+increment].push_back(part); + + increment++; + } + } + + for (int carry_column =column+1; carry_column < bitWidth; carry_column++) + { + if (toAdd[carry_column].size() ==0) + continue ; + BBNode disjunct = BBFalse; + for (int l = 0; l < toAdd[carry_column].size();l++) + { + disjunct = nf->CreateNode(OR,disjunct,toAdd[carry_column][l]); + } + + if(disjunct != BBFalse) + products[carry_column].push_back(disjunct); + toAdd[carry_column].clear(); + } + } + for (int i = 0; i < bitWidth; i++) + { + assert(toAdd[i].size() == 0); + } + + // This converts the array of lists to a vector. + return buildAdditionNetworkResult(products ,support, n); + } + + + template + BBNodeVec + BitBlaster::v7(list* products, set& support, const ASTNode&n) { + const int bitWidth = n.GetValueWidth(); // If we have details of the partial products which can be true, int ignore = -1; @@ -1975,8 +2069,9 @@ namespace BEEV template BBNodeVec - BitBlaster::v8(list* products, set& support, const int bitWidth, const ASTNode&n) + BitBlaster::v8(list* products, set& support, const ASTNode&n) { + const int bitWidth = n.GetValueWidth(); // If we have details of the partial products which can be true, int ignore = -1; diff --git a/src/to-sat/BitBlaster.h b/src/to-sat/BitBlaster.h index fa8d7f5..6b4c2f4 100644 --- a/src/to-sat/BitBlaster.h +++ b/src/to-sat/BitBlaster.h @@ -98,10 +98,13 @@ namespace BEEV void - v6(set& support, list& current, vector& currentSorted, vector& priorSorted); + sortingNetworkAdd(set& support, list& current, vector& currentSorted, vector& priorSorted); - vector v7(list* products, set& support, const int bitWidth, const ASTNode&n); - vector v8(list* products, set& support, const int bitWidth, const ASTNode&n); + + 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 multWithBounds(const ASTNode&n, list* products, set& toConjoinToTop);