Update to recent git snapshot.
This commit is contained in:
parent
5a3a024fae
commit
75cefd8104
|
@ -1 +1 @@
|
|||
/stp-stp-fe766c9.tar.gz
|
||||
/stp-stp-f8a392d.tar.gz
|
||||
|
|
2
sources
2
sources
|
@ -1 +1 @@
|
|||
3104c3fcb6e89da91f766e9b61dd87d9 stp-stp-fe766c9.tar.gz
|
||||
2ec158d56d2189d07aa09e3e05c88ca2 stp-stp-f8a392d.tar.gz
|
||||
|
|
|
@ -1,81 +1,5 @@
|
|||
diff --git a/src/AST/ASTmisc.cpp b/src/AST/ASTmisc.cpp
|
||||
index 0e028c4..7cfa7a7 100644
|
||||
--- a/src/AST/ASTmisc.cpp
|
||||
+++ b/src/AST/ASTmisc.cpp
|
||||
@@ -154,7 +154,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);
|
||||
}
|
||||
|
||||
diff --git a/src/AST/NodeFactory/SimplifyingNodeFactory.cpp b/src/AST/NodeFactory/SimplifyingNodeFactory.cpp
|
||||
index 9c18b69..4fc3320 100644
|
||||
--- a/src/AST/NodeFactory/SimplifyingNodeFactory.cpp
|
||||
+++ b/src/AST/NodeFactory/SimplifyingNodeFactory.cpp
|
||||
@@ -389,7 +389,7 @@ SimplifyingNodeFactory::CreateSimpleEQ(const ASTVec& children)
|
||||
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
|
||||
@@ -526,7 +526,7 @@ SimplifyingNodeFactory::CreateSimpleEQ(const ASTVec& children)
|
||||
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
|
||||
@@ -1176,10 +1176,12 @@ SimplifyingNodeFactory::CreateTerm(Kind kind, unsigned int width, const ASTVec &
|
||||
for (size_t i = 0; i < width; i++)
|
||||
{
|
||||
if (CONSTANTBV::BitVector_bit_test(c, i))
|
||||
- if (start == -1)
|
||||
- start = i; // first one bit.
|
||||
- else if (end != -1)
|
||||
- bad = true;
|
||||
+ {
|
||||
+ 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)
|
||||
@@ -1200,7 +1202,7 @@ SimplifyingNodeFactory::CreateTerm(Kind kind, unsigned int width, const ASTVec &
|
||||
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);
|
||||
diff --git a/src/STPManager/STP.cpp b/src/STPManager/STP.cpp
|
||||
index 395e737..ff5cc3d 100644
|
||||
--- a/src/STPManager/STP.cpp
|
||||
+++ b/src/STPManager/STP.cpp
|
||||
@@ -576,7 +576,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;
|
||||
diff --git a/src/absrefine_counterexample/AbstractionRefinement.cpp b/src/absrefine_counterexample/AbstractionRefinement.cpp
|
||||
index 4ce3767..b5c061f 100644
|
||||
--- a/src/absrefine_counterexample/AbstractionRefinement.cpp
|
||||
+++ b/src/absrefine_counterexample/AbstractionRefinement.cpp
|
||||
--- ./src/absrefine_counterexample/AbstractionRefinement.cpp.orig 2014-04-02 11:47:21.000000000 -0600
|
||||
+++ ./src/absrefine_counterexample/AbstractionRefinement.cpp 2014-04-29 14:34:45.618479266 -0600
|
||||
@@ -119,7 +119,7 @@ namespace BEEV
|
||||
}
|
||||
return result;
|
||||
|
@ -94,10 +18,8 @@ index 4ce3767..b5c061f 100644
|
|||
{
|
||||
applyAxiomToSAT(SatSolver, toBe[i], satVar);
|
||||
}
|
||||
diff --git a/src/absrefine_counterexample/CounterExample.cpp b/src/absrefine_counterexample/CounterExample.cpp
|
||||
index 0f52bce..4029a53 100644
|
||||
--- a/src/absrefine_counterexample/CounterExample.cpp
|
||||
+++ b/src/absrefine_counterexample/CounterExample.cpp
|
||||
--- ./src/absrefine_counterexample/CounterExample.cpp.orig 2014-04-02 11:47:21.000000000 -0600
|
||||
+++ ./src/absrefine_counterexample/CounterExample.cpp 2014-04-29 14:34:45.618479266 -0600
|
||||
@@ -48,7 +48,7 @@ namespace BEEV
|
||||
assert(symbol.GetKind() == SYMBOL);
|
||||
vector<bool> bitVector_array(symbolWidth,false);
|
||||
|
@ -116,10 +38,65 @@ index 0f52bce..4029a53 100644
|
|||
{
|
||||
if (v[i] == ~((unsigned)0)) // nb. special value.
|
||||
continue;
|
||||
diff --git a/src/c_interface/c_interface.cpp b/src/c_interface/c_interface.cpp
|
||||
index dd761d3..2876211 100644
|
||||
--- a/src/c_interface/c_interface.cpp
|
||||
+++ b/src/c_interface/c_interface.cpp
|
||||
--- ./src/AST/ASTmisc.cpp.orig 2014-04-02 11:47:21.000000000 -0600
|
||||
+++ ./src/AST/ASTmisc.cpp 2014-04-29 14:34:45.617479267 -0600
|
||||
@@ -154,7 +154,7 @@ namespace BEEV
|
||||
|
||||
visited.insert(n.GetNodeNum());
|
||||
|
||||
- for (int i = 0; i < n.Degree(); i++)
|
||||
+ for (size_t i = 0; i < n.Degree(); i++)
|
||||
numberOfReadsLessThan(n[i], visited, soFar,limit);
|
||||
}
|
||||
|
||||
--- ./src/AST/NodeFactory/SimplifyingNodeFactory.cpp.orig 2014-04-02 11:47:21.000000000 -0600
|
||||
+++ ./src/AST/NodeFactory/SimplifyingNodeFactory.cpp 2014-04-29 14:34:45.618479266 -0600
|
||||
@@ -389,7 +389,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
|
||||
@@ -526,7 +526,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
|
||||
@@ -1188,10 +1188,12 @@ SimplifyingNodeFactory::CreateTerm(Kind
|
||||
for (size_t i = 0; i < width; i++)
|
||||
{
|
||||
if (CONSTANTBV::BitVector_bit_test(c, i))
|
||||
- if (start == -1)
|
||||
- start = i; // first one bit.
|
||||
- else if (end != -1)
|
||||
- bad = true;
|
||||
+ {
|
||||
+ 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)
|
||||
@@ -1212,7 +1214,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);
|
||||
--- ./src/c_interface/c_interface.cpp.orig 2014-04-02 11:47:21.000000000 -0600
|
||||
+++ ./src/c_interface/c_interface.cpp 2014-04-29 14:34:45.619479265 -0600
|
||||
@@ -989,7 +989,7 @@ Expr vc_bvConstExprFromInt(VC vc,
|
||||
bmstar b = (bmstar)(((stpstar)vc)->bm);
|
||||
|
||||
|
@ -129,10 +106,8 @@ index dd761d3..2876211 100644
|
|||
//printf("%ull", max_n_bits);
|
||||
if(v > max_n_bits) {
|
||||
printf("CInterface: vc_bvConstExprFromInt: "\
|
||||
diff --git a/src/cpp_interface/cpp_interface.cpp b/src/cpp_interface/cpp_interface.cpp
|
||||
index 4da3685..3ce0c3e 100644
|
||||
--- a/src/cpp_interface/cpp_interface.cpp
|
||||
+++ b/src/cpp_interface/cpp_interface.cpp
|
||||
--- ./src/cpp_interface/cpp_interface.cpp.orig 2014-04-02 11:47:21.000000000 -0600
|
||||
+++ ./src/cpp_interface/cpp_interface.cpp 2014-04-29 14:34:45.619479265 -0600
|
||||
@@ -47,7 +47,7 @@ namespace BEEV
|
||||
// It's satisfiable, so everything beneath it is satisfiable too.
|
||||
if (last_result == SOLVER_SATISFIABLE)
|
||||
|
@ -142,11 +117,9 @@ index 4da3685..3ce0c3e 100644
|
|||
{
|
||||
assert(cache[i].result != SOLVER_UNSATISFIABLE);
|
||||
cache[i].result = SOLVER_SATISFIABLE;
|
||||
diff --git a/src/extlib-abc/aig/aig/aigShow.c b/src/extlib-abc/aig/aig/aigShow.c
|
||||
index ae8fa8b..a88f493 100644
|
||||
--- a/src/extlib-abc/aig/aig/aigShow.c
|
||||
+++ b/src/extlib-abc/aig/aig/aigShow.c
|
||||
@@ -329,7 +329,7 @@ void Aig_WriteDotAig( Aig_Man_t * pMan, char * pFileName, int fHaig, Vec_Ptr_t *
|
||||
--- ./src/extlib-abc/aig/aig/aigShow.c.orig 2014-04-02 11:47:21.000000000 -0600
|
||||
+++ ./src/extlib-abc/aig/aig/aigShow.c 2014-04-29 14:34:45.619479265 -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 );
|
||||
|
@ -155,11 +128,9 @@ index ae8fa8b..a88f493 100644
|
|||
char FileNameDot[200];
|
||||
FILE * pFile;
|
||||
// create the file name
|
||||
diff --git a/src/extlib-abc/aig/dar/darRefact.c b/src/extlib-abc/aig/dar/darRefact.c
|
||||
index d744b4f..83fb3b0 100644
|
||||
--- a/src/extlib-abc/aig/dar/darRefact.c
|
||||
+++ b/src/extlib-abc/aig/dar/darRefact.c
|
||||
@@ -230,16 +230,16 @@ int Dar_RefactTryGraph( Aig_Man_t * pAig, Aig_Obj_t * pRoot, Vec_Ptr_t * vCut, K
|
||||
--- ./src/extlib-abc/aig/dar/darRefact.c.orig 2014-04-02 11:47:21.000000000 -0600
|
||||
+++ ./src/extlib-abc/aig/dar/darRefact.c 2014-04-29 14:34:45.619479265 -0600
|
||||
@@ -230,16 +230,16 @@ int Dar_RefactTryGraph( Aig_Man_t * pAig
|
||||
Kit_GraphForEachNode( pGraph, pNode, i )
|
||||
{
|
||||
// get the children of this node
|
||||
|
@ -180,7 +151,7 @@ index d744b4f..83fb3b0 100644
|
|||
pAnd = Aig_TableLookupTwo( pAig, pAnd0, pAnd1 );
|
||||
// return -1 if the node is the same as the original root
|
||||
if ( Aig_Regular(pAnd) == pRoot )
|
||||
@@ -312,8 +312,8 @@ Aig_Obj_t * Dar_RefactBuildGraph( Aig_Man_t * pAig, Vec_Ptr_t * vCut, Kit_Graph_
|
||||
@@ -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 )
|
||||
{
|
||||
|
@ -191,11 +162,9 @@ index d744b4f..83fb3b0 100644
|
|||
pNode->pFunc = Aig_And( pAig, pAnd0, pAnd1 );
|
||||
/*
|
||||
printf( "Checking " );
|
||||
diff --git a/src/extlib-abc/aig/kit/kitAig.c b/src/extlib-abc/aig/kit/kitAig.c
|
||||
index de301f2..15d39d6 100644
|
||||
--- a/src/extlib-abc/aig/kit/kitAig.c
|
||||
+++ b/src/extlib-abc/aig/kit/kitAig.c
|
||||
@@ -54,8 +54,8 @@ Aig_Obj_t * Kit_GraphToAigInternal( Aig_Man_t * pMan, Kit_Graph_t * pGraph )
|
||||
--- ./src/extlib-abc/aig/kit/kitAig.c.orig 2014-04-02 11:47:21.000000000 -0600
|
||||
+++ ./src/extlib-abc/aig/kit/kitAig.c 2014-04-29 14:34:45.619479265 -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 )
|
||||
{
|
||||
|
@ -206,10 +175,8 @@ index de301f2..15d39d6 100644
|
|||
pNode->pFunc = Aig_And( pMan, pAnd0, pAnd1 );
|
||||
}
|
||||
// complement the result if necessary
|
||||
diff --git a/src/extlib-abc/aig/kit/kitGraph.c b/src/extlib-abc/aig/kit/kitGraph.c
|
||||
index 39ef587..1ae5891 100644
|
||||
--- a/src/extlib-abc/aig/kit/kitGraph.c
|
||||
+++ b/src/extlib-abc/aig/kit/kitGraph.c
|
||||
--- ./src/extlib-abc/aig/kit/kitGraph.c.orig 2014-04-02 11:47:21.000000000 -0600
|
||||
+++ ./src/extlib-abc/aig/kit/kitGraph.c 2014-04-29 14:34:45.620479263 -0600
|
||||
@@ -69,7 +69,7 @@ Kit_Graph_t * Kit_GraphCreateConst0()
|
||||
pGraph = ALLOC( Kit_Graph_t, 1 );
|
||||
memset( pGraph, 0, sizeof(Kit_Graph_t) );
|
||||
|
@ -219,7 +186,7 @@ index 39ef587..1ae5891 100644
|
|||
return pGraph;
|
||||
}
|
||||
|
||||
@@ -109,8 +109,8 @@ Kit_Graph_t * Kit_GraphCreateLeaf( int iLeaf, int nLeaves, int fCompl )
|
||||
@@ -109,8 +109,8 @@ Kit_Graph_t * Kit_GraphCreateLeaf( int i
|
||||
Kit_Graph_t * pGraph;
|
||||
assert( 0 <= iLeaf && iLeaf < nLeaves );
|
||||
pGraph = Kit_GraphCreate( nLeaves );
|
||||
|
@ -230,7 +197,7 @@ index 39ef587..1ae5891 100644
|
|||
return pGraph;
|
||||
}
|
||||
|
||||
@@ -174,8 +174,8 @@ Kit_Edge_t Kit_GraphAddNodeAnd( Kit_Graph_t * pGraph, Kit_Edge_t eEdge0, Kit_Edg
|
||||
@@ -174,8 +174,8 @@ Kit_Edge_t Kit_GraphAddNodeAnd( Kit_Grap
|
||||
// set the inputs and other info
|
||||
pNode->eEdge0 = eEdge0;
|
||||
pNode->eEdge1 = eEdge1;
|
||||
|
@ -241,7 +208,7 @@ index 39ef587..1ae5891 100644
|
|||
return Kit_EdgeCreate( pGraph->nSize - 1, 0 );
|
||||
}
|
||||
|
||||
@@ -198,12 +198,12 @@ Kit_Edge_t Kit_GraphAddNodeOr( Kit_Graph_t * pGraph, Kit_Edge_t eEdge0, Kit_Edge
|
||||
@@ -198,12 +198,12 @@ Kit_Edge_t Kit_GraphAddNodeOr( Kit_Graph
|
||||
// set the inputs and other info
|
||||
pNode->eEdge0 = eEdge0;
|
||||
pNode->eEdge1 = eEdge1;
|
||||
|
@ -258,7 +225,7 @@ index 39ef587..1ae5891 100644
|
|||
return Kit_EdgeCreate( pGraph->nSize - 1, 1 );
|
||||
}
|
||||
|
||||
@@ -224,11 +224,11 @@ Kit_Edge_t Kit_GraphAddNodeXor( Kit_Graph_t * pGraph, Kit_Edge_t eEdge0, Kit_Edg
|
||||
@@ -224,11 +224,11 @@ Kit_Edge_t Kit_GraphAddNodeXor( Kit_Grap
|
||||
if ( Type == 0 )
|
||||
{
|
||||
// derive the first AND
|
||||
|
@ -273,7 +240,7 @@ index 39ef587..1ae5891 100644
|
|||
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_Graph_t * pGraph, Kit_Edge_t eEdge0, Kit_Edg
|
||||
@@ -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
|
||||
|
@ -289,7 +256,7 @@ index 39ef587..1ae5891 100644
|
|||
}
|
||||
return eNode;
|
||||
}
|
||||
@@ -267,7 +267,7 @@ Kit_Edge_t Kit_GraphAddNodeMux( Kit_Graph_t * pGraph, Kit_Edge_t eEdgeC, Kit_Edg
|
||||
@@ -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
|
||||
|
@ -298,7 +265,7 @@ index 39ef587..1ae5891 100644
|
|||
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_Graph_t * pGraph, Kit_Edge_t eEdgeC, Kit_Edg
|
||||
@@ -275,16 +275,16 @@ Kit_Edge_t Kit_GraphAddNodeMux( Kit_Grap
|
||||
else
|
||||
{
|
||||
// complement the arguments
|
||||
|
@ -319,7 +286,7 @@ index 39ef587..1ae5891 100644
|
|||
}
|
||||
return eNode;
|
||||
}
|
||||
@@ -326,10 +326,10 @@ unsigned Kit_GraphToTruth( Kit_Graph_t * pGraph )
|
||||
@@ -326,10 +326,10 @@ unsigned Kit_GraphToTruth( Kit_Graph_t *
|
||||
// compute the function for each internal node
|
||||
Kit_GraphForEachNode( pGraph, pNode, i )
|
||||
{
|
||||
|
@ -334,22 +301,19 @@ index 39ef587..1ae5891 100644
|
|||
uTruth = uTruth0 & uTruth1;
|
||||
pNode->pFunc = (void *)(long)uTruth;
|
||||
}
|
||||
diff --git a/src/extlib-abc/kit.h b/src/extlib-abc/kit.h
|
||||
index af3a1a8..963a977 100644
|
||||
--- a/src/extlib-abc/kit.h
|
||||
+++ b/src/extlib-abc/kit.h
|
||||
--- ./src/extlib-abc/kit.h.orig 2014-04-02 11:47:21.000000000 -0600
|
||||
+++ ./src/extlib-abc/kit.h 2014-04-29 14:34:45.620479263 -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_
|
||||
-{
|
||||
- unsigned fCompl : 1; // the complemented bit
|
||||
- unsigned Node : 30; // the decomposition node pointed by the edge
|
||||
+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
|
||||
|
@ -358,7 +322,7 @@ index af3a1a8..963a977 100644
|
|||
};
|
||||
|
||||
typedef struct Kit_Node_t_ Kit_Node_t;
|
||||
@@ -203,18 +206,18 @@ static inline void Kit_SopShrink( Kit_Sop_t * cSop, int nCubesNew )
|
||||
@@ -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; }
|
||||
|
||||
|
@ -386,7 +350,7 @@ index af3a1a8..963a977 100644
|
|||
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( Kit_Graph_t * pGraph, int i )
|
||||
@@ -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; }
|
||||
|
@ -405,7 +369,7 @@ index af3a1a8..963a977 100644
|
|||
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( unsigned * pTruth, int nVars, int iVar )
|
||||
@@ -486,6 +487,18 @@ static inline void Kit_TruthIthVar( unsi
|
||||
/// FUNCTION DECLARATIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
|
@ -424,10 +388,8 @@ index af3a1a8..963a977 100644
|
|||
#if 0
|
||||
|
||||
/*=== kitBdd.c ==========================================================*/
|
||||
diff --git a/src/parser/smt2.y b/src/parser/smt2.y
|
||||
index c48ddaf..f756d66 100644
|
||||
--- a/src/parser/smt2.y
|
||||
+++ b/src/parser/smt2.y
|
||||
--- ./src/parser/smt2.y.orig 2014-04-02 11:47:21.000000000 -0600
|
||||
+++ ./src/parser/smt2.y 2014-04-29 14:34:45.620479263 -0600
|
||||
@@ -239,7 +239,7 @@ cmdi:
|
||||
{}
|
||||
| LPAREN_TOK PUSH_TOK NUMERAL_TOK RPAREN_TOK
|
||||
|
@ -446,7 +408,7 @@ index c48ddaf..f756d66 100644
|
|||
parserInterface->pop();
|
||||
parserInterface->success();
|
||||
}
|
||||
@@ -307,7 +307,7 @@ STRING_TOK LPAREN_TOK function_params RPAREN_TOK LPAREN_TOK UNDERSCORE_TOK BITVE
|
||||
@@ -307,7 +307,7 @@ STRING_TOK LPAREN_TOK function_params RP
|
||||
BEEV::parserInterface->storeFunction(*$1, *$3, *$11);
|
||||
|
||||
// Next time the variable is used, we want it to be fresh.
|
||||
|
@ -455,7 +417,7 @@ index c48ddaf..f756d66 100644
|
|||
BEEV::parserInterface->removeSymbol((*$3)[i]);
|
||||
|
||||
delete $1;
|
||||
@@ -321,7 +321,7 @@ STRING_TOK LPAREN_TOK function_params RPAREN_TOK BOOL_TOK an_formula
|
||||
@@ -321,7 +321,7 @@ STRING_TOK LPAREN_TOK function_params RP
|
||||
BEEV::parserInterface->storeFunction(*$1, *$3, *$6);
|
||||
|
||||
// Next time the variable is used, we want it to be fresh.
|
||||
|
@ -464,11 +426,9 @@ index c48ddaf..f756d66 100644
|
|||
BEEV::parserInterface->removeSymbol((*$3)[i]);
|
||||
|
||||
delete $1;
|
||||
diff --git a/src/printer/SMTLIB1Printer.cpp b/src/printer/SMTLIB1Printer.cpp
|
||||
index 7129f50..21a5855 100644
|
||||
--- a/src/printer/SMTLIB1Printer.cpp
|
||||
+++ b/src/printer/SMTLIB1Printer.cpp
|
||||
@@ -215,7 +215,7 @@ void printSMTLIB1VarDeclsToStream(ASTNodeSet& symbols, ostream& os)
|
||||
--- ./src/printer/SMTLIB1Printer.cpp.orig 2014-04-02 11:47:21.000000000 -0600
|
||||
+++ ./src/printer/SMTLIB1Printer.cpp 2014-04-29 14:34:45.621479262 -0600
|
||||
@@ -215,7 +215,7 @@ void printSMTLIB1VarDeclsToStream(ASTNod
|
||||
{
|
||||
string close = "";
|
||||
|
||||
|
@ -477,11 +437,9 @@ index 7129f50..21a5855 100644
|
|||
{
|
||||
os << "(" << functionToSMTLIBName(kind,true);
|
||||
os << " ";
|
||||
diff --git a/src/printer/SMTLIB2Printer.cpp b/src/printer/SMTLIB2Printer.cpp
|
||||
index 5ee4e98..d446897 100644
|
||||
--- a/src/printer/SMTLIB2Printer.cpp
|
||||
+++ b/src/printer/SMTLIB2Printer.cpp
|
||||
@@ -213,7 +213,7 @@ void printVarDeclsToStream(ASTNodeSet& symbols, ostream& os)
|
||||
--- ./src/printer/SMTLIB2Printer.cpp.orig 2014-04-02 11:47:21.000000000 -0600
|
||||
+++ ./src/printer/SMTLIB2Printer.cpp 2014-04-29 14:34:45.621479262 -0600
|
||||
@@ -213,7 +213,7 @@ void printVarDeclsToStream(ASTNodeSet& s
|
||||
{
|
||||
string close = "";
|
||||
|
||||
|
@ -490,10 +448,8 @@ index 5ee4e98..d446897 100644
|
|||
{
|
||||
os << "(" << functionToSMTLIBName(kind,false);
|
||||
os << " ";
|
||||
diff --git a/src/simplifier/AlwaysTrue.h b/src/simplifier/AlwaysTrue.h
|
||||
index e74df19..eaf0c9d 100644
|
||||
--- a/src/simplifier/AlwaysTrue.h
|
||||
+++ b/src/simplifier/AlwaysTrue.h
|
||||
--- ./src/simplifier/AlwaysTrue.h.orig 2014-04-02 11:47:21.000000000 -0600
|
||||
+++ ./src/simplifier/AlwaysTrue.h 2014-04-29 14:34:45.621479262 -0600
|
||||
@@ -85,7 +85,7 @@ public:
|
||||
else
|
||||
new_state = state;
|
||||
|
@ -503,10 +459,97 @@ index e74df19..eaf0c9d 100644
|
|||
{
|
||||
newChildren.push_back(visit(n[i],new_state,fromTo));
|
||||
}
|
||||
diff --git a/src/simplifier/EstablishIntervals.h b/src/simplifier/EstablishIntervals.h
|
||||
index 7c762b1..34c92c1 100644
|
||||
--- a/src/simplifier/EstablishIntervals.h
|
||||
+++ b/src/simplifier/EstablishIntervals.h
|
||||
--- ./src/simplifier/constantBitP/ConstantBitP_Comparison.cpp.orig 2014-04-02 11:47:21.000000000 -0600
|
||||
+++ ./src/simplifier/constantBitP/ConstantBitP_Comparison.cpp 2014-04-29 14:34:45.623479259 -0600
|
||||
@@ -129,6 +129,7 @@ fast_exit(FixedBits& c0, FixedBits& c1)
|
||||
}
|
||||
return false;
|
||||
}
|
||||
+ return true;
|
||||
}
|
||||
|
||||
|
||||
--- ./src/simplifier/constantBitP/ConstantBitP_Division.cpp.orig 2014-04-02 11:47:21.000000000 -0600
|
||||
+++ ./src/simplifier/constantBitP/ConstantBitP_Division.cpp 2014-04-29 14:34:45.623479259 -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 2014-04-02 11:47:21.000000000 -0600
|
||||
+++ ./src/simplifier/constantBitP/ConstantBitPropagation.cpp 2014-04-29 14:34:45.623479259 -0600
|
||||
@@ -433,7 +433,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]);
|
||||
}
|
||||
|
||||
@@ -469,7 +469,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 2014-04-02 11:47:21.000000000 -0600
|
||||
+++ ./src/simplifier/constantBitP/FixedBits.cpp 2014-04-29 14:34:45.623479259 -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/MersenneTwister.h.orig 2014-04-02 11:47:21.000000000 -0600
|
||||
+++ ./src/simplifier/constantBitP/MersenneTwister.h 2014-04-29 14:34:45.623479259 -0600
|
||||
@@ -231,7 +231,7 @@ inline void MTRand::seed( uint32 *const
|
||||
initialize(19650218UL);
|
||||
int i = 1;
|
||||
uint32 j = 0;
|
||||
- int k = ( N > seedLength ? N : seedLength );
|
||||
+ int k = ( N > seedLength ? (int) N : seedLength );
|
||||
for( ; k; --k )
|
||||
{
|
||||
state[i] =
|
||||
--- ./src/simplifier/consteval.cpp.orig 2014-04-02 11:47:21.000000000 -0600
|
||||
+++ ./src/simplifier/consteval.cpp 2014-04-29 14:34:45.624479258 -0600
|
||||
@@ -37,13 +37,13 @@ namespace BEEV
|
||||
CBV tmp0 = NULL;
|
||||
CBV tmp1 = NULL;
|
||||
|
||||
- unsigned int number_of_children = input_children.size();
|
||||
+ size_t number_of_children = input_children.size();
|
||||
assert(number_of_children >=1);
|
||||
assert(k != BVCONST);
|
||||
|
||||
ASTVec children;
|
||||
children.reserve(number_of_children);
|
||||
- for (int i =0; i < number_of_children; i++)
|
||||
+ for (size_t i =0; i < number_of_children; i++)
|
||||
{
|
||||
if (input_children[i].isConstant())
|
||||
children.push_back(input_children[i]);
|
||||
--- ./src/simplifier/EstablishIntervals.h.orig 2014-04-02 11:47:21.000000000 -0600
|
||||
+++ ./src/simplifier/EstablishIntervals.h 2014-04-29 14:34:45.621479262 -0600
|
||||
@@ -120,7 +120,7 @@ namespace BEEV
|
||||
ASTVec new_children;
|
||||
new_children.reserve(result.GetChildren().size());
|
||||
|
@ -626,10 +669,8 @@ index 7c762b1..34c92c1 100644
|
|||
CONSTANTBV::BitVector_Destroy(likeAutoPtr[i]);
|
||||
|
||||
likeAutoPtr.clear();
|
||||
diff --git a/src/simplifier/FindPureLiterals.h b/src/simplifier/FindPureLiterals.h
|
||||
index 4b03916..4ff05bc 100644
|
||||
--- a/src/simplifier/FindPureLiterals.h
|
||||
+++ b/src/simplifier/FindPureLiterals.h
|
||||
--- ./src/simplifier/FindPureLiterals.h.orig 2014-04-02 11:47:21.000000000 -0600
|
||||
+++ ./src/simplifier/FindPureLiterals.h 2014-04-29 14:34:45.621479262 -0600
|
||||
@@ -111,7 +111,7 @@ public:
|
||||
{
|
||||
case AND:
|
||||
|
@ -648,10 +689,8 @@ index 4b03916..4ff05bc 100644
|
|||
build(n[i],polarity);
|
||||
break;
|
||||
}
|
||||
diff --git a/src/simplifier/MutableASTNode.h b/src/simplifier/MutableASTNode.h
|
||||
index 3e9a8e2..4d37b8e 100644
|
||||
--- a/src/simplifier/MutableASTNode.h
|
||||
+++ b/src/simplifier/MutableASTNode.h
|
||||
--- ./src/simplifier/MutableASTNode.h.orig 2014-04-02 11:47:21.000000000 -0600
|
||||
+++ ./src/simplifier/MutableASTNode.h 2014-04-29 14:34:45.621479262 -0600
|
||||
@@ -46,12 +46,12 @@ public:
|
||||
vector<MutableASTNode *> tempChildren;
|
||||
tempChildren.reserve(n.Degree());
|
||||
|
@ -712,10 +751,8 @@ index 3e9a8e2..4d37b8e 100644
|
|||
delete all[i];
|
||||
all.clear();
|
||||
}
|
||||
diff --git a/src/simplifier/PropagateEqualities.cpp b/src/simplifier/PropagateEqualities.cpp
|
||||
index 09534ee..5facb98 100644
|
||||
--- a/src/simplifier/PropagateEqualities.cpp
|
||||
+++ b/src/simplifier/PropagateEqualities.cpp
|
||||
--- ./src/simplifier/PropagateEqualities.cpp.orig 2014-04-02 11:47:21.000000000 -0600
|
||||
+++ ./src/simplifier/PropagateEqualities.cpp 2014-04-29 14:34:45.622479260 -0600
|
||||
@@ -31,10 +31,10 @@ namespace BEEV
|
||||
|
||||
bool result = false;
|
||||
|
@ -742,10 +779,8 @@ index 09534ee..5facb98 100644
|
|||
if (j != i)
|
||||
others.push_back(lhs[j]);
|
||||
|
||||
diff --git a/src/simplifier/RemoveUnconstrained.cpp b/src/simplifier/RemoveUnconstrained.cpp
|
||||
index ca5dd81..0fa3803 100644
|
||||
--- a/src/simplifier/RemoveUnconstrained.cpp
|
||||
+++ b/src/simplifier/RemoveUnconstrained.cpp
|
||||
--- ./src/simplifier/RemoveUnconstrained.cpp.orig 2014-04-02 11:47:21.000000000 -0600
|
||||
+++ ./src/simplifier/RemoveUnconstrained.cpp 2014-04-29 14:34:45.622479260 -0600
|
||||
@@ -55,7 +55,7 @@ namespace BEEV
|
||||
|
||||
bool allChildrenAreUnconstrained(vector <MutableASTNode*> children)
|
||||
|
@ -827,177 +862,8 @@ index ca5dd81..0fa3803 100644
|
|||
if (children[i] != var)
|
||||
other.push_back(mutable_children[i]->toASTNode(nf));
|
||||
|
||||
diff --git a/src/simplifier/SubstitutionMap.cpp b/src/simplifier/SubstitutionMap.cpp
|
||||
index 5a2abd5..d7a2a61 100644
|
||||
--- a/src/simplifier/SubstitutionMap.cpp
|
||||
+++ b/src/simplifier/SubstitutionMap.cpp
|
||||
@@ -216,7 +216,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.
|
||||
diff --git a/src/simplifier/UseITEContext.h b/src/simplifier/UseITEContext.h
|
||||
index 5d95d39..45f8d2f 100644
|
||||
--- a/src/simplifier/UseITEContext.h
|
||||
+++ b/src/simplifier/UseITEContext.h
|
||||
@@ -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));
|
||||
}
|
||||
|
||||
diff --git a/src/simplifier/VariablesInExpression.cpp b/src/simplifier/VariablesInExpression.cpp
|
||||
index 0bdc37f..656a5a7 100644
|
||||
--- a/src/simplifier/VariablesInExpression.cpp
|
||||
+++ b/src/simplifier/VariablesInExpression.cpp
|
||||
@@ -42,7 +42,7 @@ Symbols* VariablesInExpression::getSymbol(const ASTNode& n) {
|
||||
}
|
||||
|
||||
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::SetofVarsSeenInTerm(Symbols* symbol, bool& d
|
||||
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::VarSeenInTerm(const ASTNode& var,
|
||||
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;
|
||||
|
||||
diff --git a/src/simplifier/constantBitP/ConstantBitP_Comparison.cpp b/src/simplifier/constantBitP/ConstantBitP_Comparison.cpp
|
||||
index 7958269..1dded88 100644
|
||||
--- a/src/simplifier/constantBitP/ConstantBitP_Comparison.cpp
|
||||
+++ b/src/simplifier/constantBitP/ConstantBitP_Comparison.cpp
|
||||
@@ -129,6 +129,7 @@ fast_exit(FixedBits& c0, FixedBits& c1)
|
||||
}
|
||||
return false;
|
||||
}
|
||||
+ return true;
|
||||
}
|
||||
|
||||
|
||||
diff --git a/src/simplifier/constantBitP/ConstantBitP_Division.cpp b/src/simplifier/constantBitP/ConstantBitP_Division.cpp
|
||||
index dea6eb1..4d8f64c 100644
|
||||
--- a/src/simplifier/constantBitP/ConstantBitP_Division.cpp
|
||||
+++ b/src/simplifier/constantBitP/ConstantBitP_Division.cpp
|
||||
@@ -157,14 +157,14 @@ Result bvUnsignedQuotientAndRemainder(vector<FixedBits*>& children,
|
||||
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);
|
||||
}
|
||||
|
||||
diff --git a/src/simplifier/constantBitP/ConstantBitPropagation.cpp b/src/simplifier/constantBitP/ConstantBitPropagation.cpp
|
||||
index d4f5319..8ac4a37 100644
|
||||
--- a/src/simplifier/constantBitP/ConstantBitPropagation.cpp
|
||||
+++ b/src/simplifier/constantBitP/ConstantBitPropagation.cpp
|
||||
@@ -433,7 +433,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]);
|
||||
}
|
||||
|
||||
@@ -469,7 +469,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]))
|
||||
diff --git a/src/simplifier/constantBitP/FixedBits.cpp b/src/simplifier/constantBitP/FixedBits.cpp
|
||||
index 273175a..1fe1686 100644
|
||||
--- a/src/simplifier/constantBitP/FixedBits.cpp
|
||||
+++ b/src/simplifier/constantBitP/FixedBits.cpp
|
||||
@@ -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)
|
||||
{
|
||||
diff --git a/src/simplifier/constantBitP/MersenneTwister.h b/src/simplifier/constantBitP/MersenneTwister.h
|
||||
index bd63d31..238fa3f 100644
|
||||
--- a/src/simplifier/constantBitP/MersenneTwister.h
|
||||
+++ b/src/simplifier/constantBitP/MersenneTwister.h
|
||||
@@ -231,7 +231,7 @@ inline void MTRand::seed( uint32 *const bigSeed, const uint32 seedLength )
|
||||
initialize(19650218UL);
|
||||
int i = 1;
|
||||
uint32 j = 0;
|
||||
- int k = ( N > seedLength ? N : seedLength );
|
||||
+ int k = ( N > seedLength ? (int) N : seedLength );
|
||||
for( ; k; --k )
|
||||
{
|
||||
state[i] =
|
||||
diff --git a/src/simplifier/consteval.cpp b/src/simplifier/consteval.cpp
|
||||
index 46ac6e8..24cdbf6 100644
|
||||
--- a/src/simplifier/consteval.cpp
|
||||
+++ b/src/simplifier/consteval.cpp
|
||||
@@ -37,13 +37,13 @@ namespace BEEV
|
||||
CBV tmp0 = NULL;
|
||||
CBV tmp1 = NULL;
|
||||
|
||||
- unsigned int number_of_children = input_children.size();
|
||||
+ size_t number_of_children = input_children.size();
|
||||
assert(number_of_children >=1);
|
||||
assert(k != BVCONST);
|
||||
|
||||
ASTVec children;
|
||||
children.reserve(number_of_children);
|
||||
- for (int i =0; i < number_of_children; i++)
|
||||
+ for (size_t i =0; i < number_of_children; i++)
|
||||
{
|
||||
if (input_children[i].isConstant())
|
||||
children.push_back(input_children[i]);
|
||||
diff --git a/src/simplifier/simplifier.cpp b/src/simplifier/simplifier.cpp
|
||||
index b309a8a..76cfb04 100644
|
||||
--- a/src/simplifier/simplifier.cpp
|
||||
+++ b/src/simplifier/simplifier.cpp
|
||||
--- ./src/simplifier/simplifier.cpp.orig 2014-04-02 11:47:21.000000000 -0600
|
||||
+++ ./src/simplifier/simplifier.cpp 2014-04-29 14:34:45.624479258 -0600
|
||||
@@ -248,7 +248,7 @@ namespace BEEV
|
||||
assert(false);
|
||||
}
|
||||
|
@ -1099,10 +965,79 @@ index b309a8a..76cfb04 100644
|
|||
newChildren.push_back(
|
||||
nf->CreateTerm(BVEXTRACT, output.GetValueWidth() - trailingZeroes, output[i],
|
||||
_bm->CreateBVConst(32, output.GetValueWidth() - 1),
|
||||
diff --git a/src/to-sat/ASTNode/ToSAT.cpp b/src/to-sat/ASTNode/ToSAT.cpp
|
||||
index 9fa5ebc..72d41b5 100644
|
||||
--- a/src/to-sat/ASTNode/ToSAT.cpp
|
||||
+++ b/src/to-sat/ASTNode/ToSAT.cpp
|
||||
--- ./src/simplifier/SubstitutionMap.cpp.orig 2014-04-02 11:47:21.000000000 -0600
|
||||
+++ ./src/simplifier/SubstitutionMap.cpp 2014-04-29 14:34:45.622479260 -0600
|
||||
@@ -216,7 +216,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/UseITEContext.h.orig 2014-04-02 11:47:21.000000000 -0600
|
||||
+++ ./src/simplifier/UseITEContext.h 2014-04-29 14:34:45.622479260 -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/VariablesInExpression.cpp.orig 2014-04-02 11:47:21.000000000 -0600
|
||||
+++ ./src/simplifier/VariablesInExpression.cpp 2014-04-29 14:34:45.622479260 -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/STPManager/STP.cpp.orig 2014-04-02 11:47:21.000000000 -0600
|
||||
+++ ./src/STPManager/STP.cpp 2014-04-29 14:34:45.618479266 -0600
|
||||
@@ -576,7 +576,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/to-sat/ASTNode/ToSAT.cpp.orig 2014-04-02 11:47:21.000000000 -0600
|
||||
+++ ./src/to-sat/ASTNode/ToSAT.cpp 2014-04-29 14:34:45.625479256 -0600
|
||||
@@ -53,7 +53,7 @@ namespace BEEV
|
||||
|
||||
// Copies the symbol into the map that is used to build the counter example.
|
||||
|
@ -1121,10 +1056,8 @@ index 9fa5ebc..72d41b5 100644
|
|||
{
|
||||
ClauseList *cl = (*it).second;
|
||||
sat = toSATandSolve(SatSolver,*cl, count==cb->size(),cm);
|
||||
diff --git a/src/to-sat/BitBlaster.cpp b/src/to-sat/BitBlaster.cpp
|
||||
index 401119c..d72ffa6 100644
|
||||
--- a/src/to-sat/BitBlaster.cpp
|
||||
+++ b/src/to-sat/BitBlaster.cpp
|
||||
--- ./src/to-sat/BitBlaster.cpp.orig 2014-04-02 11:47:21.000000000 -0600
|
||||
+++ ./src/to-sat/BitBlaster.cpp 2014-04-29 14:34:45.625479256 -0600
|
||||
@@ -1678,13 +1678,13 @@ namespace BEEV
|
||||
assert(ms->x.getWidth() == ms->y.getWidth());
|
||||
assert(ms->r.getWidth() == ms->y.getWidth());
|
||||
|
|
12
stp.spec
12
stp.spec
|
@ -1,13 +1,13 @@
|
|||
# Upstream occasionally releases a subversion snapshot, but no "regular"
|
||||
# releases since the 0.1 release.
|
||||
%global gitdate 20140319
|
||||
%global gittag fe766c9add6f80453ec14f4a3b4d5cf3a0385551
|
||||
%global shorttag %(echo %{gittag} | cut -b -7)
|
||||
%global gitdate 20140402
|
||||
%global gittag f8a392dea3e6942897e2213e13f23cf99d323ef4
|
||||
%global shorttag %(cut -b -7 <<< %{gittag})
|
||||
%global user stp
|
||||
|
||||
Name: stp
|
||||
Version: 0.1
|
||||
Release: 19.%{gitdate}git.%{shorttag}%{?dist}
|
||||
Release: 20.%{gitdate}git.%{shorttag}%{?dist}
|
||||
Summary: Constraint solver/decision procedure
|
||||
|
||||
Group: Applications/Engineering
|
||||
|
@ -72,6 +72,7 @@ sed -i "s/-Wno-deprecated/& -Wno-reorder/" CMakeLists.txt
|
|||
|
||||
%build
|
||||
%cmake
|
||||
make %{?_smp_mflags}
|
||||
|
||||
%install
|
||||
make install DESTDIR=%{buildroot}
|
||||
|
@ -93,6 +94,9 @@ fi
|
|||
%{_libdir}/cmake/STP/
|
||||
|
||||
%changelog
|
||||
* Tue Apr 29 2014 Jerry James <loganjerry@gmail.com> - 0.1-20.20140402git.f8a392d
|
||||
- Update to recent git snapshot
|
||||
|
||||
* Wed Mar 19 2014 Jerry James <loganjerry@gmail.com> - 0.1-19.20140319git.6110a49
|
||||
- Update to recent git snapshot, now hosted on github
|
||||
- Build now uses cmake
|
||||
|
|
Loading…
Reference in New Issue