--- ./src/c_interface/c_interface.cpp.orig 2012-04-18 06:38:48.000000000 -0600 +++ ./src/c_interface/c_interface.cpp 2012-08-07 16:26:11.734851974 -0600 @@ -557,7 +557,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; @@ -570,7 +569,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; @@ -590,7 +588,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(); @@ -982,7 +979,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: "\ @@ -1546,16 +1543,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; @@ -1730,7 +1722,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/to-sat/BitBlaster.cpp.orig 2012-04-06 18:20:57.000000000 -0600 +++ ./src/to-sat/BitBlaster.cpp 2012-08-07 16:26:11.736851970 -0600 @@ -64,7 +64,7 @@ namespace BEEV size_t operator()(const vector& n) const { int hash =0; - for (int i=0; i < std::min(n.size(),(size_t)6); i++) + for (size_t i=0; i < std::min(n.size(),(size_t)6); i++) hash += n[i].GetNodeNum(); return hash; } @@ -79,7 +79,7 @@ namespace BEEV if (n0.size() != n1.size()) return false; - for (int i=0; i < n0.size(); i++) + for (size_t i=0; i < n0.size(); i++) { if (!(n0[i] == n1[i])) return false; @@ -428,7 +428,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; @@ -451,7 +451,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); @@ -787,14 +787,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+1); - 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]); } @@ -1283,7 +1283,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; @@ -1295,7 +1295,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); @@ -1305,7 +1305,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; @@ -1319,7 +1319,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; } } @@ -1361,7 +1361,7 @@ namespace BEEV BitBlaster::buildAdditionNetworkResult(vector >& 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; @@ -1370,7 +1370,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))); @@ -1380,7 +1380,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; } @@ -1482,7 +1482,7 @@ namespace BEEV BitBlaster::multWithBounds(const ASTNode&n, vector >& products, BBNodeSet& toConjoinToTop) { - const int bitWidth = n.GetValueWidth(); + const unsigned int bitWidth = n.GetValueWidth(); int ignored=0; assert(upper_multiplication_bound); @@ -1491,7 +1491,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) { @@ -1513,7 +1513,7 @@ namespace BEEV } vector prior; - for (int i = 0; i < bitWidth; i++) + for (unsigned int i = 0; i < bitWidth; i++) { if (debug_bounds) { @@ -1533,7 +1533,7 @@ namespace BEEV if (debug_bitblaster) cerr << endl << endl; - assert(result.size() == ((unsigned)bitWidth)); + assert(result.size() == bitWidth); return result; } @@ -1557,7 +1557,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])); } @@ -1610,7 +1610,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]); } } @@ -1668,13 +1668,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 = i; - return ms; + return ms; + } } return NULL; @@ -1686,7 +1686,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; @@ -1698,7 +1698,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]; @@ -1715,7 +1715,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++) { @@ -1740,7 +1740,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]); } @@ -1820,7 +1820,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); @@ -1837,6 +1837,7 @@ namespace BEEV assert(v[i]== BBFalse); } + } } } } @@ -1850,7 +1851,7 @@ namespace BEEV BitBlaster::setColumnsToZero(vector >& 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 highestZero = -1; @@ -1861,7 +1862,7 @@ namespace BEEV if (ms == NULL) return; - for (int i = 0; i < bitWidth; i++) + for (unsigned int i = 0; i < bitWidth; i++) { if (ms->sumH[i] == 0) { @@ -2000,18 +2001,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()); @@ -2043,7 +2044,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]); } @@ -2081,11 +2082,11 @@ namespace BEEV BBNodeVec BitBlaster::v6(vector >& 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); @@ -2101,7 +2102,7 @@ namespace BEEV BBNodeVec BitBlaster::v13(vector >& products, set& support, const ASTNode&n) { - const int bitWidth = n.GetValueWidth(); + const unsigned int bitWidth = n.GetValueWidth(); int ignore = -1; simplifier::constantBitP::MultiplicationStats* ms = getMS(n, ignore); @@ -2117,7 +2118,7 @@ namespace BEEV { done = true; - for (int i = 0; i < bitWidth; i++) + for (unsigned int i = 0; i < bitWidth; i++) { if (products[i].size() > 2) done = false; @@ -2155,12 +2156,12 @@ namespace BEEV } BBPlus2(a, b, BBFalse); - for (int i = 0; i < bitWidth; i++) + for (unsigned int i = 0; i < bitWidth; i++) products[i].push_back(a[i]); } BBNodeVec results; - for (int i = 0; i < bitWidth; i++) + for (unsigned int i = 0; i < bitWidth; i++) { assert(products[i].size() ==1); results.push_back(products[i].back()); @@ -2178,22 +2179,22 @@ namespace BEEV BBNodeVec BitBlaster::v9(vector >& 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(); + const size_t 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()) @@ -2208,8 +2209,8 @@ namespace BEEV continue; // shortcut. } - int position =k; - int increment =1; + size_t position =k; + unsigned int increment =1; while (position != 0) { if (column+increment >= bitWidth) @@ -2223,12 +2224,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]); } @@ -2238,7 +2239,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); } @@ -2252,7 +2253,7 @@ namespace BEEV BBNodeVec BitBlaster::v7(vector >& 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; @@ -2264,13 +2265,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; @@ -2280,7 +2281,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; @@ -2291,7 +2292,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) @@ -2302,7 +2303,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); @@ -2312,7 +2313,7 @@ namespace BEEV products[i].pop_back(); } - assert(results.size() == ((unsigned)bitWidth)); + assert(results.size() == bitWidth); return results; } @@ -2321,7 +2322,7 @@ namespace BEEV BBNodeVec BitBlaster::v8(vector >& 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; @@ -2334,14 +2335,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; @@ -2351,7 +2352,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; @@ -2362,7 +2363,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) @@ -2373,14 +2374,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; } @@ -2392,7 +2393,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]; @@ -2429,7 +2430,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]); @@ -2439,7 +2440,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]); @@ -2450,7 +2451,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]); @@ -2495,7 +2496,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 2012-01-29 20:28:39.000000000 -0700 +++ ./src/to-sat/AIG/BBNodeManagerAIG.h 2012-08-07 16:26:11.736851970 -0600 @@ -148,7 +148,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/BBNodeAIG.h.orig 2012-02-02 20:41:30.000000000 -0700 +++ ./src/to-sat/AIG/BBNodeAIG.h 2012-08-07 16:26:11.737851968 -0600 @@ -11,6 +11,7 @@ #define BBNODEAIG_H_ #include "../../extlib-abc/aig.h" +#include #include namespace BEEV --- ./src/to-sat/AIG/ToSATAIG.cpp.orig 2012-04-03 00:43:00.000000000 -0600 +++ ./src/to-sat/AIG/ToSATAIG.cpp 2012-08-07 16:26:11.737851968 -0600 @@ -136,7 +136,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]); } @@ -144,7 +144,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]); } } @@ -195,7 +195,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. @@ -204,7 +204,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)); @@ -220,7 +220,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)); @@ -229,7 +229,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 @@ -243,7 +243,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. @@ -252,7 +252,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/to-sat/ASTNode/ToSAT.cpp.orig 2011-12-28 19:00:01.000000000 -0700 +++ ./src/to-sat/ASTNode/ToSAT.cpp 2012-08-07 16:26:11.738851967 -0600 @@ -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 (/* int count=0, flag=0 */; 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-08-07 16:26:11.739851966 -0600 @@ -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/absrefine_counterexample/AbstractionRefinement.cpp.orig 2012-04-25 07:40:33.000000000 -0600 +++ ./src/absrefine_counterexample/AbstractionRefinement.cpp 2012-08-07 16:26:11.740851965 -0600 @@ -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]; @@ -556,13 +555,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/absrefine_counterexample/CounterExample.cpp.orig 2012-06-15 08:40:15.000000000 -0600 +++ ./src/absrefine_counterexample/CounterExample.cpp 2012-08-07 16:26:11.740851965 -0600 @@ -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/sat/CryptoMinisat.cpp.orig 2012-08-07 16:26:07.496857705 -0600 +++ ./src/sat/CryptoMinisat.cpp 2012-08-07 16:26:11.741851964 -0600 @@ -44,7 +44,7 @@ namespace BEEV for (int i =0; iaddClause(v); + return s->addClause(v); } bool @@ -71,7 +71,7 @@ namespace BEEV return s->newVar(); } - int CryptoMinisat::setVerbosity(int v) + void CryptoMinisat::setVerbosity(int v) { s->conf.verbosity = v; } --- ./src/sat/MinisatCore_prop.h.orig 2012-03-11 22:07:37.000000000 -0600 +++ ./src/sat/MinisatCore_prop.h 2012-08-07 16:26:11.741851964 -0600 @@ -40,7 +40,7 @@ namespace BEEV virtual Var newVar(); - int setVerbosity(int v); + void setVerbosity(int v); int nVars(); --- ./src/sat/SimplifyingMinisat.cpp.orig 2012-01-23 21:26:37.000000000 -0700 +++ ./src/sat/SimplifyingMinisat.cpp 2012-08-07 16:26:11.741851964 -0600 @@ -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/utils/Options.h.orig 2010-11-27 19:45:43.000000000 -0700 +++ ./src/sat/utils/Options.h 2012-08-07 16:26:11.742851962 -0600 @@ -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-03-11 18:12:51.000000000 -0600 +++ ./src/sat/MinisatCore.cpp 2012-08-07 16:27:00.075801722 -0600 @@ -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; } @@ -97,7 +97,7 @@ namespace BEEV template bool MinisatCore::simplify() { - s->simplify(); + return s->simplify(); } --- ./src/sat/MinisatCore.h.orig 2012-04-19 19:01:00.000000000 -0600 +++ ./src/sat/MinisatCore.h 2012-08-07 16:26:11.743851961 -0600 @@ -47,7 +47,7 @@ namespace BEEV virtual Var newVar(); - int setVerbosity(int v); + void setVerbosity(int v); int nVars(); --- ./src/sat/SimplifyingMinisat.h.orig 2012-01-23 21:26:37.000000000 -0700 +++ ./src/sat/SimplifyingMinisat.h 2012-08-07 16:26:11.743851961 -0600 @@ -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-03-11 18:12:51.000000000 -0600 +++ ./src/sat/SATSolver.h 2012-08-07 16:26:11.743851961 -0600 @@ -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/core_prop/Solver_prop.cc.orig 2012-05-25 07:36:17.000000000 -0600 +++ ./src/sat/core_prop/Solver_prop.cc 2012-08-07 16:26:11.744851960 -0600 @@ -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())); @@ -1136,7 +1136,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 2012-01-23 21:26:37.000000000 -0700 +++ ./src/sat/core_prop/Solver_prop.h 2012-08-07 16:26:11.745851958 -0600 @@ -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/cryptominisat2/FailedVarSearcher.cpp.orig 2010-07-02 08:35:28.000000000 -0600 +++ ./src/sat/cryptominisat2/FailedVarSearcher.cpp 2012-08-07 16:26:11.746851956 -0600 @@ -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/cryptominisat2/Logger.cpp.orig 2010-06-04 12:11:26.000000000 -0600 +++ ./src/sat/cryptominisat2/Logger.cpp 2012-08-07 16:26:11.747851955 -0600 @@ -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/MinisatCore_prop.cpp.orig 2012-01-23 21:26:37.000000000 -0700 +++ ./src/sat/MinisatCore_prop.cpp 2012-08-07 16:26:11.747851955 -0600 @@ -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-08-07 16:26:07.497857703 -0600 +++ ./src/sat/CryptoMinisat.h 2012-08-07 16:26:11.747851955 -0600 @@ -33,7 +33,7 @@ namespace BEEV virtual Var newVar(); - int setVerbosity(int v); + void setVerbosity(int v); int nVars(); --- ./src/printer/SMTLIBPrinter.h.orig 2010-05-23 20:03:46.000000000 -0600 +++ ./src/printer/SMTLIBPrinter.h 2012-08-07 16:26:11.748851954 -0600 @@ -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/printer/SMTLIB2Printer.cpp.orig 2012-04-04 19:13:21.000000000 -0600 +++ ./src/printer/SMTLIB2Printer.cpp 2012-08-07 16:26:11.748851954 -0600 @@ -213,7 +213,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-08-07 16:26:11.749851953 -0600 @@ -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/cpp_interface/cpp_interface.h.orig 2012-06-15 08:28:01.000000000 -0600 +++ ./src/cpp_interface/cpp_interface.h 2012-08-07 16:26:11.750851951 -0600 @@ -197,7 +197,7 @@ namespace BEEV { bool removed=false; - for (int i=0; i < symbols.back().size(); i++) + for (size_t i=0; i < symbols.back().size(); i++) if (symbols.back()[i] == s) { symbols.back().erase(symbols.back().begin() + i); @@ -218,7 +218,7 @@ namespace BEEV f.name = name; ASTNodeMap fromTo; - for (int i=0; i < params.size();i++) + for (size_t i=0; i < params.size();i++) { ASTNode p = bm.CreateFreshVariable(params[i].GetIndexWidth(), params[i].GetValueWidth(), "STP_INTERNAL_FUNCTION_NAME"); fromTo.insert(make_pair(params[i], p)); @@ -239,7 +239,7 @@ namespace BEEV f = functions[string(name)]; ASTNodeMap fromTo; - for (int i=0; i < f.params.size();i++) + for (size_t i=0; i < f.params.size();i++) { if (f.params[i].GetValueWidth() != params[i].GetValueWidth()) FatalError("Actual parameters differ from formal"); @@ -371,7 +371,7 @@ namespace BEEV 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); checkInvariant(); @@ -402,7 +402,7 @@ namespace BEEV void printStatus() { - for (int i = 0; i < cache.size(); i++) + for (size_t i = 0; i < cache.size(); i++) { cache[i].print(); } --- ./src/extlib-abc/aig/aig/aigShow.c.orig 2010-03-06 06:48:41.000000000 -0700 +++ ./src/extlib-abc/aig/aig/aigShow.c 2012-08-07 16:38:04.988829249 -0600 @@ -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-08-07 16:26:11.750851951 -0600 @@ -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/aig/aigTable.c.orig 2010-03-06 06:48:41.000000000 -0700 +++ ./src/extlib-abc/aig/aig/aigTable.c 2012-08-07 16:26:11.750851951 -0600 @@ -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/cnf/cnfWrite.c.orig 2011-01-07 21:23:57.000000000 -0700 +++ ./src/extlib-abc/aig/cnf/cnfWrite.c 2012-08-07 16:26:11.751851950 -0600 @@ -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/kit/kitSop.c.orig 2010-03-06 06:48:41.000000000 -0700 +++ ./src/extlib-abc/aig/kit/kitSop.c 2012-08-07 16:26:11.751851950 -0600 @@ -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-08-07 16:26:11.751851950 -0600 @@ -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-08-07 16:38:39.828797982 -0600 @@ -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/dar/darRefact.c.orig 2010-03-06 06:48:41.000000000 -0700 +++ ./src/extlib-abc/aig/dar/darRefact.c 2012-08-07 16:26:11.752851949 -0600 @@ -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/extlib-abc/aig/dar/darPrec.c.orig 2010-03-06 06:48:41.000000000 -0700 +++ ./src/extlib-abc/aig/dar/darPrec.c 2012-08-07 16:26:11.752851949 -0600 @@ -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/kit.h.orig 2011-02-09 18:31:59.000000000 -0700 +++ ./src/extlib-abc/kit.h 2012-08-07 16:26:11.753851948 -0600 @@ -53,11 +53,14 @@ 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 +206,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 +225,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 +487,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/STPManager/STP.cpp.orig 2012-06-15 08:40:15.000000000 -0600 +++ ./src/STPManager/STP.cpp 2012-08-07 16:26:11.753851948 -0600 @@ -65,8 +65,8 @@ namespace BEEV { newS = new MinisatCore(bm->soft_timeout_expired); else if (bm->UserFlags.solver_to_use == UserDefinedFlags::MINISAT_PROPAGATORS) newS = new MinisatCore_prop(bm->soft_timeout_expired); - - + else + newS = NULL; SATSolver& NewSolver = *newS; @@ -566,7 +566,7 @@ namespace BEEV { ToSATAIG toSATAIG(bm, cb, arrayTransformer); - ToSATBase* satBase = bm->UserFlags.isSet("traditional-cnf", "0") ? tosat : ((ToSAT*) &toSATAIG) ; + ToSATBase* satBase = bm->UserFlags.isSet("traditional-cnf", "0") ? tosat : &toSATAIG; if (bm->soft_timeout_expired) return SOLVER_TIMEOUT; --- ./src/simplifier/constantBitP/ConstantBitP_Division.cpp.orig 2012-04-15 00:52:35.000000000 -0600 +++ ./src/simplifier/constantBitP/ConstantBitP_Division.cpp 2012-08-07 16:26:11.754851947 -0600 @@ -157,14 +157,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/ConstantBitPropagation.cpp.orig 2012-04-03 06:32:10.000000000 -0600 +++ ./src/simplifier/constantBitP/ConstantBitPropagation.cpp 2012-08-07 16:26:11.754851947 -0600 @@ -430,7 +430,7 @@ namespace simplifier void ConstantBitPropagation::scheduleDown(const ASTNode& n) { - for (int i = 0; i < n.Degree(); i++) + for (size_t i = 0; i < n.Degree(); i++) workList->push(n[i]); } @@ -465,7 +465,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/FixedBits.cpp.orig 2012-02-17 06:48:39.000000000 -0700 +++ ./src/simplifier/constantBitP/FixedBits.cpp 2012-08-07 16:34:38.053114918 -0600 @@ -382,7 +382,7 @@ namespace simplifier void FixedBits::fromUnsigned(unsigned val) { - for (unsigned i = 0; i < width; i++) + for (unsigned i = 0; i < (unsigned) width; i++) { if (i < (unsigned) width && i < sizeof(unsigned) * 8) { --- ./src/simplifier/constantBitP/ConstantBitP_Comparison.cpp.orig 2012-04-22 05:52:33.000000000 -0600 +++ ./src/simplifier/constantBitP/ConstantBitP_Comparison.cpp 2012-08-07 16:37:05.172884335 -0600 @@ -128,6 +128,7 @@ fast_exit(FixedBits& c0, FixedBits& c1) } return false; } + return false; } --- ./src/simplifier/SubstitutionMap.h.orig 2012-08-07 16:26:07.499857701 -0600 +++ ./src/simplifier/SubstitutionMap.h 2012-08-07 16:26:11.755851945 -0600 @@ -40,7 +40,7 @@ namespace BEEV bool loops(const ASTNode& n0, const ASTNode& n1); - int substitutionsLastApplied; + size_t substitutionsLastApplied; public: bool --- ./src/simplifier/VariablesInExpression.cpp.orig 2011-02-01 05:41:57.000000000 -0700 +++ ./src/simplifier/VariablesInExpression.cpp 2012-08-07 16:26:11.755851945 -0600 @@ -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/UseITEContext.h.orig 2012-08-07 16:26:07.500857699 -0600 +++ ./src/simplifier/UseITEContext.h 2012-08-07 16:26:11.756851943 -0600 @@ -28,7 +28,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) @@ -86,7 +86,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/FindPureLiterals.h.orig 2012-08-07 16:26:07.500857699 -0600 +++ ./src/simplifier/FindPureLiterals.h 2012-08-07 16:26:11.756851943 -0600 @@ -110,7 +110,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; @@ -121,7 +121,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/simplifier.cpp.orig 2012-04-29 04:49:41.000000000 -0600 +++ ./src/simplifier/simplifier.cpp 2012-08-07 16:26:11.757851942 -0600 @@ -248,7 +248,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); } @@ -523,6 +523,7 @@ namespace BEEV return getConstantBit(n[0], i); assert(false); + return -1; } ASTNode @@ -1302,7 +1303,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)); } @@ -1664,9 +1665,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()) @@ -1694,7 +1695,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()); @@ -1725,7 +1726,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()); @@ -1906,7 +1907,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])) { @@ -2247,7 +2248,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)); @@ -2647,7 +2647,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. @@ -2669,13 +2669,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; @@ -2692,7 +2692,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/RemoveUnconstrained.cpp.orig 2012-03-19 21:59:03.000000000 -0600 +++ ./src/simplifier/RemoveUnconstrained.cpp 2012-08-07 16:28:13.624742813 -0600 @@ -55,7 +55,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; @@ -100,7 +100,7 @@ namespace BEEV // Going to be rebuilt later anyway, so discard. vector variables; - for (int i =0; i n; assert(var.GetKind() == SYMBOL); @@ -151,7 +151,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); @@ -184,7 +184,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. @@ -208,7 +208,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(); @@ -217,7 +217,7 @@ namespace BEEV unsigned indexWidth = muteNode.getParent().n.GetIndexWidth(); ASTNode other; - MutableASTNode* muteOther; + MutableASTNode* muteOther = NULL; if(numberOfChildren == 2) { @@ -242,7 +242,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++; @@ -429,7 +429,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 @@ -464,7 +464,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)); @@ -617,7 +617,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)); @@ -639,7 +639,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/simplifier/AlwaysTrue.h.orig 2012-08-07 16:26:07.501857698 -0600 +++ ./src/simplifier/AlwaysTrue.h 2012-08-07 16:26:11.759851939 -0600 @@ -85,7 +85,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/PropagateEqualities.cpp.orig 2012-01-28 19:12:31.000000000 -0700 +++ ./src/simplifier/PropagateEqualities.cpp 2012-08-07 16:30:09.932731593 -0600 @@ -31,10 +31,10 @@ namespace BEEV bool result = false; if (k == XOR) - for (int i = 0; i < lhs.Degree(); i++) + for (unsigned int i = 0; i < lhs.Degree(); i++) { ASTVec others; - for (int j = 0; j < lhs.Degree(); j++) + for (unsigned int j = 0; j < lhs.Degree(); j++) if (j != i) others.push_back(lhs[j]); @@ -77,10 +77,10 @@ namespace BEEV return searchTerm(lhs[0], nf->CreateTerm(BVNEG, width, rhs)); if (lhs.GetKind() == BVXOR || lhs.GetKind() == BVPLUS) - for (int i = 0; i < lhs.Degree(); i++) + for (unsigned int i = 0; i < lhs.Degree(); i++) { ASTVec others; - for (int j = 0; j < lhs.Degree(); j++) + for (unsigned int j = 0; j < lhs.Degree(); j++) if (j != i) others.push_back(lhs[j]); --- ./src/simplifier/consteval.cpp.orig 2011-12-28 19:00:01.000000000 -0700 +++ ./src/simplifier/consteval.cpp 2012-08-07 16:26:11.759851939 -0600 @@ -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/MutableASTNode.h.orig 2011-03-29 07:18:23.000000000 -0600 +++ ./src/simplifier/MutableASTNode.h 2012-08-07 16:26:11.760851937 -0600 @@ -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); @@ -510,7 +510,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) @@ -518,13 +518,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); @@ -599,7 +599,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) { @@ -612,10 +612,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; @@ -688,7 +688,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) { @@ -717,7 +717,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); @@ -734,7 +734,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); @@ -755,7 +755,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; @@ -764,7 +764,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(); } } @@ -797,10 +797,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/AST/NodeFactory/SimplifyingNodeFactory.cpp.orig 2012-05-26 00:24:52.000000000 -0600 +++ ./src/AST/NodeFactory/SimplifyingNodeFactory.cpp 2012-08-07 16:26:11.762851935 -0600 @@ -386,7 +386,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 @@ -462,8 +462,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]) { @@ -521,7 +521,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 @@ -1107,7 +1107,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) { @@ -1126,7 +1126,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]); @@ -1166,13 +1166,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) @@ -1193,7 +1194,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); @@ -1256,7 +1257,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/AST/ArrayTransformer.cpp.orig 2012-05-11 20:18:08.000000000 -0600 +++ ./src/AST/ArrayTransformer.cpp 2012-08-07 16:26:11.762851935 -0600 @@ -60,7 +60,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/ASTmisc.cpp.orig 2012-04-03 00:43:00.000000000 -0600 +++ ./src/AST/ASTmisc.cpp 2012-08-07 16:26:11.763851934 -0600 @@ -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); }