[stp] Update to recent git snapshot.
Jerry James
jjames at fedoraproject.org
Tue Apr 29 21:22:15 UTC 2014
commit 75cefd810453695e7f738e9366e9b1200d05185f
Author: Jerry James <jamesjer at betterlinux.com>
Date: Tue Apr 29 15:22:26 2014 -0600
Update to recent git snapshot.
.gitignore | 2 +-
sources | 2 +-
stp-warning.patch | 603 ++++++++++++++++++++++++-----------------------------
stp.spec | 12 +-
4 files changed, 278 insertions(+), 341 deletions(-)
---
diff --git a/.gitignore b/.gitignore
index a8345f8..5b1cb69 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1 +1 @@
-/stp-stp-fe766c9.tar.gz
+/stp-stp-f8a392d.tar.gz
diff --git a/sources b/sources
index 2182b29..53178ac 100644
--- a/sources
+++ b/sources
@@ -1 +1 @@
-3104c3fcb6e89da91f766e9b61dd87d9 stp-stp-fe766c9.tar.gz
+2ec158d56d2189d07aa09e3e05c88ca2 stp-stp-f8a392d.tar.gz
diff --git a/stp-warning.patch b/stp-warning.patch
index a7bfb95..cace45d 100644
--- a/stp-warning.patch
+++ b/stp-warning.patch
@@ -1,7 +1,45 @@
-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
+--- ./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;
+ }
+- 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;
+@@ -217,7 +217,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);
+ }
+--- ./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);
+
+- for (int index = 0; index < v.size(); index++)
++ for (size_t index = 0; index < v.size(); index++)
+ {
+ const unsigned sat_variable_index = v[index];
+
+@@ -871,7 +871,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/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());
@@ -11,11 +49,9 @@ index 0e028c4..7cfa7a7 100644
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)
+--- ./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();
@@ -24,7 +60,7 @@ index 9c18b69..4fc3320 100644
if (in1 == in2)
//terms are syntactically the same
-@@ -526,7 +526,7 @@ SimplifyingNodeFactory::CreateSimpleEQ(const ASTVec& children)
+@@ -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();
@@ -33,7 +69,7 @@ index 9c18b69..4fc3320 100644
if (CONSTANTBV::BitVector_bit_test(in1.GetBVConst(), i))
foundOne = true;
else
-@@ -1176,10 +1176,12 @@ SimplifyingNodeFactory::CreateTerm(Kind kind, unsigned int width, const ASTVec &
+@@ -1188,10 +1188,12 @@ SimplifyingNodeFactory::CreateTerm(Kind
for (size_t i = 0; i < width; i++)
{
if (CONSTANTBV::BitVector_bit_test(c, i))
@@ -50,7 +86,7 @@ index 9c18b69..4fc3320 100644
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 &
+@@ -1212,7 +1214,7 @@ SimplifyingNodeFactory::CreateTerm(Kind
ASTNode z = bm.CreateZeroConst(start);
result = NodeFactory::CreateTerm(BVCONCAT, end + 1, result, z);
}
@@ -59,67 +95,8 @@ index 9c18b69..4fc3320 100644
{
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
-@@ -119,7 +119,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;
-@@ -217,7 +217,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);
- }
-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
-@@ -48,7 +48,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];
-
-@@ -871,7 +871,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;
-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/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());
diff --git a/stp.spec b/stp.spec
index 904b4f0..b70b2db 100644
--- a/stp.spec
+++ b/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 at gmail.com> - 0.1-20.20140402git.f8a392d
+- Update to recent git snapshot
+
* Wed Mar 19 2014 Jerry James <loganjerry at gmail.com> - 0.1-19.20140319git.6110a49
- Update to recent git snapshot, now hosted on github
- Build now uses cmake
More information about the scm-commits
mailing list