From: trevor_hansen Date: Mon, 2 Jan 2012 02:35:12 +0000 (+0000) Subject: Add missing files from the last checkin. X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=c7e39e7b2481ce2107ed37a1d34448fa80578761;p=francis%2Fstp.git Add missing files from the last checkin. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1460 e59a4935-1847-0410-ae03-e826735625c1 --- diff --git a/src/simplifier/constantBitP/multiplication/ColumnCounts.h b/src/simplifier/constantBitP/multiplication/ColumnCounts.h new file mode 100644 index 0000000..3a400f3 --- /dev/null +++ b/src/simplifier/constantBitP/multiplication/ColumnCounts.h @@ -0,0 +1,261 @@ +/* + * 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_ */ diff --git a/src/simplifier/constantBitP/multiplication/ColumnStats.h b/src/simplifier/constantBitP/multiplication/ColumnStats.h new file mode 100644 index 0000000..ca0bbe9 --- /dev/null +++ b/src/simplifier/constantBitP/multiplication/ColumnStats.h @@ -0,0 +1,79 @@ +/* + * ColumnStats.h + * + * Created on: 24/03/2010 + * Author: thansen + */ + +#ifndef COLUMNSTATS_H_ +#define COLUMNSTATS_H_ + +namespace simplifier +{ +namespace constantBitP +{ + +extern const bool debug_multiply; + + + +struct ColumnStats +{ + int columnUnfixed; // both unfixed. + int columnOneFixed; // one of the values is fixed to one, the other is unfixed. + int columnOnes; // both are fixed to one. + int columnZeroes; // one is fixed to zero. + + ColumnStats(const FixedBits & x, const FixedBits & y, int index) + { + columnUnfixed = 0; + columnOneFixed = 0; + columnOnes = 0; + columnZeroes = 0; + + assert(index < x.getWidth()); + assert(y.getWidth() == x.getWidth()); + + if (debug_multiply) + log << "ColumnStats" << index << " " << x << " " << y << endl; + + for (unsigned i = 0; i <= (unsigned) index; i++) + { + bool xIsFixed = x.isFixed(index - i); + bool yIsFixed; + + if (xIsFixed && !x.getValue(index - i)) + columnZeroes++; + else if ((yIsFixed = y.isFixed(i)) && !y.getValue(i)) + columnZeroes++; + else if (xIsFixed && x.getValue(index - i) && yIsFixed + && y.getValue(i)) + columnOnes++; + else if (yIsFixed && y.getValue(i)) + columnOneFixed++; + else if (xIsFixed && x.getValue(index - i)) + columnOneFixed++; + else + columnUnfixed++; + } + + assert(columnOnes >=0 && columnUnfixed >=0 && columnZeroes >=0 && columnOneFixed >=0); + assert(columnOnes + columnUnfixed + columnOneFixed + columnZeroes == (index+1)); + } + +}; + +std::ostream& operator<<(std::ostream& o, const ColumnStats& cs) +{ + o << "cUnfixed:" << cs.columnUnfixed << endl; // both unfixed. + o << "cOneFixed:" << cs.columnOneFixed << endl; // one of the values is fixed to one. + o << "cOnes:" << cs.columnOnes << endl; + o << "cZero:" << cs.columnZeroes << endl; + return o; +} + +} +} + + +#endif /* COLUMNSTATS_H_ */ diff --git a/src/simplifier/constantBitP/multiplication/Edge.h b/src/simplifier/constantBitP/multiplication/Edge.h new file mode 100644 index 0000000..f1338ed --- /dev/null +++ b/src/simplifier/constantBitP/multiplication/Edge.h @@ -0,0 +1,74 @@ +#ifndef EDGE_H_ +#define EDGE_H_ + +namespace simplifier +{ +namespace constantBitP +{ + + +typedef enum EdgeTypeRec +{ + STRAIGHT_IMPLIES = 1, NOT_IMPLIES = 2, IMPLIES_NOT = 4, NOT_IMPLIES_NOT = 8 +} EdgeType; + +struct Edge +{ +private: + Edge& operator=(const Edge&); + //Edge(const Edge& copy); + +public: + FixedBits& left; + const int leftIndex; + FixedBits& right; + const int rightIndex; + char type; + + Edge(FixedBits& _left, int _leftIndex, FixedBits& _right, int _rightIndex) : + left(_left), leftIndex(_leftIndex), right(_right), rightIndex( + _rightIndex) + + { + type = 0; + assert(left <= right); + assert(leftIndex < left.getWidth()); + assert(rightIndex < right.getWidth()); + assert(leftIndex >=0); + assert(rightIndex >=0); + } +}; + +std::ostream& operator<<(std::ostream& output, struct Edge e) +{ + output << e.left << "["; + output << e.leftIndex << "]"; + output << " " << ((int) e.type) << " "; + output << e.right << "["; + output << e.rightIndex << "]" << endl; + + return output; +} + +struct EdgeHasher +{ + size_t operator()(const Edge& e1) const + { + return ((size_t) &(e1.left)) + ((size_t) &(e1.right)) + e1.leftIndex + + e1.rightIndex; + } +}; + +struct eqEdge +{ + bool operator()(const Edge& e1, const Edge& e2) const + { + return (e1.left) == (e2.left) && e1.leftIndex == e2.leftIndex + && (e1.right == e2.right) && e1.rightIndex == e2.rightIndex; + } +}; + +} +} + +#endif /* EDGE_H_ */ diff --git a/src/simplifier/constantBitP/multiplication/ImplicationGraph.h b/src/simplifier/constantBitP/multiplication/ImplicationGraph.h new file mode 100644 index 0000000..fb96174 --- /dev/null +++ b/src/simplifier/constantBitP/multiplication/ImplicationGraph.h @@ -0,0 +1,749 @@ +/* + * 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 + +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 Edges; + Edges edges; + + struct Target + { + EdgeType type; + bool isLeft; + int index; + }; + + // Contains the relevants parts of the implication graph. + struct RelevantImplicationGraph + { + vector > left; + vector > 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 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 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& left_assigned, vector& right_assigned, + const int index, const bool isLeft, + const RelevantImplicationGraph& relevant) + { + + list::const_iterator it = isLeft ? relevant.left[index].begin() + : relevant.right[index].begin(); + const list::const_iterator end = + isLeft ? relevant.left[index].end() + : relevant.right[index].end(); + + vector leftToRun; + vector 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::iterator it = leftToRun.begin(); it + != leftToRun.end(); it++) + { + if (!propagate(left_assigned, right_assigned, *it, true, relevant)) + return false; + } + + for (vector::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&left_assigned, + vector&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& left_assigned, vector& right_assigned, + vector& min, vector& 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 left_assigned_copy(left_assigned); + vector 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 left_assigned_copy(left_assigned); + vector 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 left_assigned(bitWidth, 3); + vector 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 left_assigned(bitWidth, 3); + vector 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 min(bitWidth, bitWidth); + vector max(bitWidth, 0); + + // maximum. + { + vector left_assigned_copy(left_assigned); + vector 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_ */