From 307a9883e1514666ca075afd231c66061a8ea263 Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Thu, 21 Apr 2011 02:06:24 +0000 Subject: [PATCH] Change the sorting network based adder (which isn't used by default). git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1281 e59a4935-1847-0410-ae03-e826735625c1 --- src/to-sat/BitBlaster.cpp | 137 +++++++++++++++++++++++--------------- src/to-sat/BitBlaster.h | 4 +- 2 files changed, 85 insertions(+), 56 deletions(-) diff --git a/src/to-sat/BitBlaster.cpp b/src/to-sat/BitBlaster.cpp index f083cda..cfcf304 100644 --- a/src/to-sat/BitBlaster.cpp +++ b/src/to-sat/BitBlaster.cpp @@ -621,19 +621,39 @@ const BBNodeVec BitBlaster::BBTerm(const ASTNode& _term, break; } case BVPLUS: { - assert(term.Degree() >=1); - // Add children pairwise and accumulate in BBsum - - ASTVec::const_iterator it = term.begin(); - BBNodeVec tmp_res = BBTerm(*it, support); - for (++it; it < kids_end; it++) { - const BBNodeVec& tmp = BBTerm(*it, support); - assert(tmp.size() == num_bits); - BBPlus2(tmp_res, tmp, nf->getFalse()); - } - - result = tmp_res; - break; + assert(term.Degree() >=1); + if (true) + { + // Add children pairwise and accumulate in BBsum + + ASTVec::const_iterator it = term.begin(); + BBNodeVec tmp_res = BBTerm(*it, support); + for (++it; it < kids_end; it++) { + const BBNodeVec& tmp = BBTerm(*it, support); + assert(tmp.size() == num_bits); + BBPlus2(tmp_res, tmp, nf->getFalse()); + } + + result = tmp_res; + } + else + { + // Add all the children up using an addition network. + vector results; + for (int i=0; i < term.Degree();i++) + results.push_back(BBTerm(term[i], support)); + + const int bitWidth = term[0].GetValueWidth(); + stack products[bitWidth]; + for (int i=0; i < bitWidth;i++) + { + for (int j=0; j < results.size();j++) + products[i].push(results[j][i]); + } + + result = buildAdditionNetworkResult(products,support,bitWidth); + } + break; } case BVUMINUS: { const BBNodeVec& bbkid = BBTerm(term[0], support); @@ -1296,8 +1316,11 @@ BBNodeVec BitBlaster::multWithBounds(const ASTNode&n, sta 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]); + //int width = std::min(ms.sumH[i]+1, (signed)products[i].size()); + vector output; + vector prior; + mult_SortingNetwork(toConjoinToTop, products[i], output ,prior, ms.sumL[i], ms.sumH[i]); + prior = output; } else // addition network. @@ -1449,73 +1472,78 @@ BBNodeVec BitBlaster::mult_normal(const BBNodeVec& x, return prod; } + // assumes the prior column is sorted. template void 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 ) + BBNodeSet& support, stack& current, vector& currentSorted, vector& priorSorted, + const int minTrue = 0, const int maxTrue = ((unsigned)~0) >> 1 ) { - assert(i sorted(width, nf->getFalse()); + // 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]); + } + + const int height = current.size(); + + // Set the current sorted to all false. + currentSorted.clear(); + { + vector temp(height, nf->getFalse()); + currentSorted = temp; + } + + // n^2 sorting network. 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); + vector oldSorted(currentSorted); + BBNode c = current.top(); + current.pop(); + currentSorted[0] = nf->CreateNode(OR, oldSorted[0], c); - for (int j = 1; j <= std::min(l,width-1); j++) + for (int j = 1; j <= l; j++) { - sorted[j] = nf->CreateNode(OR, nf->CreateNode(AND, + currentSorted[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(current.size() == 0); - assert(products[i].size() == 0); + for (int k = 0; k < height; k++) + assert(!currentSorted[k].IsNull()); if (conjoin_to_top) { 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; + support.insert(currentSorted[j]); + currentSorted[j] = BBTrue; } - } - // Add to next up columns. - if (i + 1 != bitWidth) - { - for (int k = 1; k < width; k += 2) + for (int j = height - 1; j >= maxTrue; j--) { - products[i + 1].push(sorted[k]); + support.insert(nf->CreateNode(NOT, currentSorted[j])); + currentSorted[j] = BBFalse; } } BBNode resultNode = nf->getFalse(); // Constrain to equal the result - for (int k = 1; k < width; k += 2) + for (int k = 1; k < height; k += 2) { - BBNode part = nf->CreateNode(AND, nf->CreateNode(NOT, sorted[k]), sorted[k - 1]); + BBNode part = nf->CreateNode(AND, nf->CreateNode(NOT, currentSorted[k]), currentSorted[k - 1]); resultNode = nf->CreateNode(OR, resultNode, part); } // constraint the all '1's case. - if (width % 2 == 1) - resultNode = nf->CreateNode(OR, resultNode, sorted.at(width - 1)); + if (height % 2 == 1) + resultNode = nf->CreateNode(OR, resultNode, currentSorted.at(height - 1)); - products[i].push(resultNode); + current.push(resultNode); } @@ -1594,15 +1622,16 @@ BBNodeVec BitBlaster::BBMult(const BBNodeVec& _x, const B } else if (mv == "4") { - //cout << "v4"; + //cerr << "v4"; mult_Booth(_x, _y, support,n[0],n[1],products); + vector prior; + 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); - } + vector output; + mult_SortingNetwork(support, products[i], output ,prior); + prior = output; + assert(products[i].size() == 1); } return buildAdditionNetworkResult(products,support, bitWidth); } diff --git a/src/to-sat/BitBlaster.h b/src/to-sat/BitBlaster.h index 42d0dfd..18eb476 100644 --- a/src/to-sat/BitBlaster.h +++ b/src/to-sat/BitBlaster.h @@ -82,8 +82,8 @@ class BitBlaster { void mult_SortingNetwork( - set& support, const int bitWidth, const int width, stack * products, int i, const int minTrue, const int maxTrue ); - + set& support, stack& currentColumn, vector& currentSorted, vector& priorSorted, + 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); -- 2.47.3