--- ./src/simplifier/UseITEContext.h.orig 2011-04-07 07:38:52.000000000 -0600 +++ ./src/simplifier/UseITEContext.h 2012-01-10 16:05:21.201610452 -0700 @@ -27,7 +27,7 @@ namespace BEEV if (n.GetKind() == NOT && n[0].GetKind() == OR) { ASTVec flat = FlattenKind(OR, n[0].GetChildren()); - for (int i = 0; i < flat.size(); i++) + for (size_t i = 0; i < flat.size(); i++) context.insert(nf->CreateNode(NOT, flat[i])); } else if (n.GetKind() == AND) @@ -85,7 +85,7 @@ namespace BEEV } else { - for (int i = 0; i < n.GetChildren().size(); i++) + for (size_t i = 0; i < n.GetChildren().size(); i++) new_children.push_back(visit(n[i], visited, visited_empty, context)); } --- ./src/simplifier/AlwaysTrue.h.orig 2011-05-01 06:48:53.000000000 -0600 +++ ./src/simplifier/AlwaysTrue.h 2012-01-10 16:05:21.202610431 -0700 @@ -88,7 +88,7 @@ public: else new_state = state; - for (int i=0; i < n.Degree(); i++) + for (size_t i=0; i < n.Degree(); i++) { newChildren.push_back(visit(n[i],new_state,fromTo)); } --- ./src/simplifier/MutableASTNode.h.orig 2011-03-29 07:18:23.000000000 -0600 +++ ./src/simplifier/MutableASTNode.h 2012-01-10 16:05:21.210610269 -0700 @@ -46,12 +46,12 @@ public: vector tempChildren; tempChildren.reserve(n.Degree()); - for (int i = 0; i < n.Degree(); i++) + for (size_t i = 0; i < n.Degree(); i++) tempChildren.push_back(build(n[i], visited)); MutableASTNode * mut = createNode(n); - for (int i = 0; i < n.Degree(); i++) + for (size_t i = 0; i < n.Degree(); i++) tempChildren[i]->parents.insert(mut); mut->children.insert(mut->children.end(),tempChildren.begin(),tempChildren.end()); @@ -86,7 +86,7 @@ private: assert(found); } - for (int i = 0; i < children.size(); i++) + for (size_t i = 0; i < children.size(); i++) { // call check on all the children. children[i]->checkInvariant(); @@ -116,7 +116,7 @@ private: return n; ASTVec newChildren; - for (int i = 0; i < children.size(); i++) + for (size_t i = 0; i < children.size(); i++) newChildren.push_back(children[i]->toASTNode(nf)); // Don't use the hashing node factory here. Imagine CreateNode simplified down, @@ -189,7 +189,7 @@ private: removeChildren(vars); // ignore the result children.clear(); children.insert(children.begin(), newN->children.begin(), newN->children.end()); - for (int i = 0; i < children.size(); i++) + for (size_t i = 0; i < children.size(); i++) children[i]->parents.insert(this); propagateUpDirty(); @@ -249,7 +249,7 @@ private: ASTNode& node = all[i]->n; bool found[node.GetValueWidth()]; - for (int j=0; j maxV,i)) CONSTANTBV::BitVector_Bit_On(result->maxV,i); @@ -509,7 +509,7 @@ namespace BEEV CONSTANTBV::BitVector_Bit_Off(result->minV,i); } - for (int i=n[0].GetValueWidth(); i < n.GetValueWidth();i++) + for (unsigned int i=n[0].GetValueWidth(); i < n.GetValueWidth();i++) CONSTANTBV::BitVector_Bit_Off(result->maxV,i); } } else if (knownC1) @@ -517,13 +517,13 @@ namespace BEEV // Ignores what's already there for now.. IntervalType * circ_result = freshUnsignedInterval(n.GetValueWidth()); - for (int i=0; i < n[0].GetValueWidth()-1;i++) + for (unsigned int i=0; i < n[0].GetValueWidth()-1;i++) { CONSTANTBV::BitVector_Bit_On(circ_result->maxV,i); CONSTANTBV::BitVector_Bit_Off(circ_result->minV,i); } - for (int i=n[0].GetValueWidth()-1; i < n.GetValueWidth();i++) + for (unsigned int i=n[0].GetValueWidth()-1; i < n.GetValueWidth();i++) { CONSTANTBV::BitVector_Bit_Off(circ_result->maxV,i); CONSTANTBV::BitVector_Bit_On(circ_result->minV,i); @@ -598,7 +598,7 @@ namespace BEEV CONSTANTBV::BitVector_increment(result->maxV); bool bad= false; - for (int i =0; i < children.size(); i++) + for (size_t i =0; i < children.size(); i++) { if (children[i] == NULL) { @@ -611,10 +611,10 @@ namespace BEEV e = CONSTANTBV::BitVector_Multiply(max, result->maxV, children[i]->maxV); assert (0 == e); - if (CONSTANTBV::Set_Max(max) >= width) + if (CONSTANTBV::Set_Max(max) >= (long)width) bad = true; - for (int j = width; j < 2 * width; j++) + for (unsigned int j = width; j < 2 * width; j++) { if (CONSTANTBV::BitVector_bit_test(min, j)) bad = true; @@ -687,7 +687,7 @@ namespace BEEV bool carry = false; - for (int i =0; i < children.size(); i++) + for (size_t i =0; i < children.size(); i++) { if (children[i] == NULL) { @@ -716,7 +716,7 @@ namespace BEEV if (knownC1) { // Copy in the minimum and maximum. - for (int i=0; i < n[1].GetValueWidth();i++) + for (unsigned int i=0; i < n[1].GetValueWidth();i++) { if (CONSTANTBV::BitVector_bit_test(children[1]->maxV,i)) CONSTANTBV::BitVector_Bit_On(result->maxV,i); @@ -733,7 +733,7 @@ namespace BEEV if (knownC0) { // Copy in the minimum and maximum. - for (int i=n[1].GetValueWidth(); i < n.GetValueWidth();i++) + for (unsigned int i=n[1].GetValueWidth(); i < n.GetValueWidth();i++) { if (CONSTANTBV::BitVector_bit_test(children[0]->maxV,i- n[1].GetValueWidth())) CONSTANTBV::BitVector_Bit_On(result->maxV,i); @@ -754,7 +754,7 @@ namespace BEEV bool nonNull = true; // If all the children are known, output 'em. - for (int i=0; i < n.Degree();i++) + for (size_t i=0; i < n.Degree();i++) { if (children[i]== NULL) nonNull=false; @@ -763,7 +763,7 @@ namespace BEEV if (false && nonNull && n.GetKind() != SYMBOL && n.GetKind() != AND) { cerr << n; - for (int i=0; i < n.Degree();i++) + for (size_t i=0; i < n.Degree();i++) children[i]->print(); } } @@ -796,10 +796,10 @@ namespace BEEV ~EstablishIntervals() { - for (int i =0; i < toDeleteLater.size();i++) + for (size_t i =0; i < toDeleteLater.size();i++) delete toDeleteLater[i]; - for (int i =0; i < likeAutoPtr.size();i++) + for (size_t i =0; i < likeAutoPtr.size();i++) CONSTANTBV::BitVector_Destroy(likeAutoPtr[i]); likeAutoPtr.clear(); --- ./src/simplifier/constantBitP/ConstantBitP_Shifting.cpp.orig 2010-11-27 20:45:32.000000000 -0700 +++ ./src/simplifier/constantBitP/ConstantBitP_Shifting.cpp 2012-01-10 16:05:21.211610249 -0700 @@ -204,8 +204,6 @@ Result bvArithmeticRightShiftBothWays(ve assert(children[0]->getWidth() == children[1]->getWidth()); const unsigned MSBIndex = bitWidth-1; - Result result = NO_CHANGE; - FixedBits& op = *children[0]; FixedBits& shift = *children[1]; @@ -393,7 +391,6 @@ Result bvArithmeticRightShiftBothWays(ve { shift.setFixed(i, true); shift.setValue(i, setOfPossibleShifts.getValue(i)); - result = CHANGED; } else if (shift.isFixed(i) && shift.getValue(i) != setOfPossibleShifts.getValue(i)) @@ -550,7 +547,6 @@ Result bvArithmeticRightShiftBothWays(ve { output.setFixed(column, true); output.setValue(column, allFixedTo); - result = CHANGED; } } } @@ -563,8 +559,6 @@ Result bvLeftShiftBothWays(vector 0); - Result result = NO_CHANGE; - FixedBits& op = *children[0]; FixedBits& shift = *children[1]; @@ -761,7 +755,6 @@ Result bvLeftShiftBothWays(vectorpush(n[i]); } @@ -462,7 +462,7 @@ namespace simplifier assert(FixedBits::equals(newBits, current)); - for (int i = 0; i < n.Degree(); i++) + for (size_t i = 0; i < n.Degree(); i++) { if (!FixedBits::equals(*getUpdatedFixedBits(n[i]), childrenFixedBits[i])) --- ./src/simplifier/constantBitP/ConstantBitP_Comparison.cpp.orig 2010-11-27 20:45:32.000000000 -0700 +++ ./src/simplifier/constantBitP/ConstantBitP_Comparison.cpp 2012-01-10 16:05:21.212610229 -0700 @@ -110,8 +110,6 @@ void destroy(CBV a, CBV b, CBV c, CBV d) 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); @@ -135,7 +133,6 @@ Result bvSignedLessThanBothWays(FixedBit { output.setFixed(0, true); output.setValue(0, true); - r = CHANGED; } } @@ -153,7 +150,6 @@ Result bvSignedLessThanBothWays(FixedBit { output.setFixed(0, true); output.setValue(0, false); - r = CHANGED; } } @@ -183,7 +179,6 @@ Result bvSignedLessThanBothWays(FixedBit c0.setFixed(msb, true); c0.setValue(msb, true); setSignedMinMax(c0, c0_min, c0_max); - r = CHANGED; } else { @@ -199,7 +194,6 @@ Result bvSignedLessThanBothWays(FixedBit c1.setFixed(msb, true); c1.setValue(msb, false); setSignedMinMax(c1, c1_min, c1_max); - r = CHANGED; } else { @@ -222,7 +216,6 @@ Result bvSignedLessThanBothWays(FixedBit c0.setFixed(i, true); c0.setValue(i, false); setSignedMinMax(c0, c0_min, c0_max); - r = CHANGED; } else { @@ -242,7 +235,6 @@ Result bvSignedLessThanBothWays(FixedBit c1.setFixed(i, true); c1.setValue(i, true); setSignedMinMax(c1, c1_min, c1_max); - r = CHANGED; } else { @@ -259,8 +251,6 @@ Result bvSignedLessThanBothWays(FixedBit 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); @@ -283,7 +273,6 @@ Result bvSignedLessThanEqualsBothWays(Fi { output.setFixed(0, true); output.setValue(0, true); - r = CHANGED; } } @@ -299,7 +288,6 @@ Result bvSignedLessThanEqualsBothWays(Fi { output.setFixed(0, true); output.setValue(0, false); - r = CHANGED; } } @@ -329,7 +317,6 @@ Result bvSignedLessThanEqualsBothWays(Fi c0.setFixed(msb, true); c0.setValue(msb, true); setSignedMinMax(c0, c0_min, c0_max); - r = CHANGED; } else { @@ -345,7 +332,6 @@ Result bvSignedLessThanEqualsBothWays(Fi c1.setFixed(msb, true); c1.setValue(msb, false); setSignedMinMax(c1, c1_min, c1_max); - r = CHANGED; } else { @@ -412,8 +398,6 @@ Result bvSignedLessThanEqualsBothWays(Fi // 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); @@ -467,8 +451,6 @@ Result bvLessThanBothWays(FixedBits& c0, 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 @@ -484,7 +466,6 @@ Result bvLessThanBothWays(FixedBits& c0, c0.setFixed(i, true); c0.setValue(i, false); setUnsignedMinMax(c0, c0_min, c0_max); - changed = true; } else { @@ -504,7 +485,6 @@ Result bvLessThanBothWays(FixedBits& c0, c1.setFixed(i, true); c1.setValue(i, true); setUnsignedMinMax(c1, c1_min, c1_max); - changed = true; } else { @@ -521,8 +501,6 @@ Result bvLessThanBothWays(FixedBits& c0, 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); --- ./src/simplifier/constantBitP/multiplication/ImplicationGraph.h.orig 2012-01-01 19:35:12.000000000 -0700 +++ ./src/simplifier/constantBitP/multiplication/ImplicationGraph.h 2012-01-10 16:12:04.745158953 -0700 @@ -106,13 +106,13 @@ class ImplicationGraph if (debug_multiply) { cout << "left"; - for (int i = 0; i < left.size(); i++) + for (size_t i = 0; i < left.size(); i++) { cout << "[" << i << ":" << left[i].size() << "] "; } cout << "right"; - for (int i = 0; i < right.size(); i++) + for (size_t i = 0; i < right.size(); i++) { cout << "[" << i << ":" << right[i].size() << "] "; @@ -512,8 +512,6 @@ public: if (!ok) return CONFLICT; - Result r; - bool changed = writeIn(left_assigned, left); changed = writeIn(right_assigned, right) | changed; @@ -578,7 +576,7 @@ public: } bool allAlreadyMin = true; - for (int i = 0; i < bitWidth; i++) + for (unsigned int i = 0; i < bitWidth; i++) if (min[i] != 0) allAlreadyMin = false; --- ./src/simplifier/constantBitP/ConstantBitP_Division.cpp.orig 2012-01-01 19:28:47.000000000 -0700 +++ ./src/simplifier/constantBitP/ConstantBitP_Division.cpp 2012-01-10 16:10:56.223982228 -0700 @@ -172,14 +172,14 @@ Result bvUnsignedQuotientAndRemainder(ve if (whatIs == QUOTIENT_IS_OUTPUT) { setUnsignedMinMax(output, minQuotient, maxQuotient); - for (int i = 0; i < width; i++) + for (unsigned int i = 0; i < width; i++) CONSTANTBV::BitVector_Bit_On(maxRemainder, i); } else { setUnsignedMinMax(output, minRemainder, maxRemainder); - for (int i =0; i < width;i++) + for (unsigned int i =0; i < width;i++) CONSTANTBV::BitVector_Bit_On(maxQuotient,i); } --- ./src/simplifier/constantBitP/ConstantBitP_Arithmetic.cpp.orig 2010-11-27 20:45:32.000000000 -0700 +++ ./src/simplifier/constantBitP/ConstantBitP_Arithmetic.cpp 2012-01-10 16:05:21.213610209 -0700 @@ -33,7 +33,6 @@ Result bvSubtractBothWays(vector& children, FixedBits& output) { - Result result = NO_CHANGE; - const int bitWidth = output.getWidth(); const int numberOfChildren = children.size(); @@ -361,7 +356,6 @@ Result bvAddBothWays(vector& { output.setFixed(column, true); output.setValue(column, newResult); - result = CHANGED; changed = true; } else if (output.isFixed(column) && (output.getValue(column) != newResult)) --- ./src/simplifier/FindPureLiterals.h.orig 2011-12-19 17:30:14.000000000 -0700 +++ ./src/simplifier/FindPureLiterals.h 2012-01-10 16:05:21.214610188 -0700 @@ -109,7 +109,7 @@ public: { case AND: case OR: - for (int i =0; i < n.Degree(); i ++) + for (size_t i =0; i < n.Degree(); i ++) build(n[i],polarity); break; @@ -120,7 +120,7 @@ public: default: polarity = bothPolarity; // both - for (int i =0; i < n.Degree(); i ++) + for (size_t i =0; i < n.Degree(); i ++) build(n[i],polarity); break; } --- ./src/simplifier/VariablesInExpression.cpp.orig 2011-02-01 05:41:57.000000000 -0700 +++ ./src/simplifier/VariablesInExpression.cpp 2012-01-10 16:05:21.214610188 -0700 @@ -42,7 +42,7 @@ Symbols* VariablesInExpression::getSymbo } vector children; - for (int i = 0; i < n.Degree(); i++) { + for (size_t i = 0; i < n.Degree(); i++) { Symbols* v = getSymbol(n[i]); if (!v->empty()) children.push_back(v); @@ -111,7 +111,7 @@ ASTNodeSet * VariablesInExpression::Seto vector av; VarSeenInTerm(symbol,visited,*symbols,av); - for (int i =0; i < av.size();i++) + for (size_t i =0; i < av.size();i++) { const ASTNodeSet& sym = *TermsAlreadySeenMap.find(av[i])->second; symbols->insert(sym.begin(), sym.end()); @@ -155,7 +155,7 @@ bool VariablesInExpression::VarSeenInTer sort(av.begin(), av.end()); //cout << "===" << endl; - for (int i = 0; i < av.size(); i++) { + for (size_t i = 0; i < av.size(); i++) { if (i!=0 && av[i] == av[i-1]) continue; --- ./src/simplifier/SubstitutionMap.cpp.orig 2011-12-28 20:17:45.000000000 -0700 +++ ./src/simplifier/SubstitutionMap.cpp 2012-01-10 16:05:21.215610168 -0700 @@ -199,7 +199,7 @@ void SubstitutionMap::buildDepends(const vars.VarSeenInTerm(vars.getSymbol(n1), rhs_visited, rhs, av); sort(av.begin(), av.end()); - for (int i =0; i < av.size();i++) + for (size_t i =0; i < av.size();i++) { if (i!=0 && av[i] == av[i-1]) continue; // Treat it like a set of Symbol* in effect. --- ./src/simplifier/simplifier.cpp.orig 2012-01-05 06:04:33.000000000 -0700 +++ ./src/simplifier/simplifier.cpp 2012-01-10 16:10:08.282375196 -0700 @@ -241,7 +241,7 @@ namespace BEEV assert(false); } - for (int i = 0; i < n.Degree(); i++) + for (size_t i = 0; i < n.Degree(); i++) { checkIfInSimplifyMap(n[i], visited); } @@ -516,6 +516,7 @@ namespace BEEV return getConstantBit(n[0], i); assert(false); + return -1; } ASTNode @@ -1284,7 +1285,7 @@ namespace BEEV else { ASTVec newC; - for (int i = 0; i < a.GetChildren().size(); i++) + for (size_t i = 0; i < a.GetChildren().size(); i++) { newC.push_back(SimplifyFormula(a[i], false, VarConstMap)); } @@ -1646,9 +1647,9 @@ namespace BEEV assert(BVMULT == k || SBVDIV == k || BVPLUS ==k); const int inputValueWidth = output.GetValueWidth(); - int lengthA = output.GetChildren()[0][0].GetValueWidth(); - int lengthB = output.GetChildren()[1][0].GetValueWidth(); - int maxLength; + unsigned int lengthA = output.GetChildren()[0][0].GetValueWidth(); + unsigned int lengthB = output.GetChildren()[1][0].GetValueWidth(); + unsigned int maxLength; if (BVMULT == output.GetKind()) maxLength = lengthA + lengthB; else if (BVPLUS == output.GetKind() || SBVDIV == output.GetKind()) @@ -1676,7 +1677,7 @@ namespace BEEV { const ASTNode a = children[0]; const ASTNode b = children[1]; - const int width = children[0].GetValueWidth(); + const unsigned int width = children[0].GetValueWidth(); ASTNode output; assert(b.isConstant()); @@ -1707,7 +1708,7 @@ namespace BEEV { const ASTNode a = children[0]; const ASTNode b = children[1]; - const int width = children[0].GetValueWidth(); + const unsigned int width = children[0].GetValueWidth(); ASTNode output; assert(b.isConstant()); @@ -1888,7 +1889,7 @@ namespace BEEV //I haven't measured if this is worth the expense. { bool notSimplified = false; - for (int i = 0; i < inputterm.Degree(); i++) + for (size_t i = 0; i < inputterm.Degree(); i++) if (inputterm[i].GetType() != ARRAY_TYPE) if (!hasBeenSimplified(inputterm[i])) { @@ -2229,7 +2230,6 @@ namespace BEEV case BVEXTRACT: { const unsigned innerLow = a0[2].GetUnsignedConst(); - const unsigned innerHigh = a0[1].GetUnsignedConst(); output = nf->CreateTerm(BVEXTRACT, inputValueWidth, a0[0], _bm->CreateBVConst(32, i_val + innerLow), _bm->CreateBVConst(32, j_val + innerLow)); @@ -2629,7 +2629,7 @@ namespace BEEV assert(BVTypeCheck(output)); // If the leading bits are zero. Replace it by a concat with zero. - int i; + unsigned int i; if (output.GetKind() == BVAND && output.Degree() == 2 && ((i = numberOfLeadingZeroes(output[0])) > 0)) { // i contains the number of leading zeroes. @@ -2651,13 +2651,13 @@ namespace BEEV } if (output.GetKind() == BVAND) { - int trailingZeroes = 0; - for (int i = 0; i < output.Degree(); i++) + unsigned int trailingZeroes = 0; + for (size_t i = 0; i < output.Degree(); i++) { const ASTNode& n = output[i]; if (n.GetKind() != BVCONST) continue; - int j; + unsigned int j; for (j = 0; j < n.GetValueWidth(); j++) if (CONSTANTBV::BitVector_bit_test(n.GetBVConst(), j)) break; @@ -2674,7 +2674,7 @@ namespace BEEV //cerr << "old" << output; ASTNode zeroes = _bm->CreateZeroConst(trailingZeroes); ASTVec newChildren; - for (int i = 0; i < output.Degree(); i++) + for (size_t i = 0; i < output.Degree(); i++) newChildren.push_back( nf->CreateTerm(BVEXTRACT, output.GetValueWidth() - trailingZeroes, output[i], _bm->CreateBVConst(32, output.GetValueWidth() - 1), --- ./src/simplifier/consteval.cpp.orig 2011-12-28 19:00:01.000000000 -0700 +++ ./src/simplifier/consteval.cpp 2012-01-10 16:05:21.217610127 -0700 @@ -43,7 +43,7 @@ namespace BEEV ASTVec children; children.reserve(number_of_children); - for (int i =0; i < number_of_children; i++) + for (unsigned int i =0; i < number_of_children; i++) { if (input_children[i].isConstant()) children.push_back(input_children[i]); --- ./src/simplifier/SubstitutionMap.h.orig 2011-12-28 20:17:45.000000000 -0700 +++ ./src/simplifier/SubstitutionMap.h 2012-01-10 16:05:21.218610106 -0700 @@ -40,7 +40,7 @@ class SubstitutionMap { void loops_helper(const set& varsToCheck, set& visited); bool loops(const ASTNode& n0, const ASTNode& n1); - int substitutionsLastApplied; + size_t substitutionsLastApplied; public: bool hasUnappliedSubstitutions() --- ./src/simplifier/RemoveUnconstrained.cpp.orig 2011-12-28 19:00:01.000000000 -0700 +++ ./src/simplifier/RemoveUnconstrained.cpp 2012-01-10 16:05:21.218610106 -0700 @@ -60,7 +60,7 @@ namespace BEEV bool allChildrenAreUnconstrained(vector children) { - for (int i =0; i < children.size(); i++) + for (size_t i =0; i < children.size(); i++) if (!children[i]->isUnconstrained()) return false; @@ -105,7 +105,7 @@ namespace BEEV // Going to be rebuilt later anyway, so discard. vector variables; - for (int i =0; i n; assert(var.GetKind() == SYMBOL); @@ -156,7 +156,7 @@ namespace BEEV } ASTNode concat = concatVec[0]; - for (int i=1; i < concatVec.size();i++) + for (size_t i=1; i < concatVec.size();i++) { assert(!concat.IsNull()); concat = bm.CreateTerm(BVCONCAT, concat.GetValueWidth() + concatVec[i].GetValueWidth(),concatVec[i], concat); @@ -189,7 +189,7 @@ namespace BEEV topMutable->getAllUnconstrainedVariables(variable_array); - for (int i =0; i < variable_array.size() ; i++) + for (size_t i =0; i < variable_array.size() ; i++) { // Don't make this is a reference. If the vector gets resized, it will point to // memory that no longer contains the object. @@ -213,7 +213,7 @@ namespace BEEV //nb. The children might be dirty. i.e. not have substitutions written through them yet. ASTVec children; children.reserve(mutable_children.size()); - for (int j = 0; j n); const size_t numberOfChildren = children.size(); @@ -247,7 +247,7 @@ namespace BEEV { int found = 0; - for (int i = 0; i < numberOfChildren; i++) + for (size_t i = 0; i < numberOfChildren; i++) { if (children[i] == var) found++; @@ -434,7 +434,7 @@ namespace BEEV { ASTNodeSet already; ASTNode v =replaceParentWithFresh(muteParent, variable_array); - for (int i =0; i < numberOfChildren;i++) + for (size_t i =0; i < numberOfChildren;i++) { /* to avoid problems with: 734:(AND @@ -469,7 +469,7 @@ namespace BEEV ASTNode v =replaceParentWithFresh(muteParent, variable_array); ASTVec others; - for (int i = 0; i < numberOfChildren; i++) + for (size_t i = 0; i < numberOfChildren; i++) { if (children[i] !=var) others.push_back(mutable_children[i]->toASTNode(nf)); @@ -622,7 +622,7 @@ namespace BEEV case BVPLUS: { ASTVec other; - for (int i = 0; i < children.size(); i++) + for (size_t i = 0; i < children.size(); i++) if (children[i] != var) other.push_back(mutable_children[i]->toASTNode(nf)); @@ -644,7 +644,6 @@ namespace BEEV { ASTNode v =replaceParentWithFresh(muteParent, variable_array); - const unsigned resultWidth = width; const unsigned operandWidth = var.GetValueWidth(); assert(children[0] == var); // It can't be anywhere else. --- ./src/absrefine_counterexample/CounterExample.cpp.orig 2011-11-10 06:01:41.000000000 -0700 +++ ./src/absrefine_counterexample/CounterExample.cpp 2012-01-10 16:05:21.219610086 -0700 @@ -46,7 +46,7 @@ namespace BEEV assert(symbol.GetKind() == SYMBOL); vector bitVector_array(symbolWidth,false); - for (int index = 0; index < v.size(); index++) + for (size_t index = 0; index < v.size(); index++) { const unsigned sat_variable_index = v[index]; @@ -863,7 +863,7 @@ namespace BEEV ASTNode symbol = it->first; vector v = it->second; - for (int i =0 ; i < v.size();i++) + for (size_t i =0 ; i < v.size();i++) { if (v[i] == ~((unsigned)0)) // nb. special value. continue; --- ./src/absrefine_counterexample/AbstractionRefinement.cpp.orig 2012-01-05 06:04:33.000000000 -0700 +++ ./src/absrefine_counterexample/AbstractionRefinement.cpp 2012-01-10 16:05:21.220610066 -0700 @@ -35,7 +35,7 @@ namespace BEEV { assert(a.GetKind() == SYMBOL); // It was ommitted from the initial problem, so assign it freshly. - for (int i = 0; i < a.GetValueWidth(); i++) + for (unsigned int i = 0; i < a.GetValueWidth(); i++) { SATSolver::Var v = SatSolver.newVar(); // We probably don't want the variable eliminated. @@ -55,7 +55,7 @@ namespace BEEV getEquals(SATSolver& SatSolver, const ASTNode& a, const ASTNode& b, ToSATBase::ASTNodeToSATVar& satVar, Polarity polary = BOTH) { - const int width = a.GetValueWidth(); + const unsigned int width = a.GetValueWidth(); assert(width == b.GetValueWidth()); assert(!a.isConstant() || !b.isConstant()); @@ -72,7 +72,7 @@ namespace BEEV SATSolver::vec_literals all; const int result = SatSolver.newVar(); - for (int i = 0; i < width; i++) + for (unsigned int i = 0; i < width; i++) { SATSolver::vec_literals s; @@ -116,7 +116,7 @@ namespace BEEV } return result; } - else if (v_a.size() == 0 ^ v_b.size() == 0) + else if ((v_a.size() == 0) ^ (v_b.size() == 0)) { ASTNode constant = a.isConstant() ? a : b; vector vec = v_a.size() == 0 ? v_b : v_a; @@ -128,7 +128,7 @@ namespace BEEV all.push(SATSolver::mkLit(result, false)); CBV v = constant.GetBVConst(); - for (int i = 0; i < width; i++) + for (unsigned int i = 0; i < width; i++) { if (polary != RIGHT_ONLY) { @@ -214,7 +214,7 @@ namespace BEEV void applyAxiomsToSolver(ToSATBase::ASTNodeToSATVar & satVar, vector & toBe, SATSolver & SatSolver) { - for (int i = 0; i < toBe.size(); i++) + for (size_t i = 0; i < toBe.size(); i++) { applyAxiomToSAT(SatSolver, toBe[i], satVar); } @@ -269,7 +269,6 @@ namespace BEEV for (vector >::const_iterator iset = arrayToIndex.begin(), iset_end = arrayToIndex.end(); iset != iset_end; iset++) { - const ASTNode& ArrName = iset->first; const map& mapper = iset->second; vector listOfIndices; @@ -318,13 +317,13 @@ namespace BEEV //loop over the list of indices for the array and create LA, //and add to inputAlreadyInSAT - for (int i = 0; i < listOfIndices.size(); i++) + for (size_t i = 0; i < listOfIndices.size(); i++) { const ASTNode& index_i = listOfIndices[i]; const Kind iKind = index_i.GetKind(); // Create all distinct pairs of indexes. - for (int j = i + 1; j < listOfIndices.size(); j++) + for (size_t j = i + 1; j < listOfIndices.size(); j++) { const ASTNode& index_j = listOfIndices[j]; --- ./src/to-sat/ASTNode/ToSAT.cpp.orig 2011-12-28 19:00:01.000000000 -0700 +++ ./src/to-sat/ASTNode/ToSAT.cpp 2012-01-10 16:05:21.220610066 -0700 @@ -52,7 +52,7 @@ namespace BEEV // Copies the symbol into the map that is used to build the counter example. // For boolean we create a vector of size 1. - if (n.GetKind() == BVGETBIT && n[0].GetKind() == SYMBOL || (n.GetKind() == SYMBOL && !isTseitinVariable(n))) + if ((n.GetKind() == BVGETBIT && n[0].GetKind() == SYMBOL) || (n.GetKind() == SYMBOL && !isTseitinVariable(n))) { const ASTNode& symbol = n.GetKind() == BVGETBIT ? n[0] : n; const unsigned index = n.GetKind() == BVGETBIT ? n[1].GetUnsignedConst() : 0; @@ -98,7 +98,7 @@ namespace BEEV CountersAndStats("SAT Solver", bm); bm->GetRunTimes()->start(RunTimes::SendingToSAT); - int input_clauselist_size = cll.size(); + // int input_clauselist_size = cll.size(); if (cll.size() == 0) { FatalError("toSATandSolve: Nothing to Solve", ASTUndefined); @@ -115,7 +115,7 @@ namespace BEEV //iterate through the list (conjunction) of ASTclauses cll ClauseContainer::const_iterator i = cc.begin(), iend = cc.end(); - for (int count=0, flag=0; i != iend; i++) + for ( ; i != iend; i++) { satSolverClause.clear(); vector::const_iterator j = (*i)->begin(); @@ -312,7 +312,7 @@ namespace BEEV ClauseBuckets::iterator itend = cb->end(); bool sat = false; - for(int count=1;it!=itend;it++, count++) + for(size_t count=1;it!=itend;it++, count++) { ClauseList *cl = (*it).second; sat = toSATandSolve(SatSolver,*cl, count==cb->size(),cm); --- ./src/to-sat/ASTNode/ToCNF.cpp.orig 2011-12-28 19:00:01.000000000 -0700 +++ ./src/to-sat/ASTNode/ToCNF.cpp 2012-01-10 16:05:21.221610046 -0700 @@ -250,12 +250,14 @@ namespace BEEV return psi; } //End of SINGLETON() +#ifdef CRYPTOMINISAT__2 static ASTNode GetNodeFrom_SINGLETON(ClauseList *cl) { ClausePtr c = (*(*cl).asList())[0]; const ASTNode * a = (*c)[0]; return *a; } +#endif //######################################## //######################################## --- ./src/to-sat/BitBlaster.cpp.orig 2012-01-09 20:03:23.000000000 -0700 +++ ./src/to-sat/BitBlaster.cpp 2012-01-10 16:06:28.158957729 -0700 @@ -311,7 +311,7 @@ namespace BEEV bool BitBlaster::isConstant(const BBNodeVec& v) { - for (int i = 0; i < v.size(); i++) + for (size_t i = 0; i < v.size(); i++) { if (v[i] != nf->getTrue() && v[i] != nf->getFalse()) return false; @@ -334,7 +334,7 @@ namespace BEEV CBV bv = CONSTANTBV::BitVector_Create(v.size(), true); - for (int i = 0; i < v.size(); i++) + for (size_t i = 0; i < v.size(); i++) if (v[i] == nf->getTrue()) CONSTANTBV::BitVector_Bit_On(bv, i); @@ -670,14 +670,14 @@ namespace BEEV { // Add all the children up using an addition network. vector results; - for (int i = 0; i < term.Degree(); i++) + for (size_t i = 0; i < term.Degree(); i++) results.push_back(BBTerm(term[i], support)); - const int bitWidth = term[0].GetValueWidth(); + const unsigned int bitWidth = term[0].GetValueWidth(); std::vector > products(bitWidth); - for (int i = 0; i < bitWidth; i++) + for (unsigned int i = 0; i < bitWidth; i++) { - for (int j = 0; j < results.size(); j++) + for (size_t j = 0; j < results.size(); j++) products[i].push_back(results[j][i]); } @@ -1157,7 +1157,7 @@ namespace BEEV const BBNode& BBTrue = nf->getTrue(); const BBNode& BBFalse = nf->getFalse(); - for (int i = 0; i < v.size(); i++) + for (size_t i = 0; i < v.size(); i++) { if (v[i] == BBTrue) result[i] = ONE_MT; @@ -1169,7 +1169,7 @@ namespace BEEV // find runs of ones. int lastOne = -1; - for (int i = 0; i < v.size(); i++) + for (size_t i = 0; i < v.size(); i++) { assert(result[i] != MINUS_ONE_MT); @@ -1179,7 +1179,7 @@ namespace BEEV if (result[i] != ONE_MT && lastOne != -1 && (i - lastOne >= 3)) { result[lastOne] = MINUS_ONE_MT; - for (int j = lastOne + 1; j < i; j++) + for (size_t j = lastOne + 1; j < i; j++) result[j] = ZERO_MT; // Should this be lastOne = i? lastOne = i; @@ -1193,7 +1193,7 @@ namespace BEEV if (lastOne != -1 && (v.size() - lastOne > 1)) { result[lastOne] = MINUS_ONE_MT; - for (int j = lastOne + 1; j < v.size(); j++) + for (size_t j = lastOne + 1; j < v.size(); j++) result[j] = ZERO_MT; } } @@ -1235,7 +1235,7 @@ namespace BEEV BitBlaster::buildAdditionNetworkResult(list* products, set& support, const ASTNode& n) { - const int bitWidth = n.GetValueWidth(); + const unsigned int bitWidth = n.GetValueWidth(); // If we have details of the partial products which can be true, int ignore = -1; @@ -1244,7 +1244,7 @@ namespace BEEV ms = NULL; BBNodeVec results; - for (int i = 0; i < bitWidth; i++) + for (unsigned int i = 0; i < bitWidth; i++) { buildAdditionNetworkResult(products[i], products[i+1], support, (i + 1 == bitWidth), (ms != NULL && (ms->sumH[i] == 0))); @@ -1254,7 +1254,7 @@ namespace BEEV } assert(products[bitWidth].size() ==0); // products[bitwidth] is defined but should never be used. - assert(results.size() == ((unsigned)bitWidth)); + assert(results.size() == bitWidth); return results; } @@ -1356,7 +1356,7 @@ namespace BEEV BitBlaster::multWithBounds(const ASTNode&n, list* products, BBNodeSet& toConjoinToTop) { - const int bitWidth = n.GetValueWidth(); + const unsigned int bitWidth = n.GetValueWidth(); int ignored=0; assert(multiplication_upper_bound); @@ -1365,7 +1365,7 @@ namespace BEEV // If all of the partial products in the column must be zero, then replace - for (int i = 0; i < bitWidth; i++) + for (unsigned int i = 0; i < bitWidth; i++) { if (conjoin_to_top && ms.columnH[i] == 0) { @@ -1387,7 +1387,7 @@ namespace BEEV } vector prior; - for (int i = 0; i < bitWidth; i++) + for (unsigned int i = 0; i < bitWidth; i++) { if (debug_bounds) { @@ -1407,7 +1407,7 @@ namespace BEEV if (debug_bitblaster) cerr << endl << endl; - assert(result.size() == ((unsigned)bitWidth)); + assert(result.size() == bitWidth); return result; } @@ -1431,7 +1431,7 @@ namespace BEEV } BBNodeVec notY; - for (int i = 0; i < y.size(); i++) + for (size_t i = 0; i < y.size(); i++) { notY.push_back(nf->CreateNode(NOT, y[i])); } @@ -1484,7 +1484,7 @@ namespace BEEV t_products[i].push_back(BBFalse); sort(t_products[i].begin(), t_products[i].end()); - for (int j = 0; j < t_products[i].size(); j++) + for (size_t j = 0; j < t_products[i].size(); j++) products[i].push_back(t_products[i][j]); } } @@ -1542,13 +1542,13 @@ namespace BEEV assert(ms->x.getWidth() == ms->y.getWidth()); assert(ms->r.getWidth() == ms->y.getWidth()); assert(ms->r.getWidth() == (int)ms->bitWidth); - } - for (int i = 0; i < n.GetValueWidth(); i++) - if (ms->sumH[i] == 0) - highestZero = i; + for (unsigned int i = 0; i < n.GetValueWidth(); i++) + if (ms->sumH[i] == 0) + highestZero = (int)i; - return ms; + return ms; + } } return NULL; @@ -1560,7 +1560,7 @@ namespace BEEV BitBlaster::mult_normal(const BBNodeVec& x, const BBNodeVec& y, BBNodeSet& support, const ASTNode&n) { - const int bitWidth = n.GetValueWidth(); + const unsigned int bitWidth = n.GetValueWidth(); // If we have details of the partial products which can be true, int highestZero = -1; @@ -1572,7 +1572,7 @@ namespace BEEV BBNodeVec prod = BBNodeVec(BBAndBit(y, *x.begin())); // start prod with first partial product. - for (int i = 1; i < bitWidth; i++) // start loop at next bit. + for (unsigned int i = 1; i < bitWidth; i++) // start loop at next bit. { const BBNode& xit = x[i]; @@ -1589,7 +1589,7 @@ namespace BEEV BBNodeVec pprod = BBAndBit(ycopy, xit); // Iterate through from the current location upwards, setting anything to zero that can be.. - if (ms != NULL && highestZero >= i) + if (ms != NULL && highestZero >= (int)i) { for (int column = i; column <= highestZero; column++) { @@ -1614,7 +1614,7 @@ namespace BEEV { // Add the carry from the prior column. i.e. each second sorted formula. - for (int k = 1; k < priorSorted.size(); k += 2) + for (size_t k = 1; k < priorSorted.size(); k += 2) { current.push_back(priorSorted[k]); } @@ -1694,7 +1694,7 @@ namespace BEEV FixedBits* b = cb->fixedMap->map->find(n)->second; for (int i = 0; i < b->getWidth(); i++) { - if (b->isFixed(i)) + if (b->isFixed(i)) { if (b->getValue(i)) { assert(v[i]== BBTrue); @@ -1711,6 +1711,7 @@ namespace BEEV assert(v[i]== BBFalse); } + } } } } @@ -1734,7 +1735,7 @@ namespace BEEV y = _x; } - const int bitWidth = n.GetValueWidth(); + const unsigned int bitWidth = n.GetValueWidth(); assert(x.size() == bitWidth); assert(y.size() == bitWidth); @@ -1762,7 +1763,7 @@ namespace BEEV mult_Booth(_x, _y, support, n[0], n[1], products.data(), n); vector prior; - for (int i = 0; i < bitWidth; i++) + for (unsigned int i = 0; i < bitWidth; i++) { vector output; mult_BubbleSorterWithBounds(support, products[i], output, prior); @@ -1824,18 +1825,18 @@ namespace BEEV vector b; // half way rounded up. - const int halfWay = (((in.size()%2)==0? 0:1) + (in.size()/2) ); - for (int i =0; i < halfWay;i++) + const size_t halfWay = (((in.size()%2)==0? 0:1) + (in.size()/2) ); + for (size_t i =0; i < halfWay;i++) a.push_back(in[i]); - for (int i =halfWay; i < in.size();i++) + for (size_t i =halfWay; i < in.size();i++) b.push_back(in[i]); assert(a.size() >= b.size()); assert(a.size() + b.size() == in.size()); vector result= mergeSorted(batcher(a), batcher(b)); - for (int k = 0; k < result.size(); k++) + for (size_t k = 0; k < result.size(); k++) assert(!result[k].IsNull()); assert(result.size() == in.size()); @@ -1867,7 +1868,7 @@ namespace BEEV assert(sorted.size() == toSort.size()); vector sortedCarryIn; - for (int k = 1; k < priorSorted.size(); k += 2) + for (size_t k = 1; k < priorSorted.size(); k += 2) { sortedCarryIn.push_back(priorSorted[k]); } @@ -1905,11 +1906,11 @@ namespace BEEV BBNodeVec BitBlaster::v6(list* products, set& support, const ASTNode&n) { - const int bitWidth = n.GetValueWidth(); + const unsigned int bitWidth = n.GetValueWidth(); vector prior; - for (int i = 0; i < bitWidth; i++) + for (unsigned int i = 0; i < bitWidth; i++) { vector output; sortingNetworkAdd(support, products[i], output ,prior); @@ -1928,22 +1929,21 @@ namespace BEEV BBNodeVec BitBlaster::v9(list* products, set& support,const ASTNode&n) { - const int bitWidth = n.GetValueWidth(); + const unsigned int bitWidth = n.GetValueWidth(); vector< vector< BBNode> > toAdd(bitWidth); - for (int column = 0; column < bitWidth; column++) + for (unsigned int column = 0; column < bitWidth; column++) { vector sorted; // The current column (sorted) gets put into here. vector prior; // Prior is always empty in this.. - const int size= products[column].size(); sortingNetworkAdd(support, products[column], sorted ,prior); assert(products[column].size() == 1); assert(sorted.size() == size); - for (int k = 2; k <= sorted.size(); k++) + for (size_t k = 2; k <= sorted.size(); k++) { BBNode part; if (k==sorted.size()) @@ -1958,7 +1958,7 @@ namespace BEEV continue; // shortcut. } - int position =k; + size_t position =k; int increment =1; while (position != 0) { @@ -1973,12 +1973,12 @@ namespace BEEV } } - for (int carry_column =column+1; carry_column < bitWidth; carry_column++) + for (unsigned int carry_column =column+1; carry_column < bitWidth; carry_column++) { if (toAdd[carry_column].size() ==0) continue ; BBNode disjunct = BBFalse; - for (int l = 0; l < toAdd[carry_column].size();l++) + for (size_t l = 0; l < toAdd[carry_column].size();l++) { disjunct = nf->CreateNode(OR,disjunct,toAdd[carry_column][l]); } @@ -1988,7 +1988,7 @@ namespace BEEV toAdd[carry_column].clear(); } } - for (int i = 0; i < bitWidth; i++) + for (unsigned int i = 0; i < bitWidth; i++) { assert(toAdd[i].size() == 0); } @@ -2002,7 +2002,7 @@ namespace BEEV BBNodeVec BitBlaster::v7(list* products, set& support, const ASTNode&n) { - const int bitWidth = n.GetValueWidth(); + const unsigned int bitWidth = n.GetValueWidth(); // If we have details of the partial products which can be true, int ignore = -1; @@ -2014,13 +2014,13 @@ namespace BEEV std::vector > later(bitWidth+1); std::vector > next(bitWidth+1); - for (int i = 0; i < bitWidth; i++) + for (unsigned int i = 0; i < bitWidth; i++) { next[i+1].clear(); buildAdditionNetworkResult(products[i], next[i + 1], support, bitWidth == i+1, (ms!=NULL && (ms->sumH[i]==0))); // Calculate the carries of carries. - for (int j = i + 1; j < bitWidth; j++) + for (unsigned int j = i + 1; j < bitWidth; j++) { if (next[j].size() == 0) break; @@ -2030,7 +2030,7 @@ namespace BEEV } // Put the carries of the carries away until later. - for (int j = i + 1; j < bitWidth; j++) + for (unsigned int j = i + 1; j < bitWidth; j++) { if (next[j].size() == 0) break; @@ -2041,7 +2041,7 @@ namespace BEEV } - for (int i = 0; i < bitWidth; i++) + for (unsigned int i = 0; i < bitWidth; i++) { // Copy all the laters into products while(later[i].size() > 0) @@ -2052,7 +2052,7 @@ namespace BEEV } BBNodeVec results; - for (int i = 0; i < bitWidth; i++) + for (unsigned int i = 0; i < bitWidth; i++) { buildAdditionNetworkResult((products[i]), (products[i + 1]), support, bitWidth == i+1, false); @@ -2062,7 +2062,7 @@ namespace BEEV products[i].pop_back(); } - assert(results.size() == ((unsigned)bitWidth)); + assert(results.size() == bitWidth); return results; } @@ -2071,7 +2071,7 @@ namespace BEEV BBNodeVec BitBlaster::v8(list* products, set& support, const ASTNode&n) { - const int bitWidth = n.GetValueWidth(); + const unsigned int bitWidth = n.GetValueWidth(); // If we have details of the partial products which can be true, int ignore = -1; @@ -2084,14 +2084,14 @@ namespace BEEV std::vector > later(bitWidth+1); // +1 then ignore the topmost. std::vector > next(bitWidth+1); - for (int i = 0; i < bitWidth; i++) + for (unsigned int i = 0; i < bitWidth; i++) { // Put all the products into next. next[i+1].clear(); buildAdditionNetworkResult((products[i]), (next[i + 1]), support, i+1 ==bitWidth, (ms!=NULL && (ms->sumH[i]==0))); // Calculate the carries of carries. - for (int j = i + 1; j < bitWidth; j++) + for (unsigned int j = i + 1; j < bitWidth; j++) { if (next[j].size() == 0) break; @@ -2101,7 +2101,7 @@ namespace BEEV } // Put the carries of the carries away until later. - for (int j = i + 1; j < bitWidth; j++) + for (unsigned int j = i + 1; j < bitWidth; j++) { if (next[j].size() == 0) break; @@ -2112,7 +2112,7 @@ namespace BEEV } - for (int i = 0; i < bitWidth; i++) + for (unsigned int i = 0; i < bitWidth; i++) { // Copy all the laters into products while(later[i].size() > 0) @@ -2123,14 +2123,14 @@ namespace BEEV } BBNodeVec results; - for (int i = 0; i < bitWidth; i++) + for (unsigned int i = 0; i < bitWidth; i++) { buildAdditionNetworkResult(products[i], products[i + 1], support, i+1 ==bitWidth, false); results.push_back(products[i].back()); products[i].pop_back(); } - assert(results.size() == ((unsigned)bitWidth)); + assert(results.size() == bitWidth); return results; } @@ -2142,7 +2142,7 @@ namespace BEEV { vector result(in); - for (int i = 2; i < in.size(); i =i+ 2) + for (size_t i = 2; i < in.size(); i =i+ 2) { BBNode a = in[i-1]; BBNode b = in[i]; @@ -2179,7 +2179,7 @@ namespace BEEV { vector evenL; vector oddL; - for (int i =0; i < in1.size();i++) + for (size_t i =0; i < in1.size();i++) { if (i%2 ==0) evenL.push_back(in1[i]); @@ -2189,7 +2189,7 @@ namespace BEEV vector evenR; // Take the even of each. vector oddR; // Take the odd of each - for (int i =0; i < in2.size();i++) + for (size_t i =0; i < in2.size();i++) { if (i%2 ==0) evenR.push_back(in2[i]); @@ -2200,7 +2200,7 @@ namespace BEEV vector even = evenL.size()< evenR.size() ? mergeSorted(evenR,evenL) : mergeSorted(evenL,evenR); vector odd = oddL.size() < oddR.size() ? mergeSorted(oddR,oddL) : mergeSorted(oddL,oddR); - for (int i =0; i < std::max(even.size(),odd.size());i++) + for (size_t i =0; i < std::max(even.size(),odd.size());i++) { if (even.size() > i) result.push_back(even[i]); @@ -2245,7 +2245,7 @@ namespace BEEV // check if y is already zero. bool isZero = true; - for (int i = 0; i < rwidth; i++) + for (unsigned int i = 0; i < rwidth; i++) if (y[i] != nf->getFalse()) { isZero = false; --- ./src/to-sat/AIG/BBNodeManagerAIG.h.orig 2011-02-01 22:39:54.000000000 -0700 +++ ./src/to-sat/AIG/BBNodeManagerAIG.h 2012-01-10 16:05:21.224609986 -0700 @@ -142,7 +142,7 @@ public: Aig_Obj_t * pNode; assert (children.size() != 0); - for (int i =0; i < children.size();i++) + for (size_t i =0; i < children.size();i++) assert(!children[i].IsNull()); switch (kind) --- ./src/to-sat/AIG/ToSATAIG.cpp.orig 2011-12-31 07:51:52.000000000 -0700 +++ ./src/to-sat/AIG/ToSATAIG.cpp 2012-01-10 16:05:21.225609966 -0700 @@ -126,7 +126,7 @@ namespace BEEV if (it != nodeToSATVar.end()) { const vector& v = it->second; - for (int i = 0; i < v.size(); i++) + for (size_t i = 0; i < v.size(); i++) satSolver.setFrozen(v[i]); } @@ -134,7 +134,7 @@ namespace BEEV if (it2 != nodeToSATVar.end()) { const vector& v = it2->second; - for (int i = 0; i < v.size(); i++) + for (size_t i = 0; i < v.size(); i++) satSolver.setFrozen(v[i]); } } @@ -185,7 +185,7 @@ namespace BEEV vector v_a; assert(ar.index_symbol.GetKind() == SYMBOL); // It was ommitted from the initial problem, so assign it freshly. - for (int i = 0; i < ar.index_symbol.GetValueWidth(); i++) + for (unsigned int i = 0; i < ar.index_symbol.GetValueWidth(); i++) { SATSolver::Var v = satSolver.newVar(); // We probably don't want the variable eliminated. @@ -194,7 +194,7 @@ namespace BEEV } nodeToSATVar.insert(make_pair(ar.index_symbol, v_a)); - for (int i = 0; i < v_a.size(); i++) + for (size_t i = 0; i < v_a.size(); i++) { SATSolver::Var var = v_a[i]; index.push(SATSolver::mkLit(var, false)); @@ -210,7 +210,7 @@ namespace BEEV if (it != nodeToSATVar.end()) { vector& v = it->second; - for (int i = 0; i < v.size(); i++) + for (size_t i = 0; i < v.size(); i++) { SATSolver::Var var = v[i]; value.push(SATSolver::mkLit(var, false)); @@ -219,7 +219,7 @@ namespace BEEV else if (ar.symbol.isConstant()) { CBV c = ar.symbol.GetBVConst(); - for (int i = 0; i < ar.symbol.GetValueWidth(); i++) + for (unsigned int i = 0; i < ar.symbol.GetValueWidth(); i++) if (CONSTANTBV::BitVector_bit_test(c, i)) value_constants.push((Minisat::lbool) satSolver.true_literal()); else @@ -233,7 +233,7 @@ namespace BEEV assert(ar.symbol.GetKind() == SYMBOL); // It was ommitted from the initial problem, so assign it freshly. - for (int i = 0; i < ar.symbol.GetValueWidth(); i++) + for (unsigned int i = 0; i < ar.symbol.GetValueWidth(); i++) { SATSolver::Var v = satSolver.newVar(); // We probably don't want the variable eliminated. @@ -242,7 +242,7 @@ namespace BEEV } nodeToSATVar.insert(make_pair(ar.symbol, v_a)); - for (int i = 0; i < v_a.size(); i++) + for (size_t i = 0; i < v_a.size(); i++) { SATSolver::Var var = v_a[i]; value.push(SATSolver::mkLit(var, false)); --- ./src/c_interface/c_interface.cpp.orig 2011-12-21 22:12:52.000000000 -0700 +++ ./src/c_interface/c_interface.cpp 2012-01-10 16:05:21.225609966 -0700 @@ -516,7 +516,6 @@ void vc_printCounterExample(VC vc) { Expr vc_getCounterExample(VC vc, Expr e) { nodestar a = (nodestar)e; - bmstar b = (bmstar)(((stpstar)vc)->bm); ctrexamplestar ce = (ctrexamplestar)(((stpstar)vc)->Ctr_Example); bool t = false; @@ -529,7 +528,6 @@ Expr vc_getCounterExample(VC vc, Expr e) void vc_getCounterExampleArray(VC vc, Expr e, Expr **indices, Expr **values, int *size) { nodestar a = (nodestar)e; - bmstar b = (bmstar)(((stpstar)vc)->bm); ctrexamplestar ce = (ctrexamplestar)(((stpstar)vc)->Ctr_Example); bool t = false; @@ -549,7 +547,6 @@ void vc_getCounterExampleArray(VC vc, Ex } int vc_counterexample_size(VC vc) { - bmstar b = (bmstar)(((stpstar)vc)->bm); ctrexamplestar ce = (ctrexamplestar)(((stpstar)vc)->Ctr_Example); return ce->CounterExampleSize(); @@ -941,7 +938,7 @@ Expr vc_bvConstExprFromInt(VC vc, bmstar b = (bmstar)(((stpstar)vc)->bm); unsigned long long int v = (unsigned long long int)value; - unsigned long long int max_n_bits = 0xFFFFFFFFFFFFFFFFULL >> 64-n_bits; + unsigned long long int max_n_bits = 0xFFFFFFFFFFFFFFFFULL >> (64-n_bits); //printf("%ull", max_n_bits); if(v > max_n_bits) { printf("CInterface: vc_bvConstExprFromInt: "\ @@ -1484,16 +1481,11 @@ Expr vc_bvWriteToMemoryArray(VC vc, return vc_writeExpr(vc, array, byteIndex, element); else { int count = 1; - int hi = newBitsPerElem - 1; - int low = newBitsPerElem - 8; int low_elem = 0; int hi_elem = low_elem + 7; Expr c = vc_bvExtract(vc, element, hi_elem, low_elem); Expr newarray = vc_writeExpr(vc, array, byteIndex, c); while(--numOfBytes > 0) { - hi = low-1; - low = low-8; - low_elem = low_elem + 8; hi_elem = low_elem + 7; @@ -1668,7 +1660,6 @@ int vc_isBool(Expr e) { } void vc_Destroy(VC vc) { - bmstar b = (bmstar)(((stpstar)vc)->bm); // for(std::vector::iterator it=created_exprs.begin(), // itend=created_exprs.end();it!=itend;it++) { // BEEV::ASTNode * aaa = *it; --- ./src/printer/SMTLIB2Printer.cpp.orig 2010-07-10 08:49:13.000000000 -0600 +++ ./src/printer/SMTLIB2Printer.cpp 2012-01-10 16:05:21.226609946 -0700 @@ -210,7 +210,7 @@ void printVarDeclsToStream(ASTNodeSet& s { string close = ""; - for (int i =0; i < c.size()-1; i++) + for (size_t i =0; i < c.size()-1; i++) { os << "(" << functionToSMTLIBName(kind,false); os << " "; --- ./src/printer/SMTLIB1Printer.cpp.orig 2010-06-24 23:19:52.000000000 -0600 +++ ./src/printer/SMTLIB1Printer.cpp 2012-01-10 16:05:21.226609946 -0700 @@ -214,7 +214,7 @@ void printSMTLIB1VarDeclsToStream(ASTNod { string close = ""; - for (int i =0; i < c.size()-1; i++) + for (size_t i =0; i < c.size()-1; i++) { os << "(" << functionToSMTLIBName(kind,true); os << " "; --- ./src/printer/SMTLIBPrinter.h.orig 2010-05-23 20:03:46.000000000 -0600 +++ ./src/printer/SMTLIBPrinter.h 2012-01-10 16:05:21.227609925 -0700 @@ -24,7 +24,5 @@ namespace printer ostream& SMTLIB_Print(ostream &os, const ASTNode n, const int indentation, void (*SMTLIB_Print1)(ostream&, const ASTNode , int , bool ), bool smtlib1); bool containsAnyArrayOps(const ASTNode& n); - - static string tolower(const char * name); }; #endif --- ./src/sat/SimplifyingMinisat.h.orig 2012-01-09 21:59:09.000000000 -0700 +++ ./src/sat/SimplifyingMinisat.h 2012-01-10 16:05:21.227609925 -0700 @@ -34,7 +34,7 @@ namespace BEEV bool simplify(); // Removes already satisfied clauses. - int setVerbosity(int v); + void setVerbosity(int v); virtual uint8_t modelValue(Var x) const; --- ./src/sat/SATSolver.h.orig 2012-01-09 21:59:09.000000000 -0700 +++ ./src/sat/SATSolver.h 2012-01-10 16:05:21.227609925 -0700 @@ -61,7 +61,7 @@ namespace BEEV exit(1); } - virtual int setVerbosity(int v) =0; + virtual void setVerbosity(int v) =0; virtual lbool true_literal() =0; virtual lbool false_literal() =0; --- ./src/sat/MinisatCore_prop.h.orig 2012-01-09 21:59:09.000000000 -0700 +++ ./src/sat/MinisatCore_prop.h 2012-01-10 16:05:21.227609925 -0700 @@ -43,7 +43,7 @@ namespace BEEV virtual Var newVar(); - int setVerbosity(int v); + void setVerbosity(int v); int nVars(); --- ./src/sat/SimplifyingMinisat.cpp.orig 2012-01-09 21:59:09.000000000 -0700 +++ ./src/sat/SimplifyingMinisat.cpp 2012-01-10 16:05:21.228609904 -0700 @@ -17,7 +17,7 @@ namespace BEEV bool SimplifyingMinisat::addClause(const vec_literals& ps) // Add a clause to the solver. { - s->addClause(ps); + return s->addClause(ps); } bool @@ -47,7 +47,7 @@ namespace BEEV return Minisat::toInt(s->modelValue(x)); } - int SimplifyingMinisat::setVerbosity(int v) + void SimplifyingMinisat::setVerbosity(int v) { s->verbosity = v; } --- ./src/sat/cryptominisat2/Logger.cpp.orig 2010-06-04 12:11:26.000000000 -0600 +++ ./src/sat/cryptominisat2/Logger.cpp 2012-01-10 16:05:21.228609904 -0700 @@ -372,8 +372,9 @@ void Logger::end(const finish_type finis fprintf(proof,"}\n"); history.push_back(uniqueid); - proof = (FILE*)fclose(proof); - assert(proof == NULL); + int err = fclose(proof); + assert(err == 0); + proof = NULL; } if (statistics_on) { --- ./src/sat/cryptominisat2/FailedVarSearcher.cpp.orig 2010-07-02 08:35:28.000000000 -0600 +++ ./src/sat/cryptominisat2/FailedVarSearcher.cpp 2012-01-10 16:05:21.229609884 -0700 @@ -261,7 +261,6 @@ const bool FailedVarSearcher::search(uin }*/ end: - bool removedOldLearnts = false; binClauseAdded = solver.binaryClauses.size() - origBinClauses; //Print results if (solver.verbosity >= 1) printResults(myTime); @@ -272,7 +271,6 @@ end: double time = cpuTime(); if ((int)origHeapSize - (int)solver.order_heap.size() > (int)origHeapSize/15 && solver.nClauses() + solver.learnts.size() > 500000) { completelyDetachAndReattach(); - removedOldLearnts = true; } else { solver.clauseCleaner->removeAndCleanAll(); } --- ./src/sat/CryptoMinisat.cpp.orig 2010-08-20 06:07:42.000000000 -0600 +++ ./src/sat/CryptoMinisat.cpp 2012-01-10 16:05:21.230609864 -0700 @@ -34,7 +34,7 @@ namespace BEEV for (int i =0; iaddClause(v); + return s->addClause(v); } bool @@ -61,7 +61,7 @@ namespace BEEV return s->newVar(); } - int CryptoMinisat::setVerbosity(int v) + void CryptoMinisat::setVerbosity(int v) { s->verbosity = v; } --- ./src/sat/core_prop/Solver_prop.cc.orig 2011-11-27 19:55:18.000000000 -0700 +++ ./src/sat/core_prop/Solver_prop.cc 2012-01-10 16:05:21.230609864 -0700 @@ -171,11 +171,11 @@ Solver_prop::addArray(int array_id, cons if (!ok) return false; - if (i.size() > INDEX_BIT_WIDTH || ki.size() > INDEX_BIT_WIDTH) + if (i.size() > (int)INDEX_BIT_WIDTH || ki.size() > (int)INDEX_BIT_WIDTH) { printf("The array propagators unfortunately don't do arbitrary precision integers yet. " "With the INDICES_128BITS compile time flag STP does 128-bits on 64-bit machines compiled with GCC. " - "Currently STP is compiled to use %d bit indices. " + "Currently STP is compiled to use %zu bit indices. " "Unfortunately your problem has array indexes of size %d bits. " "STP does arbitrary precision indices with the '--oldstyle-refinement' or the '-r' flags.\n", INDEX_BIT_WIDTH, std::max(i.size(), ki.size())); @@ -1167,7 +1167,6 @@ void Solver_prop::analyze(CRef confl, ve if (debug_print) printf("%d %d\n", toInt(p), toInt(var(p))); - Minisat::Clause cl= ca[confl]; assert(ca[confl][0] ==p); assert(value(p) != l_Undef); --- ./src/sat/core_prop/Solver_prop.h.orig 2011-11-27 19:55:18.000000000 -0700 +++ ./src/sat/core_prop/Solver_prop.h 2012-01-10 16:05:21.231609844 -0700 @@ -36,8 +36,10 @@ namespace Minisat { typedef unsigned int uint128_t __attribute__((mode(TI))); static inline uint32_t hash(uint128_t x){ return (uint32_t)x; } typedef uint128_t index_type; +# define PRIuIT PRIu128 #else typedef uint64_t index_type; +# define PRIuIT PRIu64 #endif #define INDEX_BIT_WIDTH (sizeof(index_type) *8) @@ -227,7 +229,7 @@ private: printf("Value Size: %d\n", value.size()); printClause2(value); - printf("Known Index: %ld ", isIndexConstant() ? index_constant : -1); + printf("Known Index: %" PRIuIT " ", isIndexConstant() ? index_constant : (index_type)-1); printf("Known Value: %c\n", isValueConstant() ? 't' : 'f'); printf("Array ID:%d\n", array_id); printf("------------\n"); --- ./src/sat/utils/Options.h.orig 2010-11-27 19:45:43.000000000 -0700 +++ ./src/sat/utils/Options.h 2012-01-10 16:05:21.231609844 -0700 @@ -60,7 +60,7 @@ class Option struct OptionLt { bool operator()(const Option* x, const Option* y) { int test1 = strcmp(x->category, y->category); - return test1 < 0 || test1 == 0 && strcmp(x->type_name, y->type_name) < 0; + return test1 < 0 || (test1 == 0 && strcmp(x->type_name, y->type_name) < 0); } }; --- ./src/sat/MinisatCore.cpp.orig 2012-01-09 21:59:09.000000000 -0700 +++ ./src/sat/MinisatCore.cpp 2012-01-10 16:05:21.231609844 -0700 @@ -22,7 +22,7 @@ namespace BEEV bool MinisatCore::addClause(const SATSolver::vec_literals& ps) // Add a clause to the solver. { - s->addClause(ps); + return s->addClause(ps); } template @@ -58,7 +58,7 @@ namespace BEEV } template - int MinisatCore::setVerbosity(int v) + void MinisatCore::setVerbosity(int v) { s->verbosity = v; } --- ./src/sat/MinisatCore_prop.cpp.orig 2012-01-09 21:59:09.000000000 -0700 +++ ./src/sat/MinisatCore_prop.cpp 2012-01-10 16:05:21.232609824 -0700 @@ -30,7 +30,7 @@ namespace BEEV bool MinisatCore_prop::addClause(const SATSolver::vec_literals& ps) // Add a clause to the solver. { - s->addClause(ps); + return s->addClause(ps); } template @@ -66,7 +66,7 @@ namespace BEEV } template - int MinisatCore_prop::setVerbosity(int v) + void MinisatCore_prop::setVerbosity(int v) { s->verbosity = v; } --- ./src/sat/CryptoMinisat.h.orig 2012-01-09 21:59:09.000000000 -0700 +++ ./src/sat/CryptoMinisat.h 2012-01-10 16:05:21.232609824 -0700 @@ -36,7 +36,7 @@ namespace BEEV virtual Var newVar(); - int setVerbosity(int v); + void setVerbosity(int v); int nVars(); --- ./src/sat/MinisatCore.h.orig 2012-01-09 21:59:09.000000000 -0700 +++ ./src/sat/MinisatCore.h 2012-01-10 16:05:21.232609824 -0700 @@ -40,7 +40,7 @@ namespace BEEV virtual Var newVar(); - int setVerbosity(int v); + void setVerbosity(int v); int nVars(); --- ./src/extlib-abc/kit.h.orig 2011-02-09 18:31:59.000000000 -0700 +++ ./src/extlib-abc/kit.h 2012-01-10 16:05:21.232609824 -0700 @@ -53,11 +53,15 @@ struct Kit_Sop_t_ unsigned * pCubes; // the storage for cubes }; -typedef struct Kit_Edge_t_ Kit_Edge_t; -struct Kit_Edge_t_ +typedef union Kit_Edge_t_ Kit_Edge_t; +union Kit_Edge_t_ { - unsigned fCompl : 1; // the complemented bit - unsigned Node : 30; // the decomposition node pointed by the edge + struct { + unsigned fCompl : 1; // the complemented bit + unsigned Node : 30; // the decomposition node pointed by the edge + } edgeBits; + + unsigned int edgeInt; }; typedef struct Kit_Node_t_ Kit_Node_t; @@ -203,18 +207,18 @@ static inline void Kit_SopShrink static inline void Kit_SopPushCube( Kit_Sop_t * cSop, unsigned uCube ) { cSop->pCubes[cSop->nCubes++] = uCube; } static inline void Kit_SopWriteCube( Kit_Sop_t * cSop, unsigned uCube, int i ) { cSop->pCubes[i] = uCube; } -static inline Kit_Edge_t Kit_EdgeCreate( int Node, int fCompl ) { Kit_Edge_t eEdge = { fCompl, Node }; return eEdge; } -static inline unsigned Kit_EdgeToInt( Kit_Edge_t eEdge ) { return (eEdge.Node << 1) | eEdge.fCompl; } +static inline Kit_Edge_t Kit_EdgeCreate( int Node, int fCompl ) { Kit_Edge_t eEdge = { { fCompl, Node } }; return eEdge; } +static inline unsigned Kit_EdgeToInt( Kit_Edge_t eEdge ) { return (eEdge.edgeBits.Node << 1) | eEdge.edgeBits.fCompl; } static inline Kit_Edge_t Kit_IntToEdge( unsigned Edge ) { return Kit_EdgeCreate( Edge >> 1, Edge & 1 ); } -static inline unsigned Kit_EdgeToInt_( Kit_Edge_t eEdge ) { return *(unsigned *)&eEdge; } -static inline Kit_Edge_t Kit_IntToEdge_( unsigned Edge ) { return *(Kit_Edge_t *)&Edge; } +static inline unsigned Kit_EdgeToInt_( Kit_Edge_t eEdge ) { return eEdge.edgeInt; } +static inline Kit_Edge_t Kit_IntToEdge_( unsigned Edge ) { Kit_Edge_t eEdge; eEdge.edgeInt = Edge; return eEdge; } static inline int Kit_GraphIsConst( Kit_Graph_t * pGraph ) { return pGraph->fConst; } -static inline int Kit_GraphIsConst0( Kit_Graph_t * pGraph ) { return pGraph->fConst && pGraph->eRoot.fCompl; } -static inline int Kit_GraphIsConst1( Kit_Graph_t * pGraph ) { return pGraph->fConst && !pGraph->eRoot.fCompl; } -static inline int Kit_GraphIsComplement( Kit_Graph_t * pGraph ) { return pGraph->eRoot.fCompl; } -static inline int Kit_GraphIsVar( Kit_Graph_t * pGraph ) { return pGraph->eRoot.Node < (unsigned)pGraph->nLeaves; } -static inline void Kit_GraphComplement( Kit_Graph_t * pGraph ) { pGraph->eRoot.fCompl ^= 1; } +static inline int Kit_GraphIsConst0( Kit_Graph_t * pGraph ) { return pGraph->fConst && pGraph->eRoot.edgeBits.fCompl; } +static inline int Kit_GraphIsConst1( Kit_Graph_t * pGraph ) { return pGraph->fConst && !pGraph->eRoot.edgeBits.fCompl; } +static inline int Kit_GraphIsComplement( Kit_Graph_t * pGraph ) { return pGraph->eRoot.edgeBits.fCompl; } +static inline int Kit_GraphIsVar( Kit_Graph_t * pGraph ) { return pGraph->eRoot.edgeBits.Node < (unsigned)pGraph->nLeaves; } +static inline void Kit_GraphComplement( Kit_Graph_t * pGraph ) { pGraph->eRoot.edgeBits.fCompl ^= 1; } static inline void Kit_GraphSetRoot( Kit_Graph_t * pGraph, Kit_Edge_t eRoot ) { pGraph->eRoot = eRoot; } static inline int Kit_GraphLeaveNum( Kit_Graph_t * pGraph ) { return pGraph->nLeaves; } static inline int Kit_GraphNodeNum( Kit_Graph_t * pGraph ) { return pGraph->nSize - pGraph->nLeaves; } @@ -222,14 +226,12 @@ static inline Kit_Node_t * Kit_GraphNode static inline Kit_Node_t * Kit_GraphNodeLast( Kit_Graph_t * pGraph ) { return pGraph->pNodes + pGraph->nSize - 1; } static inline int Kit_GraphNodeInt( Kit_Graph_t * pGraph, Kit_Node_t * pNode ) { return pNode - pGraph->pNodes; } static inline int Kit_GraphNodeIsVar( Kit_Graph_t * pGraph, Kit_Node_t * pNode ) { return Kit_GraphNodeInt(pGraph,pNode) < pGraph->nLeaves; } -static inline Kit_Node_t * Kit_GraphVar( Kit_Graph_t * pGraph ) { assert( Kit_GraphIsVar( pGraph ) ); return Kit_GraphNode( pGraph, pGraph->eRoot.Node ); } +static inline Kit_Node_t * Kit_GraphVar( Kit_Graph_t * pGraph ) { assert( Kit_GraphIsVar( pGraph ) ); return Kit_GraphNode( pGraph, pGraph->eRoot.edgeBits.Node ); } static inline int Kit_GraphVarInt( Kit_Graph_t * pGraph ) { assert( Kit_GraphIsVar( pGraph ) ); return Kit_GraphNodeInt( pGraph, Kit_GraphVar(pGraph) ); } -static inline Kit_Node_t * Kit_GraphNodeFanin0( Kit_Graph_t * pGraph, Kit_Node_t * pNode ){ return Kit_GraphNodeIsVar(pGraph, pNode)? NULL : Kit_GraphNode(pGraph, pNode->eEdge0.Node); } -static inline Kit_Node_t * Kit_GraphNodeFanin1( Kit_Graph_t * pGraph, Kit_Node_t * pNode ){ return Kit_GraphNodeIsVar(pGraph, pNode)? NULL : Kit_GraphNode(pGraph, pNode->eEdge1.Node); } -static inline int Kit_GraphRootLevel( Kit_Graph_t * pGraph ) { return Kit_GraphNode(pGraph, pGraph->eRoot.Node)->Level; } +static inline Kit_Node_t * Kit_GraphNodeFanin0( Kit_Graph_t * pGraph, Kit_Node_t * pNode ){ return Kit_GraphNodeIsVar(pGraph, pNode)? NULL : Kit_GraphNode(pGraph, pNode->eEdge0.edgeBits.Node); } +static inline Kit_Node_t * Kit_GraphNodeFanin1( Kit_Graph_t * pGraph, Kit_Node_t * pNode ){ return Kit_GraphNodeIsVar(pGraph, pNode)? NULL : Kit_GraphNode(pGraph, pNode->eEdge1.edgeBits.Node); } +static inline int Kit_GraphRootLevel( Kit_Graph_t * pGraph ) { return Kit_GraphNode(pGraph, pGraph->eRoot.edgeBits.Node)->Level; } -static inline int Kit_Float2Int( float Val ) { return *((int *)&Val); } -static inline float Kit_Int2Float( int Num ) { return *((float *)&Num); } static inline int Kit_BitWordNum( int nBits ) { return nBits/(8*sizeof(unsigned)) + ((nBits%(8*sizeof(unsigned))) > 0); } static inline int Kit_TruthWordNum( int nVars ) { return nVars <= 5 ? 1 : (1 << (nVars - 5)); } static inline unsigned Kit_BitMask( int nBits ) { assert( nBits <= 32 ); return ~((~(unsigned)0) << nBits); } @@ -486,6 +488,18 @@ static inline void Kit_TruthIthVar( unsi /// FUNCTION DECLARATIONS /// //////////////////////////////////////////////////////////////////////// +extern Kit_Graph_t * Kit_GraphCreateConst0( void ); +extern Kit_Graph_t * Kit_GraphCreateConst1( void ); +extern void Kit_GraphFree( Kit_Graph_t * ); +extern Kit_Graph_t * Kit_SopFactor( Vec_Int_t *, int, int, Vec_Int_t * ); +extern void Kit_TruthCofactor0( unsigned *, int, int ); +extern void Kit_TruthCofactor1( unsigned *, int, int ); +extern int Kit_TruthIsop( unsigned *, int, Vec_Int_t *, int ); +extern void Kit_TruthShrink( unsigned *, unsigned *, int, int, unsigned, int ); +extern void Kit_TruthStretch( unsigned *, unsigned *, int, int, unsigned, int ); +extern Kit_Graph_t * Kit_TruthToGraph( unsigned *, int, Vec_Int_t * ); +extern int Kit_TruthVarInSupport( unsigned *, int, int ); + #if 0 /*=== kitBdd.c ==========================================================*/ --- ./src/extlib-abc/aig/kit/kitSop.c.orig 2010-03-06 06:48:41.000000000 -0700 +++ ./src/extlib-abc/aig/kit/kitSop.c 2012-01-10 16:05:21.233609804 -0700 @@ -174,7 +174,7 @@ void Kit_SopDivideByCube( Kit_Sop_t * cS ***********************************************************************/ void Kit_SopDivideInternal( Kit_Sop_t * cSop, Kit_Sop_t * cDiv, Kit_Sop_t * vQuo, Kit_Sop_t * vRem, Vec_Int_t * vMemory ) { - unsigned uCube, uDiv, uCube2, uDiv2, uQuo; + unsigned uCube, uDiv, uCube2 = 0, uDiv2, uQuo; int i, i2, k, k2, nCubesRem; assert( Kit_SopCubeNum(cSop) >= Kit_SopCubeNum(cDiv) ); // consider special case --- ./src/extlib-abc/aig/kit/kitAig.c.orig 2010-03-06 06:48:41.000000000 -0700 +++ ./src/extlib-abc/aig/kit/kitAig.c 2012-01-10 16:05:21.233609804 -0700 @@ -54,8 +54,8 @@ Aig_Obj_t * Kit_GraphToAigInternal( Aig_ // build the AIG nodes corresponding to the AND gates of the graph Kit_GraphForEachNode( pGraph, pNode, i ) { - pAnd0 = Aig_NotCond( Kit_GraphNode(pGraph, pNode->eEdge0.Node)->pFunc, pNode->eEdge0.fCompl ); - pAnd1 = Aig_NotCond( Kit_GraphNode(pGraph, pNode->eEdge1.Node)->pFunc, pNode->eEdge1.fCompl ); + pAnd0 = Aig_NotCond( Kit_GraphNode(pGraph, pNode->eEdge0.edgeBits.Node)->pFunc, pNode->eEdge0.edgeBits.fCompl ); + pAnd1 = Aig_NotCond( Kit_GraphNode(pGraph, pNode->eEdge1.edgeBits.Node)->pFunc, pNode->eEdge1.edgeBits.fCompl ); pNode->pFunc = Aig_And( pMan, pAnd0, pAnd1 ); } // complement the result if necessary --- ./src/extlib-abc/aig/kit/kitGraph.c.orig 2010-03-06 06:48:41.000000000 -0700 +++ ./src/extlib-abc/aig/kit/kitGraph.c 2012-01-10 16:05:21.234609784 -0700 @@ -69,7 +69,7 @@ Kit_Graph_t * Kit_GraphCreateConst0() pGraph = ALLOC( Kit_Graph_t, 1 ); memset( pGraph, 0, sizeof(Kit_Graph_t) ); pGraph->fConst = 1; - pGraph->eRoot.fCompl = 1; + pGraph->eRoot.edgeBits.fCompl = 1; return pGraph; } @@ -109,8 +109,8 @@ Kit_Graph_t * Kit_GraphCreateLeaf( int i Kit_Graph_t * pGraph; assert( 0 <= iLeaf && iLeaf < nLeaves ); pGraph = Kit_GraphCreate( nLeaves ); - pGraph->eRoot.Node = iLeaf; - pGraph->eRoot.fCompl = fCompl; + pGraph->eRoot.edgeBits.Node = iLeaf; + pGraph->eRoot.edgeBits.fCompl = fCompl; return pGraph; } @@ -174,8 +174,8 @@ Kit_Edge_t Kit_GraphAddNodeAnd( Kit_Grap // set the inputs and other info pNode->eEdge0 = eEdge0; pNode->eEdge1 = eEdge1; - pNode->fCompl0 = eEdge0.fCompl; - pNode->fCompl1 = eEdge1.fCompl; + pNode->fCompl0 = eEdge0.edgeBits.fCompl; + pNode->fCompl1 = eEdge1.edgeBits.fCompl; return Kit_EdgeCreate( pGraph->nSize - 1, 0 ); } @@ -198,12 +198,12 @@ Kit_Edge_t Kit_GraphAddNodeOr( Kit_Graph // set the inputs and other info pNode->eEdge0 = eEdge0; pNode->eEdge1 = eEdge1; - pNode->fCompl0 = eEdge0.fCompl; - pNode->fCompl1 = eEdge1.fCompl; + pNode->fCompl0 = eEdge0.edgeBits.fCompl; + pNode->fCompl1 = eEdge1.edgeBits.fCompl; // make adjustments for the OR gate pNode->fNodeOr = 1; - pNode->eEdge0.fCompl = !pNode->eEdge0.fCompl; - pNode->eEdge1.fCompl = !pNode->eEdge1.fCompl; + pNode->eEdge0.edgeBits.fCompl = !pNode->eEdge0.edgeBits.fCompl; + pNode->eEdge1.edgeBits.fCompl = !pNode->eEdge1.edgeBits.fCompl; return Kit_EdgeCreate( pGraph->nSize - 1, 1 ); } @@ -224,11 +224,11 @@ Kit_Edge_t Kit_GraphAddNodeXor( Kit_Grap if ( Type == 0 ) { // derive the first AND - eEdge0.fCompl ^= 1; + eEdge0.edgeBits.fCompl ^= 1; eNode0 = Kit_GraphAddNodeAnd( pGraph, eEdge0, eEdge1 ); - eEdge0.fCompl ^= 1; + eEdge0.edgeBits.fCompl ^= 1; // derive the second AND - eEdge1.fCompl ^= 1; + eEdge1.edgeBits.fCompl ^= 1; eNode1 = Kit_GraphAddNodeAnd( pGraph, eEdge0, eEdge1 ); // derive the final OR eNode = Kit_GraphAddNodeOr( pGraph, eNode0, eNode1 ); @@ -238,12 +238,12 @@ Kit_Edge_t Kit_GraphAddNodeXor( Kit_Grap // derive the first AND eNode0 = Kit_GraphAddNodeAnd( pGraph, eEdge0, eEdge1 ); // derive the second AND - eEdge0.fCompl ^= 1; - eEdge1.fCompl ^= 1; + eEdge0.edgeBits.fCompl ^= 1; + eEdge1.edgeBits.fCompl ^= 1; eNode1 = Kit_GraphAddNodeAnd( pGraph, eEdge0, eEdge1 ); // derive the final OR eNode = Kit_GraphAddNodeOr( pGraph, eNode0, eNode1 ); - eNode.fCompl ^= 1; + eNode.edgeBits.fCompl ^= 1; } return eNode; } @@ -267,7 +267,7 @@ Kit_Edge_t Kit_GraphAddNodeMux( Kit_Grap // derive the first AND eNode0 = Kit_GraphAddNodeAnd( pGraph, eEdgeC, eEdgeT ); // derive the second AND - eEdgeC.fCompl ^= 1; + eEdgeC.edgeBits.fCompl ^= 1; eNode1 = Kit_GraphAddNodeAnd( pGraph, eEdgeC, eEdgeE ); // derive the final OR eNode = Kit_GraphAddNodeOr( pGraph, eNode0, eNode1 ); @@ -275,16 +275,16 @@ Kit_Edge_t Kit_GraphAddNodeMux( Kit_Grap else { // complement the arguments - eEdgeT.fCompl ^= 1; - eEdgeE.fCompl ^= 1; + eEdgeT.edgeBits.fCompl ^= 1; + eEdgeE.edgeBits.fCompl ^= 1; // derive the first AND eNode0 = Kit_GraphAddNodeAnd( pGraph, eEdgeC, eEdgeT ); // derive the second AND - eEdgeC.fCompl ^= 1; + eEdgeC.edgeBits.fCompl ^= 1; eNode1 = Kit_GraphAddNodeAnd( pGraph, eEdgeC, eEdgeE ); // derive the final OR eNode = Kit_GraphAddNodeOr( pGraph, eNode0, eNode1 ); - eNode.fCompl ^= 1; + eNode.edgeBits.fCompl ^= 1; } return eNode; } @@ -326,10 +326,10 @@ unsigned Kit_GraphToTruth( Kit_Graph_t * // compute the function for each internal node Kit_GraphForEachNode( pGraph, pNode, i ) { - uTruth0 = (unsigned)(long)Kit_GraphNode(pGraph, pNode->eEdge0.Node)->pFunc; - uTruth1 = (unsigned)(long)Kit_GraphNode(pGraph, pNode->eEdge1.Node)->pFunc; - uTruth0 = pNode->eEdge0.fCompl? ~uTruth0 : uTruth0; - uTruth1 = pNode->eEdge1.fCompl? ~uTruth1 : uTruth1; + uTruth0 = (unsigned)(long)Kit_GraphNode(pGraph, pNode->eEdge0.edgeBits.Node)->pFunc; + uTruth1 = (unsigned)(long)Kit_GraphNode(pGraph, pNode->eEdge1.edgeBits.Node)->pFunc; + uTruth0 = pNode->eEdge0.edgeBits.fCompl? ~uTruth0 : uTruth0; + uTruth1 = pNode->eEdge1.edgeBits.fCompl? ~uTruth1 : uTruth1; uTruth = uTruth0 & uTruth1; pNode->pFunc = (void *)(long)uTruth; } --- ./src/extlib-abc/aig/aig/aigTable.c.orig 2010-03-06 06:48:41.000000000 -0700 +++ ./src/extlib-abc/aig/aig/aigTable.c 2012-01-10 16:05:21.234609784 -0700 @@ -74,8 +74,8 @@ void Aig_TableResize( Aig_Man_t * p ) { Aig_Obj_t * pEntry, * pNext; Aig_Obj_t ** pTableOld, ** ppPlace; - int nTableSizeOld, Counter, i, clk; -clk = clock(); + int nTableSizeOld, Counter, i; + // save the old table pTableOld = p->pTable; nTableSizeOld = p->nTableSize; --- ./src/extlib-abc/aig/aig/aigShow.c.orig 2010-03-06 06:48:41.000000000 -0700 +++ ./src/extlib-abc/aig/aig/aigShow.c 2012-01-10 16:05:21.234609784 -0700 @@ -329,7 +329,7 @@ void Aig_WriteDotAig( Aig_Man_t * pMan, void Aig_ManShow( Aig_Man_t * pMan, int fHaig, Vec_Ptr_t * vBold ) { extern void Abc_ShowFile( char * FileNameDot ); - static Counter = 0; + static int Counter = 0; char FileNameDot[200]; FILE * pFile; // create the file name --- ./src/extlib-abc/aig/aig/aigObj.c.orig 2010-03-06 06:48:41.000000000 -0700 +++ ./src/extlib-abc/aig/aig/aigObj.c 2012-01-10 16:05:21.234609784 -0700 @@ -299,8 +299,10 @@ void Aig_NodeFixBufferFanins( Aig_Man_t pResult = Aig_Oper( p, pFanReal0, pFanReal1, Aig_ObjType(pObj) ); // else if ( Aig_ObjIsLatch(pObj) ) // pResult = Aig_Latch( p, pFanReal0, Aig_ObjInit(pObj) ); - else + else { assert( 0 ); + pResult = NULL; + } // replace the node with buffer by the node without buffer Aig_ObjReplace( p, pObj, pResult, fNodesOnly, fUpdateLevel ); } --- ./src/extlib-abc/aig/cnf/cnfWrite.c.orig 2011-01-07 21:23:57.000000000 -0700 +++ ./src/extlib-abc/aig/cnf/cnfWrite.c 2012-01-10 16:05:21.235609764 -0700 @@ -352,7 +352,6 @@ Cnf_Dat_t * Cnf_DeriveSimple_Additional( int Number = old->nVars+1; // assign variables to the PIs - int newPI = 0; Aig_ManForEachPi( p, pObj, i ) if (pCnf->pVarNums[pObj->Id] == -1) // new! pCnf->pVarNums[pObj->Id] = Number++; --- ./src/extlib-abc/aig/dar/darPrec.c.orig 2010-03-06 06:48:41.000000000 -0700 +++ ./src/extlib-abc/aig/dar/darPrec.c 2012-01-10 16:05:21.235609764 -0700 @@ -258,11 +258,9 @@ unsigned Dar_TruthPolarize( unsigned uTr 0xFF00FF00, // 1111 1111 0000 0000 1111 1111 0000 0000 0xFFFF0000 // 1111 1111 1111 1111 0000 0000 0000 0000 }; - unsigned uTruthRes, uCof0, uCof1; - int nMints, Shift, v; + unsigned uCof0, uCof1; + int Shift, v; assert( nVars < 6 ); - nMints = (1 << nVars); - uTruthRes = uTruth; for ( v = 0; v < nVars; v++ ) if ( Polarity & (1 << v) ) { --- ./src/extlib-abc/aig/dar/darRefact.c.orig 2010-03-06 06:48:41.000000000 -0700 +++ ./src/extlib-abc/aig/dar/darRefact.c 2012-01-10 16:05:21.236609744 -0700 @@ -213,7 +213,7 @@ int Dar_RefactTryGraph( Aig_Man_t * pAig { Kit_Node_t * pNode, * pNode0, * pNode1; Aig_Obj_t * pAnd, * pAnd0, * pAnd1; - int i, Counter, LevelNew, LevelOld; + int i, Counter, LevelNew; // check for constant function or a literal if ( Kit_GraphIsConst(pGraph) || Kit_GraphIsVar(pGraph) ) return 0; @@ -230,16 +230,16 @@ int Dar_RefactTryGraph( Aig_Man_t * pAig Kit_GraphForEachNode( pGraph, pNode, i ) { // get the children of this node - pNode0 = Kit_GraphNode( pGraph, pNode->eEdge0.Node ); - pNode1 = Kit_GraphNode( pGraph, pNode->eEdge1.Node ); + pNode0 = Kit_GraphNode( pGraph, pNode->eEdge0.edgeBits.Node ); + pNode1 = Kit_GraphNode( pGraph, pNode->eEdge1.edgeBits.Node ); // get the AIG nodes corresponding to the children pAnd0 = pNode0->pFunc; pAnd1 = pNode1->pFunc; if ( pAnd0 && pAnd1 ) { // if they are both present, find the resulting node - pAnd0 = Aig_NotCond( pAnd0, pNode->eEdge0.fCompl ); - pAnd1 = Aig_NotCond( pAnd1, pNode->eEdge1.fCompl ); + pAnd0 = Aig_NotCond( pAnd0, pNode->eEdge0.edgeBits.fCompl ); + pAnd1 = Aig_NotCond( pAnd1, pNode->eEdge1.edgeBits.fCompl ); pAnd = Aig_TableLookupTwo( pAig, pAnd0, pAnd1 ); // return -1 if the node is the same as the original root if ( Aig_Regular(pAnd) == pRoot ) @@ -263,7 +263,7 @@ int Dar_RefactTryGraph( Aig_Man_t * pAig LevelNew = (int)Aig_Regular(pAnd0)->Level; else if ( Aig_Regular(pAnd) == Aig_Regular(pAnd1) ) LevelNew = (int)Aig_Regular(pAnd1)->Level; - LevelOld = (int)Aig_Regular(pAnd)->Level; +// LevelOld = (int)Aig_Regular(pAnd)->Level; // assert( LevelNew == LevelOld ); } if ( LevelNew > LevelMax ) @@ -312,8 +312,8 @@ Aig_Obj_t * Dar_RefactBuildGraph( Aig_Ma //printf( "Building (current number %d):\n", Aig_ManObjNumMax(pAig) ); Kit_GraphForEachNode( pGraph, pNode, i ) { - pAnd0 = Aig_NotCond( Kit_GraphNode(pGraph, pNode->eEdge0.Node)->pFunc, pNode->eEdge0.fCompl ); - pAnd1 = Aig_NotCond( Kit_GraphNode(pGraph, pNode->eEdge1.Node)->pFunc, pNode->eEdge1.fCompl ); + pAnd0 = Aig_NotCond( Kit_GraphNode(pGraph, pNode->eEdge0.edgeBits.Node)->pFunc, pNode->eEdge0.edgeBits.fCompl ); + pAnd1 = Aig_NotCond( Kit_GraphNode(pGraph, pNode->eEdge1.edgeBits.Node)->pFunc, pNode->eEdge1.edgeBits.fCompl ); pNode->pFunc = Aig_And( pAig, pAnd0, pAnd1 ); /* printf( "Checking " ); --- ./src/AST/ASTmisc.cpp.orig 2012-01-09 22:53:22.000000000 -0700 +++ ./src/AST/ASTmisc.cpp 2012-01-10 16:05:21.236609744 -0700 @@ -150,7 +150,7 @@ namespace BEEV visited.insert(n.GetNodeNum()); - for (int i = 0; i < n.Degree(); i++) + for (size_t i = 0; i < n.Degree(); i++) numberOfReadsLessThan(n[i], visited, soFar,limit); } --- ./src/AST/ArrayTransformer.cpp.orig 2011-12-28 19:00:01.000000000 -0700 +++ ./src/AST/ArrayTransformer.cpp 2012-01-10 16:05:21.236609744 -0700 @@ -61,7 +61,6 @@ namespace BEEV iset_end = arrayToIndexToRead.end(); iset != iset_end; iset++) { - const ASTNode& ArrName = iset->first; map& mapper = iset->second; for (map::iterator it =mapper.begin() ; it != mapper.end();it++) --- ./src/AST/NodeFactory/SimplifyingNodeFactory.cpp.orig 2012-01-09 20:39:36.000000000 -0700 +++ ./src/AST/NodeFactory/SimplifyingNodeFactory.cpp 2012-01-10 16:05:21.237609723 -0700 @@ -384,7 +384,7 @@ SimplifyingNodeFactory::CreateSimpleEQ(c const ASTNode& in2 = swap ? children[0] : children[1]; const Kind k1 = in1.GetKind(); const Kind k2 = in2.GetKind(); - const int width = in1.GetValueWidth(); + const unsigned int width = in1.GetValueWidth(); if (in1 == in2) //terms are syntactically the same @@ -401,7 +401,7 @@ SimplifyingNodeFactory::CreateSimpleEQ(c if ((k1 == BVUMINUS && k2 == BEEV::BVCONST) || (k1 == BVNEG && k2 == BEEV::BVCONST)) return NodeFactory::CreateNode(EQ, in1[0], NodeFactory::CreateTerm(k1, width, in2)); - if (k2 == BVUMINUS && k1 == BEEV::BVCONST || (k2 == BVNEG && k1 == BEEV::BVCONST)) + if ((k2 == BVUMINUS && k1 == BEEV::BVCONST) || (k2 == BVNEG && k1 == BEEV::BVCONST)) return NodeFactory::CreateNode(EQ, in2[0], NodeFactory::CreateTerm(k2, width, in1)); if ((k1 == BVNEG && in1[0] == in2) || (k2 == BVNEG && in2[0] == in1)) @@ -460,8 +460,8 @@ SimplifyingNodeFactory::CreateSimpleEQ(c { int match1 = -1, match2 = -1; - for (int i = 0; i < c1.size(); i++) - for (int j = 0; j < c2.size(); j++) + for (int i = 0; (size_t)i < c1.size(); i++) + for (int j = 0; (size_t)j < c2.size(); j++) { if (c1[i] == c2[j]) { @@ -519,7 +519,7 @@ SimplifyingNodeFactory::CreateSimpleEQ(c bool foundZero = false, foundOne = false; const unsigned original_width = in2[0].GetValueWidth(); const unsigned new_width = in2.GetValueWidth(); - for (int i = original_width - 1; i < new_width; i++) + for (unsigned int i = original_width - 1; i < new_width; i++) if (CONSTANTBV::BitVector_bit_test(in1.GetBVConst(), i)) foundOne = true; else @@ -1103,7 +1103,7 @@ SimplifyingNodeFactory::CreateTerm(Kind bool oneFound = false; bool zeroFound = false; - for (int i = 0; i < children.size(); i++) + for (size_t i = 0; i < children.size(); i++) { if (children[i].GetKind() == BEEV::BVCONST) { @@ -1122,7 +1122,7 @@ SimplifyingNodeFactory::CreateTerm(Kind else if (oneFound) { ASTVec new_children; - for (int i = 0; i < children.size(); i++) + for (size_t i = 0; i < children.size(); i++) { if (children[i].GetKind() != BEEV::BVCONST || !CONSTANTBV::BitVector_is_full(children[i].GetBVConst())) new_children.push_back(children[i]); @@ -1162,13 +1162,14 @@ SimplifyingNodeFactory::CreateTerm(Kind int end = -1; BEEV::CBV c = c0.GetBVConst(); bool bad = false; - for (int i = 0; i < width; i++) + for (unsigned int i = 0; i < width; i++) { - if (CONSTANTBV::BitVector_bit_test(c, i)) + if (CONSTANTBV::BitVector_bit_test(c, i)) { if (start == -1) start = i; // first one bit. else if (end != -1) bad = true; + } if (!CONSTANTBV::BitVector_bit_test(c, i)) if (start != -1 && end == -1) @@ -1189,7 +1190,7 @@ SimplifyingNodeFactory::CreateTerm(Kind ASTNode z = bm.CreateZeroConst(start); result = NodeFactory::CreateTerm(BVCONCAT, end + 1, result, z); } - if (end < width - 1) + if (end < (int)width - 1) { ASTNode z = bm.CreateZeroConst(width - end - 1); result = NodeFactory::CreateTerm(BVCONCAT, width, z, result); @@ -1252,7 +1253,6 @@ SimplifyingNodeFactory::CreateTerm(Kind const unsigned outerHigh = children[1].GetUnsignedConst(); const unsigned innerLow = children[0][2].GetUnsignedConst(); - const unsigned innerHigh = children[0][1].GetUnsignedConst(); result = NodeFactory::CreateTerm(BVEXTRACT, width, children[0][0], bm.CreateBVConst(32, outerHigh + innerLow), bm.CreateBVConst(32, outerLow + innerLow)); } --- ./src/STPManager/STP.cpp.orig 2012-01-09 22:38:16.000000000 -0700 +++ ./src/STPManager/STP.cpp 2012-01-10 16:05:21.237609723 -0700 @@ -59,8 +59,8 @@ namespace BEEV { newS = new MinisatCore(); else if (bm->UserFlags.solver_to_use == UserDefinedFlags::MINISAT_PROPAGATORS) newS = new MinisatCore_prop(); - - + else + newS = NULL; SATSolver& NewSolver = *newS; --- ./src/parser/ParserInterface.h.orig 2011-07-09 00:56:51.000000000 -0600 +++ ./src/parser/ParserInterface.h 2012-01-10 16:05:21.238609702 -0700 @@ -214,7 +214,7 @@ public: assert(symbols.size() == cache.size()); cache.erase(cache.end()-1); ASTVec & current = symbols.back(); - for (int i=0; i < current.size() ;i++) + for (size_t i=0; i < current.size() ;i++) letMgr._parser_symbol_table.erase(current[i]); symbols.erase(symbols.end()-1); } @@ -234,7 +234,7 @@ public: void printStatus() { - for (int i=0; i < cache.size();i++) + for (size_t i=0; i < cache.size();i++) { cache[i].print(); } @@ -271,7 +271,7 @@ public: // Loop through the set of assertions converting them to single nodes.. ASTVec v; - for (int i = 0; i < assertionsSMT2.size(); i++) + for (size_t i = 0; i < assertionsSMT2.size(); i++) { if (assertionsSMT2[i].size() == 1) {} @@ -310,7 +310,7 @@ public: // It's satisfiable, so everything beneath it is satisfiable too. if (last_result ==SOLVER_SATISFIABLE) { - for (int i=0; i < cache.size(); i++) + for (size_t i=0; i < cache.size(); i++) { assert(cache[i].result != SOLVER_UNSATISFIABLE); cache[i].result = SOLVER_SATISFIABLE;