From: trevor_hansen Date: Sat, 7 Jan 2012 13:28:32 +0000 (+0000) Subject: Refactor. Remove some bad code. X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=e44cd57d0b7ccc6906b50d5aed16df371295ad08;p=francis%2Fstp.git Refactor. Remove some bad code. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1476 e59a4935-1847-0410-ae03-e826735625c1 --- diff --git a/src/to-sat/BitBlaster.cpp b/src/to-sat/BitBlaster.cpp index 437aa44..162cb6c 100644 --- a/src/to-sat/BitBlaster.cpp +++ b/src/to-sat/BitBlaster.cpp @@ -681,7 +681,7 @@ namespace BEEV products[i].push_back(results[j][i]); } - result = buildAdditionNetworkResult(products.data(), support, bitWidth, term); + result = buildAdditionNetworkResult(products.data(), support, term); } break; } @@ -1233,45 +1233,39 @@ namespace BEEV template BBNodeVec BitBlaster::buildAdditionNetworkResult(list* products, set& support, - const int bitWidth, const ASTNode& n) + 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); + int ignore = -1; + simplifier::constantBitP::MultiplicationStats* ms = getMS(n, ignore); if (!multiplication_upper_bound) ms = NULL; BBNodeVec results; for (int i = 0; i < bitWidth; i++) { - int max_true; - if (ms != NULL && (ms->sumH[i] == 0)) - max_true = 0; - else - max_true = ((unsigned) ~0) >> 1; + buildAdditionNetworkResult(products[i], products[i+1], support, (i + 1 == bitWidth), (ms != NULL && (ms->sumH[i] == 0))); - if (i + 1 != bitWidth) - buildAdditionNetworkResult(&(products[i]), &(products[i + 1]), support, bitWidth, i, 0, max_true); - else - buildAdditionNetworkResult(&(products[i]), NULL, support, bitWidth, i, 0, max_true); assert(products[i].size() == 1); results.push_back(products[i].back()); } + assert(products[i+1].size() ==0); // i+1 is defined but should never be used. assert(results.size() == ((unsigned)bitWidth)); return results; } // Use full adders to create an addition network that adds together each of the -// partial products. +// partial products. Puts the carries into the "to" list. + template void - BitBlaster::buildAdditionNetworkResult(list* from_, list* to, - set& support, const int bitWidth, const int i, const int minTrue, const int maxTrue) + BitBlaster::buildAdditionNetworkResult(list& from, list& to, + set& support, const bool at_end, const bool all_false) { - list& from = *from_; while (from.size() >= 2) { @@ -1291,7 +1285,7 @@ namespace BEEV from.pop_back(); // Nothing can be true. All must be false. - if (conjoin_to_top && maxTrue == 0) + if (conjoin_to_top && all_false) { if (BBFalse != a) support.insert(nf->CreateNode(NOT, a)); @@ -1326,14 +1320,9 @@ namespace BEEV from.push_back(sum); - if (conjoin_to_top && maxTrue == 1) - { - support.insert(nf->CreateNode(NOT, carry)); - } - else if (i + 1 != bitWidth && carry != BBFalse) - { - to->push_back(carry); - } + if (!at_end && carry != BBFalse) + to.push_back(carry); + } if (0 == from.size()) from.push_back(BBFalse); @@ -1439,8 +1428,7 @@ namespace BEEV if (debug_bounds) cerr << "A"; - buildAdditionNetworkResult(&(products[i]), ((i + 1 == bitWidth) ? NULL : &(products[i + 1])), toConjoinToTop, - bitWidth, i, ms.sumL[i], ms.sumH[i]); + buildAdditionNetworkResult(products[i], products[i+1], toConjoinToTop, (i + 1 == bitWidth), 0 == ms.sumH[i]); } assert(products[i].size() == 1); @@ -1779,7 +1767,9 @@ namespace BEEV } const int bitWidth = x.size(); - std::vector > products(bitWidth); + + // Create one extra to avoid special cases. + std::vector > products(bitWidth+1); if (multiplication_variant == "1") { @@ -1790,13 +1780,13 @@ namespace BEEV { //cout << "v2"; mult_allPairs(x, y, support, products.data()); - return buildAdditionNetworkResult(products.data(), support, bitWidth, n); + return buildAdditionNetworkResult(products.data(), support, n); } else if (multiplication_variant == "3") { mult_Booth(_x, _y, support, n[0], n[1], products.data(), n); - return buildAdditionNetworkResult(products.data(), support, bitWidth, n); + return buildAdditionNetworkResult(products.data(), support, n); } else if (multiplication_variant == "4") { @@ -1811,14 +1801,14 @@ namespace BEEV prior = output; assert(products[i].size() == 1); } - return buildAdditionNetworkResult(products.data(), support, bitWidth, n); + return buildAdditionNetworkResult(products.data(), support, n); } else if (multiplication_variant == "5") { if (!statsFound(n)) { mult_Booth(_x, _y, support, n[0], n[1], products.data(), n); - return buildAdditionNetworkResult(products.data(), support, bitWidth, n); + return buildAdditionNetworkResult(products.data(), support, n); } mult_allPairs(x, y, support, products.data()); diff --git a/src/to-sat/BitBlaster.h b/src/to-sat/BitBlaster.h index 6c3bb67..f2dcd2e 100644 --- a/src/to-sat/BitBlaster.h +++ b/src/to-sat/BitBlaster.h @@ -101,10 +101,10 @@ namespace BEEV vector& priorSorted, const int minTrue = 0, const int maxTrue = ((unsigned) ~0) >> 1); void - buildAdditionNetworkResult(list* from, list* to, set& support, const int bitWidth, - const int index, const int minTrue = 0, const int maxTrue = ((unsigned) ~0) >> 1); + buildAdditionNetworkResult(list& from, list& to, set& support, + const bool top, const bool empty); vector - buildAdditionNetworkResult(list* products, set& support, const int bitWidth, const ASTNode& n); + buildAdditionNetworkResult(list* products, set& support, const ASTNode& n); vector BBAndBit(const vector& y, BBNode b); @@ -228,12 +228,13 @@ namespace BEEV BitBlaster(BBNodeManagerT* bnm, Simplifier* _simp, NodeFactory *astNodeF, UserDefinedFlags *_uf, simplifier::constantBitP::ConstantBitPropagation *cb_ = NULL) : - uf(_uf), division_variant_1("1" == _uf->get("division_variant_1", "1")), division_variant_2( - "1" == _uf->get("division_variant_2", "1")), division_variant_3( - "1" == _uf->get("division_variant_3", "1")), + uf(_uf), + division_variant_1("1" == _uf->get("division_variant_1", "1")), + division_variant_2("1" == _uf->get("division_variant_2", "1")), + 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")), + multiplication_variant(_uf->get("multiplication_variant", "3")), + multiplication_upper_bound("1" == _uf->get("upper_multiplication_bound", "0")), adder_variant("1" == _uf->get("adder_variant", "1")),