--- /dev/null
+#include "ConstantBitP_TransferFunctions.h"
+#include "ConstantBitP_Utility.h"
+#include <set>
+#include <stdexcept>
+#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<b. Multiplication and addition don't overflow.
+
+// returning true = conflict.
+// Fix value of a to b.
+bool fix(FixedBits& a, const FixedBits& b, const int i) {
+ if (!b.isFixed(i))
+ return false;
+
+ if (a.isFixed(i) && b.isFixed(i) && (a.getValue(i) ^ b.getValue(i)))
+ return true;
+
+ if (!a.isFixed(i) && b.isFixed(i)) {
+ a.setFixed(i, true);
+ a.setValue(i, b.getValue(i));
+ return false;
+ }
+
+ return false;
+}
+
+FixedBits cbvToFixedBits(BEEV::CBV low, unsigned width)
+{
+ FixedBits lowBits(width,false);
+ for (int i = width - 1; i >= 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<FixedBits*> 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<FixedBits*>& children,
+ FixedBits& output, STPMgr* bm, WhatIsOutput whatIs);
+
+
+Result bvUnsignedQuotientAndRemainder(vector<FixedBits*>& 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<FixedBits*>& 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<FixedBits*> addChildren;
+ addChildren.push_back(×);
+ addChildren.push_back(&r);
+
+ vector<FixedBits*> 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<FixedBits*>& children,
+ FixedBits& output, STPMgr* bm) {
+
+
+
+ Result r1 = NO_CHANGE;
+ vector<FixedBits*> 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<FixedBits*>& 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<FixedBits*> 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<FixedBits*>& children,
+ FixedBits& output, STPMgr* bm, Result(*tf)(vector<FixedBits*>&,
+ 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<FixedBits*> 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<FixedBits*> 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<FixedBits*> 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<FixedBits*> 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<FixedBits*> 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<FixedBits*> 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<FixedBits*> 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<FixedBits*> 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<FixedBits*>& 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<FixedBits*>& 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<FixedBits*>& 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);
+}
+}
+}
+;
--- /dev/null
+#include "ConstantBitP_TransferFunctions.h"
+#include "ConstantBitP_Utility.h"
+#include <set>
+#include <stdexcept>
+#include "../../AST/AST.h"
+#include "../../simplifier/simplifier.h"
+#include "MultiplicationStats.h"
+#include <hash_set>
+#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<FixedBits*>& 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<FixedBits*>& 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;
+}
+
+}
+}
projects / francis / stp.git / commitdiff