From: trevor_hansen Date: Tue, 31 Jan 2012 01:12:24 +0000 (+0000) Subject: Adds extra code that is not enabled by default. X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=66802fbe4c2704c5013296ca36620ebbd4fc2150;p=francis%2Fstp.git Adds extra code that is not enabled by default. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1541 e59a4935-1847-0410-ae03-e826735625c1 --- diff --git a/src/to-sat/BitBlaster.cpp b/src/to-sat/BitBlaster.cpp index fddf077..c056ce3 100644 --- a/src/to-sat/BitBlaster.cpp +++ b/src/to-sat/BitBlaster.cpp @@ -1240,7 +1240,7 @@ namespace BEEV // If we have details of the partial products which can be true, int ignore = -1; simplifier::constantBitP::MultiplicationStats* ms = getMS(n, ignore); - if (!multiplication_upper_bound) + if (!upper_multiplication_bound) ms = NULL; BBNodeVec results; @@ -1359,7 +1359,7 @@ namespace BEEV const int bitWidth = n.GetValueWidth(); int ignored=0; - assert(multiplication_upper_bound); + assert(upper_multiplication_bound); simplifier::constantBitP::MultiplicationStats& ms = *getMS(n, ignored); @@ -1565,7 +1565,7 @@ namespace BEEV // 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) + if (!upper_multiplication_bound) ms = NULL; BBNodeVec ycopy(y); @@ -1715,6 +1715,47 @@ namespace BEEV } } + // If it's not booth encoded, and the column sum is zero, + // then set that all the partial products must be zero. + // For this to do anything constant bit propagation must be + // turned on, and upper_multiplication_bound must be set. + template + void + BitBlaster::setColumnsToZero(vector >& products, set& support, + const ASTNode&n) + { + const int bitWidth = n.GetValueWidth(); + + // If we have details of the partial products which can be true, + int highestZero = -1; + simplifier::constantBitP::MultiplicationStats* ms = getMS(n, highestZero); + if (!upper_multiplication_bound) + ms = NULL; + + if (ms == NULL) + return; + + for (int i = 0; i < bitWidth; i++) + { + if (ms->sumH[i] == 0) + { + while (products[i].size() > 0) + { + BBNode curr = products[i].back(); + products[i].pop_back(); + + if (BBFalse == curr) + continue; + + support.insert(nf->CreateNode(NOT, curr)); + } + products[i].push_back(BBFalse); + + } + } + } + + // Multiply two bitblasted numbers template BBNodeVec @@ -1744,16 +1785,13 @@ namespace BEEV { return mult_normal(x, y, support, n); } - else if (multiplication_variant == "2") - { - //cout << "v2"; - mult_allPairs(x, y, support, products); - return buildAdditionNetworkResult(products, support, n); - } - + //else if (multiplication_variant == "2") + // V2 used to be V3 with normal rather than booth recoding. + // To recreate V2, use V3 and turn off Booth recoding. else if (multiplication_variant == "3") { mult_Booth(_x, _y, support, n[0], n[1], products, n); + setColumnsToZero(products,support,n); return buildAdditionNetworkResult(products, support, n); } else if (multiplication_variant == "4") @@ -1773,36 +1811,48 @@ namespace BEEV } else if (multiplication_variant == "5") { - if (!statsFound(n) || !multiplication_upper_bound) + if (!statsFound(n) || !upper_multiplication_bound) { mult_Booth(_x, _y, support, n[0], n[1], products, n); + setColumnsToZero(products,support,n); return buildAdditionNetworkResult(products, support, n); } mult_allPairs(x, y, support, products); + setColumnsToZero(products,support,n); return multWithBounds(n, products, support); } else if (multiplication_variant == "6") { mult_Booth(_x, _y, support,n[0],n[1],products,n); + setColumnsToZero(products,support,n); return v6(products, support, n); } else if (multiplication_variant == "7") { mult_Booth(_x, _y, support, n[0], n[1], products,n); + setColumnsToZero(products,support,n); return v7(products, support, n); } else if (multiplication_variant == "8") { mult_Booth(_x, _y, support, n[0], n[1], products,n); + setColumnsToZero(products,support,n); return v8(products, support, n); } else if (multiplication_variant == "9") { mult_Booth(_x, _y, support, n[0], n[1], products,n); + setColumnsToZero(products,support,n); return v9(products, support,n); } + else if (multiplication_variant == "13") + { + mult_Booth(_x, _y, support, n[0], n[1], products,n); + setColumnsToZero(products,support,n); + return v13(products, support,n); + } else { cerr << "Unk variant" << multiplication_variant; @@ -1921,6 +1971,80 @@ namespace BEEV return buildAdditionNetworkResult(products ,support, n); } + template + BBNodeVec + BitBlaster::v13(vector >& products, set& support, const ASTNode&n) + { + const int bitWidth = n.GetValueWidth(); + + int ignore = -1; + simplifier::constantBitP::MultiplicationStats* ms = getMS(n, ignore); + if (!upper_multiplication_bound) + ms = NULL; + + bool done = false; + + vector a(bitWidth); + vector b(bitWidth); + + while (!done) + { + done = true; + + for (int i = 0; i < bitWidth; i++) + { + if (products[i].size() > 2) + done = false; + if (products[i].size() > 0) + { + a[i] = products[i].back(); + products[i].pop_back(); + } + else + a[i] = BBFalse; + + if (products[i].size() > 0) + { + b[i] = products[i].back(); + products[i].pop_back(); + } + else + b[i] = BBFalse; + + if (ms != NULL && ms->sumH[i] == 0) + { + if (a[i] != BBFalse) + { + support.insert(nf->CreateNode(NOT, a[i])); + a[i] = BBFalse; + } + + if (b[i] != BBFalse) + { + support.insert(nf->CreateNode(NOT, b[i])); + b[i] = BBFalse; + } + }assert(!a[i].IsNull()); + assert(!b[i].IsNull()); + + } + BBPlus2(a, b, BBFalse); + for (int i = 0; i < bitWidth; i++) + products[i].push_back(a[i]); + } + + BBNodeVec results; + for (int i = 0; i < bitWidth; i++) + { + assert(products[i].size() ==1); + results.push_back(products[i].back()); + } + + assert(results.size() == ((unsigned)bitWidth)); + return results; + } + + // 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. @@ -2007,7 +2131,7 @@ namespace BEEV // If we have details of the partial products which can be true, int ignore = -1; simplifier::constantBitP::MultiplicationStats* ms = getMS(n, ignore); - if (!multiplication_upper_bound) + if (!upper_multiplication_bound) ms = NULL; @@ -2076,7 +2200,7 @@ namespace BEEV // If we have details of the partial products which can be true, int ignore = -1; simplifier::constantBitP::MultiplicationStats* ms = getMS(n, ignore); - if (!multiplication_upper_bound) + if (!upper_multiplication_bound) ms = NULL; diff --git a/src/to-sat/BitBlaster.h b/src/to-sat/BitBlaster.h index 50058c6..30fdc77 100644 --- a/src/to-sat/BitBlaster.h +++ b/src/to-sat/BitBlaster.h @@ -97,6 +97,10 @@ namespace BEEV vector compareOddEven(const vector& in); + + void setColumnsToZero(vector >& products, set& support,const ASTNode&n); + + void sortingNetworkAdd(set& support, list& current, vector& currentSorted, vector& priorSorted); @@ -105,6 +109,8 @@ namespace BEEV vector v7(vector >& products, set& support, const ASTNode&n); vector v8(vector >& products, set& support, const ASTNode&n); vector v9(vector >& products, set& support, const ASTNode&n); + vector v13(vector >& products, set& support, const ASTNode&n); + vector multWithBounds(const ASTNode&n, vector >& products, set& toConjoinToTop); @@ -224,7 +230,7 @@ namespace BEEV const bool division_variant_3; const bool adder_variant; const bool bbbvle_variant; - const bool multiplication_upper_bound; + const bool upper_multiplication_bound; const bool bvplus_variant; const string multiplication_variant; @@ -253,7 +259,7 @@ namespace BEEV 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")), + upper_multiplication_bound("1" == _uf->get("upper_multiplication_bound", "0")), adder_variant("1" == _uf->get("adder_variant", "1")),