--- /dev/null
+/*
+ * ColumnCounts.h
+ *
+ * Created on: 24/03/2010
+ * Author: thansen
+ */
+
+#ifndef COLUMNCOUNTS_H_
+#define COLUMNCOUNTS_H_
+
+namespace simplifier
+{
+namespace constantBitP
+{
+
+extern std::ostream& log;
+
+
+struct Interval
+{
+ int& low;
+ int& high;
+ Interval(int& _low, int& _high) :
+ low(_low), high(_high)
+ {
+ }
+};
+
+struct ColumnCounts
+{
+ signed *columnH; // maximum number of true partial products.
+ signed *columnL; // minimum "" ""
+ signed *sumH;
+ signed *sumL;
+ unsigned int bitWidth;
+
+ ColumnCounts(signed _columnH[], signed _columnL[], signed _sumH[],
+ signed _sumL[], unsigned _bitWidth) :
+ columnH(_columnH), columnL(_columnL), sumH(_sumH), sumL(_sumL)
+ {
+ // setup the low and highs.
+ bitWidth = _bitWidth;
+ // initialise 'em.
+ for (unsigned i = 0; i < bitWidth; i++)
+ {
+ columnL[i] = 0;
+ columnH[i] = i + 1;
+ }
+ rebuildSums();
+ }
+
+ void rebuildSums()
+ {
+ // Initialise sums.
+ sumL[0] = columnL[0];
+ sumH[0] = columnH[0];
+ for (unsigned i = /**/1 /**/; i < 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);
+ }
+ }
+
+ void print(string message)
+ {
+ log << message << endl;
+ log << " columnL:";
+ for (unsigned i = 0; i < bitWidth; i++)
+ {
+ log << columnL[bitWidth - 1 - i] << " ";
+ }
+ log << endl;
+ log << " columnH:";
+ for (unsigned i = 0; i < bitWidth; i++)
+ {
+ log << columnH[bitWidth - 1 - i] << " ";
+ }
+ log << endl;
+ log << " sumL: ";
+
+ for (unsigned i = 0; i < bitWidth; i++)
+ {
+ log << sumL[bitWidth - 1 - i] << " ";
+ }
+ log << endl;
+ log << " sumH: ";
+ for (unsigned i = 0; i < bitWidth; i++)
+ {
+ log << sumH[bitWidth - 1 - i] << " ";
+ }
+ log << endl;
+ }
+
+ // update the sum of a column to the parity of the output for that column. e.g. [0,2] if the answer is 1, goes to [1,1].
+ Result snapTo(const FixedBits& output)
+ {
+ Result r = NO_CHANGE;
+
+ // Make sure each column's sum is consistent with the output.
+ for (unsigned i = 0; i < bitWidth; i++)
+ {
+ if (output.isFixed(i))
+ {
+ //bool changed = false;
+ int expected = output.getValue(i) ? 1 : 0;
+
+ // output is true. So the maximum and minimum can only be even.
+ if ((sumH[i] & 1) != expected)
+ {
+ sumH[i]--;
+ r = CHANGED;
+ }
+ if ((sumL[i] & 1) != expected)
+ {
+ sumL[i]++;
+ r = CHANGED;
+ }
+
+ if (((sumH[i] < sumL[i]) || (sumL[i] < 0)))
+ return CONFLICT;
+ }
+ }
+ return r;
+ }
+
+ bool inConflict()
+ {
+ for (unsigned i = 0; i < bitWidth; i++)
+ if ((sumL[i] > sumH[i]) || (columnL[i] > columnH[i]))
+ return true;
+ return false;
+
+ }
+
+ Result fixedPoint(FixedBits & output)
+ {
+ if (inConflict())
+ return CONFLICT;
+
+ bool changed = true;
+ bool totalChanged = false;
+
+ while (changed)
+ {
+ changed = false;
+
+ Result r = snapTo(output);
+ if (r == CHANGED)
+ changed = true;
+ if (r == CONFLICT)
+ return CONFLICT;
+
+ r = propagate(output);
+ if (r == CHANGED)
+ changed = true;
+ if (r == CONFLICT)
+ return CONFLICT;
+
+ if (changed)
+ totalChanged = true;
+ }
+
+ if (totalChanged)
+ return CHANGED;
+ else
+ return NO_CHANGE;
+ }
+
+ //Assert that all the counts are consistent.
+ Result propagate(const FixedBits& output)
+ {
+ bool changed = false;
+
+ int i = 0;
+
+ //
+ if (sumL[i] > columnL[i])
+ {
+ columnL[i] = sumL[i];
+ changed = true;
+ }
+ if (sumL[i] < columnL[i])
+ {
+ sumL[i] = columnL[i];
+ changed = true;
+ }
+ if (sumH[i] < columnH[i])
+ {
+ columnH[i] = sumH[i];
+ changed = true;
+ }
+ if (sumH[i] > columnH[i])
+ {
+ sumH[i] = columnH[i];
+ changed = true;
+ }
+
+ for (unsigned i = 1; i < bitWidth; i++)
+ {
+ Interval a(sumL[i], sumH[i]);
+ Interval b(columnL[i], columnH[i]);
+
+ int low = sumL[i - 1] / 2; // interval takes references.
+ int high = sumH[i - 1] / 2;
+ Interval c(low, high);
+
+ if (a.low < b.low + c.low)
+ {
+ a.low = b.low + c.low;
+ changed = true;
+ }
+
+ if (a.high > b.high + c.high)
+ {
+ changed = true;
+ a.high = b.high + c.high;
+ }
+
+ if (a.low - b.high > c.low)
+ {
+ int toAssign = ((a.low - b.high) * 2);
+ assert(toAssign > sumL[i-1]);
+ sumL[i - 1] = toAssign;
+ changed = true;
+ }
+
+ if (a.high - b.low < c.high)
+ {
+ int toAssign = ((a.high - b.low) * 2) + 1;
+ assert(toAssign < sumH[i-1]);
+ sumH[i - 1] = toAssign;
+ changed = true;
+ }
+
+ if (a.low - c.high > b.low)
+ {
+ b.low = a.low - c.high;
+ changed = true;
+ }
+
+ if (a.high - c.low < b.high)
+ {
+ b.high = a.high - c.low;
+ changed = true;
+ }
+
+ }
+ if (changed)
+ return CHANGED;
+ else
+ return NO_CHANGE;
+ }
+
+};
+
+}
+
+}
+
+#endif /* COLUMNCOUNTS_H_ */
--- /dev/null
+/*
+ * ImplicationGraph.h
+ *
+ * Created on: 24/03/2010
+ * Author: thansen
+ */
+
+#ifndef IMPLICATIONGRAPH_H_
+#define IMPLICATIONGRAPH_H_
+
+#include "../ConstantBitP_TransferFunctions.h"
+#include "../ConstantBitP_Utility.h"
+#include "Edge.h"
+#include "ColumnCounts.h"
+#include "ColumnStats.h"
+#include <list>
+
+namespace simplifier
+{
+namespace constantBitP
+{
+
+extern const bool debug_multiply;
+
+// Relationship between bits. One bit may imply another bit.
+class ImplicationGraph
+{
+ typedef __gnu_cxx ::hash_set<Edge, EdgeHasher, eqEdge> Edges;
+ Edges edges;
+
+ struct Target
+ {
+ EdgeType type;
+ bool isLeft;
+ int index;
+ };
+
+ // Contains the relevants parts of the implication graph.
+ struct RelevantImplicationGraph
+ {
+ vector<list<Target> > left;
+ vector<list<Target> > right;
+ const FixedBits& l;
+ const FixedBits& r;
+
+ RelevantImplicationGraph(const FixedBits& leftFB,
+ const FixedBits& rightFB, const Edges edges) :
+ left(leftFB.getWidth()), right(leftFB.getWidth()), l(leftFB), r(
+ rightFB)
+ {
+ assert(l <= r);
+
+ Edges::iterator it = edges.begin();
+
+ // Get all the relevant implications.
+ while (it != edges.end())
+ {
+ if (!(it->left == leftFB && it->right == rightFB))
+ {
+ it++;
+ continue;
+ }
+ EdgeType et = (EdgeType) it->type;
+
+ {
+ Target t;
+ t.type = et;
+ t.isLeft = false;
+ t.index = it->rightIndex;
+ left[it->leftIndex].push_front(t);
+ }
+
+ // The other way.
+ {
+ char newEdgeType = 0;
+ if ((et & STRAIGHT_IMPLIES) != 0)
+ {
+ newEdgeType |= NOT_IMPLIES_NOT;
+ }
+ if ((et & NOT_IMPLIES) != 0)
+ {
+ newEdgeType |= NOT_IMPLIES;
+ }
+ if ((et & IMPLIES_NOT) != 0)
+ {
+ newEdgeType |= IMPLIES_NOT;
+ }
+ if ((et & NOT_IMPLIES_NOT) != 0)
+ {
+ newEdgeType |= STRAIGHT_IMPLIES;
+ }
+
+ Target t;
+ t.type = (EdgeType) newEdgeType;
+ t.isLeft = true;
+ t.index = it->leftIndex;
+ right[it->rightIndex].push_front(t);
+ }
+
+ it++;
+ }
+
+ assert(left.size() == ((unsigned) leftFB.getWidth()));
+ assert(left.size() == ((unsigned) rightFB.getWidth()));
+
+ if (debug_multiply)
+ {
+ cout << "left";
+ for (int i = 0; i < left.size(); i++)
+ {
+
+ cout << "[" << i << ":" << left[i].size() << "] ";
+ }
+ cout << "right";
+ for (int i = 0; i < right.size(); i++)
+ {
+
+ cout << "[" << i << ":" << right[i].size() << "] ";
+ }
+
+ }
+ }
+ };
+
+ void outputArray(string msg, vector<char> copy)
+ {
+ const int width = copy.size();
+ cout << msg;
+ for (int i = width - 1; i >= 0; i--)
+ if (copy[i] == (char) 3)
+ cout << "-";
+ else
+ cout << (int) copy[i];
+ cout << endl;
+ }
+
+
+ // return true if changed
+ bool addEdge(FixedBits& left, const int leftIndex, FixedBits& right,
+ const int rightIndex, const EdgeType eT)
+ {
+ Edge e = Edge(left, leftIndex, right, rightIndex);
+ Edges::iterator it = edges.find(e);
+
+ if (it != edges.end())
+ {
+ // already present.
+ // But the new type might by new.
+ char oldType = it->type;
+ if (((~oldType) & eT) == 0)
+ return false; // not changed.
+
+ e.type = oldType | eT;
+
+ edges.erase(e);
+ edges.insert(e);
+ }
+ else
+ {
+ // not present already.
+ e.type = eT;
+ edges.insert(e);
+ }
+
+ if (debug_multiply)
+ cout << "inserting" << e;
+
+ return true;
+ }
+
+ bool writeIn(vector<char> left_assigned, FixedBits& left)
+ {
+ assert(((int)left_assigned.size()) == left.getWidth());
+ unsigned bitWidth = left.getWidth();
+ bool changed = false;
+ for (unsigned i = 0; i < bitWidth; i++)
+ {
+ if (left_assigned[i] == 1)
+ {
+ if (left.isFixedToOne(i))
+ continue;
+ changed = true;
+ assert(!left.isFixedToZero(i));
+ left.setFixed(i, true);
+ left.setValue(i, true);
+ }
+ else if (left_assigned[i] == 0)
+ {
+ if (left.isFixedToZero(i))
+ continue;
+ changed = true;
+ assert(!left.isFixedToOne(i));
+ left.setFixed(i, true);
+ left.setValue(i, false);
+ }
+ else if (left_assigned[i] == 3)
+ {
+ assert(!left.isFixed(i));
+ }
+ else
+ {
+ throw new std::runtime_error("sdafas`3");
+ }
+ }
+ return changed;
+ }
+
+ // return true if consistent.
+ bool propagate(vector<char>& left_assigned, vector<char>& right_assigned,
+ const int index, const bool isLeft,
+ const RelevantImplicationGraph& relevant)
+ {
+
+ list<Target>::const_iterator it = isLeft ? relevant.left[index].begin()
+ : relevant.right[index].begin();
+ const list<Target>::const_iterator end =
+ isLeft ? relevant.left[index].end()
+ : relevant.right[index].end();
+
+ vector<int> leftToRun;
+ vector<int> rightToRun;
+
+ while (it != end)
+ {
+ const char type = (*it).type;
+ const int leftIndex = isLeft ? index : it->index;
+ const int rightIndex = isLeft ? it->index : index;
+
+ assert(isLeft != it->isLeft);
+
+ assert( 0 == ((type & ~IMPLIES_NOT) & ~NOT_IMPLIES)); // others not implemented.
+
+ // can only do something if xor set to unknown.
+ char leftValue = left_assigned[leftIndex];
+ char rightValue = right_assigned[rightIndex];
+
+ if (debug_multiply)
+ {
+ cout << "checking" << endl;
+ cout << "left[" << leftIndex << "] = " << (int) leftValue
+ << " ";
+ cout << (int) type;
+ cout << "right[" << rightIndex << "] = " << (int) rightValue
+ << endl;
+ }
+
+ if ((leftValue == 3) != (rightValue == 3))
+ {
+ if ((type & IMPLIES_NOT) != 0)
+ {
+ if (leftValue == 3 && rightValue == 1)
+ {
+ left_assigned[leftIndex] = 0;
+ leftToRun.push_back(leftIndex);
+ }
+
+ if (leftValue == 1 && rightValue == 3)
+ {
+ right_assigned[rightIndex] = 0;
+ rightToRun.push_back(rightIndex);
+ }
+ }
+
+ if ((type & NOT_IMPLIES) != 0)
+ {
+ if (leftValue == 3 && rightValue == 0)
+ {
+ left_assigned[leftIndex] = 1;
+ leftToRun.push_back(leftIndex);
+ }
+
+ if (leftValue == 0 && rightValue == 3)
+ {
+ right_assigned[rightIndex] = 1;
+ rightToRun.push_back(rightIndex);
+ }
+ }
+ }
+
+ if ((type & IMPLIES_NOT) != 0)
+ {
+ if (leftValue == 1 && rightValue == 1)
+ {
+ return false;
+ }
+ }
+
+ if ((type & NOT_IMPLIES) != 0)
+ {
+ if (leftValue == 0 && rightValue == 0)
+ {
+ return false;
+ }
+
+ }
+
+ it++;
+ }
+
+ for (vector<int>::iterator it = leftToRun.begin(); it
+ != leftToRun.end(); it++)
+ {
+ if (!propagate(left_assigned, right_assigned, *it, true, relevant))
+ return false;
+ }
+
+ for (vector<int>::iterator it = rightToRun.begin(); it
+ != rightToRun.end(); it++)
+ {
+ if (!propagate(left_assigned, right_assigned, *it, false, relevant))
+ return false;
+ }
+
+ return true;
+ }
+
+ // If there are no implications containing a particular bit, then set the value to "setTo"
+ void setIfUnconstrained(vector<char>&left_assigned,
+ vector<char>&right_assigned, const char setTo,
+ const RelevantImplicationGraph& relevant)
+ {
+ const int bitWidth = left_assigned.size();
+ bool left_specified[bitWidth];
+ bool right_specified[bitWidth];
+
+ // get everything that's already set to one.
+ for (int i = 0; i < bitWidth; i++)
+ {
+ if (left_assigned[i] != 3)
+ left_specified[i] = true;
+ else
+ left_specified[i] = false;
+
+ if (right_assigned[i] != 3)
+ right_specified[i] = true;
+ else
+ right_specified[i] = false;
+ }
+
+ for (int i = 0; i < bitWidth; i++)
+ {
+ if (relevant.left[i].size() != 0)
+ left_specified[i] = true;
+ if (relevant.right[i].size() != 0)
+ right_specified[i] = true;
+ }
+
+ for (int i = 0; i < bitWidth; i++)
+ if (!left_specified[i])
+ left_assigned[i] = setTo;
+
+ for (int i = 0; i < bitWidth; i++)
+ if (!right_specified[i])
+ right_assigned[i] = setTo;
+
+ }
+
+ // note the assigned vectors are passed by value.
+ void fill(vector<char>& left_assigned, vector<char>& right_assigned,
+ vector<int>& min, vector<int>& max,
+ const RelevantImplicationGraph& relevant)
+ {
+ const int width = left_assigned.size();
+ bool done = false;
+
+ if (debug_multiply)
+ {
+ outputArray("calling with left", left_assigned);
+ outputArray("calling with right", right_assigned);
+ }
+
+ // Lookahead to check that something intersting may comeout. i.e. a higher max, or lower min is possible.
+ {
+ bool shouldContinue = false;
+ for (int k = 0; ((k < width) && !shouldContinue); k++)
+ {
+ int ones = 0;
+ int zeroes = 0;
+ int unfixed = 0;
+
+ for (int j = 0; j <= k; j++)
+ {
+ if (left_assigned[j] == 1 && right_assigned[k - j] == 1)
+ {
+ ones++;
+ }
+ else if (left_assigned[j] == 0 || right_assigned[k - j]
+ == 0)
+ {
+ zeroes++;
+ }
+ else
+ unfixed++;
+ }
+
+ if (ones + unfixed > max[k] || ones < min[k])
+ shouldContinue = true;
+ }
+ if (!shouldContinue)
+ return;
+ }
+
+
+ for (int i = 0; i < width && !done; i++)
+ {
+ if (left_assigned[i] == 3)
+ {
+ vector<char> left_assigned_copy(left_assigned);
+ vector<char> right_assigned_copy(right_assigned);
+
+ left_assigned[i] = 0;
+ if (propagate(left_assigned, right_assigned, i, true, relevant))
+ fill(left_assigned, right_assigned, min, max, relevant);
+
+ left_assigned_copy[i] = 1;
+ if (propagate(left_assigned_copy, right_assigned_copy, i, true,
+ relevant))
+ fill(left_assigned_copy, right_assigned_copy, min, max,
+ relevant);
+ done = true;
+ }
+ else if (right_assigned[i] == 3)
+ {
+ vector<char> left_assigned_copy(left_assigned);
+ vector<char> right_assigned_copy(right_assigned);
+
+ right_assigned[i] = 0;
+ if (propagate(left_assigned, right_assigned, i, false, relevant))
+ fill(left_assigned, right_assigned, min, max, relevant);
+
+ right_assigned_copy[i] = 1;
+ if (propagate(left_assigned_copy, right_assigned_copy, i,
+ false, relevant))
+ fill(left_assigned_copy, right_assigned_copy, min, max,
+ relevant);
+ done = true;
+ }
+ }
+
+ if (debug_multiply)
+ {
+ outputArray("left", left_assigned);
+ outputArray("right", right_assigned);
+ }
+
+ if (!done)
+ {
+ for (int i = 0; i < width; i++)
+ {
+ assert(left_assigned[i]!=3);
+ assert(right_assigned[i]!=3);
+ }
+
+ for (int k = 0; k < width; k++)
+ {
+ int oneCount = 0;
+
+ for (int j = 0; j <= k; j++)
+ {
+ oneCount+= (int)(left_assigned[j] * right_assigned[k - j]);
+ }
+
+ if (oneCount < min[k])
+ {
+ min[k] = oneCount;
+ if (debug_multiply)
+ cout << "columnL[" << k << "]=" << oneCount << endl;
+ }
+ if (oneCount > max[k])
+ {
+ max[k] = oneCount;
+ if (debug_multiply)
+ cout << "columnH[" << k << "]=" << oneCount << endl;
+ }
+ }
+ }
+ }
+
+public:
+
+ // Go through all of the edges. Fix if it can be fixed.
+ Result fixUsingImplications(FixedBits& x, FixedBits& y)
+ {
+ const unsigned bitWidth = x.getWidth();
+ vector<char> left_assigned(bitWidth, 3);
+ vector<char> right_assigned(bitWidth, 3);
+
+ FixedBits& left = x <= y ? x : y;
+ FixedBits& right = x <= y ? y : x;
+
+ for (unsigned i = 0; i < bitWidth; i++)
+ {
+ if (left.isFixed(i))
+ {
+ left_assigned[i] = left.getValue(i) ? 1 : 0;
+ }
+ if (right.isFixed(i))
+ {
+ right_assigned[i] = right.getValue(i) ? 1 : 0;
+ }
+ }
+
+ RelevantImplicationGraph graph(left, right, edges);
+ bool ok = true;
+
+ for (unsigned i = 0; i < bitWidth; i++)
+ {
+ ok &= propagate(left_assigned, right_assigned, i, true, graph);
+ ok &= propagate(left_assigned, right_assigned, i, false, graph);
+ }
+
+ if (!ok)
+ return CONFLICT;
+
+ Result r;
+
+ bool changed = writeIn(left_assigned, left);
+ changed = writeIn(right_assigned, right) | changed;
+
+ if (changed)
+ return CHANGED;
+
+ return NO_CHANGE;
+ }
+
+ // Update the sums using the Implication Graph
+ Result updateSums(const FixedBits& x, const FixedBits& y, ColumnCounts& cc)
+ {
+ const unsigned int bitWidth = (unsigned) x.getWidth();
+
+ if (bitWidth > 8)
+ return NO_CHANGE; // this is currently toooo slow for larger bitwidths.
+
+ const FixedBits& left = x <= y ? x : y;
+ const FixedBits& right = x <= y ? y : x;
+
+ RelevantImplicationGraph relevant(left, right, edges);
+
+ vector<char> left_assigned(bitWidth, 3);
+ vector<char> right_assigned(bitWidth, 3);
+
+ for (unsigned i = 0; i < bitWidth; i++)
+ {
+ if (left.isFixed(i))
+ {
+ left_assigned[i] = left.getValue(i) ? 1 : 0;
+ }
+ if (right.isFixed(i))
+ {
+ right_assigned[i] = right.getValue(i) ? 1 : 0;
+ }
+ }
+
+ if (debug_multiply)
+ {
+ outputArray("initial left:", left_assigned);
+ outputArray("initial right:", right_assigned);
+ }
+
+ vector<int> min(bitWidth, bitWidth);
+ vector<int> max(bitWidth, 0);
+
+ // maximum.
+ {
+ vector<char> left_assigned_copy(left_assigned);
+ vector<char> right_assigned_copy(right_assigned);
+
+ setIfUnconstrained(left_assigned_copy, right_assigned_copy, 1,
+ relevant);
+
+ if (debug_multiply)
+ {
+ outputArray("max left", left_assigned_copy);
+ outputArray("max right", right_assigned_copy);
+ }
+
+ fill(left_assigned_copy, right_assigned_copy, min, max, relevant);
+ }
+
+ bool allAlreadyMin = true;
+ for (int i = 0; i < bitWidth; i++)
+ if (min[i] != 0)
+ allAlreadyMin = false;
+
+ // if they're already zero don't look.
+ if (!allAlreadyMin)
+ {
+ // minimum.
+ setIfUnconstrained(left_assigned, right_assigned, 0, relevant);
+ if (debug_multiply)
+ {
+ outputArray("min left", left_assigned);
+ outputArray("min right", right_assigned);
+ }
+
+ fill(left_assigned, right_assigned, min, max, relevant);
+ }
+
+ bool changed = false;
+ for (unsigned i = 0; i < bitWidth; i++)
+ {
+
+ if (min[i] > cc.columnL[i])
+ {
+ cc.columnL[i] = min[i];
+ changed = true;
+ }
+
+ if (max[i] < cc.columnH[i])
+ {
+ cc.columnH[i] = max[i];
+ changed = true;
+ }
+
+ if (min[i] > max[i])
+ {
+ cerr << min[i] << " " << max[i] << endl;
+ return CONFLICT;
+ }
+
+ }
+ if (!changed)
+ return NO_CHANGE;
+ else
+ return CHANGED;
+ }
+
+ Result discoverNewXORs(FixedBits& x, FixedBits& y, const int index,
+ const int aspirationalSum)
+ {
+ 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 calcSum = aspirationalSum - columnOnes;
+
+ if (calcSum < 0)
+ return CONFLICT;
+
+ if (columnUnfixed > 0)
+ return NO_CHANGE;
+
+ // There are two oneFixed values. They must sum to one. So the values must be opposites.
+ int a = -1, b = -1;
+ bool aY = -1, bY = -1; // quieten compiler
+ if (!(calcSum == 1 && columnOneFixed == 2))
+ return NO_CHANGE;
+
+ for (int i = 0; i <= index; i++)
+ {
+ if ((x.isFixedToOne(index - i) && !y.isFixed(i)) || (!x.isFixed(
+ index - i) && y.isFixedToOne(i)))
+ {
+ if (a == -1)
+ {
+ a = i;
+ if (y.isFixed(i))
+ aY = false;
+ else
+ aY = true;
+ }
+ else if (b == -1)
+ {
+ b = i;
+ if (y.isFixed(i))
+ bY = false;
+ else
+ bY = true;
+
+ }
+ else
+ throw std::runtime_error("bad");
+ }
+ }
+
+ // a and b now contain the y-indexes.
+ assert(a!=-1 && b!=-1);
+
+ FixedBits& fb1 = aY ? y : x;
+ FixedBits& fb2 = bY ? y : x;
+
+ if (fb1 == fb2)
+ {
+ if (debug_multiply)
+ cerr << "Not handled yet implications between the same elemtn.";
+ return NO_CHANGE;
+ }
+
+ int index1 = aY ? a : index - a;
+ int index2 = bY ? b : index - b;
+
+ if (fb1 <= fb2)
+ {
+ bool changed = addEdge(fb1, index1, fb2, index2, NOT_IMPLIES);
+ changed |= addEdge(fb1, index1, fb2, index2, IMPLIES_NOT);
+
+ if (changed)
+ return CHANGED;
+ }
+ else
+ {
+ bool changed = addEdge(fb2, index2, fb1, index1, NOT_IMPLIES);
+ changed |= addEdge(fb2, index2, fb1, index1, IMPLIES_NOT);
+
+ if (changed)
+ return CHANGED;
+ }
+ return NO_CHANGE;
+ }
+
+ Result discoverNewNANDs(FixedBits& x, FixedBits& y, const int index,
+ const int aspirationalSum)
+ {
+ Result result = NO_CHANGE;
+
+ 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.
+
+
+ if (aspirationalSum == columnOnes && (columnUnfixed > 0))
+ {
+ for (int i = 0; i <= index; i++)
+ {
+ if (!y.isFixed(i) && !(x.isFixed(index - i)))
+ {
+ if (x <= y)
+ {
+ if (addEdge(x, index - i, y, i, IMPLIES_NOT))
+ result = CHANGED;
+ }
+ else if (addEdge(y, i, x, index - i, IMPLIES_NOT))
+ result = CHANGED;
+ }
+ }
+ }
+ return result;
+ }
+};
+
+}
+}
+
+#endif /* IMPLICATIONGRAPH_H_ */
projects / francis / stp.git / commitdiff