rpms/stp
3
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity
0dad78eb89
stp/stp-warning.patch
Jerry James c9c580d386 Update to recent subversion snapshot.
2013-02-11 17:00:41 -07:00

2279 lines
92 KiB
Diff
Raw Blame History

--- ./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<BEEV::ASTNode *>::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<BBNode>& 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<BBNode, BBNodeManagerT>::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<BBNodeVec> 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<list<BBNode> > 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<BBNode, BBNodeManagerT>::buildAdditionNetworkResult(vector<list<BBNode> >& products, set<BBNode>& 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<BBNode, BBNodeManagerT>::multWithBounds(const ASTNode&n, vector<list<BBNode> >& 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<BBNode> 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<BBNode, BBNodeManagerT>::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<BBNode, BBNodeManagerT>::setColumnsToZero(vector<list<BBNode> >& products, set<BBNode>& 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<BBNode> 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 <BBNode> 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<BBNode> 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<BBNode, BBNodeManagerT>::v6(vector<list<BBNode> >& products, set<BBNode>& support, const ASTNode&n)
{
- const int bitWidth = n.GetValueWidth();
+ const unsigned int bitWidth = n.GetValueWidth();
vector<BBNode> prior;
- for (int i = 0; i < bitWidth; i++)
+ for (unsigned int i = 0; i < bitWidth; i++)
{
vector<BBNode> output;
sortingNetworkAdd(support, products[i], output ,prior);
@@ -2101,7 +2102,7 @@ namespace BEEV
BBNodeVec
BitBlaster<BBNode, BBNodeManagerT>::v13(vector<list<BBNode> >& products, set<BBNode>& 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<BBNode, BBNodeManagerT>::v9(vector<list<BBNode> >& products, set<BBNode>& 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<BBNode> sorted; // The current column (sorted) gets put into here.
vector<BBNode> 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<BBNode, BBNodeManagerT>::v7(vector<list<BBNode> >& products, set<BBNode>& 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<list<BBNode> > later(bitWidth+1);
std::vector<list<BBNode> > 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<BBNode, BBNodeManagerT>::v8(vector<list<BBNode> >& products, set<BBNode>& 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<list<BBNode> > later(bitWidth+1); // +1 then ignore the topmost.
std::vector<list<BBNode> > 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<BBNode> 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 <BBNode> evenL;
vector <BBNode> 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 <BBNode> evenR; // Take the even of each.
vector <BBNode> 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 <BBNode> even = evenL.size()< evenR.size() ? mergeSorted(evenR,evenL) : mergeSorted(evenL,evenR);
vector <BBNode> 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
@@ -149,7 +149,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 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<unsigned>& 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<unsigned>& 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<unsigned> 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<unsigned>& 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 ASTNode*>::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<unsigned> 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<AxiomToBe> & 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<pair<ASTNode, ArrayTransformer::arrTypeMap> >::const_iterator iset = arrayToIndex.begin(),
iset_end = arrayToIndex.end(); iset != iset_end; iset++)
{
- const ASTNode& ArrName = iset->first;
const map<ASTNode, ArrayTransformer::ArrayRead>& mapper = iset->second;
vector<ASTNode> 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<bool> 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<unsigned> 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; i<ps.size();i++)
v.push(CMSat::Lit(var(ps[i]), sign(ps[i])));
- s->addClause(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<T>::addClause(const SATSolver::vec_literals& ps) // Add a clause to the solver.
{
- s->addClause(ps);
+ return s->addClause(ps);
}
template <class T>
@@ -58,7 +58,7 @@ namespace BEEV
}
template <class T>
- int MinisatCore<T>::setVerbosity(int v)
+ void MinisatCore<T>::setVerbosity(int v)
{
s->verbosity = v;
}
@@ -97,7 +97,7 @@ namespace BEEV
template <class T>
bool MinisatCore<T>::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<T>::addClause(const SATSolver::vec_literals& ps) // Add a clause to the solver.
{
- s->addClause(ps);
+ return s->addClause(ps);
}
template <class T>
@@ -66,7 +66,7 @@ namespace BEEV
}
template <class T>
- int MinisatCore_prop<T>::setVerbosity(int v)
+ void MinisatCore_prop<T>::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<Minisat::Solver>(bm->soft_timeout_expired);
else if (bm->UserFlags.solver_to_use == UserDefinedFlags::MINISAT_PROPAGATORS)
newS = new MinisatCore_prop<Minisat::Solver_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<Symbols*> 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<Symbols*> 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 <MutableASTNode*> 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<MutableASTNode*> variables;
- for (int i =0; i <extracts.size(); i++)
+ for (size_t i =0; i <extracts.size(); i++)
{
ASTNode& var = extracts[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 <mutable_children.size(); j++ )
+ for (size_t j = 0; j <mutable_children.size(); j++ )
children.push_back(mutable_children[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<MutableASTNode *> 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 <node.GetValueWidth();j++)
+ for (unsigned int j=0; j <node.GetValueWidth();j++)
found[j] = false;
ParentsType::const_iterator it;
@@ -330,7 +330,7 @@ private:
static void
cleanup()
{
- for (int i = 0; i < all.size(); i++)
+ for (size_t i = 0; i < all.size(); i++)
delete all[i];
all.clear();
}
--- ./src/simplifier/SubstitutionMap.cpp.orig 2012-03-19 21:59:03.000000000 -0600
+++ ./src/simplifier/SubstitutionMap.cpp 2012-08-07 16:26:11.760851937 -0600
@@ -212,7 +212,7 @@ namespace BEEV
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/EstablishIntervals.h.orig 2012-08-07 16:26:07.504857695 -0600
+++ ./src/simplifier/EstablishIntervals.h 2012-08-07 16:26:11.761851936 -0600
@@ -118,7 +118,7 @@ namespace BEEV
ASTVec new_children;
new_children.reserve(result.GetChildren().size());
- for (int i =0; i < result.Degree();i++)
+ for (size_t i =0; i < result.Degree();i++)
new_children.push_back(replace(result[i],fromTo,cache));
if (new_children == result.GetChildren())
@@ -497,7 +497,7 @@ namespace BEEV
result = freshUnsignedInterval(n.GetValueWidth());
// Copy in the minimum and maximum.
- for (int i=0; i < n[0].GetValueWidth();i++)
+ for (unsigned int i=0; i < n[0].GetValueWidth();i++)
{
if (CONSTANTBV::BitVector_bit_test(children[0]->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<ASTNode, ArrayTransformer::ArrayRead>& mapper = iset->second;
for (map<ASTNode, ArrayTransformer::ArrayRead>::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);
}
Reference in New Issue View Git Blame Copy Permalink