helpstring +=
"-d : check counterexample\n";
-#ifdef WITHCBITP
helpstring +=
"--disable-cbitp : disable constant bit propagation\n";
-#endif
helpstring +=
"--exit-after-CNF : exit after the CNF has been generated\n";
--- /dev/null
+#include "ConstantBitP_TransferFunctions.h"
+#include "ConstantBitP_Utility.h"
+
+// Add, subtract.
+// Trevor Hansen. BSD License.
+
+namespace simplifier
+{
+namespace constantBitP
+{
+
+// Subtract is implemented in terms of plus.
+Result bvSubtractBothWays(vector<FixedBits*>& children, FixedBits& output)
+{
+ assert(children.size() ==2);
+
+ FixedBits & a = *children[0];
+ FixedBits & b = *children[1];
+
+ assert(a.getWidth() == b.getWidth());
+
+ const int bitWidth = a.getWidth();
+
+ FixedBits one(bitWidth, false);
+ one.fixToZero();
+ one.setFixed(0, true);
+ one.setValue(0, true);
+
+ FixedBits notB(bitWidth, false);
+
+ vector<FixedBits*> Addargs;
+ Addargs.push_back(&a);
+ Addargs.push_back(¬B);
+ Addargs.push_back(&one);
+
+ bool changed = false;
+ while (true) // until it fixed points
+ {
+ Result result;
+ FixedBits initialNotB(notB);
+ FixedBits initialA(a);
+ FixedBits initialOut(output);
+
+ result = bvNotBothWays(b, notB);
+ if (CONFLICT == result)
+ return CONFLICT;
+
+ result = bvAddBothWays(Addargs, output);
+ if (CONFLICT == result)
+ return CONFLICT;
+
+ if (FixedBits::equals(initialNotB, notB) && FixedBits::equals(initialA, a) && FixedBits::equals(initialOut, output))
+ break;
+ else
+ changed = true;
+ }
+
+ return NOT_IMPLEMENTED;
+}
+
+/////////////// ADDITION>
+
+const bool add_debug_messages = false;
+
+// For a given number of children. The maximum size of the carry in for addition.
+//
+// For five arguments (say). The carry can be as big as 4. But into the second column
+// it can be no bigger than 2.
+unsigned maximumCarryInForAddition(int numberOfChildren, int index)
+{
+ assert(numberOfChildren > 1);
+ assert(index >=0);
+
+ if (0 == index)
+ return 0;
+
+
+ if (numberOfChildren==2)
+ return 1; // Case that the (index==0) is already handled.
+
+
+ unsigned result = 0;
+ unsigned currIndex = 0;
+
+ while (currIndex < (unsigned)index)
+ {
+ result = (result + numberOfChildren) >> 1;
+ currIndex++;
+ }
+
+ //cerr << "max carry" << numberOfChildren << " " << index << " " << result << endl;
+ return result;
+}
+
+// Given the current fixings to a particular column, as well as the range of the columns inflow,
+// deduce values.
+// index: Column we are working on.
+// sum: What the column must sum to.
+// inflowMin: Minimum inflow expected, i.e. lowerbound of lower (index-1).
+
+Result fixIfCanForAddition(vector<FixedBits*>& children, const int index, const int sum, const int inflowMin, const int inflowMax)
+{
+ Result result = NO_CHANGE;
+
+ assert(inflowMin <= inflowMax);
+ assert(inflowMin >=0);
+ assert(index >=0);
+ assert(index < children[0]->getWidth());
+
+ const int maxCarryIn = maximumCarryInForAddition(children.size(), index);
+
+ assert(inflowMax <= maxCarryIn);
+ assert(sum <= (signed)children.size() + maxCarryIn );
+
+ if (add_debug_messages)
+ cerr << "fixIfCanForAddition " << index << " " << sum << endl;
+
+ int unfixed = 0;
+ int ones = 0;
+ int zeroes = 0;
+ for (unsigned i = 0; i < children.size(); i++)
+ {
+ if (children[i]->isFixed(index))
+ {
+ if (children[i]->getValue(index))
+ ones++;
+ if (!children[i]->getValue(index))
+ zeroes++;
+ }
+ else
+ {
+ unfixed++;
+ }
+ }
+
+ assert(ones >=0 && unfixed >=0 && zeroes >=0);
+ assert(ones + unfixed + zeroes == (signed)children.size());
+
+ ones = ones + inflowMin;
+
+ if ((ones == sum) && unfixed > 0) // set em all to false. Already have as many as we need.
+ {
+ for (unsigned i = 0; i < children.size(); i++)
+ {
+ if (!children[i]->isFixed(index))
+ {
+ children[i]->setFixed(index, true);
+ children[i]->setValue(index, false);
+ result = CHANGED;
+ }
+ }
+ }
+
+ int sumUnfixed = unfixed + inflowMax - inflowMin;
+ zeroes = zeroes + (maxCarryIn - inflowMax);
+
+ assert(ones >=0 && sumUnfixed >=0 && zeroes >=0);
+ assert(ones+sumUnfixed+zeroes == (signed) children.size()+ maxCarryIn);
+
+ if (sum == (sumUnfixed + ones) && unfixed > 0) // need 'em all fixed to ones.
+ {
+ for (unsigned i = 0; i < children.size(); i++)
+ {
+ if (!children[i]->isFixed(index))
+ {
+ children[i]->setFixed(index, true);
+ children[i]->setValue(index, true);
+ result = CHANGED;
+ }
+ }
+ }
+ else if (sum > sumUnfixed + ones)
+ return CONFLICT;
+
+ if (sum < ones)
+ return CONFLICT;
+
+ return result;
+}
+
+// Count the number of fixed ones, and zeroes. Update the low and high column counts.
+// Counts should only be monitonically changed. So this can only be run once.
+void initialiseColumnCounts(int columnL[], int columnH[], const int bitWidth, const int numberOfChildren, const vector<FixedBits*>& children)
+{
+ // setup the low and highs.
+ for (int i = 0; i < bitWidth; i++)
+ {
+ columnL[i] = 0;
+ columnH[i] = numberOfChildren;
+ }
+
+ // Set the column totals.
+ for (int i = 0; i < bitWidth; i++)
+ {
+ for (int j = 0; j < numberOfChildren; j++)
+ {
+ if (children[j]->isFixed(i))
+ {
+ if (children[j]->getValue(i))
+ columnL[i]++;
+ else
+ columnH[i]--;
+ }
+ }
+ }
+}
+
+void printArray(int f[], int width)
+{
+ for (int i = width - 1; i >= 0; i--)
+ std::cerr << f[i] << " ";
+ std::cerr << std::endl;
+}
+
+Result bvAddBothWays(vector<FixedBits*>& children, FixedBits& output)
+{
+ Result result = NO_CHANGE;
+
+ const int bitWidth = output.getWidth();
+ const int numberOfChildren = children.size();
+
+ for (int i = 0; i < numberOfChildren; i++)
+ {
+ assert(children[i]->getWidth() == bitWidth );
+ }
+
+ int columnL[bitWidth]; // minimum "" ""
+ int columnH[bitWidth]; // maximum number of true partial products.
+
+ initialiseColumnCounts(columnL, columnH, bitWidth, numberOfChildren, children);
+
+ int sumH[bitWidth];
+ int sumL[bitWidth];
+ sumL[0] = columnL[0];
+ sumH[0] = columnH[0];
+
+ for (unsigned i = /**/1 /**/; i < (unsigned) bitWidth; i++)
+ {
+ assert((columnH[i] >= columnL[i]) && (columnL[i] >= 0));
+ sumH[i] = columnH[i] + (sumH[i - 1] / 2);
+ sumL[i] = columnL[i] + (sumL[i - 1] / 2);
+ }
+
+ // Now the sums counts are all updated. And consistent with each other.
+
+ bool changed = true;
+ while (changed)
+ {
+ changed = false;
+
+ // Make sure each column's sum is consistent with the output.
+ for (int i = 0; i < bitWidth; i++)
+ {
+ if (output.isFixed(i))
+ {
+ int expected = output.getValue(i) ? 1 : 0;
+
+ // output is true. So the maximum and minimum can only be even.
+ if (sumH[i] % 2 != expected)
+ {
+ sumH[i]--;
+ changed = true;
+ }
+ if (sumL[i] % 2 != expected)
+ {
+ sumL[i]++;
+ changed = true;
+ }
+
+ if (changed && ((sumH[i] < sumL[i]) || (sumL[i] < 0)))
+ return CONFLICT;
+ }
+ }
+
+ // update the column counts to make them consistent to the totals.
+ for (int i = /**/0 /**/; i < bitWidth; i++)
+ {
+ if (sumH[i] < columnH[i])
+ {
+ columnH[i]--;
+ changed = true;
+
+ if (columnH[i] < columnL[i])
+ return CONFLICT;
+ }
+ }
+
+ // Go from low to high making each of the sums consistent.
+ for (int i = /**/1 /**/; i < bitWidth; i++)
+ {
+ assert((columnH[i] >= columnL[i]) && (columnL[i] >= 0));
+ if (sumH[i] > columnH[i] + (sumH[i - 1] / 2))
+ {
+ sumH[i] = columnH[i] + (sumH[i - 1] / 2);
+ changed = true;
+ }
+ if (sumL[i] < columnL[i] + (sumL[i - 1] / 2))
+ {
+ sumL[i] = columnL[i] + (sumL[i - 1] / 2);
+ changed = true;
+ }
+
+ if (changed && (sumH[i] < sumL[i] || sumL[i] < 0))
+ return CONFLICT;
+
+ }
+
+ // go from high to low, making each of the sums consistent.
+ for (int i = /**/bitWidth - 1 /**/; i >= 1; i--)
+ {
+ if ((sumH[i] == sumL[i]))
+ {
+ stats s = getStats(children, i);
+
+ if (0 == s.unfixed)
+ {
+ // amount that the prior column needs to contribute.
+ int toContribute = (sumH[i] - s.fixedToOne) * 2;
+
+ if (sumH[i - 1] > (toContribute + 1))
+ {
+ changed = true;
+ sumH[i - 1] = toContribute + 1; // plus one because of rounding down.
+ }
+
+ if (sumL[i - 1] < toContribute)
+ {
+ changed = true;
+ sumL[i - 1] = toContribute;
+ }
+
+ if (sumH[i - 1] < sumL[i - 1])
+ {
+ return CONFLICT;
+ }
+ }
+ }
+ }
+
+ if (add_debug_messages)
+ {
+ std::cerr << "bottom" << std::endl;
+ cerr << "columnL:";
+ printArray(columnL, bitWidth);
+ cerr << "columnH:";
+ printArray(columnH, bitWidth);
+ cerr << "sumL:";
+ printArray(sumL, bitWidth);
+ cerr << "sumH:";
+ printArray(sumH, bitWidth);
+ }
+
+ for (int column = 0; column < bitWidth; column++)
+ {
+ if (sumH[column] == sumL[column])
+ {
+ // (1) If the low and high sum is equal. Then the output is know.
+ bool newResult = (sumH[column] % 2 == 0) ? false : true;
+
+ if (!output.isFixed(column))
+ {
+ output.setFixed(column, true);
+ output.setValue(column, newResult);
+ result = CHANGED;
+ changed = true;
+ }
+ else if (output.isFixed(column) && (output.getValue(column) != newResult))
+ return CONFLICT;
+
+ // (2) If this column has some unfixed values. Then we may be able to determine them.
+ Result tempResult;
+ if (0 == column)
+ tempResult = fixIfCanForAddition(children, column, sumH[column], 0, 0);
+ else
+ tempResult = fixIfCanForAddition(children, column, sumH[column], sumL[column - 1] / 2, sumH[column - 1] / 2);
+
+ if (CONFLICT == tempResult)
+ return CONFLICT;
+
+ if (CHANGED == tempResult)
+ changed = true;
+
+ }
+
+ }
+ }
+ return NOT_IMPLEMENTED;
+}
+
+}
+}
--- /dev/null
+#include "ConstantBitP_TransferFunctions.h"
+#include "ConstantBitP_Utility.h"
+
+// AND, OR, XOR, NOT Transfer functions.
+// Trevor Hansen. BSD License.
+
+
+
+namespace simplifier
+{
+namespace constantBitP
+{
+
+Result bvXorBothWays(vector<FixedBits*>& operands, FixedBits& output)
+{
+ Result result = NO_CHANGE;
+ const int bitWidth = output.getWidth();
+
+ for (int i = 0; i < bitWidth; i++)
+ {
+ const stats status = getStats(operands, i);
+
+ if (status.unfixed == 0) // if they are all fixed. We know the answer.
+ {
+ bool answer = (status.fixedToOne % 2) != 0;
+
+ if (!output.isFixed(i))
+ {
+ output.setFixed(i, true);
+ output.setValue(i, answer);
+ result = CHANGED;
+ }
+ else if (output.getValue(i) != answer)
+ return CONFLICT;
+ }
+ else if (status.unfixed == 1 && output.isFixed(i))
+ {
+ // If there is just one unfixed, and we have the answer --> We know the value.
+ bool soFar = ((status.fixedToOne % 2) != 0);
+ if (soFar != output.getValue(i))
+ { // result needs to be flipped.
+ fixUnfixedTo(operands, i, true);
+ }
+ else
+ fixUnfixedTo(operands, i, false);
+ result = CHANGED;
+ }
+ }
+ return result;
+}
+
+// if output bit is true. Fix all the operands.
+// if all the operands are fixed. Fix the output.
+// given 1,1,1,- == 0, fix - to 0.
+Result bvAndBothWays(vector<FixedBits*>& operands, FixedBits& output)
+{
+ Result result = NO_CHANGE;
+ const int bitWidth = output.getWidth();
+
+ for (int i = 0; i < bitWidth; i++)
+ {
+ const stats status = getStats(operands, i);
+
+ // output is fixed to one. But an input value is false!
+ if (output.isFixed(i) && output.getValue(i) && status.fixedToZero > 0)
+ return CONFLICT;
+
+ // output is fixed to one. But an input value is false!
+ if (output.isFixed(i) && !output.getValue(i) && status.fixedToZero == 0
+ && status.unfixed == 0)
+ return CONFLICT;
+
+ // output is fixed to one. So all should be one.
+ if (output.isFixed(i) && output.getValue(i) && status.unfixed > 0)
+ {
+ fixUnfixedTo(operands, i, true);
+ result = CHANGED;
+ }
+
+ // The output is unfixed. At least one input is false.
+ if (!output.isFixed(i) && status.fixedToZero > 0)
+ {
+ output.setFixed(i, true);
+ output.setValue(i, false);
+ result = CHANGED;
+ }
+
+ // Everything is fixed to one!
+ if (!output.isFixed(i) && status.fixedToZero == 0 && status.unfixed
+ == 0)
+ {
+ output.setFixed(i, true);
+ output.setValue(i, true);
+ result = CHANGED;
+ }
+
+ // If the output is false, and there is a single unfixed value with everything else true..
+ if (output.isFixed(i) && !output.getValue(i) && status.fixedToZero == 0
+ && status.unfixed == 1)
+ {
+ fixUnfixedTo(operands, i, false);
+ result = CHANGED;
+ }
+ }
+ return result;
+}
+
+Result bvOrBothWays(vector<FixedBits*>& children, FixedBits& output)
+{
+ Result r = NO_CHANGE;
+ const int numberOfChildren = children.size();
+ const int bitWidth = output.getWidth();
+
+ for (int i = 0; i < bitWidth; i++)
+ {
+ bool answerKnown = output.isFixed(i);
+ bool answer = false;
+ if (answerKnown)
+ answer = output.getValue(i);
+
+ int unks = 0;
+ int ones = 0;
+ int zeroes = 0;
+
+ for (int j = 0; j < numberOfChildren; j++)
+ {
+ assert(output.getWidth() == children[j]->getWidth());
+
+ if (!children[j]->isFixed(i))
+ unks++;
+ else if (children[j]->getValue(i))
+ ones++;
+ else
+ zeroes++;
+ }
+
+ if (ones > 0) // Atleast a single one found!
+
+ {
+ if (answerKnown && !answer)
+ return CONFLICT;
+
+ if (!answerKnown)
+ {
+ output.setFixed(i, true);
+ output.setValue(i, true);
+ r = CHANGED;
+ }
+ }
+
+ if (zeroes == numberOfChildren) // all zeroes.
+
+ {
+ if (answerKnown && answer)
+ return CONFLICT;
+
+ if (!answerKnown)
+ {
+ r = CHANGED;
+ output.setFixed(i, true);
+ output.setValue(i, false);
+
+ }
+ }
+
+ if (answerKnown && !answer) // known false
+
+ {
+ if (ones > 0)
+ return CONFLICT;
+
+ // set all the column to false.
+
+ for (int j = 0; j < numberOfChildren; j++)
+ {
+ if (!children[j]->isFixed(i))
+ {
+ r = CHANGED;
+ children[j]->setFixed(i, true);
+ children[j]->setValue(i, false);
+ }
+ }
+
+ }
+
+ if (unks == 1 && answerKnown && answer && (zeroes == (numberOfChildren
+ - 1)))
+ {
+ // A single unknown, everything else is false. The answer is true. So the unknown is true.
+
+ for (int j = 0; j < numberOfChildren; j++)
+ {
+ if (!children[j]->isFixed(i))
+ {
+ r = CHANGED;
+ children[j]->setFixed(i, true);
+ children[j]->setValue(i, true);
+ }
+ }
+ }
+
+ }
+ return r;
+}
+
+Result bvNotBothWays(vector<FixedBits*>& children, FixedBits& result)
+{
+ return bvNotBothWays(*(children[0]), result);
+}
+
+Result bvImpliesBothWays(vector<FixedBits*>& children, FixedBits& result)
+{
+
+ FixedBits& a = (*children[0]);
+ FixedBits& b = (*children[1]);
+
+ assert(a.getWidth() == result.getWidth());
+ const int bitWidth = a.getWidth();
+ assert (bitWidth == 1);
+
+ Result r = NO_CHANGE;
+
+ int i = 0;
+
+ // (false -> something) is always true.
+ // (something -> true ) is always true.
+ if (a.isFixedToZero(i) || b.isFixedToOne(i))
+ {
+ if (!result.isFixed(i))
+ {
+ result.setFixed(i, true);
+ result.setValue(i, true);
+ r = CHANGED;
+ } else if (result.isFixedToZero(i))
+ return CONFLICT;
+ }
+
+ // If the result is false. it must be (true -> false)
+ if (result.isFixedToZero(i))
+ {
+ if (a.isFixedToZero(i) || b.isFixedToOne(i))
+ return CONFLICT;
+
+ if (!a.isFixed(i))
+ {
+ a.setFixed(i, true);
+ a.setValue(i, true);
+ r = CHANGED;
+ }
+ if (!b.isFixed(i))
+ {
+ b.setFixed(i, true);
+ b.setValue(i, false);
+ r = CHANGED;
+ }
+ }
+
+ if (result.isFixedToOne(i))
+ {
+ if (a.isFixedToOne(i))
+ {
+ if (!b.isFixed(i))
+ {
+ b.setFixed(i, true);
+ b.setValue(i, true);
+ r = CHANGED;
+ }
+ else if (b.isFixedToZero(i))
+ return CONFLICT;
+ }
+
+ if (b.isFixedToZero(i))
+ {
+ if (!a.isFixed(i))
+ {
+ a.setFixed(i, true);
+ a.setValue(i, false);
+ r = CHANGED;
+ }
+ }
+ }
+
+ if (a.isFixedToOne(i) && b.isFixedToZero(i))
+ {
+ if (result.isFixedToOne(i))
+ return CONFLICT;
+ if (!result.isFixed(i))
+ {
+ result.setFixed(i, true);
+ result.setValue(i, false);
+ r = CHANGED;
+ }
+ }
+
+ return r;
+
+}
+
+Result bvNotBothWays(FixedBits& a, FixedBits& output)
+{
+ assert(a.getWidth() == output.getWidth());
+ const int bitWidth = a.getWidth();
+
+ Result result = NO_CHANGE;
+
+ for (int i = 0; i < bitWidth; i++)
+ {
+ // error if they are the same.
+ if (a.isFixed(i) && output.isFixed(i) && (a.getValue(i)
+ == output.getValue(i)))
+ {
+ return CONFLICT;
+ }
+
+ if (a.isFixed(i) && !output.isFixed(i))
+ {
+ output.setFixed(i, true);
+ output.setValue(i, !a.getValue(i));
+ result = CHANGED;
+ }
+
+ if (output.isFixed(i) && !a.isFixed(i))
+ {
+ a.setFixed(i, true);
+ a.setValue(i, !output.getValue(i));
+ result = CHANGED;
+ }
+ }
+ return result;
+}
+
+}
+}
--- /dev/null
+#include "ConstantBitP_TransferFunctions.h"
+#include "ConstantBitP_Utility.h"
+#include "../../extlib-constbv/constantbv.h"
+
+
+// The signed and unsigned versions of the four comparison operations: > < >= <=
+
+// Establishes consistency over the intervals of the operations. Then
+// increase the minimum value by turning on the highest unfixed bit.
+// If that takes us past the other value's maximum. Then that bit
+// must be zero.
+
+// Trevor Hansen. BSD License.
+
+namespace simplifier
+{
+namespace constantBitP
+{
+
+Result bvSignedLessThanBothWays(FixedBits& c0, FixedBits &c1, FixedBits& output);
+Result bvSignedLessThanEqualsBothWays(FixedBits& c0, FixedBits &c1, FixedBits& output);
+
+Result bvSignedLessThanBothWays(vector<FixedBits*>& children, FixedBits& output)
+{
+ assert(children.size() == 2);
+ return bvSignedLessThanBothWays(*children[0], *children[1], output);
+}
+
+Result bvSignedGreaterThanBothWays(FixedBits & c0, FixedBits & c1, FixedBits& output)
+{
+ return bvSignedLessThanBothWays(c1, c0, output);
+}
+
+Result bvSignedGreaterThanBothWays(vector<FixedBits*>& children, FixedBits& output)
+{
+ assert(children.size() == 2);
+ return bvSignedLessThanBothWays(*children[1], *children[0], output);
+}
+
+Result bvSignedLessThanEqualsBothWays(vector<FixedBits*>& children, FixedBits& output)
+{
+ assert(children.size() == 2);
+ return bvSignedLessThanEqualsBothWays(*children[0], *children[1], output);
+}
+
+Result bvSignedGreaterThanEqualsBothWays(FixedBits & c0, FixedBits & c1, FixedBits& output)
+{
+ return bvSignedLessThanEqualsBothWays(c1, c0, output);
+}
+
+Result bvSignedGreaterThanEqualsBothWays(vector<FixedBits*>& children, FixedBits& output)
+{
+ assert(children.size() == 2);
+ return bvSignedLessThanEqualsBothWays(*children[1], *children[0], output);
+}
+
+///////// UNSIGNED.
+
+Result bvLessThanBothWays(FixedBits& c0, FixedBits &c1, FixedBits& output);
+Result bvLessThanEqualsBothWays(FixedBits& c0, FixedBits &c1, FixedBits& output);
+
+Result bvLessThanBothWays(vector<FixedBits*>& children, FixedBits& output)
+{
+ assert(children.size() == 2);
+ return bvLessThanBothWays(*children[0], *children[1], output);
+}
+
+Result bvGreaterThanBothWays(vector<FixedBits*>& children, FixedBits& output)
+{
+ assert(children.size() == 2);
+ return bvLessThanBothWays(*children[1], *children[0], output);
+}
+
+Result bvGreaterThanBothWays(FixedBits& c0, FixedBits &c1, FixedBits& output)
+{
+ return bvLessThanBothWays(c1, c0, output);
+}
+
+Result bvGreaterThanEqualsBothWays(vector<FixedBits*>& children, FixedBits& result)
+{
+ assert(children.size() == 2);
+ return bvLessThanEqualsBothWays(*children[1], *children[0], result);
+}
+
+Result bvGreaterThanEqualsBothWays(FixedBits& c0, FixedBits &c1, FixedBits& output)
+{
+ return bvLessThanEqualsBothWays(c1, c0, output);
+}
+
+Result bvLessThanEqualsBothWays(vector<FixedBits*>& children, FixedBits& output)
+{
+ assert(children.size() == 2);
+ return bvLessThanEqualsBothWays(*children[0], *children[1], output);
+}
+
+typedef unsigned int* CBV;
+
+void destroy(CBV a, CBV b, CBV c, CBV d)
+{
+ CONSTANTBV::BitVector_Destroy(a);
+ CONSTANTBV::BitVector_Destroy(b);
+ CONSTANTBV::BitVector_Destroy(c);
+ CONSTANTBV::BitVector_Destroy(d);
+}
+
+///////// Signed operations.
+
+
+
+
+Result bvSignedLessThanBothWays(FixedBits& c0, FixedBits& c1, FixedBits& output)
+{
+ Result r = NO_CHANGE;
+
+ assert(c0.getWidth() == c1.getWidth());
+
+ CBV c0_min = CONSTANTBV::BitVector_Create(c0.getWidth(), true);
+ CBV c0_max = CONSTANTBV::BitVector_Create(c0.getWidth(), true);
+ CBV c1_min = CONSTANTBV::BitVector_Create(c0.getWidth(), true);
+ CBV c1_max = CONSTANTBV::BitVector_Create(c0.getWidth(), true);
+
+ setSignedMinMax(c0, c0_min, c0_max);
+ setSignedMinMax(c1, c1_min, c1_max);
+
+ // EG. [0,5] < [6,8]. i.e. max of first is less than min of second.
+ if (signedCompare(c0_max, c1_min) < 0)
+ {
+ if (output.isFixed(0) && !output.getValue(0)) // output is fixed to false.
+ {
+ destroy(c0_min, c0_max, c1_min, c1_max);
+ return CONFLICT;
+ }
+
+ if (!output.isFixed(0))
+ {
+ output.setFixed(0, true);
+ output.setValue(0, true);
+ r = CHANGED;
+ }
+ }
+
+ // EG. [3,5] < [0,1].
+ if (signedCompare(c0_min, c1_max) >= 0)
+ {
+ // min is greater than max.
+ if (output.isFixed(0) && output.getValue(0))
+ {
+ destroy(c0_min, c0_max, c1_min, c1_max);
+ return CONFLICT;
+ }
+
+ if (!output.isFixed(0))
+ {
+ output.setFixed(0, true);
+ output.setValue(0, false);
+ r = CHANGED;
+ }
+ }
+
+ if (output.isFixed(0) && !output.getValue(0))
+ {
+ FixedBits t(1, true);
+ t.setFixed(0, true);
+ t.setValue(0, true);
+ destroy(c0_min, c0_max, c1_min, c1_max);
+ return bvSignedGreaterThanEqualsBothWays(c0, c1, t);
+ }
+
+ const int msb = c0.getWidth() - 1;
+
+ // The signed case.
+ if (output.isFixed(0) && output.getValue(0))
+ {
+ //////////// MSB
+ // turn off the sign bit of c0's minimum.
+ // If that value is greater or equal to c1's max. SEt it.
+ if (!c0.isFixed(msb))
+ {
+ // turn it on in the minimum.
+ CONSTANTBV::BitVector_Bit_Off(c0_min, msb);
+ if (signedCompare(c0_min, c1_max) >= 0)
+ {
+ c0.setFixed(msb, true);
+ c0.setValue(msb, true);
+ setSignedMinMax(c0, c0_min, c0_max);
+ r = CHANGED;
+ }
+ else
+ {
+ CONSTANTBV::BitVector_Bit_On(c0_min, msb);
+ }
+ }
+
+ if (!c1.isFixed(msb))
+ {
+ CONSTANTBV::BitVector_Bit_On(c1_max, msb);
+ if (signedCompare(c1_max, c0_min) <= 0)
+ {
+ c1.setFixed(msb, true);
+ c1.setValue(msb, false);
+ setSignedMinMax(c1, c1_min, c1_max);
+ r = CHANGED;
+ }
+ else
+ {
+ CONSTANTBV::BitVector_Bit_Off(c1_max, msb);
+ }
+ }
+
+ ///////////// Bits other than the MSB
+
+ if (output.isFixed(0) && output.getValue(0))
+ {
+ for (int i = c0.getWidth() - 1 - 1; i >= 0; i--)
+ {
+ if (!c0.isFixed(i))
+ {
+ // turn it on in the minimum.
+ CONSTANTBV::BitVector_Bit_On(c0_min, i);
+ if (signedCompare(c0_min, c1_max) >= 0)
+ {
+ c0.setFixed(i, true);
+ c0.setValue(i, false);
+ setSignedMinMax(c0, c0_min, c0_max);
+ r = CHANGED;
+ }
+ else
+ {
+ CONSTANTBV::BitVector_Bit_Off(c0_min, i);
+ break;
+ }
+ }
+ }
+
+ for (int i = c1.getWidth() - 1 - 1; i >= 0; i--)
+ {
+ if (!c1.isFixed(i))
+ {
+ CONSTANTBV::BitVector_Bit_Off(c1_max, i);
+ if (signedCompare(c1_max, c0_min) <= 0)
+ {
+ c1.setFixed(i, true);
+ c1.setValue(i, true);
+ setSignedMinMax(c1, c1_min, c1_max);
+ r = CHANGED;
+ }
+ else
+ {
+ CONSTANTBV::BitVector_Bit_On(c1_max, i);
+ break;
+ }
+ }
+ }
+ }
+ }
+ destroy(c0_min, c0_max, c1_min, c1_max);
+ return NOT_IMPLEMENTED;
+}
+
+Result bvSignedLessThanEqualsBothWays(FixedBits& c0, FixedBits &c1, FixedBits& output)
+{
+ Result r = NO_CHANGE;
+
+ assert(c0.getWidth() == c1.getWidth());
+
+ CBV c0_min = CONSTANTBV::BitVector_Create(c0.getWidth(), true);
+ CBV c0_max = CONSTANTBV::BitVector_Create(c0.getWidth(), true);
+ CBV c1_min = CONSTANTBV::BitVector_Create(c0.getWidth(), true);
+ CBV c1_max = CONSTANTBV::BitVector_Create(c0.getWidth(), true);
+
+ setSignedMinMax(c0, c0_min, c0_max);
+ setSignedMinMax(c1, c1_min, c1_max);
+
+ if (signedCompare(c0_max, c1_min) <= 0)
+ {
+ if (output.isFixed(0) && !output.getValue(0))
+ {
+ destroy(c0_min, c0_max, c1_min, c1_max);
+ return CONFLICT;
+ }
+
+ if (!output.isFixed(0))
+ {
+ output.setFixed(0, true);
+ output.setValue(0, true);
+ r = CHANGED;
+ }
+ }
+
+ if (signedCompare(c0_min, c1_max) > 0)
+ {
+ if (output.isFixed(0) && output.getValue(0))
+ {
+ destroy(c0_min, c0_max, c1_min, c1_max);
+ return CONFLICT;
+ }
+
+ if (!output.isFixed(0))
+ {
+ output.setFixed(0, true);
+ output.setValue(0, false);
+ r = CHANGED;
+ }
+ }
+
+ // If true. Reverse and send to the other..
+ if (output.isFixed(0) && !output.getValue(0))
+ {
+ FixedBits t(1, true);
+ t.setFixed(0, true);
+ t.setValue(0, true);
+ destroy(c0_min, c0_max, c1_min, c1_max);
+ return bvSignedGreaterThanBothWays(c0, c1, t);
+ }
+
+ const int msb = c0.getWidth() - 1;
+
+ if (output.isFixed(0) && output.getValue(0))
+ {
+ //////////// MSB
+ // turn off the sign bit of c0's minimum.
+ // If that value is greater or equal to c1's max. SEt it.
+ if (!c0.isFixed(msb))
+ {
+ // turn it on in the minimum.
+ CONSTANTBV::BitVector_Bit_Off(c0_min, msb);
+ if (signedCompare(c0_min, c1_max) > 0)
+ {
+ c0.setFixed(msb, true);
+ c0.setValue(msb, true);
+ setSignedMinMax(c0, c0_min, c0_max);
+ r = CHANGED;
+ }
+ else
+ {
+ CONSTANTBV::BitVector_Bit_On(c0_min, msb);
+ }
+ }
+
+ if (!c1.isFixed(msb))
+ {
+ CONSTANTBV::BitVector_Bit_On(c1_max, msb);
+ if (signedCompare(c1_max, c0_min) < 0)
+ {
+ c1.setFixed(msb, true);
+ c1.setValue(msb, false);
+ setSignedMinMax(c1, c1_min, c1_max);
+ r = CHANGED;
+ }
+ else
+ {
+ CONSTANTBV::BitVector_Bit_Off(c1_max, msb);
+ }
+ }
+ //////////// Others.
+
+
+ // Starting from the high order. Turn on each bit in turn. If it being turned on pushes it past the max of the other side
+ // then we know it must be turned off.
+ for (int i = c0.getWidth() - 1 - 1; i >= 0; i--)
+ {
+ if (!c0.isFixed(i)) // bit is variable.
+ {
+ // turn it on in the minimum.
+ CONSTANTBV::BitVector_Bit_On(c0_min, i);
+ if (signedCompare(c0_min, c1_max) > 0)
+ {
+ c0.setFixed(i, true);
+ c0.setValue(i, false);
+ setSignedMinMax(c0, c0_min, c0_max);
+ }
+ else
+ {
+ CONSTANTBV::BitVector_Bit_Off(c0_min, i);
+ break;
+ }
+ }
+ }
+
+ // Starting from the high order. Turn on each bit in turn. If it being turned on pushes it past the max of the other side
+ // then we know it must be turned off.
+ for (int i = c0.getWidth() - 1 - 1; i >= 0; i--)
+ {
+ if (!c1.isFixed(i)) // bit is variable.
+ {
+ // turn it on in the minimum.
+ CONSTANTBV::BitVector_Bit_Off(c1_max, i);
+ if (signedCompare(c1_max, c0_min) < 0)
+ {
+ c1.setFixed(i, true);
+ c1.setValue(i, true);
+ setSignedMinMax(c1, c1_min, c1_max);
+ }
+ else
+ {
+ CONSTANTBV::BitVector_Bit_On(c1_max, i);
+ break;
+ }
+ }
+ }
+ }
+
+ destroy(c0_min, c0_max, c1_min, c1_max);
+ return NOT_IMPLEMENTED;
+}
+
+///////////////////////// UNSIGNED.
+
+
+
+
+// UNSIGNED!!
+Result bvLessThanBothWays(FixedBits& c0, FixedBits &c1, FixedBits& output)
+{
+ Result r = NO_CHANGE;
+
+ assert(c0.getWidth() == c1.getWidth());
+
+ CBV c0_min = CONSTANTBV::BitVector_Create(c0.getWidth(), true);
+ CBV c0_max = CONSTANTBV::BitVector_Create(c0.getWidth(), true);
+ CBV c1_min = CONSTANTBV::BitVector_Create(c0.getWidth(), true);
+ CBV c1_max = CONSTANTBV::BitVector_Create(c0.getWidth(), true);
+
+ setUnsignedMinMax(c0, c0_min, c0_max);
+ setUnsignedMinMax(c1, c1_min, c1_max);
+
+ // EG. [0,5] < [6,8]. i.e. max of first is less than min of second.
+ if (unsignedCompare(c0_max, c1_min) < 0)
+ {
+ if (output.isFixed(0) && !output.getValue(0)) // output is fixed to false.
+ {
+ destroy(c0_min, c0_max, c1_min, c1_max);
+ return CONFLICT;
+ }
+
+ if (!output.isFixed(0))
+ {
+ output.setFixed(0, true);
+ output.setValue(0, true);
+ }
+ }
+
+ // EG. [3,5] < [0,1].
+ if (unsignedCompare(c0_min, c1_max) >= 0)
+ {
+ // min is greater than max.
+ if (output.isFixed(0) && output.getValue(0))
+ {
+ destroy(c0_min, c0_max, c1_min, c1_max);
+ return CONFLICT;
+ }
+
+ if (!output.isFixed(0))
+ {
+ output.setFixed(0, true);
+ output.setValue(0, false);
+ }
+ }
+
+ // If true. Reverse and send to the other.
+ if (output.isFixed(0) && !output.getValue(0))
+ {
+ FixedBits t(1, true);
+ t.setFixed(0, true);
+ t.setValue(0, true);
+ destroy(c0_min, c0_max, c1_min, c1_max);
+ return bvGreaterThanEqualsBothWays(c0, c1, t);
+ }
+
+ bool changed = false;
+
+ if (output.isFixed(0) && output.getValue(0))
+ {
+ // Starting from the high order. Turn on each bit in turn. If it being turned on pushes it past the max of the other side
+ // then we know it must be turned off.
+ for (int i = c0.getWidth() - 1; i >= 0; i--)
+ {
+ if (!c0.isFixed(i)) // bit is variable.
+ {
+ // turn it on in the minimum.
+ CONSTANTBV::BitVector_Bit_On(c0_min, i);
+ if (unsignedCompare(c0_min, c1_max) >= 0)
+ {
+ c0.setFixed(i, true);
+ c0.setValue(i, false);
+ setUnsignedMinMax(c0, c0_min, c0_max);
+ changed = true;
+ }
+ else
+ {
+ CONSTANTBV::BitVector_Bit_Off(c0_min, i);
+ break;
+ }
+ }
+ }
+
+ for (int i = c1.getWidth() - 1; i >= 0; i--)
+ {
+ if (!c1.isFixed(i)) // bit is variable.
+ {
+ CONSTANTBV::BitVector_Bit_Off(c1_max, i);
+ if (unsignedCompare(c1_max, c0_min) <= 0)
+ {
+ c1.setFixed(i, true);
+ c1.setValue(i, true);
+ setUnsignedMinMax(c1, c1_min, c1_max);
+ changed = true;
+ }
+ else
+ {
+ CONSTANTBV::BitVector_Bit_On(c1_max, i);
+ break;
+ }
+ }
+ }
+ }
+
+ destroy(c0_min, c0_max, c1_min, c1_max);
+ return NOT_IMPLEMENTED;
+}
+
+Result bvLessThanEqualsBothWays(FixedBits& c0, FixedBits &c1, FixedBits& output)
+{
+ Result r = NO_CHANGE;
+
+ assert(c0.getWidth() == c1.getWidth());
+
+ CBV c0_min = CONSTANTBV::BitVector_Create(c0.getWidth(), true);
+ CBV c0_max = CONSTANTBV::BitVector_Create(c0.getWidth(), true);
+ CBV c1_min = CONSTANTBV::BitVector_Create(c0.getWidth(), true);
+ CBV c1_max = CONSTANTBV::BitVector_Create(c0.getWidth(), true);
+
+ setUnsignedMinMax(c0, c0_min, c0_max);
+ setUnsignedMinMax(c1, c1_min, c1_max);
+
+ // EG. [0,5] <= [6,8]. i.e. max of first is less than min of second.
+ if (unsignedCompare(c0_max, c1_min) <= 0)
+ {
+ if (output.isFixed(0) && !output.getValue(0)) // output is fixed to false.
+ {
+ destroy(c0_min, c0_max, c1_min, c1_max);
+ return CONFLICT;
+ }
+
+ if (!output.isFixed(0))
+ {
+ output.setFixed(0, true);
+ output.setValue(0, true);
+ }
+ }
+
+ // EG. [3,5] <= [0,1].
+ if (unsignedCompare(c0_min, c1_max) > 0)
+ {
+ if (output.isFixed(0) && output.getValue(0))
+ {
+ destroy(c0_min, c0_max, c1_min, c1_max);
+ return CONFLICT;
+ }
+
+ if (!output.isFixed(0))
+ {
+ output.setFixed(0, true);
+ output.setValue(0, false);
+ }
+ }
+
+ // If true. Reverse and send to the other..
+ if (output.isFixed(0) && !output.getValue(0))
+ {
+ FixedBits t(1, true);
+ t.setFixed(0, true);
+ t.setValue(0, true);
+ destroy(c0_min, c0_max, c1_min, c1_max);
+ return bvGreaterThanBothWays(c0, c1, t);
+ }
+
+ // We only deal with the true case in this function.
+
+ if (output.isFixed(0) && output.getValue(0))
+ {
+ // Starting from the high order. Turn on each bit in turn. If it being turned on pushes it past the max of the other side
+ // then we know it must be turned off.
+ for (int i = c0.getWidth() - 1; i >= 0; i--)
+ {
+ if (!c0.isFixed(i)) // bit is variable.
+ {
+ // turn it on in the minimum.
+ CONSTANTBV::BitVector_Bit_On(c0_min, i);
+ if (unsignedCompare(c0_min, c1_max) > 0)
+ {
+ c0.setFixed(i, true);
+ c0.setValue(i, false);
+ setUnsignedMinMax(c0, c0_min, c0_max);
+ }
+ else
+ {
+ CONSTANTBV::BitVector_Bit_Off(c0_min, i);
+ break;
+ }
+ }
+ }
+
+ // Starting from the high order. Turn on each bit in turn. If it being turned on pushes it past the max of the other side
+ // then we know it must be turned off.
+ for (int i = c0.getWidth() - 1; i >= 0; i--)
+ {
+ if (!c1.isFixed(i)) // bit is variable.
+ {
+ // turn it on in the minimum.
+ CONSTANTBV::BitVector_Bit_Off(c1_max, i);
+ if (unsignedCompare(c1_max, c0_min) < 0)
+ {
+ c1.setFixed(i, true);
+ c1.setValue(i, true);
+ setUnsignedMinMax(c1, c1_min, c1_max);
+ }
+ else
+ {
+ CONSTANTBV::BitVector_Bit_On(c1_max, i);
+ break;
+ }
+ }
+ }
+ }
+ destroy(c0_min, c0_max, c1_min, c1_max);
+ return NOT_IMPLEMENTED;
+}
+
+}
+}
--- /dev/null
+#include "ConstantBitP_TransferFunctions.h"
+#include "ConstantBitP_Utility.h"
+#include "../../extlib-constbv/constantbv.h"
+
+// Left shift, right shift.
+// Trevor Hansen. BSD License.
+
+// smtlib & x86 semantics differ for what happens when a value is shifted by greater
+// than the bitWidth. On x86, in 64-bit mode, only the bottom 6 bits of the shift are
+// used. In SMTLIB the total value is used.
+
+
+namespace simplifier
+{
+namespace constantBitP
+{
+
+const bool debug_shift = false;
+
+Result bvRightShiftBothWays(vector<FixedBits*>& children, FixedBits& output)
+{
+ Result result = NO_CHANGE;
+ const unsigned bitWidth = output.getWidth();
+
+ assert(2 == children.size());
+
+ FixedBits& op = *children[0];
+ FixedBits& shift = *children[1];
+
+ FixedBits outputReverse(bitWidth,false);
+ FixedBits opReverse(bitWidth,false);
+
+ // Reverse the output and the input.
+ for (unsigned i =0; i < bitWidth;i++)
+ {
+ if (op.isFixed(i))
+ {
+ opReverse.setFixed(bitWidth-1-i,true);
+ opReverse.setValue(bitWidth-1-i,op.getValue(i));
+ }
+
+ if (output.isFixed(i))
+ {
+ outputReverse.setFixed(bitWidth-1-i,true);
+ outputReverse.setValue(bitWidth-1-i,output.getValue(i));
+ }
+ }
+
+ vector<FixedBits*> args;
+ args.push_back(&opReverse);
+ args.push_back(&shift); // shift is unmodified.
+ result = bvLeftShiftBothWays(args, outputReverse);
+
+ if (CONFLICT == result)
+ return CONFLICT;
+
+ // Now write the reversed values back.
+ // Reverse the output and the input.
+ for (unsigned i =0; i < bitWidth;i++)
+ {
+ if (opReverse.isFixed(i) && !op.isFixed(bitWidth-1-i))
+ {
+ op.setFixed(bitWidth-1-i,true);
+ op.setValue(bitWidth-1-i,opReverse.getValue(i));
+ }
+
+ if (outputReverse.isFixed(i) && !output.isFixed(bitWidth-1-i))
+ {
+ output.setFixed(bitWidth-1-i,true);
+ output.setValue(bitWidth-1-i,outputReverse.getValue(i));
+ }
+ }
+
+ return result;
+}
+
+// Converts the array of possible shifts into a set that represents the values.
+FixedBits getPossible(unsigned bitWidth, bool possibleShift[], unsigned numberOfPossibleShifts, const FixedBits& shift)
+{
+ FixedBits v(bitWidth, false);
+ bool first = true;
+ for (unsigned i = 0; i < numberOfPossibleShifts - 1; i++)
+ {
+ if (possibleShift[i])
+ {
+ if (first)
+ {
+ first = false;
+ for (unsigned j = 0; j < (unsigned) v.getWidth(); j++)
+ {
+ v.setFixed(j, true);
+ if (j < sizeof(unsigned) * 8)
+ v.setValue(j, 0 != (i & (1 << j)));
+ else
+ v.setValue(j, false);
+ }
+ }
+ else
+ {
+ // join.
+ for (unsigned j = 0; j < (unsigned) v.getWidth() && j
+ < sizeof(unsigned) * 8; j++)
+ {
+ if (v.isFixed(j))
+ {
+ // union.
+ if (v.getValue(j) != (0 != (i & (1 << j))))
+ v.setFixed(j, false);
+ }
+ }
+ }
+ }
+ }
+
+ unsigned firstShift;
+ for (firstShift=0; firstShift<numberOfPossibleShifts; firstShift++)
+ if (possibleShift[firstShift])
+ break;
+
+
+ // The top most entry of the shift table is special. It means all values of shift
+ // that fill it completely with zeroes /ones. We take the union of all of the values >bitWidth
+ // in this function.
+ if (possibleShift[numberOfPossibleShifts - 1])
+ {
+ FixedBits bitWidthFB = FixedBits::fromUnsignedInt(bitWidth, bitWidth);
+ FixedBits output(1, true);
+ output.setFixed(0, true);
+ output.setValue(0, true);
+ FixedBits working(shift);
+
+ vector<FixedBits*> args;
+ args.push_back(&working);
+ args.push_back(&bitWidthFB);
+
+ //Write into working anything that can be determined given it's >=bitWidth.
+ Result r = bvGreaterThanEqualsBothWays(args,output);
+ assert(CONFLICT != r);
+
+ // Get the union of "working" with the prior union.
+ for (unsigned i = 0; i < bitWidth; i++)
+ {
+ if (!working.isFixed(i) && v.isFixed(i))
+ v.setFixed(i, false);
+ if (working.isFixed(i) && v.isFixed(i) && (working.getValue(i) != v.getValue(i)))
+ v.setFixed(i, false);
+ if (firstShift == numberOfPossibleShifts - 1) // no less shifts possible.
+ {
+ if (working.isFixed(i))
+ {
+ v.setFixed(i, true);
+ v.setValue(i, working.getValue(i));
+ }
+ }
+ }
+ }
+
+ if (debug_shift)
+ cerr << "Set of possible shifts:" << v << endl;
+
+ return v;
+}
+
+
+unsigned getMaxShiftFromValueViaAlternation(const unsigned bitWidth, const FixedBits& output)
+{
+ unsigned maxShiftFromValue = UINT_MAX;
+
+ // The shift must be less than the position of the first alternation.
+ bool foundTrue = false;
+ bool foundFalse = false;
+ for (int i = bitWidth - 1; i >= 0; i--)
+ {
+ if (output.isFixed(i))
+ {
+ if (output.getValue(i) && foundFalse)
+ {
+ maxShiftFromValue = i;
+ break;
+ }
+ if (!output.getValue(i) && foundTrue)
+ {
+ maxShiftFromValue = i;
+ break;
+ }
+ if (output.getValue(i))
+ foundTrue = true;
+ else if (!output.getValue(i))
+ foundFalse = true;
+ }
+ }
+
+ if (maxShiftFromValue != UINT_MAX)
+ maxShiftFromValue = bitWidth - 2 - maxShiftFromValue;
+
+ return maxShiftFromValue;
+}
+
+Result bvArithmeticRightShiftBothWays(vector<FixedBits*>& children, FixedBits& output)
+{
+ const unsigned bitWidth = output.getWidth();
+ assert(2== children.size());
+ assert(bitWidth > 0);
+ assert(children[0]->getWidth() == children[1]->getWidth());
+ const unsigned MSBIndex = bitWidth-1;
+
+ Result result = NO_CHANGE;
+
+ FixedBits& op = *children[0];
+ FixedBits& shift = *children[1];
+
+ // If the MSB isn't set, create a copy with it set each way and take the meet.
+ if (!op.isFixed(MSBIndex))
+ {
+ vector<FixedBits*> children1;
+ vector<FixedBits*> children2;
+ FixedBits op1(op);
+ FixedBits op2(op);
+ FixedBits shift1(shift);
+ FixedBits shift2(shift);
+ FixedBits output1(output);
+ FixedBits output2(output);
+
+ children1.push_back(&op1);
+ children1.push_back(&shift1);
+ op1.setFixed(MSBIndex, true);
+ op1.setValue(MSBIndex, true);
+
+ children2.push_back(&op2);
+ children2.push_back(&shift2);
+ op2.setFixed(MSBIndex, true);
+ op2.setValue(MSBIndex, false);
+
+ Result r1 = bvArithmeticRightShiftBothWays(children1, output1);
+ Result r2 = bvArithmeticRightShiftBothWays(children2, output2);
+
+ if (r1 == CONFLICT && r2 == CONFLICT)
+ return CONFLICT;
+
+ if (r1 == CONFLICT)
+ {
+ op = op2;
+ shift = shift2;
+ output = output2;
+ return r2;
+ }
+
+ if (r2 == CONFLICT)
+ {
+ op = op1;
+ shift = shift1;
+ output = output1;
+ return r1;
+ }
+
+ op = FixedBits::meet(op1,op2);
+ shift = FixedBits::meet(shift1,shift2);
+ output = FixedBits::meet(output1,output2);
+ return r1;
+
+ }
+
+ assert(op.isFixed(MSBIndex));
+
+ if (debug_shift)
+ {
+ cerr << "=========" << endl;
+ cerr << op << " >a> ";
+ cerr << shift;
+ cerr << " = " << output << endl;
+ }
+
+ // The topmost number of possible shifts corresponds to all
+ // the values of shift that shift out everything.
+ // i.e. possibleShift[bitWidth+1] is the SET of all operations that shift past the end.
+ const unsigned numberOfPossibleShifts = bitWidth + 1;
+ bool possibleShift[numberOfPossibleShifts];
+ for (unsigned i = 0; i < numberOfPossibleShifts; i++)
+ possibleShift[i] = false;
+
+
+ // If either of the top two bits are fixed they should be equal.
+ if (op.isFixed(MSBIndex) ^ output.isFixed(MSBIndex))
+ {
+ if (op.isFixed(MSBIndex))
+ {
+ output.setFixed(MSBIndex, true);
+ output.setValue(MSBIndex, op.getValue(MSBIndex));
+ }
+
+ if (output.isFixed(MSBIndex))
+ {
+ op.setFixed(MSBIndex, true);
+ op.setValue(MSBIndex, output.getValue(MSBIndex));
+ }
+ }
+
+ // Both the MSB of the operand and the output should be fixed now..
+ assert(output.isFixed(MSBIndex));
+
+ unsigned minShiftFromShift, maxShiftFromShift; // The range of the "shift" value.
+ shift.getUnsignedMinMax(minShiftFromShift, maxShiftFromShift);
+
+ // The shift can't be any bigger than the topmost alternation in the output.
+ // For example if the output is 0.01000, then the shift can not be bigger than
+ // 3.
+ unsigned maxShiftFromOutput = getMaxShiftFromValueViaAlternation(bitWidth, output);
+
+ maxShiftFromShift = std::min(maxShiftFromShift, (unsigned) maxShiftFromOutput);
+
+ if (debug_shift)
+ {
+ cerr << "minshift:" << minShiftFromShift << endl;
+ cerr << "maxshift:" << maxShiftFromShift << endl;
+ cerr << "total:" << maxShiftFromShift << endl;
+ }
+
+
+ for (unsigned i = minShiftFromShift; i <= std::min(bitWidth, maxShiftFromShift); i++)
+ {
+ // if the bit-pattern of 'i' is in the set represented by the 'shift'.
+ if (shift.unsignedHolds(i))
+ possibleShift[i] = true;
+ }
+
+ // Complication. Given a shift like [.1] possibleShift[2] is now false.
+ // A shift of 2 isn't possible. But one of three is.
+ // possibleShift[2] means any shift >=2 is possible. So it needs to be set
+ // to true.
+ {
+ if (maxShiftFromShift >= bitWidth)
+ possibleShift[bitWidth] = true;
+ }
+
+ // Now check one-by-one each shifting.
+ // If we are shifting a zero to where a one is (say), then that shifting isn't possible.
+ for (unsigned shiftIt = minShiftFromShift; shiftIt < numberOfPossibleShifts; shiftIt++)
+ {
+ if (possibleShift[shiftIt])
+ {
+ for (unsigned column = 0; column < bitWidth; column++)
+ {
+ // if they are fixed to different values. That's wrong.
+ if (column + shiftIt <= bitWidth - 1)
+ {
+ if (output.isFixed(column) && op.isFixed(column + shiftIt)
+ && (output.getValue(column) != op.getValue(column
+ + shiftIt)))
+ {
+ possibleShift[shiftIt] = false;
+ break;
+ }
+ }
+ }
+ }
+ }
+
+ int nOfPossibleShifts = 0;
+ for (unsigned i = 0; i < numberOfPossibleShifts; i++)
+ {
+ if (possibleShift[i])
+ {
+ nOfPossibleShifts++;
+ maxShiftFromShift = i;
+ if (debug_shift)
+ {
+ std::cerr << "Possible Shift:" << i << std::endl;
+ }
+ }
+ }
+
+ if (debug_shift)
+ {
+ std::cerr << "Number of possible shifts:" << nOfPossibleShifts << endl;
+ }
+
+ // If it's empty. It's a conflict.
+ if (0 == nOfPossibleShifts)
+ {
+ return CONFLICT;
+ }
+
+ // We have a list of all the possible shift amounts.
+ // We take the union of all the bits that are possible.
+ FixedBits setOfPossibleShifts = getPossible(bitWidth, possibleShift, numberOfPossibleShifts,shift);
+
+ // Write in any fixed values to the shift.
+ for (unsigned i = 0; i < bitWidth; i++)
+ {
+ if (setOfPossibleShifts.isFixed(i))
+ {
+ if (!shift.isFixed(i))
+ {
+ shift.setFixed(i, true);
+ shift.setValue(i, setOfPossibleShifts.getValue(i));
+ result = CHANGED;
+ }
+ else if (shift.isFixed(i) && shift.getValue(i)
+ != setOfPossibleShifts.getValue(i))
+ {
+ return CONFLICT;
+ }
+ }
+ }
+
+ // If a particular input bit appears in every possible shifting,
+ // and if that bit is unfixed,
+ // and if the result it is fixed to the same value in every position.
+ // Then, that bit must be fixed.
+ // E.g. [--] << [0-] == [00]
+
+ bool candidates[bitWidth];
+ for (unsigned i = 0; i < bitWidth; i++)
+ {
+ candidates[i] = !op.isFixed(i);
+ }
+
+ // candidates: So far: the bits that are unfixed in the operand.
+
+ for (unsigned i = 0; i < numberOfPossibleShifts; i++)
+ {
+ if (possibleShift[i])
+ {
+ // If this shift is possible, then some bits will be shifted out.
+ for (unsigned j = 0; j < i; j++)
+ candidates[j] = false;
+ }
+ }
+
+ // candidates: So far: + the input bits that are unfixed.
+ // + the input bits that are in every possible fixing.
+
+ // Check all candidates have the same output values.
+ for (unsigned candidate = 0; candidate < bitWidth; candidate++)
+ {
+ bool first = true;
+ bool setTo = false; // value that's never read. To quieten gcc.
+
+ if (candidates[candidate])
+ {
+ for (unsigned shiftIT = 0; shiftIT < bitWidth; shiftIT++)
+ {
+ // If the shift isn't possible continue.
+ if (!possibleShift[shiftIT])
+ continue;
+
+ if (shiftIT > candidate)
+ continue;
+
+ unsigned idx = candidate - shiftIT;
+
+ if (!output.isFixed(idx))
+ {
+ candidates[candidate] = false;
+ break;
+ }
+ else
+ {
+ if (first)
+ {
+ first = false;
+ setTo = output.getValue(idx);
+ }
+ else
+ {
+ if (setTo != output.getValue(idx))
+ {
+ candidates[candidate] = false;
+ break;
+ }
+
+ }
+ }
+ }
+ }
+
+ if (candidates[candidate])
+ {
+ assert(!op.isFixed(candidate));
+ op.setFixed(candidate, true);
+ op.setValue(candidate, setTo);
+ }
+ }
+
+ if (debug_shift)
+ {
+ cerr << op << " >a> ";
+ cerr << shift;
+ cerr << " = " << output << endl;
+ }
+
+ // Go through each of the possible shifts. If the same value is fixed
+ // at every location. Then it's fixed too in the result.
+ // Looping over the output columns.
+ bool MSBValue = op.getValue(MSBIndex);
+
+ for (unsigned column = 0; column < bitWidth; column++)
+ {
+ bool allFixedToSame = true;
+ bool allFixedTo = false; // value that's never read. To quieten gcc.
+ bool first = true;
+
+ for (unsigned shiftIt = 0; (shiftIt < numberOfPossibleShifts)
+ && allFixedToSame; shiftIt++)
+ {
+ if (possibleShift[shiftIt])
+ {
+ // Will have shifted in something..
+ if (shiftIt > (bitWidth - 1 -column))
+ {
+ if (first)
+ {
+ allFixedTo = MSBValue;
+ first = false;
+ }
+ else
+ {
+ if (allFixedTo != MSBValue)
+ {
+ allFixedToSame = false;
+ }
+ }
+ }
+ else
+ {
+ unsigned index = column + shiftIt;
+ if (!op.isFixed(index))
+ allFixedToSame = false;
+ else if (first && op.isFixed(index))
+ {
+ first = false;
+ allFixedTo = op.getValue(index);
+ }
+ if (op.isFixed(index) && allFixedTo != op.getValue(
+ index))
+ allFixedToSame = false;
+ }
+ }
+ }
+
+ // If it can be just one possible value. Then we can fix 'em.
+ if (allFixedToSame)
+ {
+ if (output.isFixed(column) && (output.getValue(column)
+ != allFixedTo))
+ {
+ return CONFLICT;
+ }
+ if (!output.isFixed(column))
+ {
+ output.setFixed(column, true);
+ output.setValue(column, allFixedTo);
+ result = CHANGED;
+ }
+ }
+ }
+ return NOT_IMPLEMENTED;
+}
+
+Result bvLeftShiftBothWays(vector<FixedBits*>& children, FixedBits& output)
+{
+ const unsigned bitWidth = output.getWidth();
+ assert(2== children.size());
+ assert(bitWidth > 0);
+
+ Result result = NO_CHANGE;
+
+ FixedBits& op = *children[0];
+ FixedBits& shift = *children[1];
+
+ if (debug_shift)
+ {
+ cerr << "op:" << op << endl;
+ cerr << "shift:" << shift << endl;
+ cerr << "output:" << output << endl;
+ }
+
+ // The topmost number of possible shifts corresponds to all
+ // the values of shift that shift out everything.
+ // i.e. possibleShift[bitWidth+1] is the SET of all operations that shift past the end.
+ const unsigned numberOfPossibleShifts = bitWidth + 1;
+ bool possibleShift[numberOfPossibleShifts];
+ for (unsigned i = 0; i < numberOfPossibleShifts; i++)
+ possibleShift[i] = false;
+
+ unsigned minShift, maxShift;
+ shift.getUnsignedMinMax(minShift,maxShift);
+
+ // The shift must be less than the position of the first one in the output
+ int positionOfFirstOne = -1;
+ for (unsigned i = 0; i < bitWidth; i++)
+ {
+ if (output.isFixed(i) && output.getValue(i))
+ {
+ positionOfFirstOne = i;
+ break;
+ }
+ }
+
+ if (positionOfFirstOne >= 0)
+ {
+ if ((unsigned) positionOfFirstOne < minShift)
+ return CONFLICT;
+
+ maxShift = std::min(maxShift, (unsigned) positionOfFirstOne);
+ }
+
+ for (unsigned i = minShift; i <= std::min(bitWidth, maxShift); i++)
+ {
+ // if the bit-pattern of 'i' is in the set represented by the 'shift'.
+ if (shift.unsignedHolds(i))
+ possibleShift[i] = true;
+ }
+
+ // Complication. Given a shift like [-1]. possibleShift[2] is now false.
+ // A shift of 2 isn't possible. But one of three is.
+ // possibleShift[2] means any shift >=2 is possible. So it needs to be set
+ // to true.
+ {
+ if (maxShift >= bitWidth)
+ possibleShift[bitWidth] = true;
+ }
+
+ // Now check one-by-one each shifting.
+ // If we are shifting a zero to where a one is (say), then that shifting isn't possible.
+ for (unsigned shiftIt = 0; shiftIt < numberOfPossibleShifts; shiftIt++)
+ {
+ if (possibleShift[shiftIt])
+ {
+ for (unsigned column = 0; column < bitWidth; column++)
+ {
+ if (column < shiftIt)
+ {
+ if (output.isFixed(column) && output.getValue(column)) // output is one in the column. That's wrong.
+ {
+ possibleShift[shiftIt] = false;
+ break;
+ }
+ }
+ else
+ {
+ // if they are fixed to different values. That's wrong.
+ if (output.isFixed(column) && op.isFixed(column - shiftIt) && (output.getValue(column) != op.getValue(column - shiftIt)))
+ {
+ possibleShift[shiftIt] = false;
+ break;
+ }
+ }
+ }
+ }
+ }
+
+ int nOfPossibleShifts = 0;
+ int shiftIndex = 0;
+ for (unsigned i = 0; i < numberOfPossibleShifts; i++)
+ {
+ if (possibleShift[i])
+ {
+ nOfPossibleShifts++;
+ shiftIndex = i;
+ if (debug_shift)
+ {
+ std::cerr << "Possible:" << i << std::endl;
+ }
+ }
+ }
+
+ if (debug_shift)
+ {
+ std::cerr << "Number of possible shifts:" << nOfPossibleShifts << endl;
+ }
+
+ // If it's empty. It's a conflict.
+ if (0 == nOfPossibleShifts)
+ return CONFLICT;
+
+ // We have a list of all the possible shift amounts.
+ // We take the union of all the bits that are possible.
+
+ FixedBits v(bitWidth, false);
+ bool first = true;
+ for (unsigned i = 0; i < numberOfPossibleShifts-1; i++)
+ {
+ if (possibleShift[i])
+ {
+ if (first)
+ {
+ first = false;
+ for (unsigned j = 0; j < (unsigned) v.getWidth(); j++)
+ {
+ v.setFixed(j, true);
+ if (j < sizeof(unsigned)*8)
+ v.setValue(j, 0 != (i & (1 << j)));
+ else
+ v.setValue(j, false);
+ }
+ }
+ else
+ {
+ // join.
+ for (unsigned j = 0; j < (unsigned) v.getWidth() && j < sizeof(unsigned)*8; j++)
+ {
+ if (v.isFixed(j))
+ {
+ // union.
+ if (v.getValue(j) != (0!=(i & (1 << j))))
+ v.setFixed(j, false);
+ }
+ }
+ }
+ }
+ }
+
+ // The top most entry of the shift table is special. It means all values of shift
+ // that fill it completely with zeroes. We take the union of all of the values >bitWidth
+ // in this function.
+ if (possibleShift[numberOfPossibleShifts - 1])
+ {
+ FixedBits bitWidthFB = FixedBits::fromUnsignedInt(bitWidth, bitWidth);
+ FixedBits output(1, true);
+ output.setFixed(0, true);
+ output.setValue(0, true);
+ FixedBits working(shift);
+
+ vector<FixedBits*> args;
+ args.push_back(&working);
+ args.push_back(&bitWidthFB);
+
+ //Write into working anything that can be determined given it's >=bitWidth.
+ Result r = bvGreaterThanEqualsBothWays(args,output);
+ assert(CONFLICT != r);
+
+ // Get the union of "working" with the prior union.
+ for (unsigned i = 0; i < bitWidth; i++)
+ {
+ if (!working.isFixed(i) && v.isFixed(i))
+ v.setFixed(i, false);
+ if (working.isFixed(i) && v.isFixed(i) && (working.getValue(i) != v.getValue(i)))
+ v.setFixed(i, false);
+ if (first) // no less shifts possible.
+ {
+ if (working.isFixed(i))
+ {
+ v.setFixed(i, true);
+ v.setValue(i, working.getValue(i));
+ }
+ }
+ }
+ }
+
+ if (debug_shift)
+ {
+ std::cerr << "Shift Amount:" << v << std::endl;
+ }
+
+ for (unsigned i = 0; i < bitWidth; i++)
+ {
+ if (v.isFixed(i))
+ {
+ if (!shift.isFixed(i))
+ {
+ shift.setFixed(i, true);
+ shift.setValue(i, v.getValue(i));
+ result = CHANGED;
+ }
+ else if (shift.isFixed(i) && shift.getValue(i) != v.getValue(i))
+ return CONFLICT;
+ }
+ }
+
+ // If a particular input bit appears in every possible shifting,
+ // and if that bit is unfixed,
+ // and if the result it is fixed to the same value in every position.
+ // Then, that bit must be fixed.
+ // E.g. [--] << [0-] == [00]
+
+ bool candidates[bitWidth];
+ for (unsigned i = 0; i < bitWidth; i++)
+ {
+ candidates[i] = !op.isFixed(i);
+ }
+
+ // candidates: So far: the bits that are unfixed.
+
+ for (unsigned i = 0; i < numberOfPossibleShifts; i++)
+ {
+ if (possibleShift[i])
+ {
+ // If this shift is possible, then some bits will be shifted out.
+ for (unsigned j = 0; j < i; j++)
+ candidates[bitWidth - 1 - j] = false;
+ }
+ }
+
+ // candidates: So far: + the input bits that are unfixed.
+ // + the input bits that are in every possible fixing.
+
+ // Check all candidates have the same output values.
+ for (unsigned candidate = 0; candidate < bitWidth; candidate++)
+ {
+ bool first = true;
+ bool setTo = false; // value that's never read. To quieten gcc.
+
+ if (candidates[candidate])
+ {
+ for (unsigned shiftIT = 0; shiftIT < bitWidth; shiftIT++)
+ {
+ // If the shift isn't possible continue.
+ if (!possibleShift[shiftIT])
+ continue;
+
+ unsigned idx = candidate + shiftIT;
+
+ if (!output.isFixed(idx))
+ {
+ candidates[candidate] = false;
+ break;
+ }
+ else
+ {
+ if (first)
+ {
+ first = false;
+ setTo = output.getValue(idx);
+ }
+ else
+ {
+ if (setTo != output.getValue(idx))
+ {
+ candidates[candidate] = false;
+ break;
+ }
+
+ }
+ }
+ }
+ }
+
+ if (candidates[candidate])
+ {
+ assert(!op.isFixed(candidate));
+ op.setFixed(candidate, true);
+ op.setValue(candidate, setTo);
+ }
+ }
+
+ // done.
+
+ // Go through each of the possible shifts. If the same value is fixed
+ // at every location. Then it's fixed too in the result.
+ for (unsigned column = 0; column < bitWidth; column++)
+ {
+ bool allFixedToSame = true;
+ bool allFixedTo = false; // value that's never read. To quieten gcc.
+ bool first = true;
+
+ for (unsigned shiftIt = minShift; (shiftIt < numberOfPossibleShifts) && allFixedToSame; shiftIt++)
+ {
+ if (possibleShift[shiftIt])
+ {
+ // Will have shifted in zeroes.
+ if (shiftIt > column)
+ {
+ if (first)
+ {
+ allFixedTo = false;
+ first = false;
+ }
+ else
+ {
+ if (allFixedTo)
+ {
+ allFixedToSame = false;
+ }
+ }
+ }
+ else
+ {
+ unsigned index = column - shiftIt;
+ if (!op.isFixed(index))
+ allFixedToSame = false;
+ else if (first && op.isFixed(index))
+ {
+ first = false;
+ allFixedTo = op.getValue(index);
+ }
+ if (op.isFixed(index) && allFixedTo != op.getValue(index))
+ allFixedToSame = false;
+ }
+ }
+ }
+
+ // If it can be just one possible value. Then we can fix 'em.
+ if (allFixedToSame)
+ {
+ if (output.isFixed(column) && (output.getValue(column) != allFixedTo))
+ return CONFLICT;
+ if (!output.isFixed(column))
+ {
+ output.setFixed(column, true);
+ output.setValue(column, allFixedTo);
+ result = CHANGED;
+ }
+ }
+ }
+
+ /*
+ // If there is only one possible shift value. Then, we can push from the output back.
+ if (1 == nOfPossibleShifts)
+ {
+ for (unsigned i = shiftIndex; i < bitWidth; i++)
+ {
+ if (!op.isFixed(i - shiftIndex) && output.isFixed(i))
+ {
+ op.setFixed(i - shiftIndex, true);
+ op.setValue(i - shiftIndex, output.getValue(i));
+ result = CHANGED;
+ }
+ }
+ }
+*/
+
+ return NOT_IMPLEMENTED;
+}
+
+}
+}
--- /dev/null
+#include "ConstantBitP_TransferFunctions.h"
+#include "ConstantBitP_Utility.h"
+
+namespace simplifier
+{
+namespace constantBitP
+{
+
+namespace BEEV
+{
+typedef unsigned int * CBV;
+}
+
+// Misc (easy) transfer functions.
+// Trevor Hansen. BSD License.
+
+// if the result is fixed to true. Then fix a==b.
+// if the result is fixed to false, there is a single unspecied value, and all the rest are the same. Fix it to the opposite.
+
+// if a==b then fix the result to true.
+// if a!=b then fix the result to false.
+Result bvEqualsBothWays(FixedBits& a, FixedBits& b, FixedBits& output)
+{
+ assert(a.getWidth() == b.getWidth());
+ assert(1 == output.getWidth());
+
+ const int childWidth = a.getWidth();
+
+ Result r = NO_CHANGE;
+
+ bool allSame = true;
+ bool definatelyFalse = false;
+
+ for (int i = 0; i < childWidth; i++)
+ {
+ // if both fixed
+ if (a.isFixed(i) && b.isFixed(i))
+ {
+ // And have different values.
+ if (a.getValue(i) != b.getValue(i))
+ {
+ definatelyFalse = true;
+ }
+ else
+ {
+ allSame &= true;
+ continue;
+ }
+ }
+ allSame &= false;
+ }
+
+ if (definatelyFalse)
+ {
+ if (output.isFixed(0) && output.getValue(0))
+ {
+ return CONFLICT;
+ }
+ else if (!output.isFixed(0))
+ {
+ output.setFixed(0, true);
+ output.setValue(0, false);
+ r = CHANGED;
+ }
+ }
+ else if (allSame)
+ {
+ if (output.isFixed(0) && !output.getValue(0))
+ {
+ return CONFLICT;
+ }
+ else if (!output.isFixed(0))
+ {
+ output.setFixed(0, true);
+ output.setValue(0, true);
+ r = CHANGED;
+ }
+ }
+
+ if (output.isFixed(0) && output.getValue(0)) // all should be the same.
+ {
+ for (int i = 0; i < childWidth; i++)
+ {
+ if (a.isFixed(i) && b.isFixed(i))
+ {
+ if (a.getValue(i) != b.getValue(i))
+ {
+ return CONFLICT;
+ }
+ }
+ else if (a.isFixed(i) != b.isFixed(i)) // both same but only one is fixed.
+ {
+ if (a.isFixed(i))
+ {
+ b.setFixed(i, true);
+ b.setValue(i, a.getValue(i));
+ r = CHANGED;
+ }
+ else
+ {
+ a.setFixed(i, true);
+ a.setValue(i, b.getValue(i));
+ r = CHANGED;
+ }
+ }
+ }
+ }
+
+ // if the result is fixed to false, there is a single unspecied value, and all the rest are the same. Fix it to the opposite.
+ if (output.isFixed(0) && !output.getValue(0))
+ {
+ int unknown = 0;
+
+ for (int i = 0; i < childWidth; i++)
+ {
+ if (!a.isFixed(i))
+ unknown++;
+ if (!b.isFixed(i))
+ unknown++;
+ else if (a.isFixed(i) && b.isFixed(i) && a.getValue(i) != b.getValue(i))
+ {
+ unknown = 10; // hack, don't do the next loop.
+ break;
+ }
+ }
+
+ if (1 == unknown)
+ {
+ for (int i = 0; i < childWidth; i++)
+ {
+ if (!a.isFixed(i))
+ {
+ a.setFixed(i, true);
+ a.setValue(i, !b.getValue(i));
+ r = CHANGED;
+ }
+ if (!b.isFixed(i))
+ {
+ b.setFixed(i, true);
+ b.setValue(i, !a.getValue(i));
+ r = CHANGED;
+ }
+ }
+ }
+ }
+ return r;
+}
+
+Result bvEqualsBothWays(vector<FixedBits*>& children, FixedBits& result)
+{
+ return bvEqualsBothWays(*(children[0]), *(children[1]), result);
+}
+
+Result bvZeroExtendBothWays(vector<FixedBits*>& children, FixedBits& output)
+{
+ assert(children.size() ==2 );
+ // The second argument is a junk size arugment.
+
+
+ FixedBits& input = *children[0];
+ const int inputBitWidth = input.getWidth();
+ const int outputBitWidth = output.getWidth();
+
+ Result result = makeEqual(input, output, 0, inputBitWidth);
+ if (CONFLICT == result)
+ return CONFLICT;
+
+ // Fix all the topmost bits of the output to zero.
+ for (int i = inputBitWidth; i < outputBitWidth; i++)
+ {
+ if (output.isFixed(i) && output.getValue(i))
+ return CONFLICT; // set to one. Never right.
+ else if (!output.isFixed(i))
+ {
+ output.setFixed(i, true);
+ output.setValue(i, false);
+ result = CHANGED;
+ }
+ }
+ return result;
+}
+
+Result bvSignExtendBothWays(vector<FixedBits*>& children, FixedBits& output)
+{
+ assert(children.size() ==2 );
+ // The second argument is a junk size arugment.
+
+ FixedBits& input = *children[0];
+ const int inputBitWidth = input.getWidth();
+ const int outputBitWidth = output.getWidth();
+ assert(inputBitWidth <= outputBitWidth);
+
+ Result result = makeEqual(input, output, 0, inputBitWidth);
+ if (CONFLICT == result)
+ return CONFLICT;
+
+ // If any of the topmost bits of the output are fixed. Then they all should be.
+ // They should all be fixed to the same value.
+ bool found = false;
+ bool setTo;
+ for (int i = inputBitWidth - /**/1 /**/; i < outputBitWidth; i++)
+ {
+ if (output.isFixed(i))
+ {
+ setTo = output.getValue(i);
+ found = true;
+ break;
+ }
+ }
+
+ if (found)
+ {
+ for (int i = inputBitWidth - 1; i < outputBitWidth; i++)
+ {
+ if (output.isFixed(i) && (output.getValue(i) != setTo))
+ return CONFLICT; // if any are set to the wrong value! bad.
+ else if (!output.isFixed(i))
+ {
+ output.setFixed(i, true);
+ output.setValue(i, setTo);
+ result = CHANGED;
+ }
+ }
+
+ Result result2 = makeEqual(input, output, 0, inputBitWidth);
+ if (CONFLICT == result2)
+ return CONFLICT;
+
+ }
+ return result;
+}
+
+Result bvExtractBothWays(vector<FixedBits*>& children, FixedBits& output)
+{
+ const int numberOfChildren = children.size();
+ const int outputBitWidth = output.getWidth();
+
+ Result result = NO_CHANGE;
+
+ assert(3 == numberOfChildren);
+
+ int top = children[1]->getUnsignedValue();
+ int bottom = children[2]->getUnsignedValue();
+
+ FixedBits& input = *(children[0]);
+
+ assert(top >= bottom);
+ assert(bottom >=0);
+ assert(top - bottom + 1 == outputBitWidth);
+ assert(top < input.getWidth());
+
+ for (int outputPosition = 0; outputPosition < outputBitWidth; outputPosition++)
+ {
+ int inputPosition = outputPosition + bottom;
+
+ if (input.isFixed(inputPosition) && output.isFixed(outputPosition))
+ if (input.getValue(inputPosition) ^ output.getValue(outputPosition))
+ return CONFLICT;
+
+ if (input.isFixed(inputPosition) ^ output.isFixed(outputPosition))
+ {
+ if (input.isFixed(inputPosition))
+ {
+ output.setFixed(outputPosition, true);
+ output.setValue(outputPosition, input.getValue(inputPosition));
+ result = CHANGED;
+ }
+ else
+ {
+ input.setFixed(inputPosition, true);
+ input.setValue(inputPosition, output.getValue(outputPosition));
+ result = CHANGED;
+ }
+ }
+ }
+
+ //cerr << "extract[" << top << ":" << bottom << "]" << input << "=" << output<< endl;
+
+ return result;
+}
+
+// UMINUS, is NEG followed by +1
+Result bvUnaryMinusBothWays(vector<FixedBits*>& children, FixedBits& output)
+{
+ assert(children.size() == 1);
+ const int bitWidth = children[0]->getWidth();
+
+ // If it's only one bit. This will be negative one.
+ FixedBits one(bitWidth, false);
+ one.fixToZero();
+ one.setFixed(0, true);
+ one.setValue(0, true);
+
+ FixedBits notted(bitWidth, false);
+
+ vector<FixedBits*> args;
+ args.push_back(¬ted);
+ args.push_back(&one);
+
+ Result result = NO_CHANGE;
+ while (true) // until it fixed points
+ {
+ FixedBits initialNot(notted);
+ FixedBits initialIn(*children[0]);
+ FixedBits initialOut(output);
+
+ result = bvNotBothWays(*children[0], notted);
+ if (CONFLICT == result)
+ return CONFLICT;
+
+ result = bvAddBothWays(args, output);
+ if (CONFLICT == result)
+ return CONFLICT;
+
+ if (FixedBits::equals(initialNot, notted) && FixedBits::equals(initialIn, *children[0]) && FixedBits::equals(initialOut, output))
+ break;
+ }
+
+ return NOT_IMPLEMENTED; // don't set the status properly yet..
+}
+
+Result bvConcatBothWays(vector<FixedBits*>& children, FixedBits& output)
+{
+ Result r = NO_CHANGE;
+ const int numberOfChildren = children.size();
+ int current = 0;
+ for (int i = numberOfChildren - 1; i >= 0; i--) // least significant is last.
+
+ {
+ FixedBits& child = *children[i];
+ for (int j = 0; j < child.getWidth(); j++)
+ {
+ // values are different. Bad.
+ if (output.isFixed(current) && child.isFixed(j) && (output.getValue(current) != child.getValue(j)))
+ return CONFLICT;
+
+ if (output.isFixed(current) && !child.isFixed(j))
+ {
+ // only output is fixed.
+ child.setFixed(j, true);
+ child.setValue(j, output.getValue(current));
+ r = CHANGED;
+ }
+ else if (!output.isFixed(current) && child.isFixed(j))
+ {
+ // only input is fixed.
+ output.setFixed(current, true);
+ output.setValue(current, child.getValue(j));
+ r = CHANGED;
+ }
+ current++;
+ }
+ }
+ return r;
+}
+
+// If the guard is fixed, make equal the appropriate input and output.
+// If one input can not possibly be the output. Then set the guard to make it the other one.
+// If both values are the same. Set the output to that value.
+Result bvITEBothWays(vector<FixedBits*>& children, FixedBits& output)
+{
+ Result result = NO_CHANGE;
+
+ assert(3 == children.size());
+ const int bitWidth = output.getWidth();
+ FixedBits& guard = *children[0];
+ FixedBits& c1 = *children[1];
+ FixedBits& c2 = *children[2];
+
+ assert(c1.getWidth() == c2.getWidth());
+ assert(output.getWidth() == c2.getWidth());
+
+ if (guard.isFixed(0) && guard.getValue(0))
+ { // guard fixed to true. So make (first arg == output)
+ result = makeEqual(output, c1, 0, bitWidth);
+ if (CONFLICT == result)
+ return CONFLICT;
+
+ }
+ else if (guard.isFixed(0) && !guard.getValue(0))
+ {
+ result = makeEqual(output, c2, 0, bitWidth);
+ if (CONFLICT == result)
+ return CONFLICT;
+
+ }
+ else
+ {
+ for (int i = 0; i < bitWidth; i++)
+ {
+ if (c1.isFixed(i) && c2.isFixed(i) && (c1.getValue(i) == c2.getValue(i)))
+ {
+
+ if (output.isFixed(i) && (output.getValue(i) != c1.getValue(i)))
+ return CONFLICT;
+
+ if (!output.isFixed(i))
+ {
+ output.setFixed(i, true);
+ output.setValue(i, c1.getValue(i));
+ result = CHANGED;
+ }
+ }
+ }
+ }
+
+ bool changed = false;
+ if (CHANGED == result)
+ changed = true;
+
+ for (int i = 0; i < bitWidth; i++)
+ {
+ if (output.isFixed(i))
+ {
+ if (c1.isFixed(i) && (c1.getValue(i) != output.getValue(i)))
+ {
+ //c1 is fixed to a value that's not the same as the output.
+ if (!guard.isFixed(0))
+ {
+ guard.setFixed(0, true);
+ guard.setValue(0, false);
+ result = bvITEBothWays(children, output);
+ if (CONFLICT == result)
+ return CONFLICT;
+ changed = true;
+ }
+ else if (guard.getValue(0))
+ return CONFLICT;
+ }
+
+ if (c2.isFixed(i) && (c2.getValue(i) != output.getValue(i)))
+ {
+ //c2 is fixed to a value that's not the same as the output.
+ if (!guard.isFixed(0))
+ {
+ guard.setFixed(0, true);
+ guard.setValue(0, true);
+ result = bvITEBothWays(children, output);
+ if (CONFLICT == result)
+ return CONFLICT;
+ changed = true;
+
+ }
+ else if (!guard.getValue(0))
+ return CONFLICT;
+ }
+ }
+ }
+
+ if (result == CONFLICT)
+ return CONFLICT;
+ if (changed)
+ return CHANGED;
+
+ return result;
+}
+
+}
+
+}
--- /dev/null
+/*
+ * ConstantBitPropagation_TransferFunctions.h
+ *
+ */
+// Trevor Hansen. BSD License.
+
+#ifndef CONSTANTBITPROPAGATION_TRANSFERFUNCTIONS_H_
+#define CONSTANTBITPROPAGATION_TRANSFERFUNCTIONS_H_
+
+#include "ConstantBitPropagation.h"
+namespace simplifier
+{
+namespace constantBitP
+{
+class MultiplicationStats;
+
+// Multiply is not yet maximally precise.
+//!!!!!!!
+Result bvMultiplyBothWays(vector<FixedBits*>& children, FixedBits& output, BEEV::STPMgr* bm, MultiplicationStats* ms = NULL);
+Result bvUnsignedDivisionBothWays(vector<FixedBits*>& children, FixedBits& output, BEEV::STPMgr* bm);
+Result bvUnsignedModulusBothWays(vector<FixedBits*>& children, FixedBits& output, BEEV::STPMgr* bm);
+Result bvSignedDivisionBothWays(vector<FixedBits*>& children, FixedBits& output, BEEV::STPMgr* bm);
+Result bvSignedRemainderBothWays(vector<FixedBits*>& children, FixedBits& output, BEEV::STPMgr* bm);
+Result bvSignedModulusBothWays(vector<FixedBits*>& children, FixedBits& output, BEEV::STPMgr* bm);
+//!!!!!!!
+
+
+// BOTH WAY FUNCTIONS..-------MAXIMALLY PRECISE..........
+Result bvEqualsBothWays(vector<FixedBits*>& children, FixedBits& output);
+
+Result bvAndBothWays(vector<FixedBits*>& operands, FixedBits& output);
+
+Result bvOrBothWays(vector<FixedBits*>& children, FixedBits& output);
+Result bvXorBothWays(vector<FixedBits*>& children, FixedBits& output);
+
+Result bvImpliesBothWays(vector<FixedBits*>& children, FixedBits& result);
+
+Result bvAddBothWays(vector<FixedBits*>& children, FixedBits& output);
+Result bvSubtractBothWays(vector<FixedBits*>& children, FixedBits& output);
+
+Result bvNotBothWays(FixedBits& a, FixedBits& output);
+Result bvNotBothWays(vector<FixedBits*>& children, FixedBits& output);
+
+Result bvITEBothWays(vector<FixedBits*>& children, FixedBits& output);
+
+Result bvExtractBothWays(vector<FixedBits*>& children, FixedBits& output);
+
+Result bvConcatBothWays(vector<FixedBits*>& children, FixedBits& output);
+
+Result bvSignExtendBothWays(vector<FixedBits*>& children, FixedBits& output);
+Result bvZeroExtendBothWays(vector<FixedBits*>& children, FixedBits& output);
+
+Result bvUnaryMinusBothWays(vector<FixedBits*>& children, FixedBits& output);
+
+Result bvLeftShiftBothWays(vector<FixedBits*>& children, FixedBits& output);
+Result bvRightShiftBothWays(vector<FixedBits*>& children, FixedBits& output);
+Result bvArithmeticRightShiftBothWays(vector<FixedBits*>& children, FixedBits& output);
+
+// FOUR signed operations.
+Result bvSignedGreaterThanBothWays(vector<FixedBits*>& children, FixedBits& output);
+
+Result bvSignedLessThanBothWays(vector<FixedBits*>& children, FixedBits& output);
+
+Result bvSignedLessThanEqualsBothWays(vector<FixedBits*>& children, FixedBits& output);
+
+Result bvSignedGreaterThanEqualsBothWays(vector<FixedBits*>& children, FixedBits& output);
+
+// FOUR unsigned operations.
+
+Result bvLessThanBothWays(vector<FixedBits*>& children, FixedBits& output);
+Result bvLessThanBothWays(FixedBits& c0, FixedBits &c1, FixedBits& output);
+
+Result bvLessThanEqualsBothWays(vector<FixedBits*>& children, FixedBits& output);
+
+Result bvGreaterThanBothWays(vector<FixedBits*>& children, FixedBits& output);
+
+Result bvGreaterThanEqualsBothWays(vector<FixedBits*>& children, FixedBits& output);
+
+}
+}
+
+#endif /* CONSTANTBITPROPAGATION_TRANSFERFUNCTIONS_H_ */
assert(!n.isConstant());
-#ifdef WITHCBITP
-
Result(*transfer)(vector<FixedBits*>&, FixedBits&);
switch (k)
MAPTFN(ITE,bvITEBothWays)
MAPTFN(BVCONCAT, bvConcatBothWays)
+#ifdef WITHCBITP
case BVMULT: // handled specially later.
case BVDIV:
case BVMOD:
case SBVMOD:
transfer = NULL;
break;
+#endif
default:
{
notHandled(k);
#undef MAPTFN
bool mult_like = false;
+#ifdef WITHCBITP
// safe approximation to no overflow multiplication.
if (k == BVMULT)
{
mult_like=true;
}
else
+#endif
result = transfer(children, output);
if (mult_like && output_mult_like)
cerr << *children[1] << std::endl;
}
-#endif
return result;
}
projects / francis / stp.git / commitdiff