1978 lines
81 KiB
Diff
1978 lines
81 KiB
Diff
|
--- ./src/simplifier/UseITEContext.h.orig 2011-04-07 07:38:52.000000000 -0600
|
||
|
+++ ./src/simplifier/UseITEContext.h 2011-12-13 13:08:15.892474675 -0700
|
||
|
@@ -27,7 +27,7 @@ namespace BEEV
|
||
|
if (n.GetKind() == NOT && n[0].GetKind() == OR)
|
||
|
{
|
||
|
ASTVec flat = FlattenKind(OR, n[0].GetChildren());
|
||
|
- for (int i = 0; i < flat.size(); i++)
|
||
|
+ for (size_t i = 0; i < flat.size(); i++)
|
||
|
context.insert(nf->CreateNode(NOT, flat[i]));
|
||
|
}
|
||
|
else if (n.GetKind() == AND)
|
||
|
@@ -85,7 +85,7 @@ namespace BEEV
|
||
|
}
|
||
|
else
|
||
|
{
|
||
|
- for (int i = 0; i < n.GetChildren().size(); i++)
|
||
|
+ for (size_t i = 0; i < n.GetChildren().size(); i++)
|
||
|
new_children.push_back(visit(n[i], visited, visited_empty, context));
|
||
|
}
|
||
|
|
||
|
--- ./src/simplifier/AlwaysTrue.h.orig 2011-05-01 06:48:53.000000000 -0600
|
||
|
+++ ./src/simplifier/AlwaysTrue.h 2011-12-13 13:08:15.892474675 -0700
|
||
|
@@ -88,7 +88,7 @@ public:
|
||
|
else
|
||
|
new_state = state;
|
||
|
|
||
|
- for (int i=0; i < n.Degree(); i++)
|
||
|
+ for (size_t i=0; i < n.Degree(); i++)
|
||
|
{
|
||
|
newChildren.push_back(visit(n[i],new_state,fromTo));
|
||
|
}
|
||
|
--- ./src/simplifier/MutableASTNode.h.orig 2011-03-29 07:18:23.000000000 -0600
|
||
|
+++ ./src/simplifier/MutableASTNode.h 2011-12-13 13:08:15.893474673 -0700
|
||
|
@@ -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/EstablishIntervals.h.orig 2011-08-08 23:15:54.000000000 -0600
|
||
|
+++ ./src/simplifier/EstablishIntervals.h 2011-12-13 13:09:21.387399946 -0700
|
||
|
@@ -117,7 +117,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())
|
||
|
@@ -496,7 +496,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);
|
||
|
@@ -509,7 +509,7 @@ namespace BEEV
|
||
|
CONSTANTBV::BitVector_Bit_Off(result->minV,i);
|
||
|
}
|
||
|
|
||
|
- for (int i=n[0].GetValueWidth(); i < n.GetValueWidth();i++)
|
||
|
+ for (unsigned int i=n[0].GetValueWidth(); i < n.GetValueWidth();i++)
|
||
|
CONSTANTBV::BitVector_Bit_Off(result->maxV,i);
|
||
|
}
|
||
|
} else if (knownC1)
|
||
|
@@ -517,13 +517,13 @@ namespace BEEV
|
||
|
// Ignores what's already there for now..
|
||
|
|
||
|
IntervalType * circ_result = freshUnsignedInterval(n.GetValueWidth());
|
||
|
- for (int i=0; i < n[0].GetValueWidth()-1;i++)
|
||
|
+ for (unsigned int i=0; i < n[0].GetValueWidth()-1;i++)
|
||
|
{
|
||
|
CONSTANTBV::BitVector_Bit_On(circ_result->maxV,i);
|
||
|
CONSTANTBV::BitVector_Bit_Off(circ_result->minV,i);
|
||
|
}
|
||
|
|
||
|
- for (int i=n[0].GetValueWidth()-1; i < n.GetValueWidth();i++)
|
||
|
+ for (unsigned int i=n[0].GetValueWidth()-1; i < n.GetValueWidth();i++)
|
||
|
{
|
||
|
CONSTANTBV::BitVector_Bit_Off(circ_result->maxV,i);
|
||
|
CONSTANTBV::BitVector_Bit_On(circ_result->minV,i);
|
||
|
@@ -598,7 +598,7 @@ namespace BEEV
|
||
|
CONSTANTBV::BitVector_increment(result->maxV);
|
||
|
|
||
|
bool bad= false;
|
||
|
- for (int i =0; i < children.size(); i++)
|
||
|
+ for (size_t i =0; i < children.size(); i++)
|
||
|
{
|
||
|
if (children[i] == NULL)
|
||
|
{
|
||
|
@@ -611,10 +611,10 @@ namespace BEEV
|
||
|
e = CONSTANTBV::BitVector_Multiply(max, result->maxV, children[i]->maxV);
|
||
|
assert (0 == e);
|
||
|
|
||
|
- if (CONSTANTBV::Set_Max(max) >= width)
|
||
|
+ if (CONSTANTBV::Set_Max(max) >= (long)width)
|
||
|
bad = true;
|
||
|
|
||
|
- for (int j = width; j < 2 * width; j++)
|
||
|
+ for (unsigned int j = width; j < 2 * width; j++)
|
||
|
{
|
||
|
if (CONSTANTBV::BitVector_bit_test(min, j))
|
||
|
bad = true;
|
||
|
@@ -687,7 +687,7 @@ namespace BEEV
|
||
|
|
||
|
bool carry = false;
|
||
|
|
||
|
- for (int i =0; i < children.size(); i++)
|
||
|
+ for (size_t i =0; i < children.size(); i++)
|
||
|
{
|
||
|
if (children[i] == NULL)
|
||
|
{
|
||
|
@@ -716,7 +716,7 @@ namespace BEEV
|
||
|
if (knownC1)
|
||
|
{
|
||
|
// Copy in the minimum and maximum.
|
||
|
- for (int i=0; i < n[1].GetValueWidth();i++)
|
||
|
+ for (unsigned int i=0; i < n[1].GetValueWidth();i++)
|
||
|
{
|
||
|
if (CONSTANTBV::BitVector_bit_test(children[1]->maxV,i))
|
||
|
CONSTANTBV::BitVector_Bit_On(result->maxV,i);
|
||
|
@@ -733,7 +733,7 @@ namespace BEEV
|
||
|
if (knownC0)
|
||
|
{
|
||
|
// Copy in the minimum and maximum.
|
||
|
- for (int i=n[1].GetValueWidth(); i < n.GetValueWidth();i++)
|
||
|
+ for (unsigned int i=n[1].GetValueWidth(); i < n.GetValueWidth();i++)
|
||
|
{
|
||
|
if (CONSTANTBV::BitVector_bit_test(children[0]->maxV,i- n[1].GetValueWidth()))
|
||
|
CONSTANTBV::BitVector_Bit_On(result->maxV,i);
|
||
|
@@ -754,7 +754,7 @@ namespace BEEV
|
||
|
|
||
|
bool nonNull = true;
|
||
|
// If all the children are known, output 'em.
|
||
|
- for (int i=0; i < n.Degree();i++)
|
||
|
+ for (size_t i=0; i < n.Degree();i++)
|
||
|
{
|
||
|
if (children[i]== NULL)
|
||
|
nonNull=false;
|
||
|
@@ -763,7 +763,7 @@ namespace BEEV
|
||
|
if (false && nonNull && n.GetKind() != SYMBOL && n.GetKind() != AND)
|
||
|
{
|
||
|
cerr << n;
|
||
|
- for (int i=0; i < n.Degree();i++)
|
||
|
+ for (size_t i=0; i < n.Degree();i++)
|
||
|
children[i]->print();
|
||
|
}
|
||
|
}
|
||
|
@@ -796,10 +796,10 @@ namespace BEEV
|
||
|
|
||
|
~EstablishIntervals()
|
||
|
{
|
||
|
- for (int i =0; i < toDeleteLater.size();i++)
|
||
|
+ for (size_t i =0; i < toDeleteLater.size();i++)
|
||
|
delete toDeleteLater[i];
|
||
|
|
||
|
- for (int i =0; i < likeAutoPtr.size();i++)
|
||
|
+ for (size_t i =0; i < likeAutoPtr.size();i++)
|
||
|
CONSTANTBV::BitVector_Destroy(likeAutoPtr[i]);
|
||
|
|
||
|
likeAutoPtr.clear();
|
||
|
--- ./src/simplifier/constantBitP/ConstantBitP_Shifting.cpp.orig 2010-11-27 20:45:32.000000000 -0700
|
||
|
+++ ./src/simplifier/constantBitP/ConstantBitP_Shifting.cpp 2011-12-13 13:08:15.894474671 -0700
|
||
|
@@ -204,8 +204,6 @@ Result bvArithmeticRightShiftBothWays(ve
|
||
|
assert(children[0]->getWidth() == children[1]->getWidth());
|
||
|
const unsigned MSBIndex = bitWidth-1;
|
||
|
|
||
|
- Result result = NO_CHANGE;
|
||
|
-
|
||
|
FixedBits& op = *children[0];
|
||
|
FixedBits& shift = *children[1];
|
||
|
|
||
|
@@ -393,7 +391,6 @@ Result bvArithmeticRightShiftBothWays(ve
|
||
|
{
|
||
|
shift.setFixed(i, true);
|
||
|
shift.setValue(i, setOfPossibleShifts.getValue(i));
|
||
|
- result = CHANGED;
|
||
|
}
|
||
|
else if (shift.isFixed(i) && shift.getValue(i)
|
||
|
!= setOfPossibleShifts.getValue(i))
|
||
|
@@ -550,7 +547,6 @@ Result bvArithmeticRightShiftBothWays(ve
|
||
|
{
|
||
|
output.setFixed(column, true);
|
||
|
output.setValue(column, allFixedTo);
|
||
|
- result = CHANGED;
|
||
|
}
|
||
|
}
|
||
|
}
|
||
|
@@ -563,8 +559,6 @@ Result bvLeftShiftBothWays(vector<FixedB
|
||
|
assert(2== children.size());
|
||
|
assert(bitWidth > 0);
|
||
|
|
||
|
- Result result = NO_CHANGE;
|
||
|
-
|
||
|
FixedBits& op = *children[0];
|
||
|
FixedBits& shift = *children[1];
|
||
|
|
||
|
@@ -761,7 +755,6 @@ Result bvLeftShiftBothWays(vector<FixedB
|
||
|
{
|
||
|
shift.setFixed(i, true);
|
||
|
shift.setValue(i, v.getValue(i));
|
||
|
- result = CHANGED;
|
||
|
}
|
||
|
else if (shift.isFixed(i) && shift.getValue(i) != v.getValue(i))
|
||
|
return CONFLICT;
|
||
|
@@ -899,7 +892,6 @@ Result bvLeftShiftBothWays(vector<FixedB
|
||
|
{
|
||
|
output.setFixed(column, true);
|
||
|
output.setValue(column, allFixedTo);
|
||
|
- result = CHANGED;
|
||
|
}
|
||
|
}
|
||
|
}
|
||
|
@@ -914,7 +906,6 @@ Result bvLeftShiftBothWays(vector<FixedB
|
||
|
{
|
||
|
op.setFixed(i - shiftIndex, true);
|
||
|
op.setValue(i - shiftIndex, output.getValue(i));
|
||
|
- result = CHANGED;
|
||
|
}
|
||
|
}
|
||
|
}
|
||
|
--- ./src/simplifier/constantBitP/ConstantBitPropagation.cpp.orig 2011-09-11 06:53:41.000000000 -0600
|
||
|
+++ ./src/simplifier/constantBitP/ConstantBitPropagation.cpp 2011-12-13 13:08:15.896474668 -0700
|
||
|
@@ -427,7 +427,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]);
|
||
|
}
|
||
|
|
||
|
@@ -462,7 +462,7 @@ namespace simplifier
|
||
|
|
||
|
assert(FixedBits::equals(newBits, current));
|
||
|
|
||
|
- for (int i = 0; i < n.Degree(); i++)
|
||
|
+ for (size_t i = 0; i < n.Degree(); i++)
|
||
|
{
|
||
|
if (!FixedBits::equals(*getUpdatedFixedBits(n[i]),
|
||
|
childrenFixedBits[i]))
|
||
|
--- ./src/simplifier/constantBitP/ConstantBitP_Comparison.cpp.orig 2010-11-27 20:45:32.000000000 -0700
|
||
|
+++ ./src/simplifier/constantBitP/ConstantBitP_Comparison.cpp 2011-12-13 13:08:15.897474668 -0700
|
||
|
@@ -110,8 +110,6 @@ void destroy(CBV a, CBV b, CBV c, CBV d)
|
||
|
|
||
|
Result bvSignedLessThanBothWays(FixedBits& c0, FixedBits& c1, FixedBits& output)
|
||
|
{
|
||
|
- Result r = NO_CHANGE;
|
||
|
-
|
||
|
assert(c0.getWidth() == c1.getWidth());
|
||
|
|
||
|
CBV c0_min = CONSTANTBV::BitVector_Create(c0.getWidth(), true);
|
||
|
@@ -135,7 +133,6 @@ Result bvSignedLessThanBothWays(FixedBit
|
||
|
{
|
||
|
output.setFixed(0, true);
|
||
|
output.setValue(0, true);
|
||
|
- r = CHANGED;
|
||
|
}
|
||
|
}
|
||
|
|
||
|
@@ -153,7 +150,6 @@ Result bvSignedLessThanBothWays(FixedBit
|
||
|
{
|
||
|
output.setFixed(0, true);
|
||
|
output.setValue(0, false);
|
||
|
- r = CHANGED;
|
||
|
}
|
||
|
}
|
||
|
|
||
|
@@ -183,7 +179,6 @@ Result bvSignedLessThanBothWays(FixedBit
|
||
|
c0.setFixed(msb, true);
|
||
|
c0.setValue(msb, true);
|
||
|
setSignedMinMax(c0, c0_min, c0_max);
|
||
|
- r = CHANGED;
|
||
|
}
|
||
|
else
|
||
|
{
|
||
|
@@ -199,7 +194,6 @@ Result bvSignedLessThanBothWays(FixedBit
|
||
|
c1.setFixed(msb, true);
|
||
|
c1.setValue(msb, false);
|
||
|
setSignedMinMax(c1, c1_min, c1_max);
|
||
|
- r = CHANGED;
|
||
|
}
|
||
|
else
|
||
|
{
|
||
|
@@ -222,7 +216,6 @@ Result bvSignedLessThanBothWays(FixedBit
|
||
|
c0.setFixed(i, true);
|
||
|
c0.setValue(i, false);
|
||
|
setSignedMinMax(c0, c0_min, c0_max);
|
||
|
- r = CHANGED;
|
||
|
}
|
||
|
else
|
||
|
{
|
||
|
@@ -242,7 +235,6 @@ Result bvSignedLessThanBothWays(FixedBit
|
||
|
c1.setFixed(i, true);
|
||
|
c1.setValue(i, true);
|
||
|
setSignedMinMax(c1, c1_min, c1_max);
|
||
|
- r = CHANGED;
|
||
|
}
|
||
|
else
|
||
|
{
|
||
|
@@ -259,8 +251,6 @@ Result bvSignedLessThanBothWays(FixedBit
|
||
|
|
||
|
Result bvSignedLessThanEqualsBothWays(FixedBits& c0, FixedBits &c1, FixedBits& output)
|
||
|
{
|
||
|
- Result r = NO_CHANGE;
|
||
|
-
|
||
|
assert(c0.getWidth() == c1.getWidth());
|
||
|
|
||
|
CBV c0_min = CONSTANTBV::BitVector_Create(c0.getWidth(), true);
|
||
|
@@ -283,7 +273,6 @@ Result bvSignedLessThanEqualsBothWays(Fi
|
||
|
{
|
||
|
output.setFixed(0, true);
|
||
|
output.setValue(0, true);
|
||
|
- r = CHANGED;
|
||
|
}
|
||
|
}
|
||
|
|
||
|
@@ -299,7 +288,6 @@ Result bvSignedLessThanEqualsBothWays(Fi
|
||
|
{
|
||
|
output.setFixed(0, true);
|
||
|
output.setValue(0, false);
|
||
|
- r = CHANGED;
|
||
|
}
|
||
|
}
|
||
|
|
||
|
@@ -329,7 +317,6 @@ Result bvSignedLessThanEqualsBothWays(Fi
|
||
|
c0.setFixed(msb, true);
|
||
|
c0.setValue(msb, true);
|
||
|
setSignedMinMax(c0, c0_min, c0_max);
|
||
|
- r = CHANGED;
|
||
|
}
|
||
|
else
|
||
|
{
|
||
|
@@ -345,7 +332,6 @@ Result bvSignedLessThanEqualsBothWays(Fi
|
||
|
c1.setFixed(msb, true);
|
||
|
c1.setValue(msb, false);
|
||
|
setSignedMinMax(c1, c1_min, c1_max);
|
||
|
- r = CHANGED;
|
||
|
}
|
||
|
else
|
||
|
{
|
||
|
@@ -412,8 +398,6 @@ Result bvSignedLessThanEqualsBothWays(Fi
|
||
|
// UNSIGNED!!
|
||
|
Result bvLessThanBothWays(FixedBits& c0, FixedBits &c1, FixedBits& output)
|
||
|
{
|
||
|
- Result r = NO_CHANGE;
|
||
|
-
|
||
|
assert(c0.getWidth() == c1.getWidth());
|
||
|
|
||
|
CBV c0_min = CONSTANTBV::BitVector_Create(c0.getWidth(), true);
|
||
|
@@ -467,8 +451,6 @@ Result bvLessThanBothWays(FixedBits& c0,
|
||
|
return bvGreaterThanEqualsBothWays(c0, c1, t);
|
||
|
}
|
||
|
|
||
|
- bool changed = false;
|
||
|
-
|
||
|
if (output.isFixed(0) && output.getValue(0))
|
||
|
{
|
||
|
// Starting from the high order. Turn on each bit in turn. If it being turned on pushes it past the max of the other side
|
||
|
@@ -484,7 +466,6 @@ Result bvLessThanBothWays(FixedBits& c0,
|
||
|
c0.setFixed(i, true);
|
||
|
c0.setValue(i, false);
|
||
|
setUnsignedMinMax(c0, c0_min, c0_max);
|
||
|
- changed = true;
|
||
|
}
|
||
|
else
|
||
|
{
|
||
|
@@ -504,7 +485,6 @@ Result bvLessThanBothWays(FixedBits& c0,
|
||
|
c1.setFixed(i, true);
|
||
|
c1.setValue(i, true);
|
||
|
setUnsignedMinMax(c1, c1_min, c1_max);
|
||
|
- changed = true;
|
||
|
}
|
||
|
else
|
||
|
{
|
||
|
@@ -521,8 +501,6 @@ Result bvLessThanBothWays(FixedBits& c0,
|
||
|
|
||
|
Result bvLessThanEqualsBothWays(FixedBits& c0, FixedBits &c1, FixedBits& output)
|
||
|
{
|
||
|
- Result r = NO_CHANGE;
|
||
|
-
|
||
|
assert(c0.getWidth() == c1.getWidth());
|
||
|
|
||
|
CBV c0_min = CONSTANTBV::BitVector_Create(c0.getWidth(), true);
|
||
|
--- ./src/simplifier/constantBitP/ConstantBitP_Arithmetic.cpp.orig 2010-11-27 20:45:32.000000000 -0700
|
||
|
+++ ./src/simplifier/constantBitP/ConstantBitP_Arithmetic.cpp 2011-12-13 13:08:15.897474668 -0700
|
||
|
@@ -33,7 +33,6 @@ Result bvSubtractBothWays(vector<FixedBi
|
||
|
Addargs.push_back(¬B);
|
||
|
Addargs.push_back(&one);
|
||
|
|
||
|
- bool changed = false;
|
||
|
while (true) // until it fixed points
|
||
|
{
|
||
|
Result result;
|
||
|
@@ -51,8 +50,6 @@ Result bvSubtractBothWays(vector<FixedBi
|
||
|
|
||
|
if (FixedBits::equals(initialNotB, notB) && FixedBits::equals(initialA, a) && FixedBits::equals(initialOut, output))
|
||
|
break;
|
||
|
- else
|
||
|
- changed = true;
|
||
|
}
|
||
|
|
||
|
return NOT_IMPLEMENTED;
|
||
|
@@ -214,8 +211,6 @@ void printArray(int f[], int width)
|
||
|
|
||
|
Result bvAddBothWays(vector<FixedBits*>& children, FixedBits& output)
|
||
|
{
|
||
|
- Result result = NO_CHANGE;
|
||
|
-
|
||
|
const int bitWidth = output.getWidth();
|
||
|
const int numberOfChildren = children.size();
|
||
|
|
||
|
@@ -361,7 +356,6 @@ Result bvAddBothWays(vector<FixedBits*>&
|
||
|
{
|
||
|
output.setFixed(column, true);
|
||
|
output.setValue(column, newResult);
|
||
|
- result = CHANGED;
|
||
|
changed = true;
|
||
|
}
|
||
|
else if (output.isFixed(column) && (output.getValue(column) != newResult))
|
||
|
--- ./src/simplifier/FindPureLiterals.h.orig 2011-02-25 20:56:39.000000000 -0700
|
||
|
+++ ./src/simplifier/FindPureLiterals.h 2011-12-13 13:08:15.897474668 -0700
|
||
|
@@ -108,7 +108,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;
|
||
|
|
||
|
@@ -119,7 +119,7 @@ public:
|
||
|
|
||
|
default:
|
||
|
polarity = bothPolarity; // both
|
||
|
- for (int i =0; i < n.Degree(); i ++)
|
||
|
+ for (size_t i =0; i < n.Degree(); i ++)
|
||
|
build(n[i],polarity);
|
||
|
break;
|
||
|
}
|
||
|
--- ./src/simplifier/VariablesInExpression.cpp.orig 2011-02-01 05:41:57.000000000 -0700
|
||
|
+++ ./src/simplifier/VariablesInExpression.cpp 2011-12-13 13:08:15.898474667 -0700
|
||
|
@@ -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/SubstitutionMap.cpp.orig 2011-05-01 08:20:34.000000000 -0600
|
||
|
+++ ./src/simplifier/SubstitutionMap.cpp 2011-12-13 13:08:15.899474666 -0700
|
||
|
@@ -366,7 +366,7 @@ void SubstitutionMap::buildDepends(const
|
||
|
vars.VarSeenInTerm(vars.getSymbol(n1), rhs_visited, rhs, av);
|
||
|
|
||
|
sort(av.begin(), av.end());
|
||
|
- for (int i =0; i < av.size();i++)
|
||
|
+ for (size_t i =0; i < av.size();i++)
|
||
|
{
|
||
|
if (i!=0 && av[i] == av[i-1])
|
||
|
continue; // Treat it like a set of Symbol* in effect.
|
||
|
--- ./src/simplifier/simplifier.cpp.orig 2011-11-18 04:12:27.000000000 -0700
|
||
|
+++ ./src/simplifier/simplifier.cpp 2011-12-13 13:08:15.900474665 -0700
|
||
|
@@ -250,7 +250,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);
|
||
|
}
|
||
|
@@ -525,6 +525,7 @@ namespace BEEV
|
||
|
return getConstantBit(n[0], i);
|
||
|
|
||
|
assert(false);
|
||
|
+ return -1;
|
||
|
}
|
||
|
|
||
|
ASTNode
|
||
|
@@ -1293,7 +1294,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));
|
||
|
}
|
||
|
@@ -1655,9 +1656,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())
|
||
|
@@ -1685,7 +1686,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());
|
||
|
@@ -1716,7 +1717,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());
|
||
|
@@ -1897,7 +1898,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]))
|
||
|
{
|
||
|
@@ -2238,7 +2239,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));
|
||
|
@@ -2638,7 +2638,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.
|
||
|
@@ -2660,13 +2660,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;
|
||
|
@@ -2683,7 +2683,7 @@ namespace BEEV
|
||
|
//cerr << "old" << output;
|
||
|
ASTNode zeroes = _bm->CreateZeroConst(trailingZeroes);
|
||
|
ASTVec newChildren;
|
||
|
- for (int i = 0; i < output.Degree(); i++)
|
||
|
+ for (size_t i = 0; i < output.Degree(); i++)
|
||
|
newChildren.push_back(
|
||
|
nf->CreateTerm(BVEXTRACT, output.GetValueWidth() - trailingZeroes, output[i],
|
||
|
_bm->CreateBVConst(32, output.GetValueWidth() - 1),
|
||
|
--- ./src/simplifier/consteval.cpp.orig 2011-06-15 21:54:40.000000000 -0600
|
||
|
+++ ./src/simplifier/consteval.cpp 2011-12-13 13:08:15.900474665 -0700
|
||
|
@@ -43,7 +43,7 @@ namespace BEEV
|
||
|
|
||
|
ASTVec children;
|
||
|
children.reserve(number_of_children);
|
||
|
- for (int i =0; i < number_of_children; i++)
|
||
|
+ for (unsigned int i =0; i < number_of_children; i++)
|
||
|
{
|
||
|
if (input_children[i].isConstant())
|
||
|
children.push_back(input_children[i]);
|
||
|
--- ./src/simplifier/SubstitutionMap.h.orig 2011-04-12 20:00:29.000000000 -0600
|
||
|
+++ ./src/simplifier/SubstitutionMap.h 2011-12-13 13:08:15.901474664 -0700
|
||
|
@@ -40,7 +40,7 @@ class SubstitutionMap {
|
||
|
void loops_helper(const set<ASTNode>& varsToCheck, set<ASTNode>& visited);
|
||
|
bool loops(const ASTNode& n0, const ASTNode& n1);
|
||
|
|
||
|
- int substitutionsLastApplied;
|
||
|
+ size_t substitutionsLastApplied;
|
||
|
public:
|
||
|
|
||
|
bool hasUnappliedSubstitutions()
|
||
|
--- ./src/simplifier/RemoveUnconstrained.cpp.orig 2011-08-05 22:02:44.000000000 -0600
|
||
|
+++ ./src/simplifier/RemoveUnconstrained.cpp 2011-12-13 13:08:15.901474664 -0700
|
||
|
@@ -60,7 +60,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;
|
||
|
|
||
|
@@ -105,7 +105,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);
|
||
|
@@ -156,7 +156,7 @@ namespace BEEV
|
||
|
}
|
||
|
|
||
|
ASTNode concat = concatVec[0];
|
||
|
- for (int i=1; i < concatVec.size();i++)
|
||
|
+ for (size_t i=1; i < concatVec.size();i++)
|
||
|
{
|
||
|
assert(!concat.IsNull());
|
||
|
concat = bm.CreateTerm(BVCONCAT, concat.GetValueWidth() + concatVec[i].GetValueWidth(),concatVec[i], concat);
|
||
|
@@ -189,7 +189,7 @@ namespace BEEV
|
||
|
|
||
|
topMutable->getAllUnconstrainedVariables(variable_array);
|
||
|
|
||
|
- for (int i =0; i < variable_array.size() ; i++)
|
||
|
+ for (size_t i =0; i < variable_array.size() ; i++)
|
||
|
{
|
||
|
// Don't make this is a reference. If the vector gets resized, it will point to
|
||
|
// memory that no longer contains the object.
|
||
|
@@ -213,7 +213,7 @@ namespace BEEV
|
||
|
//nb. The children might be dirty. i.e. not have substitutions written through them yet.
|
||
|
ASTVec children;
|
||
|
children.reserve(mutable_children.size());
|
||
|
- for (int j = 0; j <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();
|
||
|
@@ -247,7 +247,7 @@ namespace BEEV
|
||
|
{
|
||
|
int found = 0;
|
||
|
|
||
|
- for (int i = 0; i < numberOfChildren; i++)
|
||
|
+ for (size_t i = 0; i < numberOfChildren; i++)
|
||
|
{
|
||
|
if (children[i] == var)
|
||
|
found++;
|
||
|
@@ -434,7 +434,7 @@ namespace BEEV
|
||
|
{
|
||
|
ASTNodeSet already;
|
||
|
ASTNode v =replaceParentWithFresh(muteParent, variable_array);
|
||
|
- for (int i =0; i < numberOfChildren;i++)
|
||
|
+ for (size_t i =0; i < numberOfChildren;i++)
|
||
|
{
|
||
|
/* to avoid problems with:
|
||
|
734:(AND
|
||
|
@@ -469,7 +469,7 @@ namespace BEEV
|
||
|
ASTNode v =replaceParentWithFresh(muteParent, variable_array);
|
||
|
|
||
|
ASTVec others;
|
||
|
- for (int i = 0; i < numberOfChildren; i++)
|
||
|
+ for (size_t i = 0; i < numberOfChildren; i++)
|
||
|
{
|
||
|
if (children[i] !=var)
|
||
|
others.push_back(mutable_children[i]->toASTNode(nf));
|
||
|
@@ -622,7 +622,7 @@ namespace BEEV
|
||
|
case BVPLUS:
|
||
|
{
|
||
|
ASTVec other;
|
||
|
- for (int i = 0; i < children.size(); i++)
|
||
|
+ for (size_t i = 0; i < children.size(); i++)
|
||
|
if (children[i] != var)
|
||
|
other.push_back(mutable_children[i]->toASTNode(nf));
|
||
|
|
||
|
@@ -644,7 +644,6 @@ namespace BEEV
|
||
|
{
|
||
|
ASTNode v =replaceParentWithFresh(muteParent, variable_array);
|
||
|
|
||
|
- const unsigned resultWidth = width;
|
||
|
const unsigned operandWidth = var.GetValueWidth();
|
||
|
assert(children[0] == var); // It can't be anywhere else.
|
||
|
|
||
|
--- ./src/absrefine_counterexample/CounterExample.cpp.orig 2011-11-10 06:01:41.000000000 -0700
|
||
|
+++ ./src/absrefine_counterexample/CounterExample.cpp 2011-12-13 13:08:15.902474663 -0700
|
||
|
@@ -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/absrefine_counterexample/AbstractionRefinement.cpp.orig 2011-08-30 22:02:27.000000000 -0600
|
||
|
+++ ./src/absrefine_counterexample/AbstractionRefinement.cpp 2011-12-13 13:08:15.902474663 -0700
|
||
|
@@ -35,7 +35,7 @@ namespace BEEV
|
||
|
{
|
||
|
assert(a.GetKind() == SYMBOL);
|
||
|
// It was ommitted from the initial problem, so assign it freshly.
|
||
|
- for (int i = 0; i < a.GetValueWidth(); i++)
|
||
|
+ for (unsigned int i = 0; i < a.GetValueWidth(); i++)
|
||
|
{
|
||
|
SATSolver::Var v = SatSolver.newVar();
|
||
|
// We probably don't want the variable eliminated.
|
||
|
@@ -55,7 +55,7 @@ namespace BEEV
|
||
|
getEquals(SATSolver& SatSolver, const ASTNode& a, const ASTNode& b, ToSATBase::ASTNodeToSATVar& satVar,
|
||
|
Polarity polary = BOTH)
|
||
|
{
|
||
|
- const int width = a.GetValueWidth();
|
||
|
+ const unsigned int width = a.GetValueWidth();
|
||
|
assert(width == b.GetValueWidth());
|
||
|
assert(!a.isConstant() || !b.isConstant());
|
||
|
|
||
|
@@ -72,7 +72,7 @@ namespace BEEV
|
||
|
SATSolver::vec_literals all;
|
||
|
const int result = SatSolver.newVar();
|
||
|
|
||
|
- for (int i = 0; i < width; i++)
|
||
|
+ for (unsigned int i = 0; i < width; i++)
|
||
|
{
|
||
|
SATSolver::vec_literals s;
|
||
|
|
||
|
@@ -116,7 +116,7 @@ namespace BEEV
|
||
|
}
|
||
|
return result;
|
||
|
}
|
||
|
- else if (v_a.size() == 0 ^ v_b.size() == 0)
|
||
|
+ else if ((v_a.size() == 0) ^ (v_b.size() == 0))
|
||
|
{
|
||
|
ASTNode constant = a.isConstant() ? a : b;
|
||
|
vector<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];
|
||
|
|
||
|
--- ./src/to-sat/ASTNode/ToSAT.cpp.orig 2011-02-01 22:39:54.000000000 -0700
|
||
|
+++ ./src/to-sat/ASTNode/ToSAT.cpp 2011-12-13 13:08:15.903474662 -0700
|
||
|
@@ -52,7 +52,7 @@ namespace BEEV
|
||
|
|
||
|
// Copies the symbol into the map that is used to build the counter example.
|
||
|
// For boolean we create a vector of size 1.
|
||
|
- if (n.GetKind() == BVGETBIT && n[0].GetKind() == SYMBOL || (n.GetKind() == SYMBOL && !isTseitinVariable(n)))
|
||
|
+ if ((n.GetKind() == BVGETBIT && n[0].GetKind() == SYMBOL) || (n.GetKind() == SYMBOL && !isTseitinVariable(n)))
|
||
|
{
|
||
|
const ASTNode& symbol = n.GetKind() == BVGETBIT ? n[0] : n;
|
||
|
const unsigned index = n.GetKind() == BVGETBIT ? n[1].GetUnsignedConst() : 0;
|
||
|
@@ -98,7 +98,7 @@ namespace BEEV
|
||
|
CountersAndStats("SAT Solver", bm);
|
||
|
bm->GetRunTimes()->start(RunTimes::SendingToSAT);
|
||
|
|
||
|
- int input_clauselist_size = cll.size();
|
||
|
+ // int input_clauselist_size = cll.size();
|
||
|
if (cll.size() == 0)
|
||
|
{
|
||
|
FatalError("toSATandSolve: Nothing to Solve", ASTUndefined);
|
||
|
@@ -115,7 +115,7 @@ namespace BEEV
|
||
|
|
||
|
//iterate through the list (conjunction) of ASTclauses cll
|
||
|
ClauseContainer::const_iterator i = cc.begin(), iend = cc.end();
|
||
|
- for (int count=0, flag=0; i != iend; i++)
|
||
|
+ for ( ; i != iend; i++)
|
||
|
{
|
||
|
satSolverClause.clear();
|
||
|
vector<const 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-01-23 06:08:12.000000000 -0700
|
||
|
+++ ./src/to-sat/ASTNode/ToCNF.cpp 2011-12-13 13:08:15.903474663 -0700
|
||
|
@@ -250,12 +250,14 @@ namespace BEEV
|
||
|
return psi;
|
||
|
} //End of SINGLETON()
|
||
|
|
||
|
+#ifdef CRYPTOMINISAT__2
|
||
|
static ASTNode GetNodeFrom_SINGLETON(ClauseList *cl)
|
||
|
{
|
||
|
ClausePtr c = (*(*cl).asList())[0];
|
||
|
const ASTNode * a = (*c)[0];
|
||
|
return *a;
|
||
|
}
|
||
|
+#endif
|
||
|
|
||
|
//########################################
|
||
|
//########################################
|
||
|
--- ./src/to-sat/BitBlaster.cpp.orig 2011-11-15 03:40:28.000000000 -0700
|
||
|
+++ ./src/to-sat/BitBlaster.cpp 2011-12-13 13:08:15.904474662 -0700
|
||
|
@@ -299,7 +299,7 @@ void BitBlaster<BBNode,BBNodeManagerT>::
|
||
|
template <class BBNode, class BBNodeManagerT>
|
||
|
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;
|
||
|
@@ -322,7 +322,7 @@ ASTNode BitBlaster<BBNode,BBNodeManagerT
|
||
|
|
||
|
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);
|
||
|
|
||
|
@@ -640,14 +640,14 @@ const BBNodeVec BitBlaster<BBNode,BBNode
|
||
|
{
|
||
|
// 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();
|
||
|
std::vector<stack<BBNode> > products(bitWidth);
|
||
|
for (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(results[j][i]);
|
||
|
}
|
||
|
|
||
|
@@ -1070,7 +1070,7 @@ void convert(const BBNodeVec& v, BBNodeM
|
||
|
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;
|
||
|
@@ -1082,7 +1082,7 @@ void convert(const BBNodeVec& v, BBNodeM
|
||
|
|
||
|
// 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);
|
||
|
|
||
|
@@ -1092,7 +1092,7 @@ void convert(const BBNodeVec& v, BBNodeM
|
||
|
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;
|
||
|
@@ -1105,7 +1105,7 @@ void convert(const BBNodeVec& v, BBNodeM
|
||
|
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;
|
||
|
}
|
||
|
}
|
||
|
@@ -1310,7 +1310,7 @@ BBNodeVec BitBlaster<BBNode,BBNodeManage
|
||
|
cerr << "["<< ms.columnL[i] << ":"<< ms.columnH[i] << "]["<< ms.sumL[i] << ":" << ms.sumH[i] << "]";
|
||
|
}
|
||
|
|
||
|
- if ((products[i].size() > ms.sumH[i]) && ms.sumH[i] < 10)
|
||
|
+ if (((int)products[i].size() > ms.sumH[i]) && ms.sumH[i] < 10)
|
||
|
{
|
||
|
if (debug_bounds)
|
||
|
cerr << "S";
|
||
|
@@ -1361,7 +1361,7 @@ void BitBlaster<BBNode,BBNodeManagerT>::
|
||
|
}
|
||
|
|
||
|
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]));
|
||
|
}
|
||
|
@@ -1414,7 +1414,7 @@ void BitBlaster<BBNode,BBNodeManagerT>::
|
||
|
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(t_products[i][j]);
|
||
|
}
|
||
|
}
|
||
|
@@ -1488,7 +1488,7 @@ BBNodeVec BitBlaster<BBNode,BBNodeManage
|
||
|
{
|
||
|
|
||
|
// 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(priorSorted[k]);
|
||
|
}
|
||
|
@@ -1570,7 +1570,7 @@ BBNodeVec BitBlaster<BBNode,BBNodeManage
|
||
|
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);
|
||
|
@@ -1587,6 +1587,7 @@ BBNodeVec BitBlaster<BBNode,BBNodeManage
|
||
|
|
||
|
assert(v[i]== BBFalse);
|
||
|
}
|
||
|
+ }
|
||
|
}
|
||
|
}
|
||
|
}
|
||
|
@@ -1701,7 +1702,7 @@ void BitBlaster<BBNode,BBNodeManagerT>::
|
||
|
|
||
|
// check if y is already zero.
|
||
|
bool isZero=true;
|
||
|
- for (int i =0; i < rwidth;i++)
|
||
|
+ for (unsigned int i =0; i < rwidth;i++)
|
||
|
if (y[i] != nf->getFalse())
|
||
|
{
|
||
|
isZero = false;
|
||
|
--- ./src/to-sat/AIG/BBNodeManagerAIG.h.orig 2011-02-01 22:39:54.000000000 -0700
|
||
|
+++ ./src/to-sat/AIG/BBNodeManagerAIG.h 2011-12-13 13:08:15.905474660 -0700
|
||
|
@@ -142,7 +142,7 @@ public:
|
||
|
Aig_Obj_t * pNode;
|
||
|
assert (children.size() != 0);
|
||
|
|
||
|
- for (int i =0; i < children.size();i++)
|
||
|
+ for (size_t i =0; i < children.size();i++)
|
||
|
assert(!children[i].IsNull());
|
||
|
|
||
|
switch (kind)
|
||
|
--- ./src/to-sat/AIG/ToSATAIG.cpp.orig 2011-11-27 19:55:18.000000000 -0700
|
||
|
+++ ./src/to-sat/AIG/ToSATAIG.cpp 2011-12-13 13:08:15.905474660 -0700
|
||
|
@@ -126,7 +126,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]);
|
||
|
}
|
||
|
|
||
|
@@ -134,7 +134,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]);
|
||
|
}
|
||
|
}
|
||
|
@@ -185,7 +185,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.
|
||
|
@@ -194,7 +194,7 @@ namespace BEEV
|
||
|
}
|
||
|
nodeToSATVar.insert(make_pair(ar.index_symbol, v_a));
|
||
|
|
||
|
- for (int i = 0; i < v_a.size(); i++)
|
||
|
+ for (size_t i = 0; i < v_a.size(); i++)
|
||
|
{
|
||
|
SATSolver::Var var = v_a[i];
|
||
|
index.push(SATSolver::mkLit(var, false));
|
||
|
@@ -210,7 +210,7 @@ namespace BEEV
|
||
|
if (it != nodeToSATVar.end())
|
||
|
{
|
||
|
vector<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));
|
||
|
@@ -219,7 +219,7 @@ namespace BEEV
|
||
|
else if (ar.symbol.isConstant())
|
||
|
{
|
||
|
CBV c = ar.symbol.GetBVConst();
|
||
|
- for (int i = 0; i < ar.symbol.GetValueWidth(); i++)
|
||
|
+ for (unsigned int i = 0; i < ar.symbol.GetValueWidth(); i++)
|
||
|
if (CONSTANTBV::BitVector_bit_test(c, i))
|
||
|
value_constants.push((Minisat::lbool) satSolver.true_literal());
|
||
|
else
|
||
|
@@ -233,7 +233,7 @@ namespace BEEV
|
||
|
|
||
|
assert(ar.symbol.GetKind() == SYMBOL);
|
||
|
// It was ommitted from the initial problem, so assign it freshly.
|
||
|
- for (int i = 0; i < ar.symbol.GetValueWidth(); i++)
|
||
|
+ for (unsigned int i = 0; i < ar.symbol.GetValueWidth(); i++)
|
||
|
{
|
||
|
SATSolver::Var v = satSolver.newVar();
|
||
|
// We probably don't want the variable eliminated.
|
||
|
@@ -242,7 +242,7 @@ namespace BEEV
|
||
|
}
|
||
|
nodeToSATVar.insert(make_pair(ar.symbol, v_a));
|
||
|
|
||
|
- for (int i = 0; i < v_a.size(); i++)
|
||
|
+ for (size_t i = 0; i < v_a.size(); i++)
|
||
|
{
|
||
|
SATSolver::Var var = v_a[i];
|
||
|
value.push(SATSolver::mkLit(var, false));
|
||
|
--- ./src/c_interface/c_interface.cpp.orig 2011-11-10 06:01:41.000000000 -0700
|
||
|
+++ ./src/c_interface/c_interface.cpp 2011-12-13 13:08:15.906474658 -0700
|
||
|
@@ -613,7 +613,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;
|
||
|
@@ -626,7 +625,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;
|
||
|
@@ -646,7 +644,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();
|
||
|
@@ -1038,7 +1035,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: "\
|
||
|
@@ -1581,16 +1578,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;
|
||
|
|
||
|
@@ -1765,7 +1757,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/printer/SMTLIB2Printer.cpp.orig 2010-07-10 08:49:13.000000000 -0600
|
||
|
+++ ./src/printer/SMTLIB2Printer.cpp 2011-12-13 13:08:15.906474658 -0700
|
||
|
@@ -210,7 +210,7 @@ void printVarDeclsToStream(ASTNodeSet& s
|
||
|
{
|
||
|
string close = "";
|
||
|
|
||
|
- for (int i =0; i < c.size()-1; i++)
|
||
|
+ for (size_t i =0; i < c.size()-1; i++)
|
||
|
{
|
||
|
os << "(" << functionToSMTLIBName(kind,false);
|
||
|
os << " ";
|
||
|
--- ./src/printer/SMTLIB1Printer.cpp.orig 2010-06-24 23:19:52.000000000 -0600
|
||
|
+++ ./src/printer/SMTLIB1Printer.cpp 2011-12-13 13:08:15.906474658 -0700
|
||
|
@@ -214,7 +214,7 @@ void printSMTLIB1VarDeclsToStream(ASTNod
|
||
|
{
|
||
|
string close = "";
|
||
|
|
||
|
- for (int i =0; i < c.size()-1; i++)
|
||
|
+ for (size_t i =0; i < c.size()-1; i++)
|
||
|
{
|
||
|
os << "(" << functionToSMTLIBName(kind,true);
|
||
|
os << " ";
|
||
|
--- ./src/printer/SMTLIBPrinter.h.orig 2010-05-23 20:03:46.000000000 -0600
|
||
|
+++ ./src/printer/SMTLIBPrinter.h 2011-12-13 13:08:15.907474657 -0700
|
||
|
@@ -24,7 +24,5 @@ namespace printer
|
||
|
ostream& SMTLIB_Print(ostream &os, const ASTNode n, const int indentation, void (*SMTLIB_Print1)(ostream&, const ASTNode , int , bool ), bool smtlib1);
|
||
|
|
||
|
bool containsAnyArrayOps(const ASTNode& n);
|
||
|
-
|
||
|
- static string tolower(const char * name);
|
||
|
};
|
||
|
#endif
|
||
|
--- ./src/sat/SimplifyingMinisat.h.orig 2011-06-22 20:17:24.000000000 -0600
|
||
|
+++ ./src/sat/SimplifyingMinisat.h 2011-12-13 13:08:15.907474657 -0700
|
||
|
@@ -34,7 +34,7 @@ namespace BEEV
|
||
|
bool
|
||
|
simplify(); // Removes already satisfied clauses.
|
||
|
|
||
|
- int setVerbosity(int v);
|
||
|
+ void setVerbosity(int v);
|
||
|
|
||
|
virtual uint8_t modelValue(Var x) const;
|
||
|
|
||
|
--- ./src/sat/SATSolver.h.orig 2011-10-22 06:12:28.000000000 -0600
|
||
|
+++ ./src/sat/SATSolver.h 2011-12-13 13:08:15.907474657 -0700
|
||
|
@@ -58,7 +58,7 @@ namespace BEEV
|
||
|
virtual void setSeed(int i)
|
||
|
{}
|
||
|
|
||
|
- virtual int setVerbosity(int v) =0;
|
||
|
+ virtual void setVerbosity(int v) =0;
|
||
|
|
||
|
virtual lbool true_literal() =0;
|
||
|
virtual lbool false_literal() =0;
|
||
|
--- ./src/sat/MinisatCore_prop.h.orig 2011-10-22 06:12:28.000000000 -0600
|
||
|
+++ ./src/sat/MinisatCore_prop.h 2011-12-13 13:08:15.907474657 -0700
|
||
|
@@ -43,7 +43,7 @@ namespace BEEV
|
||
|
|
||
|
virtual Var newVar();
|
||
|
|
||
|
- int setVerbosity(int v);
|
||
|
+ void setVerbosity(int v);
|
||
|
|
||
|
int nVars();
|
||
|
|
||
|
--- ./src/sat/SimplifyingMinisat.cpp.orig 2011-06-22 20:17:24.000000000 -0600
|
||
|
+++ ./src/sat/SimplifyingMinisat.cpp 2011-12-13 13:08:15.908474656 -0700
|
||
|
@@ -17,7 +17,7 @@ namespace BEEV
|
||
|
bool
|
||
|
SimplifyingMinisat::addClause(const vec_literals& ps) // Add a clause to the solver.
|
||
|
{
|
||
|
- s->addClause(ps);
|
||
|
+ return s->addClause(ps);
|
||
|
}
|
||
|
|
||
|
bool
|
||
|
@@ -47,7 +47,7 @@ namespace BEEV
|
||
|
return Minisat::toInt(s->modelValue(x));
|
||
|
}
|
||
|
|
||
|
- int SimplifyingMinisat::setVerbosity(int v)
|
||
|
+ void SimplifyingMinisat::setVerbosity(int v)
|
||
|
{
|
||
|
s->verbosity = v;
|
||
|
}
|
||
|
--- ./src/sat/cryptominisat2/Logger.cpp.orig 2010-06-04 12:11:26.000000000 -0600
|
||
|
+++ ./src/sat/cryptominisat2/Logger.cpp 2011-12-13 13:08:15.908474656 -0700
|
||
|
@@ -372,8 +372,9 @@ void Logger::end(const finish_type finis
|
||
|
fprintf(proof,"}\n");
|
||
|
history.push_back(uniqueid);
|
||
|
|
||
|
- proof = (FILE*)fclose(proof);
|
||
|
- assert(proof == NULL);
|
||
|
+ int err = fclose(proof);
|
||
|
+ assert(err == 0);
|
||
|
+ proof = NULL;
|
||
|
}
|
||
|
|
||
|
if (statistics_on) {
|
||
|
--- ./src/sat/cryptominisat2/FailedVarSearcher.cpp.orig 2010-07-02 08:35:28.000000000 -0600
|
||
|
+++ ./src/sat/cryptominisat2/FailedVarSearcher.cpp 2011-12-13 13:08:15.909474655 -0700
|
||
|
@@ -261,7 +261,6 @@ const bool FailedVarSearcher::search(uin
|
||
|
}*/
|
||
|
|
||
|
end:
|
||
|
- bool removedOldLearnts = false;
|
||
|
binClauseAdded = solver.binaryClauses.size() - origBinClauses;
|
||
|
//Print results
|
||
|
if (solver.verbosity >= 1) printResults(myTime);
|
||
|
@@ -272,7 +271,6 @@ end:
|
||
|
double time = cpuTime();
|
||
|
if ((int)origHeapSize - (int)solver.order_heap.size() > (int)origHeapSize/15 && solver.nClauses() + solver.learnts.size() > 500000) {
|
||
|
completelyDetachAndReattach();
|
||
|
- removedOldLearnts = true;
|
||
|
} else {
|
||
|
solver.clauseCleaner->removeAndCleanAll();
|
||
|
}
|
||
|
--- ./src/sat/CryptoMinisat.cpp.orig 2010-08-20 06:07:42.000000000 -0600
|
||
|
+++ ./src/sat/CryptoMinisat.cpp 2011-12-13 13:08:15.909474655 -0700
|
||
|
@@ -34,7 +34,7 @@ namespace BEEV
|
||
|
for (int i =0; i<ps.size();i++)
|
||
|
v.push(MINISAT::Lit(var(ps[i]), sign(ps[i])));
|
||
|
|
||
|
- s->addClause(v);
|
||
|
+ return s->addClause(v);
|
||
|
}
|
||
|
|
||
|
bool
|
||
|
@@ -61,7 +61,7 @@ namespace BEEV
|
||
|
return s->newVar();
|
||
|
}
|
||
|
|
||
|
- int CryptoMinisat::setVerbosity(int v)
|
||
|
+ void CryptoMinisat::setVerbosity(int v)
|
||
|
{
|
||
|
s->verbosity = v;
|
||
|
}
|
||
|
--- ./src/sat/core_prop/Solver_prop.cc.orig 2011-11-27 19:55:18.000000000 -0700
|
||
|
+++ ./src/sat/core_prop/Solver_prop.cc 2011-12-13 13:08:15.909474655 -0700
|
||
|
@@ -171,11 +171,11 @@ Solver_prop::addArray(int array_id, cons
|
||
|
|
||
|
if (!ok) return false;
|
||
|
|
||
|
- if (i.size() > INDEX_BIT_WIDTH || ki.size() > INDEX_BIT_WIDTH)
|
||
|
+ if (i.size() > (int)INDEX_BIT_WIDTH || ki.size() > (int)INDEX_BIT_WIDTH)
|
||
|
{
|
||
|
printf("The array propagators unfortunately don't do arbitrary precision integers yet. "
|
||
|
"With the INDICES_128BITS compile time flag STP does 128-bits on 64-bit machines compiled with GCC. "
|
||
|
- "Currently STP is compiled to use %d bit indices. "
|
||
|
+ "Currently STP is compiled to use %zu bit indices. "
|
||
|
"Unfortunately your problem has array indexes of size %d bits. "
|
||
|
"STP does arbitrary precision indices with the '--oldstyle-refinement' or the '-r' flags.\n",
|
||
|
INDEX_BIT_WIDTH, std::max(i.size(), ki.size()));
|
||
|
@@ -1167,7 +1167,6 @@ void Solver_prop::analyze(CRef confl, ve
|
||
|
|
||
|
if (debug_print)
|
||
|
printf("%d %d\n", toInt(p), toInt(var(p)));
|
||
|
- Minisat::Clause cl= ca[confl];
|
||
|
|
||
|
assert(ca[confl][0] ==p);
|
||
|
assert(value(p) != l_Undef);
|
||
|
--- ./src/sat/core_prop/Solver_prop.h.orig 2011-11-27 19:55:18.000000000 -0700
|
||
|
+++ ./src/sat/core_prop/Solver_prop.h 2011-12-13 13:08:15.910474654 -0700
|
||
|
@@ -36,8 +36,10 @@ namespace Minisat {
|
||
|
typedef unsigned int uint128_t __attribute__((mode(TI)));
|
||
|
static inline uint32_t hash(uint128_t x){ return (uint32_t)x; }
|
||
|
typedef uint128_t index_type;
|
||
|
+# define PRIuIT PRIu128
|
||
|
#else
|
||
|
typedef uint64_t index_type;
|
||
|
+# define PRIuIT PRIu64
|
||
|
#endif
|
||
|
|
||
|
#define INDEX_BIT_WIDTH (sizeof(index_type) *8)
|
||
|
@@ -227,7 +229,7 @@ private:
|
||
|
printf("Value Size: %d\n", value.size());
|
||
|
printClause2(value);
|
||
|
|
||
|
- printf("Known Index: %ld ", isIndexConstant() ? index_constant : -1);
|
||
|
+ printf("Known Index: %" PRIuIT " ", isIndexConstant() ? index_constant : (index_type)-1);
|
||
|
printf("Known Value: %c\n", isValueConstant() ? 't' : 'f');
|
||
|
printf("Array ID:%d\n", array_id);
|
||
|
printf("------------\n");
|
||
|
--- ./src/sat/utils/Options.h.orig 2010-11-27 19:45:43.000000000 -0700
|
||
|
+++ ./src/sat/utils/Options.h 2011-12-13 13:08:15.911474653 -0700
|
||
|
@@ -60,7 +60,7 @@ class Option
|
||
|
struct OptionLt {
|
||
|
bool operator()(const Option* x, const Option* y) {
|
||
|
int test1 = strcmp(x->category, y->category);
|
||
|
- return test1 < 0 || test1 == 0 && strcmp(x->type_name, y->type_name) < 0;
|
||
|
+ return test1 < 0 || (test1 == 0 && strcmp(x->type_name, y->type_name) < 0);
|
||
|
}
|
||
|
};
|
||
|
|
||
|
--- ./src/sat/MinisatCore.cpp.orig 2011-10-22 06:12:28.000000000 -0600
|
||
|
+++ ./src/sat/MinisatCore.cpp 2011-12-13 13:08:15.911474653 -0700
|
||
|
@@ -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;
|
||
|
}
|
||
|
--- ./src/sat/MinisatCore_prop.cpp.orig 2011-10-22 06:12:28.000000000 -0600
|
||
|
+++ ./src/sat/MinisatCore_prop.cpp 2011-12-13 13:08:15.911474653 -0700
|
||
|
@@ -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 2010-08-20 06:07:42.000000000 -0600
|
||
|
+++ ./src/sat/CryptoMinisat.h 2011-12-13 13:08:15.912474651 -0700
|
||
|
@@ -36,7 +36,7 @@ namespace BEEV
|
||
|
|
||
|
virtual Var newVar();
|
||
|
|
||
|
- int setVerbosity(int v);
|
||
|
+ void setVerbosity(int v);
|
||
|
|
||
|
int nVars();
|
||
|
|
||
|
--- ./src/sat/MinisatCore.h.orig 2010-08-20 06:07:42.000000000 -0600
|
||
|
+++ ./src/sat/MinisatCore.h 2011-12-13 13:08:15.912474651 -0700
|
||
|
@@ -40,7 +40,7 @@ namespace BEEV
|
||
|
|
||
|
virtual Var newVar();
|
||
|
|
||
|
- int setVerbosity(int v);
|
||
|
+ void setVerbosity(int v);
|
||
|
|
||
|
int nVars();
|
||
|
|
||
|
--- ./src/extlib-abc/kit.h.orig 2011-02-09 18:31:59.000000000 -0700
|
||
|
+++ ./src/extlib-abc/kit.h 2011-12-13 13:08:15.912474651 -0700
|
||
|
@@ -53,11 +53,15 @@ struct Kit_Sop_t_
|
||
|
unsigned * pCubes; // the storage for cubes
|
||
|
};
|
||
|
|
||
|
-typedef struct Kit_Edge_t_ Kit_Edge_t;
|
||
|
-struct Kit_Edge_t_
|
||
|
+typedef union Kit_Edge_t_ Kit_Edge_t;
|
||
|
+union Kit_Edge_t_
|
||
|
{
|
||
|
- unsigned fCompl : 1; // the complemented bit
|
||
|
- unsigned Node : 30; // the decomposition node pointed by the edge
|
||
|
+ struct {
|
||
|
+ unsigned fCompl : 1; // the complemented bit
|
||
|
+ unsigned Node : 30; // the decomposition node pointed by the edge
|
||
|
+ } edgeBits;
|
||
|
+
|
||
|
+ unsigned int edgeInt;
|
||
|
};
|
||
|
|
||
|
typedef struct Kit_Node_t_ Kit_Node_t;
|
||
|
@@ -203,18 +207,18 @@ static inline void Kit_SopShrink
|
||
|
static inline void Kit_SopPushCube( Kit_Sop_t * cSop, unsigned uCube ) { cSop->pCubes[cSop->nCubes++] = uCube; }
|
||
|
static inline void Kit_SopWriteCube( Kit_Sop_t * cSop, unsigned uCube, int i ) { cSop->pCubes[i] = uCube; }
|
||
|
|
||
|
-static inline Kit_Edge_t Kit_EdgeCreate( int Node, int fCompl ) { Kit_Edge_t eEdge = { fCompl, Node }; return eEdge; }
|
||
|
-static inline unsigned Kit_EdgeToInt( Kit_Edge_t eEdge ) { return (eEdge.Node << 1) | eEdge.fCompl; }
|
||
|
+static inline Kit_Edge_t Kit_EdgeCreate( int Node, int fCompl ) { Kit_Edge_t eEdge = { { fCompl, Node } }; return eEdge; }
|
||
|
+static inline unsigned Kit_EdgeToInt( Kit_Edge_t eEdge ) { return (eEdge.edgeBits.Node << 1) | eEdge.edgeBits.fCompl; }
|
||
|
static inline Kit_Edge_t Kit_IntToEdge( unsigned Edge ) { return Kit_EdgeCreate( Edge >> 1, Edge & 1 ); }
|
||
|
-static inline unsigned Kit_EdgeToInt_( Kit_Edge_t eEdge ) { return *(unsigned *)&eEdge; }
|
||
|
-static inline Kit_Edge_t Kit_IntToEdge_( unsigned Edge ) { return *(Kit_Edge_t *)&Edge; }
|
||
|
+static inline unsigned Kit_EdgeToInt_( Kit_Edge_t eEdge ) { return eEdge.edgeInt; }
|
||
|
+static inline Kit_Edge_t Kit_IntToEdge_( unsigned Edge ) { Kit_Edge_t eEdge; eEdge.edgeInt = Edge; return eEdge; }
|
||
|
|
||
|
static inline int Kit_GraphIsConst( Kit_Graph_t * pGraph ) { return pGraph->fConst; }
|
||
|
-static inline int Kit_GraphIsConst0( Kit_Graph_t * pGraph ) { return pGraph->fConst && pGraph->eRoot.fCompl; }
|
||
|
-static inline int Kit_GraphIsConst1( Kit_Graph_t * pGraph ) { return pGraph->fConst && !pGraph->eRoot.fCompl; }
|
||
|
-static inline int Kit_GraphIsComplement( Kit_Graph_t * pGraph ) { return pGraph->eRoot.fCompl; }
|
||
|
-static inline int Kit_GraphIsVar( Kit_Graph_t * pGraph ) { return pGraph->eRoot.Node < (unsigned)pGraph->nLeaves; }
|
||
|
-static inline void Kit_GraphComplement( Kit_Graph_t * pGraph ) { pGraph->eRoot.fCompl ^= 1; }
|
||
|
+static inline int Kit_GraphIsConst0( Kit_Graph_t * pGraph ) { return pGraph->fConst && pGraph->eRoot.edgeBits.fCompl; }
|
||
|
+static inline int Kit_GraphIsConst1( Kit_Graph_t * pGraph ) { return pGraph->fConst && !pGraph->eRoot.edgeBits.fCompl; }
|
||
|
+static inline int Kit_GraphIsComplement( Kit_Graph_t * pGraph ) { return pGraph->eRoot.edgeBits.fCompl; }
|
||
|
+static inline int Kit_GraphIsVar( Kit_Graph_t * pGraph ) { return pGraph->eRoot.edgeBits.Node < (unsigned)pGraph->nLeaves; }
|
||
|
+static inline void Kit_GraphComplement( Kit_Graph_t * pGraph ) { pGraph->eRoot.edgeBits.fCompl ^= 1; }
|
||
|
static inline void Kit_GraphSetRoot( Kit_Graph_t * pGraph, Kit_Edge_t eRoot ) { pGraph->eRoot = eRoot; }
|
||
|
static inline int Kit_GraphLeaveNum( Kit_Graph_t * pGraph ) { return pGraph->nLeaves; }
|
||
|
static inline int Kit_GraphNodeNum( Kit_Graph_t * pGraph ) { return pGraph->nSize - pGraph->nLeaves; }
|
||
|
@@ -222,14 +226,12 @@ static inline Kit_Node_t * Kit_GraphNode
|
||
|
static inline Kit_Node_t * Kit_GraphNodeLast( Kit_Graph_t * pGraph ) { return pGraph->pNodes + pGraph->nSize - 1; }
|
||
|
static inline int Kit_GraphNodeInt( Kit_Graph_t * pGraph, Kit_Node_t * pNode ) { return pNode - pGraph->pNodes; }
|
||
|
static inline int Kit_GraphNodeIsVar( Kit_Graph_t * pGraph, Kit_Node_t * pNode ) { return Kit_GraphNodeInt(pGraph,pNode) < pGraph->nLeaves; }
|
||
|
-static inline Kit_Node_t * Kit_GraphVar( Kit_Graph_t * pGraph ) { assert( Kit_GraphIsVar( pGraph ) ); return Kit_GraphNode( pGraph, pGraph->eRoot.Node ); }
|
||
|
+static inline Kit_Node_t * Kit_GraphVar( Kit_Graph_t * pGraph ) { assert( Kit_GraphIsVar( pGraph ) ); return Kit_GraphNode( pGraph, pGraph->eRoot.edgeBits.Node ); }
|
||
|
static inline int Kit_GraphVarInt( Kit_Graph_t * pGraph ) { assert( Kit_GraphIsVar( pGraph ) ); return Kit_GraphNodeInt( pGraph, Kit_GraphVar(pGraph) ); }
|
||
|
-static inline Kit_Node_t * Kit_GraphNodeFanin0( Kit_Graph_t * pGraph, Kit_Node_t * pNode ){ return Kit_GraphNodeIsVar(pGraph, pNode)? NULL : Kit_GraphNode(pGraph, pNode->eEdge0.Node); }
|
||
|
-static inline Kit_Node_t * Kit_GraphNodeFanin1( Kit_Graph_t * pGraph, Kit_Node_t * pNode ){ return Kit_GraphNodeIsVar(pGraph, pNode)? NULL : Kit_GraphNode(pGraph, pNode->eEdge1.Node); }
|
||
|
-static inline int Kit_GraphRootLevel( Kit_Graph_t * pGraph ) { return Kit_GraphNode(pGraph, pGraph->eRoot.Node)->Level; }
|
||
|
+static inline Kit_Node_t * Kit_GraphNodeFanin0( Kit_Graph_t * pGraph, Kit_Node_t * pNode ){ return Kit_GraphNodeIsVar(pGraph, pNode)? NULL : Kit_GraphNode(pGraph, pNode->eEdge0.edgeBits.Node); }
|
||
|
+static inline Kit_Node_t * Kit_GraphNodeFanin1( Kit_Graph_t * pGraph, Kit_Node_t * pNode ){ return Kit_GraphNodeIsVar(pGraph, pNode)? NULL : Kit_GraphNode(pGraph, pNode->eEdge1.edgeBits.Node); }
|
||
|
+static inline int Kit_GraphRootLevel( Kit_Graph_t * pGraph ) { return Kit_GraphNode(pGraph, pGraph->eRoot.edgeBits.Node)->Level; }
|
||
|
|
||
|
-static inline int Kit_Float2Int( float Val ) { return *((int *)&Val); }
|
||
|
-static inline float Kit_Int2Float( int Num ) { return *((float *)&Num); }
|
||
|
static inline int Kit_BitWordNum( int nBits ) { return nBits/(8*sizeof(unsigned)) + ((nBits%(8*sizeof(unsigned))) > 0); }
|
||
|
static inline int Kit_TruthWordNum( int nVars ) { return nVars <= 5 ? 1 : (1 << (nVars - 5)); }
|
||
|
static inline unsigned Kit_BitMask( int nBits ) { assert( nBits <= 32 ); return ~((~(unsigned)0) << nBits); }
|
||
|
@@ -486,6 +488,18 @@ static inline void Kit_TruthIthVar( unsi
|
||
|
/// FUNCTION DECLARATIONS ///
|
||
|
////////////////////////////////////////////////////////////////////////
|
||
|
|
||
|
+extern Kit_Graph_t * Kit_GraphCreateConst0( void );
|
||
|
+extern Kit_Graph_t * Kit_GraphCreateConst1( void );
|
||
|
+extern void Kit_GraphFree( Kit_Graph_t * );
|
||
|
+extern Kit_Graph_t * Kit_SopFactor( Vec_Int_t *, int, int, Vec_Int_t * );
|
||
|
+extern void Kit_TruthCofactor0( unsigned *, int, int );
|
||
|
+extern void Kit_TruthCofactor1( unsigned *, int, int );
|
||
|
+extern int Kit_TruthIsop( unsigned *, int, Vec_Int_t *, int );
|
||
|
+extern void Kit_TruthShrink( unsigned *, unsigned *, int, int, unsigned, int );
|
||
|
+extern void Kit_TruthStretch( unsigned *, unsigned *, int, int, unsigned, int );
|
||
|
+extern Kit_Graph_t * Kit_TruthToGraph( unsigned *, int, Vec_Int_t * );
|
||
|
+extern int Kit_TruthVarInSupport( unsigned *, int, int );
|
||
|
+
|
||
|
#if 0
|
||
|
|
||
|
/*=== kitBdd.c ==========================================================*/
|
||
|
--- ./src/extlib-abc/aig/kit/kitSop.c.orig 2010-03-06 06:48:41.000000000 -0700
|
||
|
+++ ./src/extlib-abc/aig/kit/kitSop.c 2011-12-13 13:08:15.913474649 -0700
|
||
|
@@ -174,7 +174,7 @@ void Kit_SopDivideByCube( Kit_Sop_t * cS
|
||
|
***********************************************************************/
|
||
|
void Kit_SopDivideInternal( Kit_Sop_t * cSop, Kit_Sop_t * cDiv, Kit_Sop_t * vQuo, Kit_Sop_t * vRem, Vec_Int_t * vMemory )
|
||
|
{
|
||
|
- unsigned uCube, uDiv, uCube2, uDiv2, uQuo;
|
||
|
+ unsigned uCube, uDiv, uCube2 = 0, uDiv2, uQuo;
|
||
|
int i, i2, k, k2, nCubesRem;
|
||
|
assert( Kit_SopCubeNum(cSop) >= Kit_SopCubeNum(cDiv) );
|
||
|
// consider special case
|
||
|
--- ./src/extlib-abc/aig/kit/kitAig.c.orig 2010-03-06 06:48:41.000000000 -0700
|
||
|
+++ ./src/extlib-abc/aig/kit/kitAig.c 2011-12-13 13:08:15.913474649 -0700
|
||
|
@@ -54,8 +54,8 @@ Aig_Obj_t * Kit_GraphToAigInternal( Aig_
|
||
|
// build the AIG nodes corresponding to the AND gates of the graph
|
||
|
Kit_GraphForEachNode( pGraph, pNode, i )
|
||
|
{
|
||
|
- pAnd0 = Aig_NotCond( Kit_GraphNode(pGraph, pNode->eEdge0.Node)->pFunc, pNode->eEdge0.fCompl );
|
||
|
- pAnd1 = Aig_NotCond( Kit_GraphNode(pGraph, pNode->eEdge1.Node)->pFunc, pNode->eEdge1.fCompl );
|
||
|
+ pAnd0 = Aig_NotCond( Kit_GraphNode(pGraph, pNode->eEdge0.edgeBits.Node)->pFunc, pNode->eEdge0.edgeBits.fCompl );
|
||
|
+ pAnd1 = Aig_NotCond( Kit_GraphNode(pGraph, pNode->eEdge1.edgeBits.Node)->pFunc, pNode->eEdge1.edgeBits.fCompl );
|
||
|
pNode->pFunc = Aig_And( pMan, pAnd0, pAnd1 );
|
||
|
}
|
||
|
// complement the result if necessary
|
||
|
--- ./src/extlib-abc/aig/kit/kitGraph.c.orig 2010-03-06 06:48:41.000000000 -0700
|
||
|
+++ ./src/extlib-abc/aig/kit/kitGraph.c 2011-12-13 13:08:15.914474647 -0700
|
||
|
@@ -69,7 +69,7 @@ Kit_Graph_t * Kit_GraphCreateConst0()
|
||
|
pGraph = ALLOC( Kit_Graph_t, 1 );
|
||
|
memset( pGraph, 0, sizeof(Kit_Graph_t) );
|
||
|
pGraph->fConst = 1;
|
||
|
- pGraph->eRoot.fCompl = 1;
|
||
|
+ pGraph->eRoot.edgeBits.fCompl = 1;
|
||
|
return pGraph;
|
||
|
}
|
||
|
|
||
|
@@ -109,8 +109,8 @@ Kit_Graph_t * Kit_GraphCreateLeaf( int i
|
||
|
Kit_Graph_t * pGraph;
|
||
|
assert( 0 <= iLeaf && iLeaf < nLeaves );
|
||
|
pGraph = Kit_GraphCreate( nLeaves );
|
||
|
- pGraph->eRoot.Node = iLeaf;
|
||
|
- pGraph->eRoot.fCompl = fCompl;
|
||
|
+ pGraph->eRoot.edgeBits.Node = iLeaf;
|
||
|
+ pGraph->eRoot.edgeBits.fCompl = fCompl;
|
||
|
return pGraph;
|
||
|
}
|
||
|
|
||
|
@@ -174,8 +174,8 @@ Kit_Edge_t Kit_GraphAddNodeAnd( Kit_Grap
|
||
|
// set the inputs and other info
|
||
|
pNode->eEdge0 = eEdge0;
|
||
|
pNode->eEdge1 = eEdge1;
|
||
|
- pNode->fCompl0 = eEdge0.fCompl;
|
||
|
- pNode->fCompl1 = eEdge1.fCompl;
|
||
|
+ pNode->fCompl0 = eEdge0.edgeBits.fCompl;
|
||
|
+ pNode->fCompl1 = eEdge1.edgeBits.fCompl;
|
||
|
return Kit_EdgeCreate( pGraph->nSize - 1, 0 );
|
||
|
}
|
||
|
|
||
|
@@ -198,12 +198,12 @@ Kit_Edge_t Kit_GraphAddNodeOr( Kit_Graph
|
||
|
// set the inputs and other info
|
||
|
pNode->eEdge0 = eEdge0;
|
||
|
pNode->eEdge1 = eEdge1;
|
||
|
- pNode->fCompl0 = eEdge0.fCompl;
|
||
|
- pNode->fCompl1 = eEdge1.fCompl;
|
||
|
+ pNode->fCompl0 = eEdge0.edgeBits.fCompl;
|
||
|
+ pNode->fCompl1 = eEdge1.edgeBits.fCompl;
|
||
|
// make adjustments for the OR gate
|
||
|
pNode->fNodeOr = 1;
|
||
|
- pNode->eEdge0.fCompl = !pNode->eEdge0.fCompl;
|
||
|
- pNode->eEdge1.fCompl = !pNode->eEdge1.fCompl;
|
||
|
+ pNode->eEdge0.edgeBits.fCompl = !pNode->eEdge0.edgeBits.fCompl;
|
||
|
+ pNode->eEdge1.edgeBits.fCompl = !pNode->eEdge1.edgeBits.fCompl;
|
||
|
return Kit_EdgeCreate( pGraph->nSize - 1, 1 );
|
||
|
}
|
||
|
|
||
|
@@ -224,11 +224,11 @@ Kit_Edge_t Kit_GraphAddNodeXor( Kit_Grap
|
||
|
if ( Type == 0 )
|
||
|
{
|
||
|
// derive the first AND
|
||
|
- eEdge0.fCompl ^= 1;
|
||
|
+ eEdge0.edgeBits.fCompl ^= 1;
|
||
|
eNode0 = Kit_GraphAddNodeAnd( pGraph, eEdge0, eEdge1 );
|
||
|
- eEdge0.fCompl ^= 1;
|
||
|
+ eEdge0.edgeBits.fCompl ^= 1;
|
||
|
// derive the second AND
|
||
|
- eEdge1.fCompl ^= 1;
|
||
|
+ eEdge1.edgeBits.fCompl ^= 1;
|
||
|
eNode1 = Kit_GraphAddNodeAnd( pGraph, eEdge0, eEdge1 );
|
||
|
// derive the final OR
|
||
|
eNode = Kit_GraphAddNodeOr( pGraph, eNode0, eNode1 );
|
||
|
@@ -238,12 +238,12 @@ Kit_Edge_t Kit_GraphAddNodeXor( Kit_Grap
|
||
|
// derive the first AND
|
||
|
eNode0 = Kit_GraphAddNodeAnd( pGraph, eEdge0, eEdge1 );
|
||
|
// derive the second AND
|
||
|
- eEdge0.fCompl ^= 1;
|
||
|
- eEdge1.fCompl ^= 1;
|
||
|
+ eEdge0.edgeBits.fCompl ^= 1;
|
||
|
+ eEdge1.edgeBits.fCompl ^= 1;
|
||
|
eNode1 = Kit_GraphAddNodeAnd( pGraph, eEdge0, eEdge1 );
|
||
|
// derive the final OR
|
||
|
eNode = Kit_GraphAddNodeOr( pGraph, eNode0, eNode1 );
|
||
|
- eNode.fCompl ^= 1;
|
||
|
+ eNode.edgeBits.fCompl ^= 1;
|
||
|
}
|
||
|
return eNode;
|
||
|
}
|
||
|
@@ -267,7 +267,7 @@ Kit_Edge_t Kit_GraphAddNodeMux( Kit_Grap
|
||
|
// derive the first AND
|
||
|
eNode0 = Kit_GraphAddNodeAnd( pGraph, eEdgeC, eEdgeT );
|
||
|
// derive the second AND
|
||
|
- eEdgeC.fCompl ^= 1;
|
||
|
+ eEdgeC.edgeBits.fCompl ^= 1;
|
||
|
eNode1 = Kit_GraphAddNodeAnd( pGraph, eEdgeC, eEdgeE );
|
||
|
// derive the final OR
|
||
|
eNode = Kit_GraphAddNodeOr( pGraph, eNode0, eNode1 );
|
||
|
@@ -275,16 +275,16 @@ Kit_Edge_t Kit_GraphAddNodeMux( Kit_Grap
|
||
|
else
|
||
|
{
|
||
|
// complement the arguments
|
||
|
- eEdgeT.fCompl ^= 1;
|
||
|
- eEdgeE.fCompl ^= 1;
|
||
|
+ eEdgeT.edgeBits.fCompl ^= 1;
|
||
|
+ eEdgeE.edgeBits.fCompl ^= 1;
|
||
|
// derive the first AND
|
||
|
eNode0 = Kit_GraphAddNodeAnd( pGraph, eEdgeC, eEdgeT );
|
||
|
// derive the second AND
|
||
|
- eEdgeC.fCompl ^= 1;
|
||
|
+ eEdgeC.edgeBits.fCompl ^= 1;
|
||
|
eNode1 = Kit_GraphAddNodeAnd( pGraph, eEdgeC, eEdgeE );
|
||
|
// derive the final OR
|
||
|
eNode = Kit_GraphAddNodeOr( pGraph, eNode0, eNode1 );
|
||
|
- eNode.fCompl ^= 1;
|
||
|
+ eNode.edgeBits.fCompl ^= 1;
|
||
|
}
|
||
|
return eNode;
|
||
|
}
|
||
|
@@ -326,10 +326,10 @@ unsigned Kit_GraphToTruth( Kit_Graph_t *
|
||
|
// compute the function for each internal node
|
||
|
Kit_GraphForEachNode( pGraph, pNode, i )
|
||
|
{
|
||
|
- uTruth0 = (unsigned)(long)Kit_GraphNode(pGraph, pNode->eEdge0.Node)->pFunc;
|
||
|
- uTruth1 = (unsigned)(long)Kit_GraphNode(pGraph, pNode->eEdge1.Node)->pFunc;
|
||
|
- uTruth0 = pNode->eEdge0.fCompl? ~uTruth0 : uTruth0;
|
||
|
- uTruth1 = pNode->eEdge1.fCompl? ~uTruth1 : uTruth1;
|
||
|
+ uTruth0 = (unsigned)(long)Kit_GraphNode(pGraph, pNode->eEdge0.edgeBits.Node)->pFunc;
|
||
|
+ uTruth1 = (unsigned)(long)Kit_GraphNode(pGraph, pNode->eEdge1.edgeBits.Node)->pFunc;
|
||
|
+ uTruth0 = pNode->eEdge0.edgeBits.fCompl? ~uTruth0 : uTruth0;
|
||
|
+ uTruth1 = pNode->eEdge1.edgeBits.fCompl? ~uTruth1 : uTruth1;
|
||
|
uTruth = uTruth0 & uTruth1;
|
||
|
pNode->pFunc = (void *)(long)uTruth;
|
||
|
}
|
||
|
--- ./src/extlib-abc/aig/aig/aigTable.c.orig 2010-03-06 06:48:41.000000000 -0700
|
||
|
+++ ./src/extlib-abc/aig/aig/aigTable.c 2011-12-13 13:08:15.914474647 -0700
|
||
|
@@ -74,8 +74,8 @@ void Aig_TableResize( Aig_Man_t * p )
|
||
|
{
|
||
|
Aig_Obj_t * pEntry, * pNext;
|
||
|
Aig_Obj_t ** pTableOld, ** ppPlace;
|
||
|
- int nTableSizeOld, Counter, i, clk;
|
||
|
-clk = clock();
|
||
|
+ int nTableSizeOld, Counter, i;
|
||
|
+
|
||
|
// save the old table
|
||
|
pTableOld = p->pTable;
|
||
|
nTableSizeOld = p->nTableSize;
|
||
|
--- ./src/extlib-abc/aig/aig/aigShow.c.orig 2010-03-06 06:48:41.000000000 -0700
|
||
|
+++ ./src/extlib-abc/aig/aig/aigShow.c 2011-12-13 13:08:15.914474647 -0700
|
||
|
@@ -329,7 +329,7 @@ void Aig_WriteDotAig( Aig_Man_t * pMan,
|
||
|
void Aig_ManShow( Aig_Man_t * pMan, int fHaig, Vec_Ptr_t * vBold )
|
||
|
{
|
||
|
extern void Abc_ShowFile( char * FileNameDot );
|
||
|
- static Counter = 0;
|
||
|
+ static int Counter = 0;
|
||
|
char FileNameDot[200];
|
||
|
FILE * pFile;
|
||
|
// create the file name
|
||
|
--- ./src/extlib-abc/aig/aig/aigObj.c.orig 2010-03-06 06:48:41.000000000 -0700
|
||
|
+++ ./src/extlib-abc/aig/aig/aigObj.c 2011-12-13 13:08:15.915474646 -0700
|
||
|
@@ -299,8 +299,10 @@ void Aig_NodeFixBufferFanins( Aig_Man_t
|
||
|
pResult = Aig_Oper( p, pFanReal0, pFanReal1, Aig_ObjType(pObj) );
|
||
|
// else if ( Aig_ObjIsLatch(pObj) )
|
||
|
// pResult = Aig_Latch( p, pFanReal0, Aig_ObjInit(pObj) );
|
||
|
- else
|
||
|
+ else {
|
||
|
assert( 0 );
|
||
|
+ pResult = NULL;
|
||
|
+ }
|
||
|
// replace the node with buffer by the node without buffer
|
||
|
Aig_ObjReplace( p, pObj, pResult, fNodesOnly, fUpdateLevel );
|
||
|
}
|
||
|
--- ./src/extlib-abc/aig/cnf/cnfWrite.c.orig 2011-01-07 21:23:57.000000000 -0700
|
||
|
+++ ./src/extlib-abc/aig/cnf/cnfWrite.c 2011-12-13 13:08:15.915474646 -0700
|
||
|
@@ -352,7 +352,6 @@ Cnf_Dat_t * Cnf_DeriveSimple_Additional(
|
||
|
int Number = old->nVars+1;
|
||
|
|
||
|
// assign variables to the PIs
|
||
|
- int newPI = 0;
|
||
|
Aig_ManForEachPi( p, pObj, i )
|
||
|
if (pCnf->pVarNums[pObj->Id] == -1) // new!
|
||
|
pCnf->pVarNums[pObj->Id] = Number++;
|
||
|
--- ./src/extlib-abc/aig/dar/darPrec.c.orig 2010-03-06 06:48:41.000000000 -0700
|
||
|
+++ ./src/extlib-abc/aig/dar/darPrec.c 2011-12-13 13:08:15.915474646 -0700
|
||
|
@@ -258,11 +258,9 @@ unsigned Dar_TruthPolarize( unsigned uTr
|
||
|
0xFF00FF00, // 1111 1111 0000 0000 1111 1111 0000 0000
|
||
|
0xFFFF0000 // 1111 1111 1111 1111 0000 0000 0000 0000
|
||
|
};
|
||
|
- unsigned uTruthRes, uCof0, uCof1;
|
||
|
- int nMints, Shift, v;
|
||
|
+ unsigned uCof0, uCof1;
|
||
|
+ int Shift, v;
|
||
|
assert( nVars < 6 );
|
||
|
- nMints = (1 << nVars);
|
||
|
- uTruthRes = uTruth;
|
||
|
for ( v = 0; v < nVars; v++ )
|
||
|
if ( Polarity & (1 << v) )
|
||
|
{
|
||
|
--- ./src/extlib-abc/aig/dar/darRefact.c.orig 2010-03-06 06:48:41.000000000 -0700
|
||
|
+++ ./src/extlib-abc/aig/dar/darRefact.c 2011-12-13 13:08:15.916474646 -0700
|
||
|
@@ -213,7 +213,7 @@ int Dar_RefactTryGraph( Aig_Man_t * pAig
|
||
|
{
|
||
|
Kit_Node_t * pNode, * pNode0, * pNode1;
|
||
|
Aig_Obj_t * pAnd, * pAnd0, * pAnd1;
|
||
|
- int i, Counter, LevelNew, LevelOld;
|
||
|
+ int i, Counter, LevelNew;
|
||
|
// check for constant function or a literal
|
||
|
if ( Kit_GraphIsConst(pGraph) || Kit_GraphIsVar(pGraph) )
|
||
|
return 0;
|
||
|
@@ -230,16 +230,16 @@ int Dar_RefactTryGraph( Aig_Man_t * pAig
|
||
|
Kit_GraphForEachNode( pGraph, pNode, i )
|
||
|
{
|
||
|
// get the children of this node
|
||
|
- pNode0 = Kit_GraphNode( pGraph, pNode->eEdge0.Node );
|
||
|
- pNode1 = Kit_GraphNode( pGraph, pNode->eEdge1.Node );
|
||
|
+ pNode0 = Kit_GraphNode( pGraph, pNode->eEdge0.edgeBits.Node );
|
||
|
+ pNode1 = Kit_GraphNode( pGraph, pNode->eEdge1.edgeBits.Node );
|
||
|
// get the AIG nodes corresponding to the children
|
||
|
pAnd0 = pNode0->pFunc;
|
||
|
pAnd1 = pNode1->pFunc;
|
||
|
if ( pAnd0 && pAnd1 )
|
||
|
{
|
||
|
// if they are both present, find the resulting node
|
||
|
- pAnd0 = Aig_NotCond( pAnd0, pNode->eEdge0.fCompl );
|
||
|
- pAnd1 = Aig_NotCond( pAnd1, pNode->eEdge1.fCompl );
|
||
|
+ pAnd0 = Aig_NotCond( pAnd0, pNode->eEdge0.edgeBits.fCompl );
|
||
|
+ pAnd1 = Aig_NotCond( pAnd1, pNode->eEdge1.edgeBits.fCompl );
|
||
|
pAnd = Aig_TableLookupTwo( pAig, pAnd0, pAnd1 );
|
||
|
// return -1 if the node is the same as the original root
|
||
|
if ( Aig_Regular(pAnd) == pRoot )
|
||
|
@@ -263,8 +263,6 @@ 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;
|
||
|
-// assert( LevelNew == LevelOld );
|
||
|
}
|
||
|
if ( LevelNew > LevelMax )
|
||
|
return -1;
|
||
|
@@ -312,8 +310,8 @@ Aig_Obj_t * Dar_RefactBuildGraph( Aig_Ma
|
||
|
//printf( "Building (current number %d):\n", Aig_ManObjNumMax(pAig) );
|
||
|
Kit_GraphForEachNode( pGraph, pNode, i )
|
||
|
{
|
||
|
- pAnd0 = Aig_NotCond( Kit_GraphNode(pGraph, pNode->eEdge0.Node)->pFunc, pNode->eEdge0.fCompl );
|
||
|
- pAnd1 = Aig_NotCond( Kit_GraphNode(pGraph, pNode->eEdge1.Node)->pFunc, pNode->eEdge1.fCompl );
|
||
|
+ pAnd0 = Aig_NotCond( Kit_GraphNode(pGraph, pNode->eEdge0.edgeBits.Node)->pFunc, pNode->eEdge0.edgeBits.fCompl );
|
||
|
+ pAnd1 = Aig_NotCond( Kit_GraphNode(pGraph, pNode->eEdge1.edgeBits.Node)->pFunc, pNode->eEdge1.edgeBits.fCompl );
|
||
|
pNode->pFunc = Aig_And( pAig, pAnd0, pAnd1 );
|
||
|
/*
|
||
|
printf( "Checking " );
|
||
|
--- ./src/AST/ASTmisc.cpp.orig 2011-09-12 08:58:35.000000000 -0600
|
||
|
+++ ./src/AST/ASTmisc.cpp 2011-12-13 13:08:15.916474646 -0700
|
||
|
@@ -76,7 +76,7 @@ bool containsArrayOps(const ASTNode& n,
|
||
|
|
||
|
visited.insert(n.GetNodeNum());
|
||
|
|
||
|
- for (int i =0; i < n.Degree();i++)
|
||
|
+ for (size_t i =0; i < n.Degree();i++)
|
||
|
if (containsArrayOps(n[i],visited))
|
||
|
return true;
|
||
|
|
||
|
--- ./src/AST/ArrayTransformer.cpp.orig 2011-09-12 08:58:35.000000000 -0600
|
||
|
+++ ./src/AST/ArrayTransformer.cpp 2011-12-13 13:08:15.916474646 -0700
|
||
|
@@ -61,7 +61,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/NodeFactory/SimplifyingNodeFactory.cpp.orig 2011-11-30 06:57:18.000000000 -0700
|
||
|
+++ ./src/AST/NodeFactory/SimplifyingNodeFactory.cpp 2011-12-13 13:08:15.917474646 -0700
|
||
|
@@ -369,7 +369,7 @@ ASTNode SimplifyingNodeFactory::CreateSi
|
||
|
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
|
||
|
@@ -386,7 +386,7 @@ ASTNode SimplifyingNodeFactory::CreateSi
|
||
|
if ((k1 == BEEV::BVUMINUS && k2 == BEEV::BVCONST) || (k1 == BEEV::BVNEG && k2 == BEEV::BVCONST))
|
||
|
return NodeFactory::CreateNode(BEEV::EQ, in1[0], NodeFactory::CreateTerm(k1,width, in2 ));
|
||
|
|
||
|
- if (k2 == BEEV::BVUMINUS && k1 == BEEV::BVCONST || (k2 == BEEV::BVNEG && k1 == BEEV::BVCONST))
|
||
|
+ if ((k2 == BEEV::BVUMINUS && k1 == BEEV::BVCONST) || (k2 == BEEV::BVNEG && k1 == BEEV::BVCONST))
|
||
|
return NodeFactory::CreateNode(BEEV::EQ, in2[0], NodeFactory::CreateTerm(k2,width, in1 ));
|
||
|
|
||
|
if ((k1 == BEEV::BVNEG && in1[0] == in2) || (k2 == BEEV::BVNEG && in2[0] == in1))
|
||
|
@@ -449,13 +449,13 @@ ASTNode SimplifyingNodeFactory::CreateSi
|
||
|
{
|
||
|
int match1 =-1, match2=-1;
|
||
|
|
||
|
- for (int i =0; i < c1.size();i++)
|
||
|
- for (int j =0; j < c2.size();j++)
|
||
|
+ for (size_t i =0; i < c1.size();i++)
|
||
|
+ for (size_t j =0; j < c2.size();j++)
|
||
|
{
|
||
|
if (c1[i] == c2[j])
|
||
|
{
|
||
|
- match1 = i;
|
||
|
- match2 = j;
|
||
|
+ match1 = (int)i;
|
||
|
+ match2 = (int)j;
|
||
|
}
|
||
|
}
|
||
|
|
||
|
@@ -510,7 +510,7 @@ ASTNode SimplifyingNodeFactory::CreateSi
|
||
|
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 i = original_width-1; i < new_width;i++)
|
||
|
if (CONSTANTBV::BitVector_bit_test(in1.GetBVConst(),i))
|
||
|
foundOne=true;
|
||
|
else
|
||
|
@@ -1044,7 +1044,7 @@ ASTNode SimplifyingNodeFactory::CreateTe
|
||
|
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)
|
||
|
{
|
||
|
@@ -1063,7 +1063,7 @@ ASTNode SimplifyingNodeFactory::CreateTe
|
||
|
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]);
|
||
|
@@ -1103,13 +1103,14 @@ ASTNode SimplifyingNodeFactory::CreateTe
|
||
|
int end=-1;
|
||
|
BEEV::CBV c = c0.GetBVConst();
|
||
|
bool bad= false;
|
||
|
- for (int i =0; i < width; i++)
|
||
|
+ for (unsigned 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)
|
||
|
@@ -1129,7 +1130,7 @@ ASTNode SimplifyingNodeFactory::CreateTe
|
||
|
ASTNode z = bm.CreateZeroConst(start);
|
||
|
result = NodeFactory::CreateTerm(BEEV::BVCONCAT, end+1, result,z);
|
||
|
}
|
||
|
- if (end < width-1)
|
||
|
+ if (end < (int)width-1)
|
||
|
{
|
||
|
ASTNode z = bm.CreateZeroConst(width-end-1);
|
||
|
result = NodeFactory::CreateTerm(BEEV::BVCONCAT, width, z,result);
|
||
|
@@ -1190,7 +1191,6 @@ ASTNode SimplifyingNodeFactory::CreateTe
|
||
|
const unsigned outerHigh = children[1].GetUnsignedConst();
|
||
|
|
||
|
const unsigned innerLow = children[0][2].GetUnsignedConst();
|
||
|
- const unsigned innerHigh = children[0][1].GetUnsignedConst();
|
||
|
result = NodeFactory::CreateTerm(BEEV::BVEXTRACT, width, children[0][0], bm.CreateBVConst(32, outerHigh
|
||
|
+ innerLow), bm.CreateBVConst(32, outerLow + innerLow));
|
||
|
}
|
||
|
--- ./src/STPManager/STP.cpp.orig 2011-11-27 22:33:34.000000000 -0700
|
||
|
+++ ./src/STPManager/STP.cpp 2011-12-13 13:08:15.917474646 -0700
|
||
|
@@ -61,8 +61,8 @@ namespace BEEV {
|
||
|
newS = new MinisatCore<Minisat::Solver>();
|
||
|
else if (bm->UserFlags.solver_to_use == UserDefinedFlags::MINISAT_PROPAGATORS)
|
||
|
newS = new MinisatCore_prop<Minisat::Solver_prop>();
|
||
|
-
|
||
|
-
|
||
|
+ else
|
||
|
+ newS = NULL;
|
||
|
|
||
|
SATSolver& NewSolver = *newS;
|
||
|
|
||
|
--- ./src/parser/ParserInterface.h.orig 2011-07-09 00:56:51.000000000 -0600
|
||
|
+++ ./src/parser/ParserInterface.h 2011-12-13 13:08:15.918474645 -0700
|
||
|
@@ -214,7 +214,7 @@ public:
|
||
|
assert(symbols.size() == cache.size());
|
||
|
cache.erase(cache.end()-1);
|
||
|
ASTVec & current = symbols.back();
|
||
|
- for (int i=0; i < current.size() ;i++)
|
||
|
+ for (size_t i=0; i < current.size() ;i++)
|
||
|
letMgr._parser_symbol_table.erase(current[i]);
|
||
|
symbols.erase(symbols.end()-1);
|
||
|
}
|
||
|
@@ -234,7 +234,7 @@ public:
|
||
|
|
||
|
void printStatus()
|
||
|
{
|
||
|
- for (int i=0; i < cache.size();i++)
|
||
|
+ for (size_t i=0; i < cache.size();i++)
|
||
|
{
|
||
|
cache[i].print();
|
||
|
}
|
||
|
@@ -271,7 +271,7 @@ public:
|
||
|
|
||
|
// Loop through the set of assertions converting them to single nodes..
|
||
|
ASTVec v;
|
||
|
- for (int i = 0; i < assertionsSMT2.size(); i++)
|
||
|
+ for (size_t i = 0; i < assertionsSMT2.size(); i++)
|
||
|
{
|
||
|
if (assertionsSMT2[i].size() == 1)
|
||
|
{}
|
||
|
@@ -310,7 +310,7 @@ public:
|
||
|
// It's satisfiable, so everything beneath it is satisfiable too.
|
||
|
if (last_result ==SOLVER_SATISFIABLE)
|
||
|
{
|
||
|
- for (int i=0; i < cache.size(); i++)
|
||
|
+ for (size_t i=0; i < cache.size(); i++)
|
||
|
{
|
||
|
assert(cache[i].result != SOLVER_UNSATISFIABLE);
|
||
|
cache[i].result = SOLVER_SATISFIABLE;
|