From: trevor_hansen Date: Sun, 15 Aug 2010 04:06:33 +0000 (+0000) Subject: Change non-enabled code. X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=975f3c2ff25cca4b1a182255d25697950571781a;p=francis%2Fstp.git Change non-enabled code. This improves the bounds aware multiplication encoding (which is not the default encoding for multiplication). git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@984 e59a4935-1847-0410-ae03-e826735625c1 --- diff --git a/src/to-sat/BitBlaster.cpp b/src/to-sat/BitBlaster.cpp index 421140f..553d9a7 100644 --- a/src/to-sat/BitBlaster.cpp +++ b/src/to-sat/BitBlaster.cpp @@ -201,7 +201,7 @@ const BBNodeVec BitBlaster::BBTerm(const ASTNode& term, B typename BBNodeVecMap::iterator it = BBTermMemo.find(term); if (it != BBTermMemo.end()) { // Constant bit propagation may have updated something. - //updateTerm(term,it->second,support); + updateTerm(term,it->second,support); return it->second; } @@ -524,8 +524,8 @@ const BBNode BitBlaster::BBForm(const ASTNode& form) cb->propagate(); } - BBNodeSet support; - BBNode r= BBForm(form,support); + BBNodeSet support; + BBNode r= BBForm(form,support); vector v; v.insert(v.end(), support.begin(), support.end()); @@ -852,6 +852,7 @@ template BBNodeVec BitBlaster::buildAdditionNetworkResult(stack* products, set& support, const int bitWidth) { + BBNodeVec results; for (int i = 0; i < bitWidth; i++) { @@ -871,7 +872,6 @@ template void BitBlaster::buildAdditionNetworkResult(stack* products, set& support, const int bitWidth, const int i, const int minTrue = 0, const int maxTrue = ((unsigned)~0) >> 1 ) { - while (products[i].size() >= 2) { BBNode c; @@ -910,61 +910,84 @@ void BitBlaster::buildAdditionNetworkResult(stack cerr << "Sum" << sum; } - // I experimented with making products[] a deque and accessing the front and back of the queue. - // As a stack is works considerably better. - products[i].push(sum); - // If we know the carry must be less than 2. // Constraint each of the carries to zero. - if (maxTrue < 2) + if (conjoin_to_top && maxTrue ==0) + { + support.insert(nf->CreateNode(NOT, a)); + support.insert(nf->CreateNode(NOT, b)); + support.insert(nf->CreateNode(NOT, c)); + } + else + { + // I experimented with making products[] a deque and accessing the front and back of the queue. + // As a stack is works considerably better. + products[i].push(sum); + } + if (conjoin_to_top && maxTrue ==1) { - support.insert(nf->CreateNode(NOT, carry)); + support.insert(nf->CreateNode(NOT, carry)); } else if (i + 1 != bitWidth) + { products[i + 1].push(carry); + } } assert(1==products[i].size()); } -const bool debug_bounds = true; +const bool debug_bounds = false; + + template + bool + BitBlaster::statsFound(const ASTNode& n) + { + if (NULL == cb) + return false; + + if (NULL == cb->msm) + return false; + + simplifier::constantBitP::MultiplicationStatsMap::NodeToStats::const_iterator it; + it = cb->msm->map.find(n); + return (it != cb->msm->map.end()); + } // Make sure x and y are the parameters in the correct order. THIS ISNT COMMUTATIVE. template BBNodeVec BitBlaster::multWithBounds(const ASTNode&n, stack* products, BBNodeSet& toConjoinToTop) { - bool statsFound = false; + simplifier::constantBitP::MultiplicationStats ms; const int bitWidth = n.GetValueWidth(); + assert(statsFound(n)); + assert (NULL != cb); assert (NULL != cb->msm); - { - simplifier::constantBitP::MultiplicationStatsMap::NodeToStats::const_iterator - it; - it = cb->msm->map.find(n); - if (it != cb->msm->map.end()) - { - //it->second->print(); - ms = it->second; - statsFound = true; - - assert(ms.x.getWidth() == ms.y.getWidth()); - assert(ms.r.getWidth() == ms.y.getWidth()); - assert(ms.r.getWidth() == (int)ms.bitWidth); - assert(ms.r.getWidth() == bitWidth); - } - } - if (!statsFound) - return buildAdditionNetworkResult(products, toConjoinToTop, bitWidth); + simplifier::constantBitP::MultiplicationStatsMap::NodeToStats::const_iterator it; + it = cb->msm->map.find(n); + if (it != cb->msm->map.end()) + { + //it->second->print(); + ms = it->second; + + + assert(ms.x.getWidth() == ms.y.getWidth()); + assert(ms.r.getWidth() == ms.y.getWidth()); + assert(ms.r.getWidth() == (int)ms.bitWidth); + assert(ms.r.getWidth() == bitWidth); + + } // If all of the partial products in the column must be zero, then replace for (int i = 0; i < bitWidth; i++) { - if (ms.columnH[i] == 0) + if (conjoin_to_top && ms.columnH[i] == 0) { while (products[i].size() > 0) { @@ -986,13 +1009,12 @@ BBNodeVec BitBlaster::multWithBounds(const ASTNode&n, sta for (int i = 0; i < bitWidth; i++) { if (debug_bounds) - cerr << " " << products[i].size(); - if (statsFound) - { + { + cerr << " " << products[i].size(); cerr << "["<< ms.columnL[i] << ":"<< ms.columnH[i] << "]["<< ms.sumL[i] << ":" << ms.sumH[i] << "]"; } - if ((products[i].size() > ms.sumH[i]) && ms.sumH[i] < 6) + if ((products[i].size() > ms.sumH[i]) && ms.sumH[i] < 10) { if (debug_bounds) cerr << "S"; @@ -1176,16 +1198,19 @@ BBNodeVec BitBlaster::mult_normal(const BBNodeVec& x, assert(products[i].size() == 0); - for (int j = 0; j < minTrue; j++) + if (conjoin_to_top) { - support.insert(sorted[j]); - sorted[j] = BBTrue; - } + 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; + for (int j = width - 1; j >= maxTrue; j--) + { + support.insert(nf->CreateNode(NOT, sorted[j])); + sorted[j] = BBFalse; + } } // Add to next up columns. @@ -1310,10 +1335,18 @@ BBNodeVec BitBlaster::BBMult(const BBNodeVec& _x, const B return buildAdditionNetworkResult(products,support, bitWidth); } - if (multiplication_variant5) { - mult_allPairs(x, y, support,products); - return multWithBounds(n,products,support); - } + if (multiplication_variant5) + { + + if (!statsFound(n)) + { + mult_Booth(_x, _y, support, n[0], n[1], products); + return buildAdditionNetworkResult(products, support, bitWidth); + } + + mult_allPairs(x, y, support, products); + return multWithBounds(n, products, support); + } FatalError("sda44f"); } diff --git a/src/to-sat/BitBlaster.h b/src/to-sat/BitBlaster.h index a791c5b..e73f3e3 100644 --- a/src/to-sat/BitBlaster.h +++ b/src/to-sat/BitBlaster.h @@ -76,6 +76,8 @@ class BitBlaster { vector mult_normal(const vector& x, const vector& y, set& support); vector multWithBounds(const ASTNode&n, stack* products, set& toConjoinToTop); + bool + statsFound(const ASTNode& n); void