From: trevor_hansen Date: Sat, 7 Jan 2012 14:04:40 +0000 (+0000) Subject: Adds improved code and extra multiplication variants that aren't currently enabled. X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=35c95e2d5c1b0111c62606dd9ae9c2f913262c36;p=francis%2Fstp.git Adds improved code and extra multiplication variants that aren't currently enabled. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1477 e59a4935-1847-0410-ae03-e826735625c1 --- diff --git a/src/to-sat/BitBlaster.cpp b/src/to-sat/BitBlaster.cpp index 162cb6c..9aca000 100644 --- a/src/to-sat/BitBlaster.cpp +++ b/src/to-sat/BitBlaster.cpp @@ -1814,10 +1814,266 @@ namespace BEEV mult_allPairs(x, y, support, products.data()); return multWithBounds(n, products.data(), support); } + else if (multiplication_variant == "6") + { + //TODO PUT A NEW VERSION 6 in!!!! + //TODO PUT A NEW VERSION 6 in!!!! + + + + mult_Booth(_x, _y, support, n[0], n[1], products.data(),n); + return v7(products.data(), support, bitWidth); + } + else if (multiplication_variant == "7") + { + mult_Booth(_x, _y, support, n[0], n[1], products.data(),n); + return v7(products.data(), support, bitWidth); + } + else if (multiplication_variant == "8") + { + mult_Booth(_x, _y, support, n[0], n[1], products.data(),n); + return v8(products.data(), support, bitWidth); + } else + { + cerr << "Unk variant" << multiplication_variant; FatalError("sda44f"); + } + } + // Takes an unsorted array, and returns a sorted array. + template + BBNodeVec BitBlaster::batcher(const vector& in) + { + assert(in.size() != 0); + + if (in.size() ==1) + return in; + + vector a; + vector b; + + // half way rounded up. + const int halfWay = (((in.size()%2)==0? 0:1) + (in.size()/2) ); + for (int i =0; i < halfWay;i++) + a.push_back(in[i]); + + for (int i =halfWay; i < in.size();i++) + b.push_back(in[i]); + + assert(a.size() >= b.size()); + assert(a.size() + b.size() == in.size()); + vector result= mergeSorted(batcher(a), batcher(b)); + + for (int k = 0; k < result.size(); k++) + assert(!result[k].IsNull()); + + assert(result.size() == in.size()); + return result; + } + + + template + BBNodeVec + BitBlaster::v7(list* products, set& support, const int bitWidth) + { + std::vector > later(bitWidth+1); + std::vector > next(bitWidth+1); + + for (int i = 0; i < bitWidth; i++) + { + next[i+1].clear(); + buildAdditionNetworkResult((products[i]), (next[i + 1]), support, bitWidth == i+1, false); + + // Calculate the carries of carries. + for (int j = i + 1; j < bitWidth; j++) + { + if (next[j].size() == 0) + break; + + buildAdditionNetworkResult((next[j]), (next[j + 1]), support, bitWidth == i+1, false); + } + + // Put the carries of the carries away until later. + for (int j = i + 1; j < bitWidth; j++) + { + if (next[j].size() == 0) + break; + + assert(next[j].size() <=1); + later[j].push_back(next[j].back()); + } + } + + + for (int i = 0; i < bitWidth; i++) + { + // Copy all the laters into products + while(later[i].size() > 0) + { + products[i].push_front(later[i].front()); + later[i].pop_front(); + } + } + + BBNodeVec results; + for (int i = 0; i < bitWidth; i++) + { + + buildAdditionNetworkResult((products[i]), (products[i + 1]), support, bitWidth == i+1, false); + + + results.push_back(products[i].back()); + products[i].pop_back(); + } + + assert(results.size() == ((unsigned)bitWidth)); + return results; + } + + + template + BBNodeVec + BitBlaster::v8(list* products, set& support, const int bitWidth) + { + std::vector > later(bitWidth+1); // +1 then ignore the topmost. + std::vector > next(bitWidth+1); + + for (int i = 0; i < bitWidth; i++) + { + // Put all the products into next. + next[i+1].clear(); + buildAdditionNetworkResult((products[i]), (next[i + 1]), support, i+1 ==bitWidth, false); + + // Calculate the carries of carries. + for (int j = i + 1; j < bitWidth; j++) + { + if (next[j].size() == 0) + break; + + next[j+1].clear(); + buildAdditionNetworkResult(next[j], next[j + 1], support, i+1 ==bitWidth, false); + } + + // Put the carries of the carries away until later. + for (int j = i + 1; j < bitWidth; j++) + { + if (next[j].size() == 0) + break; + + assert(next[j].size() <=1); + later[j].push_back(next[j].back()); + } + } + + + for (int i = 0; i < bitWidth; i++) + { + // Copy all the laters into products + while(later[i].size() > 0) + { + products[i].push_back(later[i].back()); + later[i].pop_back(); + } + } + + BBNodeVec results; + for (int i = 0; i < bitWidth; i++) + { + buildAdditionNetworkResult(products[i], products[i + 1], support, i+1 ==bitWidth, false); + results.push_back(products[i].back()); + products[i].pop_back(); + } + + assert(results.size() == ((unsigned)bitWidth)); + return results; + } + + + // compare element 1 with 2, 3 with 4, and so on. + template + vector + BitBlaster:: compareOddEven(const vector& in) + { + vector result(in); + + for (int i = 2; i < in.size(); i =i+ 2) + { + BBNode a = in[i-1]; + BBNode b = in[i]; + //comparators++; + result[i-1] = nf->CreateNode(OR,a,b); + result[i] = nf->CreateNode(AND,a,b); + } + return result; + } + + + template + vector + BitBlaster::mergeSorted(const vector& in1, const vector& in2) + { + + assert(in1.size() >= in2.size()); + assert(in1.size() >0); + + vector result; + + if (in2.size() ==0) + { + result = in1; + } + else if (in1.size() == 1 && in2.size() ==1) + { + //comparators++; + result.push_back(nf->CreateNode(OR,in1[0], in2[0])); + result.push_back(nf->CreateNode(AND,in1[0], in2[0])); + + } + else + { + vector evenL; + vector oddL; + for (int i =0; i < in1.size();i++) + { + if (i%2 ==0) + evenL.push_back(in1[i]); + else + oddL.push_back(in1[i]); + } + + vector evenR; // Take the even of each. + vector oddR; // Take the odd of each + for (int i =0; i < in2.size();i++) + { + if (i%2 ==0) + evenR.push_back(in2[i]); + else + oddR.push_back(in2[i]); + } + + vector even = evenL.size()< evenR.size() ? mergeSorted(evenR,evenL) : mergeSorted(evenL,evenR); + vector odd = oddL.size() < oddR.size() ? mergeSorted(oddR,oddL) : mergeSorted(oddL,oddR); + + for (int i =0; i < std::max(even.size(),odd.size());i++) + { + if (even.size() > i) + result.push_back(even[i]); + + if (odd.size() > i) + result.push_back(odd[i]); + } + result = compareOddEven(result); + } + + assert(result.size() == in1.size() + in2.size()); + return result; + + } + + + // All combinations of division_variant_1, _2, _3 /* on factoring12bitsx12.cvc with MINISAT2. 000: 0m2.764s diff --git a/src/to-sat/BitBlaster.h b/src/to-sat/BitBlaster.h index f2dcd2e..6a4ac21 100644 --- a/src/to-sat/BitBlaster.h +++ b/src/to-sat/BitBlaster.h @@ -91,6 +91,14 @@ namespace BEEV vector mult_normal(const vector& x, const vector& y, set& support, const ASTNode&n); + + vector batcher(const vector& in); + vector mergeSorted(const vector& in1, const vector& in2); + vector compareOddEven(const vector& in); + + vector v7(list* products, set& support, const int bitWidth); + vector v8(list* products, set& support, const int bitWidth); + vector multWithBounds(const ASTNode&n, list* products, set& toConjoinToTop); bool @@ -112,6 +120,8 @@ namespace BEEV MultiplicationStats* getMS(const ASTNode&n, int& highestZero); + /////////// The end of the multiplication stuff.. + void checkFixed(const vector& v, const ASTNode& n); @@ -212,6 +222,7 @@ namespace BEEV const string multiplication_variant; ASTNodeSet booth_recoded; // Nodes that have been recoded. + public: simplifier::constantBitP::ConstantBitPropagation* cb;