From 1a99e458a0c814b95e0458adb41d347db4c31aae Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Tue, 31 Jan 2012 14:17:02 +0000 Subject: [PATCH] Refactor. Automatically layout. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1545 e59a4935-1847-0410-ae03-e826735625c1 --- .../ConstantBitP_Multiplication.cpp | 1109 ++++++++--------- 1 file changed, 549 insertions(+), 560 deletions(-) diff --git a/src/simplifier/constantBitP/ConstantBitP_Multiplication.cpp b/src/simplifier/constantBitP/ConstantBitP_Multiplication.cpp index bbfec03..3dd4a21 100644 --- a/src/simplifier/constantBitP/ConstantBitP_Multiplication.cpp +++ b/src/simplifier/constantBitP/ConstantBitP_Multiplication.cpp @@ -9,654 +9,643 @@ #include "multiplication/ColumnStats.h" // Multiply. - namespace simplifier { -namespace constantBitP -{ -using std::endl; -using std::pair; -using std::set; + namespace constantBitP + { + using std::endl; + using std::pair; + using std::set; -const bool debug_multiply = false; -std::ostream& log = std::cerr; + const bool debug_multiply = false; + std::ostream& log = std::cerr; // The maximum size of the carry into a column for MULTIPLICATION -int maximumCarryInForMultiplication(int column) -{ - int result = 0; - int currIndex = 0; + int + maximumCarryInForMultiplication(int column) + { + int result = 0; + int currIndex = 0; + + while (currIndex < column) + { + currIndex++; + result = (result + currIndex) / 2; + } - while (currIndex < column) - { - currIndex++; - result = (result + currIndex) / 2; - } + return result; + } - return result; -} + Result + fixIfCanForMultiplication(vector& children, const int index, const int aspirationalSum) + { + assert(index >=0); + assert(index < children[0]->getWidth()); + FixedBits& x = *children[0]; + FixedBits& y = *children[1]; -Result fixIfCanForMultiplication(vector& children, const int index, - const int aspirationalSum) -{ - assert(index >=0); - assert(index < children[0]->getWidth()); - - FixedBits& x = *children[0]; - FixedBits& y = *children[1]; - - ColumnStats cs(x, y, index); - - int columnUnfixed = cs.columnUnfixed; // both unfixed. - int columnOneFixed = cs.columnOneFixed; // one of the values is fixed to one. - int columnOnes = cs.columnOnes; // both are ones. - //int columnZeroes = cs.columnZeroes; // either are zero. - - Result result = NO_CHANGE; - - // We need every value that is unfixed to be set to one. - if (aspirationalSum == columnOnes + columnOneFixed + columnUnfixed - && ((columnOneFixed + columnUnfixed) > 0)) - { - for (unsigned i = 0; i <= (unsigned) index; i++) - { - // If y is unfixed, and it's not anded with zero. - if (!y.isFixed(i) && !(x.isFixed(index - i) && !x.getValue(index - - i))) - { - y.setFixed(i, true); - y.setValue(i, true); - result = CHANGED; - } - - if (!x.isFixed(index - i) && !(y.isFixed(i) && !y.getValue(i))) - { - x.setFixed(index - i, true); - x.setValue(index - i, true); - result = CHANGED; - } - } - } - - // We have all the ones that we need already. (thanks). Set everything we can to zero. - if (aspirationalSum == columnOnes && (columnUnfixed > 0 || columnOneFixed - > 0)) - { - for (unsigned i = 0; i <= (unsigned) index; i++) - { - if (!y.isFixed(i) && x.isFixed(index - i) && x.getValue(index - i)) // one fixed. - - { - y.setFixed(i, true); - y.setValue(i, false); - //columnZeroes++; - //columnOneFixed--; - result = CHANGED; - } - - if (!x.isFixed(index - i) && y.isFixed(i) && y.getValue(i)) // one fixed other way. - { - x.setFixed(index - i, true); - x.setValue(index - i, false); - //columnZeroes++; - //columnOneFixed--; - result = CHANGED; - } - } - } - if (debug_multiply && result == CONFLICT) - log << "CONFLICT" << endl; - - return result; -} + ColumnStats cs(x, y, index); + + int columnUnfixed = cs.columnUnfixed; // both unfixed. + int columnOneFixed = cs.columnOneFixed; // one of the values is fixed to one. + int columnOnes = cs.columnOnes; // both are ones. + //int columnZeroes = cs.columnZeroes; // either are zero. + + Result result = NO_CHANGE; + + // We need every value that is unfixed to be set to one. + if (aspirationalSum == columnOnes + columnOneFixed + columnUnfixed && ((columnOneFixed + columnUnfixed) > 0)) + { + for (unsigned i = 0; i <= (unsigned) index; i++) + { + // If y is unfixed, and it's not anded with zero. + if (!y.isFixed(i) && !(x.isFixed(index - i) && !x.getValue(index - i))) + { + y.setFixed(i, true); + y.setValue(i, true); + result = CHANGED; + } + + if (!x.isFixed(index - i) && !(y.isFixed(i) && !y.getValue(i))) + { + x.setFixed(index - i, true); + x.setValue(index - i, true); + result = CHANGED; + } + } + } + + // We have all the ones that we need already. (thanks). Set everything we can to zero. + if (aspirationalSum == columnOnes && (columnUnfixed > 0 || columnOneFixed > 0)) + { + for (unsigned i = 0; i <= (unsigned) index; i++) + { + if (!y.isFixed(i) && x.isFixed(index - i) && x.getValue(index - i)) // one fixed. + + { + y.setFixed(i, true); + y.setValue(i, false); + //columnZeroes++; + //columnOneFixed--; + result = CHANGED; + } + + if (!x.isFixed(index - i) && y.isFixed(i) && y.getValue(i)) // one fixed other way. + { + x.setFixed(index - i, true); + x.setValue(index - i, false); + //columnZeroes++; + //columnOneFixed--; + result = CHANGED; + } + } + } + if (debug_multiply && result == CONFLICT) + log << "CONFLICT" << endl; + + return result; + } // Uses the zeroes / ones present adjust the column counts. -Result adjustColumns(const FixedBits& x, const FixedBits& y, int* columnL, - int * columnH) -{ - const unsigned bitWidth = x.getWidth(); - - bool yFixedFalse[bitWidth]; - bool xFixedFalse[bitWidth]; - - for (unsigned i = 0; i < bitWidth; i++) - { - yFixedFalse[i] = y.isFixed(i) && !y.getValue(i); - xFixedFalse[i] = x.isFixed(i) && !x.getValue(i); - } - - for (unsigned i = 0; i < bitWidth; i++) - { - // decrease using zeroes. - if (yFixedFalse[i]) - { - for (unsigned j = i; j < bitWidth; j++) - { - columnH[j]--; - } - } - - if (xFixedFalse[i]) - { - for (unsigned j = i; j < bitWidth; j++) - { - // if the row hasn't already been zeroed out. - if (!yFixedFalse[j - i]) - columnH[j]--; - } - } - - // check if there are any pairs of ones. - if (x.isFixed(i) && x.getValue(i)) - for (unsigned j = 0; j < (bitWidth - i); j++) - { - assert(i + j < bitWidth); - if (y.isFixed(j) && y.getValue(j)) - { - // a pair of ones. Increase the lower bound. - columnL[i + j]++; - } - } - } - return NO_CHANGE; -} + Result + adjustColumns(const FixedBits& x, const FixedBits& y, int* columnL, int * columnH) + { + const unsigned bitWidth = x.getWidth(); -Result -setToZero(FixedBits& y, int from, int to) -{ - Result r = NO_CHANGE; - assert(from<=to); - assert(from>= 0); - assert(to <= y.getWidth()); + bool yFixedFalse[bitWidth]; + bool xFixedFalse[bitWidth]; + + for (unsigned i = 0; i < bitWidth; i++) + { + yFixedFalse[i] = y.isFixed(i) && !y.getValue(i); + xFixedFalse[i] = x.isFixed(i) && !x.getValue(i); + } - /***NB < to ***/ - for (int i=from; i < to; i++) + for (unsigned i = 0; i < bitWidth; i++) + { + // decrease using zeroes. + if (yFixedFalse[i]) + { + for (unsigned j = i; j < bitWidth; j++) + { + columnH[j]--; + } + } + + if (xFixedFalse[i]) + { + for (unsigned j = i; j < bitWidth; j++) + { + // if the row hasn't already been zeroed out. + if (!yFixedFalse[j - i]) + columnH[j]--; + } + } + + // check if there are any pairs of ones. + if (x.isFixed(i) && x.getValue(i)) + for (unsigned j = 0; j < (bitWidth - i); j++) + { + assert(i + j < bitWidth); + if (y.isFixed(j) && y.getValue(j)) + { + // a pair of ones. Increase the lower bound. + columnL[i + j]++; + } + } + } + return NO_CHANGE; + } + + Result + setToZero(FixedBits& y, int from, int to) { - if (y[i] == '*') + Result r = NO_CHANGE; + assert(from<=to); + assert(from>= 0); + assert(to <= y.getWidth()); + + /***NB < to ***/ + for (int i = from; i < to; i++) { - y.setFixed(i, true); - y.setValue(i, false); - r = CHANGED; + if (y[i] == '*') + { + y.setFixed(i, true); + y.setValue(i, false); + r = CHANGED; + } + else if (y[i] == '1') + return CONFLICT; } - else if (y[i] == '1') - return CONFLICT; + return r; } - return r; -} // Finds the leading one in each of the two inputs. // If this position is i & j, then in the output // there can be no ones higher than i+j+1. -Result useLeadingZeroesToFix_OLD(FixedBits& x, FixedBits&y, FixedBits& output) -{ - // Count the leading zeroes on x & y. - // Output should have about that many.. - int xTop = x.topmostPossibleLeadingOne(); - int yTop = y.topmostPossibleLeadingOne(); - - int maxOutputOneFromInputs = xTop + yTop + 1; - - for (int i = output.getWidth() - 1; i > maxOutputOneFromInputs; i--) - if (!output.isFixed(i)) - { - output.setFixed(i, true); - output.setValue(i, false); - } - else - { - if (output.getValue(i)) - return CONFLICT; - } - - return NOT_IMPLEMENTED; -} + Result + useLeadingZeroesToFix_OLD(FixedBits& x, FixedBits&y, FixedBits& output) + { + // Count the leading zeroes on x & y. + // Output should have about that many.. + int xTop = x.topmostPossibleLeadingOne(); + int yTop = y.topmostPossibleLeadingOne(); + + int maxOutputOneFromInputs = xTop + yTop + 1; + + for (int i = output.getWidth() - 1; i > maxOutputOneFromInputs; i--) + if (!output.isFixed(i)) + { + output.setFixed(i, true); + output.setValue(i, false); + } + else + { + if (output.getValue(i)) + return CONFLICT; + } + + return NOT_IMPLEMENTED; + } Result useLeadingZeroesToFix(FixedBits& x, FixedBits&y, FixedBits& output) { // To check that the new implementation subsumes the old. - #ifndef NDEBUG +#ifndef NDEBUG FixedBits x_p = x; FixedBits y_p = y; FixedBits o_p = output; useLeadingZeroesToFix_OLD(x_p, y_p, o_p); - #endif +#endif const int bitWidth = x.getWidth(); - CBV x_c = CONSTANTBV::BitVector_Create(2*bitWidth, true); - CBV y_c = CONSTANTBV::BitVector_Create(2*bitWidth, true); + CBV x_c = CONSTANTBV::BitVector_Create(2 * bitWidth, true); + CBV y_c = CONSTANTBV::BitVector_Create(2 * bitWidth, true); for (int i = 0; i < bitWidth; i++) { - if (x[i] == '1' || x[i] == '*') - CONSTANTBV::BitVector_Bit_On(x_c, i); + if (x[i] == '1' || x[i] == '*') + CONSTANTBV::BitVector_Bit_On(x_c, i); - if (y[i] == '1' || y[i] == '*') - CONSTANTBV::BitVector_Bit_On(y_c, i); + if (y[i] == '1' || y[i] == '*') + CONSTANTBV::BitVector_Bit_On(y_c, i); } - BEEV::CBV result = CONSTANTBV::BitVector_Create(2 * bitWidth+1, true); + BEEV::CBV result = CONSTANTBV::BitVector_Create(2 * bitWidth + 1, true); CONSTANTBV::ErrCode ec = CONSTANTBV::BitVector_Multiply(result, x_c, y_c); - assert (ec == CONSTANTBV::ErrCode_Ok); + assert(ec == CONSTANTBV::ErrCode_Ok); - for (int j = (2 * bitWidth) - 1; j >= 0; j--) - { + for (int j = (2 * bitWidth) - 1; j >= 0; j--) + { if (CONSTANTBV::BitVector_bit_test(result, j)) break; if (j < bitWidth) { - if (!output.isFixed(j)) - { - output.setFixed(j, true); - output.setValue(j, false); - } - else - { - if (output.getValue(j)) - return CONFLICT; - } + if (!output.isFixed(j)) + { + output.setFixed(j, true); + output.setValue(j, false); + } + else + { + if (output.getValue(j)) + return CONFLICT; + } } - } + } #ifndef NDEBUG - // Assert the new implementation fixes more than the old. - assert(FixedBits::in(x,x_p )); - assert(FixedBits::in(y,y_p )); - assert(FixedBits::in(output, o_p)); + // Assert the new implementation fixes more than the old. + assert(FixedBits::in(x,x_p )); + assert(FixedBits::in(y,y_p )); + assert(FixedBits::in(output, o_p)); #endif - CONSTANTBV::BitVector_Destroy(x_c); - CONSTANTBV::BitVector_Destroy(y_c); - CONSTANTBV::BitVector_Destroy(result); + CONSTANTBV::BitVector_Destroy(x_c); + CONSTANTBV::BitVector_Destroy(y_c); + CONSTANTBV::BitVector_Destroy(result); return NOT_IMPLEMENTED; } // Remove from x any trailing "boths", that don't have support in y and output. -Result -trailingOneReasoning(FixedBits& x, FixedBits&y, FixedBits& output) -{ - Result r = NO_CHANGE; + Result + trailingOneReasoning(FixedBits& x, FixedBits&y, FixedBits& output) + { + Result r = NO_CHANGE; - const int bitwidth = output.getWidth(); + const int bitwidth = output.getWidth(); - const int x_min = x.minimum_trailingOne(); - const int x_max = x.maximum_trailingOne(); + const int x_min = x.minimum_trailingOne(); + const int x_max = x.maximum_trailingOne(); - const int y_min = y.minimum_trailingOne(); - const int y_max = y.maximum_trailingOne(); + const int y_min = y.minimum_trailingOne(); + const int y_max = y.maximum_trailingOne(); - int output_max = output.maximum_trailingOne(); + int output_max = output.maximum_trailingOne(); - bool done=false; - for (int i =x_min; i <=std::min(x_max,bitwidth-1);i++) - { - if (x[i] == '1') - break; + bool done = false; + for (int i = x_min; i <= std::min(x_max, bitwidth - 1); i++) + { + if (x[i] == '1') + break; - if (x[i] == '0') - continue; + if (x[i] == '0') + continue; - assert (!done); - for (int j =y_min; j <= std::min(y_max,output_max);j++) - { - if (j+i >= bitwidth || (y[j] != '0' && output[i+j] != '0')) + assert(!done); + for (int j = y_min; j <= std::min(y_max, output_max); j++) + { + if (j + i >= bitwidth || (y[j] != '0' && output[i + j] != '0')) + { + done = true; + break; + } + } + if (!done) { - done=true; - break; + x.setFixed(i, true); + x.setValue(i, false); + r = CHANGED; } + else + break; } - if (!done) + return r; + } + +// if x has n trailing zeroes, and y has m trailing zeroes, then the output has n+m trailing zeroes. +// if the output has n trailing zeroes and x has p trailing zeroes, then y has n-p trailing zeroes. + Result + useTrailingZeroesToFix(FixedBits& x, FixedBits&y, FixedBits& output) + { + const int bitwidth = output.getWidth(); + + Result r0 = trailingOneReasoning(x, y, output); + Result r1 = trailingOneReasoning(y, x, output); + + //Calculate the minimum number of trailing zeroes in the operands, + //the result has a >= number. + int min = x.minimum_numberOfTrailingZeroes() + y.minimum_numberOfTrailingZeroes(); + min = std::min(min, bitwidth); + + Result r2 = setToZero(output, 0, min); + if (r2 == CONFLICT) + return CONFLICT; + + if (r0 == CHANGED || r1 == CHANGED || r2 == CHANGED) + return CHANGED; + + return NO_CHANGE; + } + + Result + useInversesToSolve(FixedBits& x, FixedBits&y, FixedBits& output, BEEV::STPMgr* bm) + { + // Position of the first unfixed value +1. + int xBottom = x.leastUnfixed(); + int yBottom = y.leastUnfixed(); + int outputBottom = output.leastUnfixed(); + + int invertCount = std::min(std::max(xBottom, yBottom), outputBottom); + + if (invertCount == 0) + return NO_CHANGE; + + FixedBits* toInvert; + FixedBits* toSet; + + if (xBottom > yBottom) { - x.setFixed(i, true); - x.setValue(i, false); - r = CHANGED; + toInvert = &x; + toSet = &y; } else - break; - } - return r; -} + { + toInvert = &y; + toSet = &x; + } + invertCount--; // position of the least fixed. -// if x has n trailing zeroes, and y has m trailing zeroes, then the output has n+m trailing zeroes. -// if the output has n trailing zeroes and x has p trailing zeroes, then y has n-p trailing zeroes. - Result - useTrailingZeroesToFix(FixedBits& x, FixedBits&y, FixedBits& output) - { - const int bitwidth = output.getWidth(); + const unsigned int width = invertCount + 1; + BEEV::CBV toInvertCBV = toInvert->GetBVConst(invertCount, 0); - Result r0 = trailingOneReasoning(x,y,output); - Result r1 = trailingOneReasoning(y,x,output); + //cerr << "value to invert:" << *toInvertCBV << " "; - //Calculate the minimum number of trailing zeroes in the operands, - //the result has a >= number. - int min = x.minimum_numberOfTrailingZeroes() + y.minimum_numberOfTrailingZeroes(); - min = std::min(min, bitwidth); + Result status = NOT_IMPLEMENTED; - Result r2 = setToZero(output,0,min); - if (r2 == CONFLICT) - return CONFLICT; + if (CONSTANTBV::BitVector_bit_test(toInvertCBV, 0)) + { - if (r0 == CHANGED || r1 == CHANGED || r2 == CHANGED) - return CHANGED; + if (debug_multiply) + cerr << "Value to Invert:" << *toInvertCBV << endl; - return NO_CHANGE; - } + BEEV::Simplifier simplifier(bm); + BEEV::CBV inverse = simplifier.MultiplicativeInverse(bm->CreateBVConst(toInvertCBV, width)).GetBVConst(); + BEEV::CBV toMultiplyBy = output.GetBVConst(invertCount, 0); -Result useInversesToSolve(FixedBits& x, FixedBits&y, FixedBits& output, - BEEV::STPMgr* bm) -{ - // Position of the first unfixed value +1. - int xBottom = x.leastUnfixed(); - int yBottom = y.leastUnfixed(); - int outputBottom = output.leastUnfixed(); - - int invertCount = std::min(std::max(xBottom, yBottom), outputBottom); - - if (invertCount == 0) - return NO_CHANGE; - - FixedBits* toInvert; - FixedBits* toSet; - - if (xBottom > yBottom) - { - toInvert = &x; - toSet = &y; - } - else - { - toInvert = &y; - toSet = &x; - } - - invertCount--; // position of the least fixed. - - - const unsigned int width = invertCount + 1; - BEEV::CBV toInvertCBV = toInvert->GetBVConst(invertCount, 0); - - //cerr << "value to invert:" << *toInvertCBV << " "; - - Result status = NOT_IMPLEMENTED; - - if (CONSTANTBV::BitVector_bit_test(toInvertCBV, 0)) - { - - if (debug_multiply) - cerr << "Value to Invert:" << *toInvertCBV << endl; - - BEEV::Simplifier simplifier(bm); - BEEV::CBV inverse = simplifier.MultiplicativeInverse(bm->CreateBVConst( - toInvertCBV, width)).GetBVConst(); - BEEV::CBV toMultiplyBy = output.GetBVConst(invertCount, 0); - - BEEV::CBV toSetEqualTo = - CONSTANTBV::BitVector_Create(2 * (width), true); - - CONSTANTBV::ErrCode ec = CONSTANTBV::BitVector_Multiply(toSetEqualTo, - inverse, toMultiplyBy); - if (ec != CONSTANTBV::ErrCode_Ok) - { - assert(false); - throw 2314231; - } - - if (false && debug_multiply) - { - cerr << x << "*" << y << "=" << output << endl; - cerr << "Invert bit count" << invertCount << endl; - cerr << "To set" << *toSet; - cerr << "To set equal to:" << *toSetEqualTo << endl; - } - - // Write in the value. - for (int i = 0; i <= invertCount; i++) - { - bool expected = CONSTANTBV::BitVector_bit_test(toSetEqualTo, i); - - if (toSet->isFixed(i) && (toSet->getValue(i) ^ expected)) - { - status = CONFLICT; - } - else if (!toSet->isFixed(i)) - { - toSet->setFixed(i, true); - toSet->setValue(i, expected); - } - } - - // Don't delete the "inverse" because it's reference counted by the ASTNode. - - CONSTANTBV::BitVector_Destroy(toSetEqualTo); - CONSTANTBV::BitVector_Destroy(toMultiplyBy); - - //cerr << "result" << *toSet; - } - else - CONSTANTBV::BitVector_Destroy(toInvertCBV); - - //cerr << endl; - return status; -} + BEEV::CBV toSetEqualTo = CONSTANTBV::BitVector_Create(2 * (width), true); + + CONSTANTBV::ErrCode ec = CONSTANTBV::BitVector_Multiply(toSetEqualTo, inverse, toMultiplyBy); + if (ec != CONSTANTBV::ErrCode_Ok) + { + assert(false); + throw 2314231; + } + + if (false && debug_multiply) + { + cerr << x << "*" << y << "=" << output << endl; + cerr << "Invert bit count" << invertCount << endl; + cerr << "To set" << *toSet; + cerr << "To set equal to:" << *toSetEqualTo << endl; + } + + // Write in the value. + for (int i = 0; i <= invertCount; i++) + { + bool expected = CONSTANTBV::BitVector_bit_test(toSetEqualTo, i); + + if (toSet->isFixed(i) && (toSet->getValue(i) ^ expected)) + { + status = CONFLICT; + } + else if (!toSet->isFixed(i)) + { + toSet->setFixed(i, true); + toSet->setValue(i, expected); + } + } + + // Don't delete the "inverse" because it's reference counted by the ASTNode. + + CONSTANTBV::BitVector_Destroy(toSetEqualTo); + CONSTANTBV::BitVector_Destroy(toMultiplyBy); + + //cerr << "result" << *toSet; + } + else + CONSTANTBV::BitVector_Destroy(toInvertCBV); + + //cerr << endl; + return status; + } // Use trailing fixed to fix. // Create two constants and multiply them out fixing the result. -Result useTrailingFixedToFix(FixedBits& x, FixedBits&y, FixedBits& output) -{ - int xBottom = x.leastUnfixed(); - int yBottom = y.leastUnfixed(); - - int minV = std::min(xBottom, yBottom); - - if (minV == 0) - return NO_CHANGE; // nothing determined. - - // It gives the position of the first non-fixed. We want the last fixed. - minV--; - - // The multiply doesn't like to overflow. So we widen the output. - BEEV::CBV xCBV = x.GetBVConst(minV, 0); - BEEV::CBV yCBV = y.GetBVConst(minV, 0); - BEEV::CBV result = CONSTANTBV::BitVector_Create(2 * (minV + 1), true); - - CONSTANTBV::ErrCode ec = CONSTANTBV::BitVector_Multiply(result, xCBV, yCBV); - if (ec != CONSTANTBV::ErrCode_Ok) - { - assert(false); - throw 2314231; - } - - Result status = NOT_IMPLEMENTED; - for (int i = 0; i <= minV; i++) - { - bool expected = CONSTANTBV::BitVector_bit_test(result, i); - - if (output.isFixed(i) && (output.getValue(i) ^ expected)) - status = CONFLICT; - else if (!output.isFixed(i)) - { - output.setFixed(i, true); - output.setValue(i, expected); - } - } - - CONSTANTBV::BitVector_Destroy(xCBV); - CONSTANTBV::BitVector_Destroy(yCBV); - CONSTANTBV::BitVector_Destroy(result); - - return status; -} + Result + useTrailingFixedToFix(FixedBits& x, FixedBits&y, FixedBits& output) + { + int xBottom = x.leastUnfixed(); + int yBottom = y.leastUnfixed(); -void printColumns(signed *sumL, signed * sumH, int bitWidth) -{ - for (int i = 0; i < bitWidth; i++) - { - log << sumL[bitWidth - 1 - i] << " "; - } - log << endl; - for (int i = 0; i < bitWidth; i++) - { - log << sumH[bitWidth - 1 - i] << " "; - } - log << endl; -} + int minV = std::min(xBottom, yBottom); + if (minV == 0) + return NO_CHANGE; // nothing determined. + // It gives the position of the first non-fixed. We want the last fixed. + minV--; -Result bvMultiplyBothWays(vector& children, FixedBits& output, - BEEV::STPMgr* bm, MultiplicationStats* ms) -{ - FixedBits & x = *children[0]; - FixedBits & y = *children[1]; - - assert(x.getWidth() == y.getWidth()); - assert(x.getWidth() == output.getWidth()); - - const unsigned bitWidth = x.getWidth(); - - if (debug_multiply) - cerr << "======================" << endl; - - if (debug_multiply) - { - cerr << "Initial Fixing"; - cerr << x << "*"; - cerr << y << "="; - cerr << output << endl; - } - - Result r = useTrailingZeroesToFix(x, y, output); - if (CONFLICT == r) - return r; - - bool changed = true; - while (changed) - { - changed = false; - signed columnH[bitWidth]; // maximum number of true partial products. - signed columnL[bitWidth]; // minimum "" "" - signed sumH[bitWidth]; - signed sumL[bitWidth]; - - ColumnCounts cc(columnH, columnL, sumH, sumL, bitWidth); - - // Use the number of zeroes and ones in a column to update the possible counts. - adjustColumns(x, y, columnL, columnH); - - cc.rebuildSums(); - Result r = cc.fixedPoint(output); - - assert(cc.fixedPoint(output) != CHANGED); // idempotent - - if (r == CONFLICT) - return CONFLICT; - - r = NO_CHANGE; - - // If any of the sums have a cardinality of 1. Set the result. - for (unsigned column = 0; column < bitWidth; column++) - { - if (cc.sumL[column] == cc.sumH[column]) - { - //(1) If the output has a known value. Set the output. - bool newValue = !(sumH[column] % 2 == 0); - if (!output.isFixed(column)) - { - output.setFixed(column, true); - output.setValue(column, newValue); - r = CHANGED; - } - else if (output.getValue(column) != newValue) - return CONFLICT; - } - } - - if (CHANGED == r) - changed = true; - - for (unsigned column = 0; column < bitWidth; column++) - { - if (cc.columnL[column] == cc.columnH[column]) - { - //(2) Knowledge of the sum may fix the operands. - Result tempResult = fixIfCanForMultiplication(children, column, - cc.columnH[column]); - - if (CONFLICT == tempResult) - return CONFLICT; - - if (CHANGED == tempResult) - r = CHANGED; - } - } - - if (debug_multiply) - { - cerr << "At end"; - cerr << "x:" << x << endl; - cerr << "y:" << y << endl; - cerr << "output:" << output << endl; - } - - assert(CONFLICT != r); - - if (CHANGED == r) - changed = true; - - if (ms != NULL) - { - *ms = MultiplicationStats(bitWidth, cc.columnL, cc.columnH, - cc.sumL, cc.sumH); - ms->x = *children[0]; - ms->y = *children[1]; - ms->r = output; - } - - if (changed) - { - useTrailingZeroesToFix(x, y, output); - // if (r == NO_CHANGE) - // changed= false; - } - } - - if (children[0]->isTotallyFixed() && children[1]->isTotallyFixed()) - { - assert(output.isTotallyFixed()); - } + // The multiply doesn't like to overflow. So we widen the output. + BEEV::CBV xCBV = x.GetBVConst(minV, 0); + BEEV::CBV yCBV = y.GetBVConst(minV, 0); + BEEV::CBV result = CONSTANTBV::BitVector_Create(2 * (minV + 1), true); + + CONSTANTBV::ErrCode ec = CONSTANTBV::BitVector_Multiply(result, xCBV, yCBV); + if (ec != CONSTANTBV::ErrCode_Ok) + { + assert(false); + throw 2314231; + } + + Result status = NOT_IMPLEMENTED; + for (int i = 0; i <= minV; i++) + { + bool expected = CONSTANTBV::BitVector_bit_test(result, i); + + if (output.isFixed(i) && (output.getValue(i) ^ expected)) + status = CONFLICT; + else if (!output.isFixed(i)) + { + output.setFixed(i, true); + output.setValue(i, expected); + } + } + + CONSTANTBV::BitVector_Destroy(xCBV); + CONSTANTBV::BitVector_Destroy(yCBV); + CONSTANTBV::BitVector_Destroy(result); + + return status; + } + + void + printColumns(signed *sumL, signed * sumH, int bitWidth) + { + for (int i = 0; i < bitWidth; i++) + { + log << sumL[bitWidth - 1 - i] << " "; + } + log << endl; + for (int i = 0; i < bitWidth; i++) + { + log << sumH[bitWidth - 1 - i] << " "; + } + log << endl; + } + + Result + bvMultiplyBothWays(vector& children, FixedBits& output, BEEV::STPMgr* bm, MultiplicationStats* ms) + { + FixedBits & x = *children[0]; + FixedBits & y = *children[1]; + + assert(x.getWidth() == y.getWidth()); + assert(x.getWidth() == output.getWidth()); + + const unsigned bitWidth = x.getWidth(); + + if (debug_multiply) + cerr << "======================" << endl; + + if (debug_multiply) + { + cerr << "Initial Fixing"; + cerr << x << "*"; + cerr << y << "="; + cerr << output << endl; + } + + Result r = useTrailingZeroesToFix(x, y, output); + if (CONFLICT == r) + return r; + + bool changed = true; + while (changed) + { + changed = false; + signed columnH[bitWidth]; // maximum number of true partial products. + signed columnL[bitWidth]; // minimum "" "" + signed sumH[bitWidth]; + signed sumL[bitWidth]; + + ColumnCounts cc(columnH, columnL, sumH, sumL, bitWidth); + + // Use the number of zeroes and ones in a column to update the possible counts. + adjustColumns(x, y, columnL, columnH); + + cc.rebuildSums(); + Result r = cc.fixedPoint(output); + + assert(cc.fixedPoint(output) != CHANGED); + // idempotent + + if (r == CONFLICT) + return CONFLICT; + + r = NO_CHANGE; + + // If any of the sums have a cardinality of 1. Set the result. + for (unsigned column = 0; column < bitWidth; column++) + { + if (cc.sumL[column] == cc.sumH[column]) + { + //(1) If the output has a known value. Set the output. + bool newValue = !(sumH[column] % 2 == 0); + if (!output.isFixed(column)) + { + output.setFixed(column, true); + output.setValue(column, newValue); + r = CHANGED; + } + else if (output.getValue(column) != newValue) + return CONFLICT; + } + } + + if (CHANGED == r) + changed = true; + + for (unsigned column = 0; column < bitWidth; column++) + { + if (cc.columnL[column] == cc.columnH[column]) + { + //(2) Knowledge of the sum may fix the operands. + Result tempResult = fixIfCanForMultiplication(children, column, cc.columnH[column]); + + if (CONFLICT == tempResult) + return CONFLICT; + + if (CHANGED == tempResult) + r = CHANGED; + } + } + + if (debug_multiply) + { + cerr << "At end"; + cerr << "x:" << x << endl; + cerr << "y:" << y << endl; + cerr << "output:" << output << endl; + } + + assert(CONFLICT != r); + + if (CHANGED == r) + changed = true; + + if (ms != NULL) + { + *ms = MultiplicationStats(bitWidth, cc.columnL, cc.columnH, cc.sumL, cc.sumH); + ms->x = *children[0]; + ms->y = *children[1]; + ms->r = output; + } + + if (changed) + { + useTrailingZeroesToFix(x, y, output); + // if (r == NO_CHANGE) + // changed= false; + } + } + + if (children[0]->isTotallyFixed() && children[1]->isTotallyFixed()) + { + assert(output.isTotallyFixed()); + } // The below assertions are for performance only. It's not maximally precise anyway!!! #ifndef NDEBUG - if (r != CONFLICT) - { - FixedBits x_c(x), y_c(y), o_c(output); - - // These are subsumed by the consistency over the columns.. - useTrailingFixedToFix(x_c, y_c, o_c); - useLeadingZeroesToFix(x_c, y_c, o_c); - useInversesToSolve(x_c, y_c, o_c, bm); - - // This one should have been called to fixed point! - useTrailingZeroesToFix(x_c, y_c, o_c); - - if(!FixedBits::equals(x_c , x) || - !FixedBits::equals(y_c , y) || - !FixedBits::equals(o_c , output)) - { - cerr << x << y << output << endl; - cerr << x_c << y_c << o_c << endl; - assert(false); - } - } + if (r != CONFLICT) + { + FixedBits x_c(x), y_c(y), o_c(output); + + // These are subsumed by the consistency over the columns.. + useTrailingFixedToFix(x_c, y_c, o_c); + useLeadingZeroesToFix(x_c, y_c, o_c); + useInversesToSolve(x_c, y_c, o_c, bm); + + // This one should have been called to fixed point! + useTrailingZeroesToFix(x_c, y_c, o_c); + + if (!FixedBits::equals(x_c, x) || !FixedBits::equals(y_c, y) || !FixedBits::equals(o_c, output)) + { + cerr << x << y << output << endl; + cerr << x_c << y_c << o_c << endl; + assert(false); + } + } #endif - return NOT_IMPLEMENTED; -} + return NOT_IMPLEMENTED; + } -} + } } -- 2.47.3