From 4dc7a965e70c8c7df61b8322907640e5cb26419f Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Mon, 2 Jan 2012 02:28:47 +0000 Subject: [PATCH] Improvement. Better constant bit propagation of multiplication and division. I wanted to clean this up before checkin, but I'm short on time. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1459 e59a4935-1847-0410-ae03-e826735625c1 --- .../constantBitP/ConstantBitP_Division.cpp | 1106 +++++++++++++++++ .../ConstantBitP_Multiplication.cpp | 593 +++++++++ .../constantBitP/ConstantBitPropagation.cpp | 9 +- src/simplifier/constantBitP/FixedBits.cpp | 7 +- 4 files changed, 1707 insertions(+), 8 deletions(-) create mode 100644 src/simplifier/constantBitP/ConstantBitP_Division.cpp create mode 100644 src/simplifier/constantBitP/ConstantBitP_Multiplication.cpp diff --git a/src/simplifier/constantBitP/ConstantBitP_Division.cpp b/src/simplifier/constantBitP/ConstantBitP_Division.cpp new file mode 100644 index 0000000..6f89f68 --- /dev/null +++ b/src/simplifier/constantBitP/ConstantBitP_Division.cpp @@ -0,0 +1,1106 @@ +#include "ConstantBitP_TransferFunctions.h" +#include "ConstantBitP_Utility.h" +#include +#include +#include "../../AST/AST.h" +#include "../../simplifier/simplifier.h" + +namespace simplifier { +namespace constantBitP { +using std::endl; +using std::pair; +using std::set; + +const bool debug_division = false; +extern std::ostream& log; + +using BEEV::STPMgr; + +enum WhatIsOutput { + REMAINDER_IS_OUTPUT, QUOTIENT_IS_OUTPUT +}; + +enum Operation { + SIGNED_DIVISION, SIGNED_REMAINDER, SIGNED_MODULUS +}; + +// For unsigned 3-bit exhaustive, there are 1119 differences for unsigned division. + + +// a/b and a%b. a=bq +r. Where b!=0 implies r= 0; i--) + { + if (CONSTANTBV::BitVector_bit_test(low, i)) + { + lowBits.setFixed(i, true); + lowBits.setValue(i, true); + } + else + { + lowBits.setFixed(i, true); + lowBits.setValue(i, false); + + } + } + return lowBits; + } + +Result merge(Result r1, Result r2) +{ + if (r1 == CONFLICT || r2 == CONFLICT ) + return CONFLICT; + + if (r1 == CHANGED || r2 == CHANGED) + return CHANGED; + + if (r1 == NO_CHANGE && r2 == NO_CHANGE) + return NO_CHANGE; + + return NOT_IMPLEMENTED; + +} + +// The value "b" is in the range [low,high] inclusive. +Result fix(FixedBits& b, BEEV::CBV low, BEEV::CBV high) +{ + FixedBits init =b; + const int width = b.getWidth(); + + FixedBits highBits = cbvToFixedBits(high,width); + FixedBits lowBits = cbvToFixedBits(low,width); + + vector c; + c.push_back(&b); + c.push_back(&highBits); + + + FixedBits t(1,true); + t.setFixed(0,true); + t.setValue(0,true); + Result result1 = bvLessThanEqualsBothWays(c,t); + + c.clear(); + c.push_back(&lowBits); + c.push_back(&b); + Result result2 = bvLessThanEqualsBothWays(c,t); + + Result result = merge(result1, result2); + if (result == CONFLICT) + return CONFLICT; + + for (int i = width - 1; i >= 0; i--) { + if ((CONSTANTBV::BitVector_bit_test(low, i) + == CONSTANTBV::BitVector_bit_test(high, i))) { + bool toFix = CONSTANTBV::BitVector_bit_test(low, i); + if (b.isFixed(i)) { + if (b.getValue(i) != toFix) { + return CONFLICT; + } + } else { + b.setFixed(i, true); + b.setValue(i, toFix); + } + } else + break; + } + + if (!FixedBits::equals(init, b)) + return CHANGED; + return NO_CHANGE; +} + +Result bvUnsignedQuotientAndRemainder2(vector& children, + FixedBits& output, STPMgr* bm, WhatIsOutput whatIs); + + +Result bvUnsignedQuotientAndRemainder(vector& children, + FixedBits& output, STPMgr* bm, WhatIsOutput whatIs) { + assert(output.getWidth() == children[0]->getWidth()); + assert(output.getWidth() == children[1]->getWidth()); + assert(children.size() == 2); + + if (whatIs != QUOTIENT_IS_OUTPUT) + { + return bvUnsignedQuotientAndRemainder2(children, output, bm, whatIs); + } + + FixedBits& a = *children[0]; + FixedBits& b = *children[1]; + + const unsigned width = a.getWidth(); + + assert(!b.containsZero()); + + BEEV::CBV minTop = CONSTANTBV::BitVector_Create(width, true); + BEEV::CBV maxTop = CONSTANTBV::BitVector_Create(width, true); + + setUnsignedMinMax(a, minTop, maxTop); + + BEEV::CBV minBottom = CONSTANTBV::BitVector_Create(width, true); + BEEV::CBV maxBottom = CONSTANTBV::BitVector_Create(width, true); + + setUnsignedMinMax(b, minBottom, maxBottom); + + BEEV::CBV minQuotient = CONSTANTBV::BitVector_Create(width, true); + BEEV::CBV maxQuotient = CONSTANTBV::BitVector_Create(width, true); + + BEEV::CBV minRemainder = CONSTANTBV::BitVector_Create(width, true); + BEEV::CBV maxRemainder = CONSTANTBV::BitVector_Create(width, true); + + if (whatIs == QUOTIENT_IS_OUTPUT) { + setUnsignedMinMax(output, minQuotient, maxQuotient); + + for (int i = 0; i < width; i++) + CONSTANTBV::BitVector_Bit_On(maxRemainder, i); + } + else + { + setUnsignedMinMax(output, minRemainder, maxRemainder); + + for (int i =0; i < width;i++) + CONSTANTBV::BitVector_Bit_On(maxQuotient,i); + } + + // need to clean up these at end. + BEEV::CBV one = CONSTANTBV::BitVector_Create(width, true); + CONSTANTBV::BitVector_increment(one); + // quotient and remainder. + BEEV::CBV q = CONSTANTBV::BitVector_Create(width, true); + BEEV::CBV r = CONSTANTBV::BitVector_Create(width, true); + // misc. + BEEV::CBV copy = CONSTANTBV::BitVector_Create(width, true); + BEEV::CBV copy2 = CONSTANTBV::BitVector_Create(width, true); + BEEV::CBV multR = CONSTANTBV::BitVector_Create(width, true); + + if (debug_division) { + log << "--" << endl; + log << "initial" << endl; + log << "a:[" << *minTop << "," << *maxTop << "]"; + log << " / b:[" << *minBottom << "," << *maxBottom << "] = "; + log << "[" << *minQuotient << "," << *maxQuotient << "]"; + log << " rem [" << *minRemainder << "," << *maxRemainder << "]"; + log << endl; + } + + // We loop. There are 6 cases. + + Result result = NO_CHANGE; + + // If a bit is changed, then we fixed point again. + bool bitEverChanged = false; + bool bitJustChanged = true; + while (bitJustChanged) { + bitJustChanged = false; + + bool changed = true; + + int iteration = 0; + while (changed) { + changed = false; + CONSTANTBV::ErrCode e; + + bool carry_1 = false; + CONSTANTBV::BitVector_sub(copy, minTop, minRemainder, &carry_1); + if (!carry_1) // Not sure if it goes negative. + { + e = CONSTANTBV::BitVector_Div_Pos(q, copy, maxBottom, r); + assert(e == CONSTANTBV::ErrCode_Ok); + + if (CONSTANTBV::BitVector_Lexicompare(minQuotient, q) < 0) { + if (debug_division) { + log << "1 minQ) " << *minTop; + log << " / " << *maxBottom; + log << " = " << *q; + log << " r " << *r << endl; + } + + // min quotient is bigger. Bring in. + CONSTANTBV::BitVector_Copy(minQuotient, q); + changed = true; + } + } + + CONSTANTBV::BitVector_Copy(copy, maxTop); + //bool carry_2 = false; + //CONSTANTBV::BitVector_sub(copy,maxTop,minRemainder,&carry_2); + //assert(!carry_1); // Not sure if it goes negative. + e = CONSTANTBV::BitVector_Div_Pos(q, copy, minBottom, r); + assert(e == CONSTANTBV::ErrCode_Ok); + + if (CONSTANTBV::BitVector_Lexicompare(maxQuotient, q) > 0) { + if (debug_division) { + log << "2 maxQ) " << *maxTop; + log << " / " << *minBottom; + log << " = " << *q; + log << " r " << *r << endl; + } + + CONSTANTBV::BitVector_Copy(maxQuotient, q); // copy the reduced value in. + changed = true; + } + + CONSTANTBV::BitVector_Copy(copy, maxQuotient); + e = CONSTANTBV::BitVector_Mul_Pos(multR, copy, maxBottom, true); + bool carry = false; + CONSTANTBV::BitVector_sub(copy, maxBottom, one, &carry); + CONSTANTBV::BitVector_add(copy2, multR, copy, &carry); + CONSTANTBV::BitVector_Copy(multR, copy2); + // involved. eek. + + + if (e == CONSTANTBV::ErrCode_Ok + && CONSTANTBV::BitVector_Lexicompare(maxTop, multR) > 0) { + if (debug_division) { + log << "3 maxT) " << *maxQuotient; + log << " * " << *maxBottom; + log << " = " << *multR << endl; + } + CONSTANTBV::BitVector_Copy(maxTop, multR); + changed = true; + } + + CONSTANTBV::BitVector_Copy(copy, minBottom); + + // If this is strict then it seems to be treated as signed, so it is considered to overflow + // if a bit moves into the top of multR. + e = CONSTANTBV::BitVector_Mul_Pos(multR, copy, minQuotient, false); + //cerr << e << endl; + + + if (e == CONSTANTBV::ErrCode_Ok && CONSTANTBV::BitVector_Lexicompare(minTop, multR) < 0) + { + if (debug_division) { + log << "4 minT) " << *minQuotient; + log << " * " << *minBottom; + log << " = " << *multR << endl; + } + CONSTANTBV::BitVector_Copy(minTop, multR); + changed = true; + } + + if (CONSTANTBV::BitVector_Lexicompare(minQuotient, one) >= 0) { + // not going to divide by zero. + + CONSTANTBV::BitVector_Copy(copy, maxTop); + e = CONSTANTBV::BitVector_Div_Pos(q, copy, minQuotient, r); + assert(e == CONSTANTBV::ErrCode_Ok); + + if (CONSTANTBV::BitVector_Lexicompare(maxBottom, q) > 0) { + if (debug_division) { + log << "5 maxB) " << *maxTop; + log << " / " << *minQuotient; + log << " = " << *q; + log << " r " << *r << endl; + } + + // min quotient is bigger. Bring in. + CONSTANTBV::BitVector_Copy(maxBottom, q); + changed = true; + } + } + + + // This rule increases the minimum of the bottom. + // let a be the min of the top, + // let q be the maximum of the quotient, + // let b be the min. of the bottom. + // then a= bq +r + // so a = bq + (b-1) // if the max. of r is one less than b. + // so (1+a) / (q+1) = b. + // We round the division up. + { + bool carry = false; + CONSTANTBV::BitVector_add(copy, minTop, one, &carry); + bool carry2 = false; + CONSTANTBV::BitVector_add(copy2, maxQuotient, one, &carry2); + if (!carry && !carry2) + { + e = CONSTANTBV::BitVector_Div_Pos(q, copy, copy2, r); + assert(e == CONSTANTBV::ErrCode_Ok); + if (CONSTANTBV::BitVector_Lexicompare(q, one) >= 0) + { + CONSTANTBV::BitVector_add(copy, q, one, &carry); + if (!carry && (CONSTANTBV::BitVector_Lexicompare(minBottom, q) < 0)) + { + + if (debug_division) + { + log << "6 min_3_B) "; + log << "minBottom" << *minBottom << " " ; + log << "q" << *q << endl; + } + + // min quotient is bigger. Bring in. + CONSTANTBV::BitVector_Copy(minBottom, q); + changed = true; + } + } + + + } + } + + // Don't know why we don't need to check the intervals on the others? + if (CONSTANTBV::BitVector_Lexicompare(minQuotient, maxQuotient) > 0) { + if (debug_division) { + log << "conflict" << endl; + log << "a:[" << *minTop << "," << *maxTop << "]"; + log << " / b:[" << *minBottom << "," << *maxBottom + << "] = "; + log << "[" << *minQuotient << "," << *maxQuotient << "]"; + log << endl; + } + + result = CONFLICT; + goto end; + } + + + if (debug_division) { + log << "intermediate" << endl; + log << "a:[" << *minTop << "," << *maxTop << "]"; + log << " / b:[" << *minBottom << "," << *maxBottom << "] = "; + log << "[" << *minQuotient << "," << *maxQuotient << "]"; + log << endl; + } + iteration++; + //if (iteration==2 && changed) + //exit(1); + } + + if (debug_division) { + log << "final" << endl; + log << "a:[" << *minTop << "," << *maxTop << "]"; + log << " / b:[" << *minBottom << "," << *maxBottom << "] = "; + log << "[" << *minQuotient << "," << *maxQuotient << "]"; + log << endl; + } + + { + Result r1 = fix(a, minTop, maxTop); + Result r2 = fix(b, minBottom, maxBottom); + Result r3; + if (whatIs == QUOTIENT_IS_OUTPUT) + r3 = fix(output, minQuotient, maxQuotient); + else + r3 = fix(output, minRemainder, maxRemainder); + + if (r1 == CONFLICT || r2 == CONFLICT || r3 == CONFLICT) + { + result = CONFLICT; + goto end; + } + assert(result != CONFLICT); + + if (r1 == CHANGED || r2 == CHANGED || r3 == CHANGED) + result = CHANGED; + } + + // check that fixing bits hasn't tightened intervals. If it has we need to resolve. + if (result == CHANGED) { + bool tightened = false; + + setUnsignedMinMax(output, copy, copy2); + + if (whatIs == QUOTIENT_IS_OUTPUT) + { + if (CONSTANTBV::BitVector_Lexicompare(minQuotient, copy) < 0 + || CONSTANTBV::BitVector_Lexicompare(maxQuotient, copy2) + > 0) + tightened = true; + } + else + { + if (CONSTANTBV::BitVector_Lexicompare(minRemainder, copy) < 0 + || CONSTANTBV::BitVector_Lexicompare(maxRemainder, copy2) + > 0) + tightened = true; + } + + setUnsignedMinMax(b, copy, copy2); + if (CONSTANTBV::BitVector_Lexicompare(minBottom, copy) < 0 + || CONSTANTBV::BitVector_Lexicompare(maxBottom, copy2) > 0) + tightened = true; + + setUnsignedMinMax(a, copy, copy2); + if (CONSTANTBV::BitVector_Lexicompare(minTop, copy) < 0 + || CONSTANTBV::BitVector_Lexicompare(maxTop, copy2) > 0) + tightened = true; + + if (tightened) { + setUnsignedMinMax(a, minTop, maxTop); + setUnsignedMinMax(b, minBottom, maxBottom); + if (whatIs == QUOTIENT_IS_OUTPUT) + setUnsignedMinMax(output, minQuotient, maxQuotient); + else + setUnsignedMinMax(output, minRemainder, maxRemainder); + + bitEverChanged = true; + bitJustChanged = true; + } + } + + } + + end: + // Destroy range variables. + CONSTANTBV::BitVector_Destroy(minTop); + CONSTANTBV::BitVector_Destroy(maxTop); + CONSTANTBV::BitVector_Destroy(minBottom); + CONSTANTBV::BitVector_Destroy(maxBottom); + CONSTANTBV::BitVector_Destroy(minQuotient); + CONSTANTBV::BitVector_Destroy(maxQuotient); + CONSTANTBV::BitVector_Destroy(minRemainder); + CONSTANTBV::BitVector_Destroy(maxRemainder); + + + // Destroy helpers. + CONSTANTBV::BitVector_Destroy(copy); + CONSTANTBV::BitVector_Destroy(copy2); + CONSTANTBV::BitVector_Destroy(multR); + CONSTANTBV::BitVector_Destroy(q); + CONSTANTBV::BitVector_Destroy(r); + CONSTANTBV::BitVector_Destroy(one); + + if (result == CONFLICT) + return CONFLICT; + + if (bitEverChanged) + return CHANGED; + return result; +} + +// (a/b) = q +// Solving: (a = q * b + r) AND (r < b). +Result bvUnsignedQuotientAndRemainder2(vector& children, + FixedBits& output, STPMgr* bm, WhatIsOutput whatIs) { + assert(output.getWidth() == children[0]->getWidth()); + assert(output.getWidth() == children[1]->getWidth()); + assert(children.size() == 2); + + unsigned int newWidth = 2 * output.getWidth(); + // Create Widenend copies. + FixedBits a(newWidth, false); + FixedBits b(newWidth, false); + + FixedBits q(newWidth, false); + FixedBits r(newWidth, false); + + // intermediate values. + FixedBits times(newWidth, false); + + a.copyIn(*children[0]); + b.copyIn(*children[1]); + + assert(!b.containsZero()); + + if (whatIs == QUOTIENT_IS_OUTPUT) + q.copyIn(output); + else if (whatIs == REMAINDER_IS_OUTPUT) + r.copyIn(output); + else + throw std::runtime_error("sdjjfas"); + + FixedBits aCopy(newWidth, false); + FixedBits bCopy(newWidth, false); + FixedBits rCopy(newWidth, false); + FixedBits qCopy(newWidth, false); + + // Times and plus must not overflow. + for (unsigned i = (unsigned) output.getWidth(); i < newWidth; i++) { + //No overflow. + times.setFixed(i, true); + times.setValue(i, false); + + // Everything is zero extended. + a.setFixed(i, true); + a.setValue(i, false); + b.setFixed(i, true); + b.setValue(i, false); + + //Multiplication must not overflow. + r.setFixed(i, true); + r.setValue(i, false); + q.setFixed(i, true); + q.setValue(i, false); + } + + // True bit. + FixedBits trueBit(1, true); + trueBit.setFixed(0, true); + trueBit.setValue(0, true); + + Result result = NO_CHANGE; + + vector addChildren; + addChildren.push_back(×); + addChildren.push_back(&r); + + vector multiplicationChildren; + multiplicationChildren.push_back(&q); + multiplicationChildren.push_back(&b); + + do { + aCopy = a; + bCopy = b; + rCopy = r; + qCopy = q; + + if (debug_division) { + log << "p1:" << a << "/" << b << "=" << q << "rem(" << r << ")" + << endl; + log << "times" << times << endl; + } + + result = bvLessThanBothWays(r, b, trueBit); // (r < b) + if (result == CONFLICT) + return CONFLICT; + + result = bvMultiplyBothWays(multiplicationChildren, times, bm); + if (result == CONFLICT) + return CONFLICT; + + result = bvAddBothWays(addChildren, a); + if (result == CONFLICT) + return CONFLICT; + } while (!(FixedBits::equals(aCopy, a) && FixedBits::equals(bCopy, b) + && FixedBits::equals(rCopy, r) && FixedBits::equals(qCopy, q))); + + bool conflict = false; + for (int i = 0; i < output.getWidth(); i++) { + if (whatIs == QUOTIENT_IS_OUTPUT) + conflict |= fix(output, q, i); + else if (whatIs == REMAINDER_IS_OUTPUT) + conflict |= fix(output, r, i); + else + throw std::runtime_error("sdjjfas"); + + conflict |= fix(*children[0], a, i); + conflict |= fix(*children[1], b, i); + } + + if (debug_division) + cerr << endl; + + if (conflict) + return CONFLICT; + + return NOT_IMPLEMENTED; +} + +Result bvUnsignedModulusBothWays(vector& children, + FixedBits& output, STPMgr* bm) { + + + + Result r1 = NO_CHANGE; + vector v; + v.push_back(&output); + v.push_back(children[0]); + FixedBits truN(1,true); + truN.setFixed(0,true); + truN.setValue(0,true); + r1= bvLessThanEqualsBothWays(v, truN); + + + if (children[1]->containsZero()) + return r1; + + if (debug_division) + log << *(children[0]) << "bvmod" << *(children[1]) << "=" + << output << endl; + + Result r = bvUnsignedQuotientAndRemainder(children, output, bm, + REMAINDER_IS_OUTPUT); + + // Doesn't even do constant propagation. + // <10>bvmod<11>=<--> + if (r != CONFLICT && children[0]->isTotallyFixed() + && children[1]->isTotallyFixed() && !output.isTotallyFixed()) { + + if (debug_division) + { + log << "Not even constant prop!" << *(children[0]) << "bvmod" + << *(children[1]) << "=" << output << endl; + } + + //assert(output.isTotallyFixed()); + } + + if (r == CONFLICT || r==CHANGED) + return r; + + return r1; +} + +Result bvUnsignedDivisionBothWays(vector& children, + FixedBits& output, STPMgr* bm) { + + if (children[1]->containsZero()) + return NO_CHANGE; + + Result r = bvUnsignedQuotientAndRemainder(children, output, bm, + QUOTIENT_IS_OUTPUT); + + // The current unsigned division doesn't even do constant propagation!!!!! + /* + if (r!= CONFLICT && children[0]->isTotallyFixed() && children[1]->isTotallyFixed()) + { + cerr << *children[0] << " / "; + cerr << *children[1]; + cerr << output << endl; + assert(output.isTotallyFixed()); + } + */ + + return r; +} + +bool canBe(const FixedBits& b, int index, bool value) { + if (!b.isFixed(index)) + return true; + else + return (!(b.getValue(index) ^ value)); +} + +// This provides a way to call the process function with fewer arguments. +struct Data { + FixedBits &tempA; + FixedBits &tempB; + FixedBits &tempOutput; + FixedBits &workingA; + FixedBits &workingB; + FixedBits &workingOutput; + unsigned int signBit; + + Data(FixedBits &_tempA, FixedBits &_tempB, FixedBits &_tempOutput, + FixedBits &_workingA, FixedBits &_workingB, + FixedBits &_workingOutput) : + tempA(_tempA), tempB(_tempB), tempOutput(_tempOutput), workingA( + _workingA), workingB(_workingB), workingOutput(_workingOutput) { + signBit = tempOutput.getWidth() - 1; + } + + void process(bool& first) { + if (first) { + workingA = tempA; + workingB = tempB; + workingOutput = tempOutput; + } else { + workingA = FixedBits::meet(workingA, tempA); + workingB = FixedBits::meet(workingB, tempB); + workingOutput = FixedBits::meet(workingOutput, tempOutput); + } + first = false; + } + + void set(const FixedBits& a, const FixedBits&b, const FixedBits& output, + bool aTop, bool bTop) { + tempA = a; + tempB = b; + tempOutput = output; + tempA.setFixed(signBit, true); + tempA.setValue(signBit, aTop); + + tempB.setFixed(signBit, true); + tempB.setValue(signBit, bTop); + } + + void print() { + cerr << "Working: "; + cerr << workingA << "/"; + cerr << workingB << "="; + cerr << workingOutput << endl; + + cerr << "Temps: "; + cerr << tempA << "/"; + cerr << tempB << "="; + cerr << tempOutput << endl; + } +}; + +Result negate(FixedBits& input, FixedBits& output) { + vector negChildren; + + negChildren.push_back(&input); + return bvUnaryMinusBothWays(negChildren, output); +} + +// This is preposterously complicated. We execute four cases then take the union of them. +// +Result bvSignedDivisionRemainderBothWays(vector& children, + FixedBits& output, STPMgr* bm, Result(*tf)(vector&, + FixedBits&, STPMgr* bm), const Operation op) { + assert(output.getWidth() == children[0]->getWidth()); + assert(output.getWidth() == children[1]->getWidth()); + assert(children.size() == 2); + + const FixedBits& a = *children[0]; + const FixedBits& b = *children[1]; + + assert(&a != &b); + + const unsigned int inputWidth = output.getWidth(); + const unsigned int signBit = output.getWidth() - 1; + + FixedBits workingA(inputWidth, false); + FixedBits workingB(inputWidth, false); + FixedBits workingOutput(inputWidth, false); + + FixedBits tempA = a; + FixedBits tempB = b; + FixedBits tempOutput = output; + + vector tempChildren; + tempChildren.push_back(&tempA); + tempChildren.push_back(&tempB); + Result r = NO_CHANGE; + + if (b.containsZero()) + return NO_CHANGE; + + Data data(tempA, tempB, tempOutput, workingA, workingB, workingOutput); + + while (true) + { + if (debug_division) + { + cerr << "start:"; + cerr << a << "/"; + cerr << b << "="; + cerr << output << endl; + } + + bool first = true; + + if (canBe(a, signBit, false) && canBe(b, signBit, false)) { + // (bvudiv s t) + r = NO_CHANGE; + data.set(a, b, output, false, false); + + r = tf(tempChildren, tempOutput, bm); + if (r != CONFLICT) { + if (debug_division) + cerr << "case A" << endl; + data.process(first); + } + } + + if (canBe(a, signBit, true) && canBe(b, signBit, false)) { + // (bvneg (bvudiv (bvneg a) b)) + r = NO_CHANGE; + data.set(a, b, output, true, false); + + FixedBits negA(inputWidth, false); + + vector negChildren; + negChildren.push_back(&negA); + r = bvUnaryMinusBothWays(negChildren, tempA); // get NegA + //cerr << negA << " " << tempA << endl; + assert(r != CONFLICT); + + //modulus: (bvadd (bvneg (bvurem (bvneg s) t)) t) + FixedBits wO(inputWidth, false); + if (op == SIGNED_MODULUS) { + vector ch; + ch.push_back(&wO); + ch.push_back(&tempB); + r = bvAddBothWays(ch, tempOutput); + assert(r != CONFLICT); + } else + wO = tempOutput; + + FixedBits negOutput(inputWidth, false); + negChildren.clear(); + negChildren.push_back(&negOutput); + r = bvUnaryMinusBothWays(negChildren, wO); + assert(r != CONFLICT); + + negChildren.clear(); + negChildren.push_back(&negA); + negChildren.push_back(&tempB); + + r = tf(negChildren, negOutput, bm); + if (r != CONFLICT) { + negChildren.clear(); + negChildren.push_back(&wO); + r = bvUnaryMinusBothWays(negChildren, negOutput); + + if (r != CONFLICT) { + if (op == SIGNED_MODULUS) { + vector ch; + ch.push_back(&wO); + ch.push_back(&tempB); + r = bvAddBothWays(ch, tempOutput); + } else + tempOutput = wO; + + if (r != CONFLICT) { + negChildren.clear(); + negChildren.push_back(&tempA); + //cerr << negA << " " << tempA << endl; + r = bvUnaryMinusBothWays(negChildren, negA); + //data.print(); + if (r != CONFLICT) { + + if (debug_division) + cerr << "case B" << endl; + + data.process(first); + + } + } + } + } + } + + if (canBe(a, signBit, false) && canBe(b, signBit, true)) { + // (bvneg (bvudiv a (bvneg b))) + r = NO_CHANGE; + data.set(a, b, output, false, true); + + FixedBits negB(inputWidth, false); + //FixedBits negA(inputWidth, false); + + vector negChildren; + negChildren.push_back(&negB); + r = bvUnaryMinusBothWays(negChildren, tempB); // get NegB + assert(r != CONFLICT); + + // Create a negated version of the output if necessary. Modulus and remainder aren't both negated. Division is. + FixedBits wO(inputWidth, false); + if (op == SIGNED_DIVISION) { + r = negate(tempOutput, wO); + assert(r != CONFLICT); + } else if (op == SIGNED_REMAINDER || op == SIGNED_MODULUS) + wO = tempOutput; + + // (bvadd (bvurem s (bvneg t)) t) + if (op == SIGNED_MODULUS) { + FixedBits wTemp(inputWidth, false); + vector ch; + ch.push_back(&wTemp); + ch.push_back(&tempB); + r = bvAddBothWays(ch, tempOutput); + assert(r != CONFLICT); + wO = wTemp; + } + + negChildren.clear(); + negChildren.push_back(&tempA); + negChildren.push_back(&negB); + + r = tf(negChildren, wO, bm); + if (r != CONFLICT) { + FixedBits t(wO.getWidth(), false); + if (op == SIGNED_MODULUS) { + vector ch; + ch.push_back(&wO); + ch.push_back(&tempB); + r = bvAddBothWays(ch, tempOutput); + t = tempOutput; + } else + t = wO; + + if (r != CONFLICT) { + if (op == SIGNED_DIVISION) { + r = negate(tempOutput, t); + } else if (op == SIGNED_REMAINDER || op == SIGNED_MODULUS) { + tempOutput = t; + } + + if (r != CONFLICT) { + negChildren.clear(); + negChildren.push_back(&tempB); + r = bvUnaryMinusBothWays(negChildren, negB); + if (r != CONFLICT) { + if (debug_division) + cerr << "case C" << endl; + + data.process(first); + } + } + } + } + } + + if (canBe(a, signBit, true) && canBe(b, signBit, true)) { + // (bvudiv (bvneg a) (bvneg b))))))) + r = NO_CHANGE; + data.set(a, b, output, true, true); + + FixedBits negA(inputWidth, false); + FixedBits negB(inputWidth, false); + + vector negChildren; + negChildren.push_back(&negA); + r = bvUnaryMinusBothWays(negChildren, tempA); // get NegA + assert(r != CONFLICT); + + negChildren.clear(); + negChildren.push_back(&negB); + r = bvUnaryMinusBothWays(negChildren, tempB); // get NegB + assert(r != CONFLICT); + + negChildren.clear(); + negChildren.push_back(&negA); + negChildren.push_back(&negB); + + FixedBits wO(inputWidth, false); + if (op == SIGNED_REMAINDER || op == SIGNED_MODULUS) { + r = negate(tempOutput, wO); + assert(r != CONFLICT); + } else if (op == SIGNED_DIVISION) + wO = tempOutput; + + r = tf(negChildren, wO, bm); + if (r != CONFLICT) { + negChildren.clear(); + negChildren.push_back(&tempB); + r = bvUnaryMinusBothWays(negChildren, negB); + + if (r != CONFLICT) { + negChildren.clear(); + negChildren.push_back(&tempA); + r = bvUnaryMinusBothWays(negChildren, negA); + //data.print(); + if (r != CONFLICT) { + if (op == SIGNED_REMAINDER || op == SIGNED_MODULUS) { + r = negate(tempOutput, wO); + } else if (op == SIGNED_DIVISION) + tempOutput = wO; + + if (r != CONFLICT) { + if (debug_division) + cerr << "case D" << endl; + + data.process(first); + } + } + } + } + + } + + if (first) + return CONFLICT; // All are conflicts. + + // The results be subsets of the originals. + assert(FixedBits::in(workingA, *children[0])); + assert(FixedBits::in(workingB, *children[1])); + assert(FixedBits::in(workingOutput, output)); + + if (FixedBits::equals(a, workingA) && FixedBits::equals(b, workingB) + && FixedBits::equals(output, workingOutput)) + break; + else + { + *children[0] = workingA; + *children[1] = workingB; + output = workingOutput; + } + } + + return NOT_IMPLEMENTED; +} + +Result bvSignedModulusBothWays(vector& children, FixedBits& output, + STPMgr* bm) { + /* + (bvsmod s t) abbreviates + (let (?msb_s (extract[|m-1|:|m-1|] s)) + (let (?msb_t (extract[|m-1|:|m-1|] t)) + (ite (and (= ?msb_s bit0) (= ?msb_t bit0)) + (bvurem s t) + (ite (and (= ?msb_s bit1) (= ?msb_t bit0)) + (bvadd (bvneg (bvurem (bvneg s) t)) t) + (ite (and (= ?msb_s bit0) (= ?msb_t bit1)) + (bvadd (bvurem s (bvneg t)) t) + (bvneg (bvurem (bvneg s) (bvneg t))))))) + */ + + if (children[0] == children[1]) // same pointer. + { + return NO_CHANGE; + } + + return bvSignedDivisionRemainderBothWays(children, output, bm, + bvUnsignedModulusBothWays, SIGNED_MODULUS); +} + +Result bvSignedRemainderBothWays(vector& children, + FixedBits& output, STPMgr* bm) { + /* + (bvsrem s t) abbreviates + (let (?msb_s (extract[|m-1|:|m-1|] s)) + (let (?msb_t (extract[|m-1|:|m-1|] t)) + (ite (and (= ?msb_s bit0) (= ?msb_t bit0)) + (bvurem s t) + (ite (and (= ?msb_s bit1) (= ?msb_t bit0)) + (bvneg (bvurem (bvneg s) t)) + (ite (and (= ?msb_s bit0) (= ?msb_t bit1)) + (bvurem s (bvneg t))) + (bvneg (bvurem (bvneg s) (bvneg t))))))) + */ + + + if (children[0] == children[1]) // same pointer. + { + return NO_CHANGE; + } + + + return bvSignedDivisionRemainderBothWays(children, output, bm, + bvUnsignedModulusBothWays, SIGNED_REMAINDER); +} + +Result bvSignedDivisionBothWays(vector& children, + FixedBits& output, STPMgr* bm) { + /* + * (bvsdiv s t) abbreviates + (let (?msb_s (extract[|m-1|:|m-1|] s)) + (let (?msb_t (extract[|m-1|:|m-1|] t)) + (ite (and (= ?msb_s bit0) (= ?msb_t bit0)) + (bvudiv s t) + (ite (and (= ?msb_s bit1) (= ?msb_t bit0)) + (bvneg (bvudiv (bvneg s) t)) + (ite (and (= ?msb_s bit0) (= ?msb_t bit1)) + (bvneg (bvudiv s (bvneg t))) + (bvudiv (bvneg s) (bvneg t))))))) + * + */ + + if (children[0] == children[1]) // same pointer. + { + return NO_CHANGE; + } + + + return bvSignedDivisionRemainderBothWays(children, output, bm, + bvUnsignedDivisionBothWays, SIGNED_DIVISION); +} +} +} +; diff --git a/src/simplifier/constantBitP/ConstantBitP_Multiplication.cpp b/src/simplifier/constantBitP/ConstantBitP_Multiplication.cpp new file mode 100644 index 0000000..03be6d2 --- /dev/null +++ b/src/simplifier/constantBitP/ConstantBitP_Multiplication.cpp @@ -0,0 +1,593 @@ +#include "ConstantBitP_TransferFunctions.h" +#include "ConstantBitP_Utility.h" +#include +#include +#include "../../AST/AST.h" +#include "../../simplifier/simplifier.h" +#include "MultiplicationStats.h" +#include +#include "multiplication/ImplicationGraph.h" +#include "multiplication/ColumnCounts.h" +// Multiply. + + +namespace simplifier +{ +namespace constantBitP +{ +using std::endl; +using std::pair; +using std::set; + +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; + + while (currIndex < column) + { + currIndex++; + result = (result + currIndex) / 2; + } + + 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]; + + 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; +} + +// 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(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 useTrailingZeroesToFix(FixedBits& x, FixedBits&y, FixedBits& output) +{ + int min = x.numberOfTrailingZeroes(); + min += y.numberOfTrailingZeroes(); + + min = std::min(min, output.getWidth()); + + for (int i = 0; i < min; i++) + if (!output.isFixed(i)) + { + output.setFixed(i, true); + output.setValue(i, false); + } + else if (output.getValue(i)) + { + return CONFLICT; + } + + return NOT_IMPLEMENTED; +} + +// About 80% of multipliction runtime is in this function. +// 48% is generating the multiplicative inverse. +// 17% is constructing the Simpliier. +// 12% is destroying the simplifier. +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; +} + +// 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; +} + +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(); + + ImplicationGraph graph; + + if (debug_multiply) + cerr << "======================" << endl; + + if (debug_multiply) + { + cerr << "Initial Fixing"; + cerr << x << "*"; + cerr << y << "="; + cerr << output << endl; + } + + Result r = NO_CHANGE; + r = useLeadingZeroesToFix(x, y, output); + if (CONFLICT == r) + { + if (debug_multiply) + cerr << "conflict 1"; + return r; + } + + r = useTrailingFixedToFix(x, y, output); + if (CONFLICT == r) + { + if (debug_multiply) + cerr << "conflict 2"; + return r; + } + + r = useTrailingZeroesToFix(x, y, output); + if (CONFLICT == r) + { + if (debug_multiply) + cerr << "conflict 3"; + return r; + } + + r = useInversesToSolve(x, y, output, bm); + if (CONFLICT == r) + { + if (debug_multiply) + cerr << "conflict 4"; + 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); + + if (debug_multiply) + { + cc.print("initially"); + } + + // 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; + + do + { + r = NO_CHANGE; + + if (debug_multiply) + { + cc.print("At start"); + } + + for (unsigned column = 0; column < bitWidth; column++) + { + if (cc.columnL[column] == cc.columnH[column]) + { + r= graph.discoverNewNANDs(x, y, column, + cc.columnL[column]); + if (CONFLICT == r) + return CONFLICT; + + r = graph.discoverNewXORs(x, y, column, cc.columnL[column]); + if (CONFLICT == r) + return CONFLICT; + + } + } + + r = graph.fixUsingImplications(x, y); + if (CONFLICT == r) + return CONFLICT; + + if (debug_multiply) + { + cc.print("After fixing using implications"); + } + + r = graph.updateSums(x, y, cc); + + if (CONFLICT == r) + return CONFLICT; + + if (debug_multiply) + { + cc.print("After implication graph updating sums"); + } + + r = cc.fixedPoint(output); + + if (debug_multiply) + { + cc.print("After last fixed point"); + } + + if (r == CONFLICT) + return CONFLICT; + } while (r != NO_CHANGE); + + 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 (children[0]->isTotallyFixed() && children[1]->isTotallyFixed() + && !output.isTotallyFixed()) + { + cerr << *children[0] << " * "; + cerr << *children[1]; + cerr << output << endl; + assert(output.isTotallyFixed()); + } + + return NOT_IMPLEMENTED; +} + +} +} diff --git a/src/simplifier/constantBitP/ConstantBitPropagation.cpp b/src/simplifier/constantBitP/ConstantBitPropagation.cpp index 217cee5..8ce77de 100644 --- a/src/simplifier/constantBitP/ConstantBitPropagation.cpp +++ b/src/simplifier/constantBitP/ConstantBitPropagation.cpp @@ -693,7 +693,7 @@ namespace simplifier MAPTFN(ITE,bvITEBothWays) MAPTFN(BVCONCAT, bvConcatBothWays) -#ifdef WITHCBITP + case BVMULT: // handled specially later. case BVDIV: case BVMOD: @@ -702,7 +702,7 @@ namespace simplifier case SBVMOD: transfer = NULL; break; -#endif + default: { notHandled(k); @@ -712,7 +712,7 @@ namespace simplifier #undef MAPTFN bool mult_like = false; -#ifdef WITHCBITP + // safe approximation to no overflow multiplication. if (k == BVMULT) { @@ -748,7 +748,8 @@ namespace simplifier mult_like=true; } else -#endif + + result = transfer(children, output); if (mult_like && output_mult_like) diff --git a/src/simplifier/constantBitP/FixedBits.cpp b/src/simplifier/constantBitP/FixedBits.cpp index 49368c9..88604ca 100644 --- a/src/simplifier/constantBitP/FixedBits.cpp +++ b/src/simplifier/constantBitP/FixedBits.cpp @@ -1,9 +1,6 @@ #include "../../AST/AST.h" #include "FixedBits.h" -#ifdef WITHCBITP - #include "MersenneTwister.h" -#endif #include "ConstantBitP_Utility.h" @@ -154,7 +151,9 @@ namespace simplifier return result; } -#ifdef WITHCBITP +#if 0 + #include "MersenneTwister.h" + // Getting a new random number is expensive. Not sure why. FixedBits FixedBits::createRandom(const int length, const int probabilityOfSetting, MTRand& trand) { -- 2.47.3