[stp] Update to recent git snapshot. Drop upstreamed -undefined patch.
Jerry James
jjames at fedoraproject.org
Wed Jun 18 23:27:40 UTC 2014
commit 31e34f55e7950372ef793ff9a4166df561ea03b2
Author: Jerry James <jamesjer at betterlinux.com>
Date: Wed Jun 18 17:27:24 2014 -0600
Update to recent git snapshot.
Drop upstreamed -undefined patch.
.gitignore | 2 +-
sources | 2 +-
stp-unbundle.patch | 18 +-
stp-undefined.patch | 80 ----
stp-warning.patch | 1090 +++------------------------------------------------
stp.spec | 25 +-
6 files changed, 82 insertions(+), 1135 deletions(-)
---
diff --git a/.gitignore b/.gitignore
index 5b1cb69..3569748 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1 +1 @@
-/stp-stp-f8a392d.tar.gz
+/stp-stp-44de620.tar.gz
diff --git a/sources b/sources
index 53178ac..db2a34f 100644
--- a/sources
+++ b/sources
@@ -1 +1 @@
-2ec158d56d2189d07aa09e3e05c88ca2 stp-stp-f8a392d.tar.gz
+3744bde4e5a1d5108506adf1c929563d stp-stp-44de620.tar.gz
diff --git a/stp-unbundle.patch b/stp-unbundle.patch
index 3e1b906..6b1f268 100644
--- a/stp-unbundle.patch
+++ b/stp-unbundle.patch
@@ -1,16 +1,16 @@
diff --git a/CMakeLists.txt b/CMakeLists.txt
-index cc5bb76..169c064 100644
+index a43eb68..c0db102 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
-@@ -69,6 +69,7 @@ endmacro()
+@@ -109,6 +109,7 @@ endmacro()
if(BUILD_SHARED_LIBS)
message(STATUS "Building shared library currently broken due to mix of C++/C code")
add_cxx_flag_if_supported("-fPIC")
+ set(CMAKE_C_FLAGS "${CMAKE_C_FLAGS} -fPIC")
endif()
- check_cxx_compiler_flag("-std=gnu++11" HAVE_FLAG_STD_GNUPP11)
-@@ -179,6 +180,7 @@ include_directories(${Boost_INCLUDE_DIRS})
+ check_cxx_compiler_flag("-std=gnu++11" HAVE_FLAG_STD_GNUCPP11)
+@@ -219,6 +220,7 @@ include_directories(${Boost_INCLUDE_DIRS})
find_package(BISON REQUIRED)
find_package(FLEX REQUIRED)
@@ -92,7 +92,7 @@ index 191711e..9a44acd 100644
class RunTimes : boost::noncopyable
{
diff --git a/src/libstp/CMakeLists.txt b/src/libstp/CMakeLists.txt
-index eabc0d6..8cc3bc7 100644
+index 8ad9ccb..045b8ac 100644
--- a/src/libstp/CMakeLists.txt
+++ b/src/libstp/CMakeLists.txt
@@ -13,7 +13,6 @@ set(stp_lib_targets
@@ -103,7 +103,7 @@ index eabc0d6..8cc3bc7 100644
simplifier
constantbv
abc
-@@ -58,7 +57,7 @@ set_target_properties(libstp PROPERTIES
+@@ -74,7 +73,7 @@ endif()
# Clients of libstp that don't use CMake will have to link the Boost libraries
# in manually.
# -----------------------------------------------------------------------------
@@ -122,7 +122,7 @@ index 4749a77..ffb169e 100644
add_library(sat OBJECT
diff --git a/src/sat/CryptoMinisat.cpp b/src/sat/CryptoMinisat.cpp
-index 27f372d..93e9b85 100644
+index 8646824..0d77ff5 100644
--- a/src/sat/CryptoMinisat.cpp
+++ b/src/sat/CryptoMinisat.cpp
@@ -7,15 +7,26 @@
@@ -177,7 +177,7 @@ index 27f372d..93e9b85 100644
int CryptoMinisat::nVars()
diff --git a/src/sat/CryptoMinisat.h b/src/sat/CryptoMinisat.h
-index 9c11c1d..50d55fc 100644
+index 76e7a47..9ecb5b6 100644
--- a/src/sat/CryptoMinisat.h
+++ b/src/sat/CryptoMinisat.h
@@ -6,16 +6,13 @@
@@ -201,7 +201,7 @@ index 9c11c1d..50d55fc 100644
public:
CryptoMinisat();
diff --git a/tests/api/C/CMakeLists.txt b/tests/api/C/CMakeLists.txt
-index 99c1478..2a490ff 100644
+index dcdcc3d..e0146a8 100644
--- a/tests/api/C/CMakeLists.txt
+++ b/tests/api/C/CMakeLists.txt
@@ -1,4 +1,6 @@
diff --git a/stp-warning.patch b/stp-warning.patch
index cace45d..468f1e4 100644
--- a/stp-warning.patch
+++ b/stp-warning.patch
@@ -1,5 +1,20 @@
---- ./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
+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 4cc543d..25102bd 100644
+--- a/src/absrefine_counterexample/AbstractionRefinement.cpp
++++ b/src/absrefine_counterexample/AbstractionRefinement.cpp
@@ -119,7 +119,7 @@ namespace BEEV
}
return result;
@@ -9,367 +24,55 @@
{
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());
-
-- 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);
-
- 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: "\
---- ./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)
- {
-- 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;
---- ./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 );
-- static Counter = 0;
-+ static int Counter = 0;
- char FileNameDot[200];
- FILE * pFile;
- // create the file name
---- ./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
-- 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 )
-@@ -312,8 +312,8 @@ Aig_Obj_t * Dar_RefactBuildGraph( Aig_Ma
- //printf( "Building (current number %d):\n", Aig_ManObjNumMax(pAig) );
- Kit_GraphForEachNode( pGraph, pNode, i )
- {
-- pAnd0 = Aig_NotCond( Kit_GraphNode(pGraph, pNode->eEdge0.Node)->pFunc, pNode->eEdge0.fCompl );
-- pAnd1 = Aig_NotCond( Kit_GraphNode(pGraph, pNode->eEdge1.Node)->pFunc, pNode->eEdge1.fCompl );
-+ pAnd0 = Aig_NotCond( Kit_GraphNode(pGraph, pNode->eEdge0.edgeBits.Node)->pFunc, pNode->eEdge0.edgeBits.fCompl );
-+ pAnd1 = Aig_NotCond( Kit_GraphNode(pGraph, pNode->eEdge1.edgeBits.Node)->pFunc, pNode->eEdge1.edgeBits.fCompl );
- pNode->pFunc = Aig_And( pAig, pAnd0, pAnd1 );
- /*
- printf( "Checking " );
---- ./src/extlib-abc/aig/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 )
- {
-- 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 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) );
- 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/kit.h.orig 2014-04-02 11:47:21.000000000 -0600
-+++ ./src/extlib-abc/kit.h 2014-04-29 14:34:45.620479263 -0600
+diff --git a/src/extlib-abc/kit.h b/src/extlib-abc/kit.h
+index af3a1a8..b8db70f 100644
+--- a/src/extlib-abc/kit.h
++++ b/src/extlib-abc/kit.h
@@ -53,11 +53,14 @@ struct Kit_Sop_t_
unsigned * pCubes; // the storage for cubes
};
-typedef struct Kit_Edge_t_ Kit_Edge_t;
-struct Kit_Edge_t_
-+typedef union Kit_Edge_t_ Kit_Edge_t;
-+union Kit_Edge_t_
- {
+-{
- unsigned fCompl : 1; // the complemented bit
- unsigned Node : 30; // the decomposition node pointed by the edge
++typedef union Kit_Edge_t_ Kit_Edge_t;
++union Kit_Edge_t_
++{
+ struct {
+ unsigned fCompl : 1; // the complemented bit
+ unsigned Node : 30; // the decomposition node pointed by the edge
-+ } edgeBits;
++ };
+ unsigned int edgeInt;
};
typedef struct Kit_Node_t_ Kit_Node_t;
-@@ -203,18 +206,18 @@ static inline void Kit_SopShrink
+@@ -203,11 +206,11 @@ static inline void Kit_SopShrink( Kit_Sop_t * cSop, int nCubesNew )
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 unsigned Kit_EdgeToInt( Kit_Edge_t eEdge ) { return (eEdge.Node << 1) | eEdge.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 Kit_Edge_t Kit_IntToEdge_( unsigned Edge ) { Kit_Edge_t e; e.edgeInt = Edge; return e; }
static inline int Kit_GraphIsConst( Kit_Graph_t * pGraph ) { return pGraph->fConst; }
--static inline int Kit_GraphIsConst0( Kit_Graph_t * pGraph ) { return pGraph->fConst && pGraph->eRoot.fCompl; }
--static inline int Kit_GraphIsConst1( Kit_Graph_t * pGraph ) { return pGraph->fConst && !pGraph->eRoot.fCompl; }
--static inline int Kit_GraphIsComplement( Kit_Graph_t * pGraph ) { return pGraph->eRoot.fCompl; }
--static inline int Kit_GraphIsVar( Kit_Graph_t * pGraph ) { return pGraph->eRoot.Node < (unsigned)pGraph->nLeaves; }
--static inline void Kit_GraphComplement( Kit_Graph_t * pGraph ) { pGraph->eRoot.fCompl ^= 1; }
-+static inline int Kit_GraphIsConst0( Kit_Graph_t * pGraph ) { return pGraph->fConst && pGraph->eRoot.edgeBits.fCompl; }
-+static inline int Kit_GraphIsConst1( Kit_Graph_t * pGraph ) { return pGraph->fConst && !pGraph->eRoot.edgeBits.fCompl; }
-+static inline int Kit_GraphIsComplement( Kit_Graph_t * pGraph ) { return pGraph->eRoot.edgeBits.fCompl; }
-+static inline int Kit_GraphIsVar( Kit_Graph_t * pGraph ) { return pGraph->eRoot.edgeBits.Node < (unsigned)pGraph->nLeaves; }
-+static inline void Kit_GraphComplement( Kit_Graph_t * pGraph ) { pGraph->eRoot.edgeBits.fCompl ^= 1; }
- static inline void Kit_GraphSetRoot( Kit_Graph_t * pGraph, Kit_Edge_t eRoot ) { pGraph->eRoot = eRoot; }
- static inline int Kit_GraphLeaveNum( Kit_Graph_t * pGraph ) { return pGraph->nLeaves; }
- static inline int Kit_GraphNodeNum( Kit_Graph_t * pGraph ) { return pGraph->nSize - pGraph->nLeaves; }
-@@ -222,14 +225,12 @@ static inline Kit_Node_t * Kit_GraphNode
- static inline Kit_Node_t * Kit_GraphNodeLast( Kit_Graph_t * pGraph ) { return pGraph->pNodes + pGraph->nSize - 1; }
- static inline int Kit_GraphNodeInt( Kit_Graph_t * pGraph, Kit_Node_t * pNode ) { return pNode - pGraph->pNodes; }
- static inline int Kit_GraphNodeIsVar( Kit_Graph_t * pGraph, Kit_Node_t * pNode ) { return Kit_GraphNodeInt(pGraph,pNode) < pGraph->nLeaves; }
--static inline Kit_Node_t * Kit_GraphVar( Kit_Graph_t * pGraph ) { assert( Kit_GraphIsVar( pGraph ) ); return Kit_GraphNode( pGraph, pGraph->eRoot.Node ); }
-+static inline Kit_Node_t * Kit_GraphVar( Kit_Graph_t * pGraph ) { assert( Kit_GraphIsVar( pGraph ) ); return Kit_GraphNode( pGraph, pGraph->eRoot.edgeBits.Node ); }
- static inline int Kit_GraphVarInt( Kit_Graph_t * pGraph ) { assert( Kit_GraphIsVar( pGraph ) ); return Kit_GraphNodeInt( pGraph, Kit_GraphVar(pGraph) ); }
--static inline Kit_Node_t * Kit_GraphNodeFanin0( Kit_Graph_t * pGraph, Kit_Node_t * pNode ){ return Kit_GraphNodeIsVar(pGraph, pNode)? NULL : Kit_GraphNode(pGraph, pNode->eEdge0.Node); }
--static inline Kit_Node_t * Kit_GraphNodeFanin1( Kit_Graph_t * pGraph, Kit_Node_t * pNode ){ return Kit_GraphNodeIsVar(pGraph, pNode)? NULL : Kit_GraphNode(pGraph, pNode->eEdge1.Node); }
--static inline int Kit_GraphRootLevel( Kit_Graph_t * pGraph ) { return Kit_GraphNode(pGraph, pGraph->eRoot.Node)->Level; }
-+static inline Kit_Node_t * Kit_GraphNodeFanin0( Kit_Graph_t * pGraph, Kit_Node_t * pNode ){ return Kit_GraphNodeIsVar(pGraph, pNode)? NULL : Kit_GraphNode(pGraph, pNode->eEdge0.edgeBits.Node); }
-+static inline Kit_Node_t * Kit_GraphNodeFanin1( Kit_Graph_t * pGraph, Kit_Node_t * pNode ){ return Kit_GraphNodeIsVar(pGraph, pNode)? NULL : Kit_GraphNode(pGraph, pNode->eEdge1.edgeBits.Node); }
-+static inline int Kit_GraphRootLevel( Kit_Graph_t * pGraph ) { return Kit_GraphNode(pGraph, pGraph->eRoot.edgeBits.Node)->Level; }
+ static inline int Kit_GraphIsConst0( Kit_Graph_t * pGraph ) { return pGraph->fConst && pGraph->eRoot.fCompl; }
+@@ -228,8 +231,6 @@ static inline Kit_Node_t * Kit_GraphNodeFanin0( Kit_Graph_t * pGraph, Kit_Node_t
+ 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 int Kit_Float2Int( float Val ) { return *((int *)&Val); }
-static inline float Kit_Int2Float( int Num ) { return *((float *)&Num); }
static inline int Kit_BitWordNum( int nBits ) { return nBits/(8*sizeof(unsigned)) + ((nBits%(8*sizeof(unsigned))) > 0); }
static inline int Kit_TruthWordNum( int nVars ) { return nVars <= 5 ? 1 : (1 << (nVars - 5)); }
static inline unsigned Kit_BitMask( int nBits ) { assert( nBits <= 32 ); return ~((~(unsigned)0) << nBits); }
-@@ -486,6 +487,18 @@ static inline void Kit_TruthIthVar( unsi
+@@ -486,6 +487,18 @@ static inline void Kit_TruthIthVar( unsigned * pTruth, int nVars, int iVar )
/// FUNCTION DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
@@ -388,79 +91,23 @@
#if 0
/*=== kitBdd.c ==========================================================*/
---- ./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
- {
-- for (int i=0; i < $3;i++)
-+ for (unsigned int i=0; i < $3;i++)
- {
- parserInterface->push();
- }
-@@ -247,7 +247,7 @@ cmdi:
- }
- | LPAREN_TOK POP_TOK NUMERAL_TOK RPAREN_TOK
- {
-- for (int i=0; i < $3;i++)
-+ for (unsigned int i=0; i < $3;i++)
- parserInterface->pop();
- parserInterface->success();
- }
-@@ -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.
-- for (int i = 0; i < $3->size(); i++)
-+ for (size_t i = 0; i < $3->size(); i++)
- BEEV::parserInterface->removeSymbol((*$3)[i]);
-
- delete $1;
-@@ -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.
-- for (int i = 0; i < $3->size(); i++)
-+ for (size_t i = 0; i < $3->size(); i++)
- BEEV::parserInterface->removeSymbol((*$3)[i]);
-
- delete $1;
---- ./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 = "";
-
-- 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/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 = "";
-
-- 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/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;
+diff --git a/src/interface/C/c_interface.cpp b/src/interface/C/c_interface.cpp
+index ee838d1..8179d57 100644
+--- a/src/interface/C/c_interface.cpp
++++ b/src/interface/C/c_interface.cpp
+@@ -994,7 +994,7 @@ Expr vc_bvConstExprFromInt(VC vc,
+ bmstar b = (bmstar)(((stpstar)vc)->bm);
-- 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/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
+ 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: "\
+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;
@@ -469,410 +116,10 @@
}
---- ./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());
-
-- 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())
-@@ -499,7 +499,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);
-@@ -512,7 +512,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)
-@@ -520,13 +520,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);
-@@ -601,7 +601,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)
- {
-@@ -617,7 +617,7 @@ namespace BEEV
- if (CONSTANTBV::Set_Max(max) >= 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;
-@@ -690,7 +690,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)
- {
-@@ -719,7 +719,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);
-@@ -736,7 +736,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);
-@@ -757,7 +757,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;
-@@ -766,7 +766,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();
- }
- }
-@@ -799,10 +799,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/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:
- case OR:
-- for (int i =0; i < n.Degree(); i ++)
-+ for (size_t i =0; i < n.Degree(); i ++)
- build(n[i],polarity);
- break;
-
-@@ -122,7 +122,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/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());
-
-- 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/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;
- if (k == XOR)
-- for (int i = 0; i < lhs.Degree(); i++)
-+ for (size_t i = 0; i < lhs.Degree(); i++)
- {
- ASTVec others;
-- for (int j = 0; j < lhs.Degree(); j++)
-+ for (size_t j = 0; j < lhs.Degree(); j++)
- if (j != i)
- others.push_back(lhs[j]);
-
-@@ -77,10 +77,10 @@ namespace BEEV
- return searchTerm(lhs[0], nf->CreateTerm(BVNEG, width, rhs));
-
- if (lhs.GetKind() == BVXOR || lhs.GetKind() == BVPLUS)
-- for (int i = 0; i < lhs.Degree(); i++)
-+ for (size_t i = 0; i < lhs.Degree(); i++)
- {
- ASTVec others;
-- for (int j = 0; j < lhs.Degree(); j++)
-+ for (size_t j = 0; j < lhs.Degree(); j++)
- if (j != i)
- others.push_back(lhs[j]);
-
---- ./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)
- {
-- for (int i =0; i < children.size(); i++)
-+ for (size_t i =0; i < children.size(); i++)
- if (!children[i]->isUnconstrained())
- return false;
-
-@@ -100,7 +100,7 @@ namespace BEEV
- // Going to be rebuilt later anyway, so discard.
- vector<MutableASTNode*> variables;
-
-- for (int i =0; i <extracts.size(); i++)
-+ for (size_t i =0; i <extracts.size(); i++)
- {
- ASTNode& var = extracts[i]->n;
- assert(var.GetKind() == SYMBOL);
-@@ -151,7 +151,7 @@ namespace BEEV
- }
-
- ASTNode concat = concatVec[0];
-- for (int i=1; i < concatVec.size();i++)
-+ for (size_t i=1; i < concatVec.size();i++)
- {
- assert(!concat.IsNull());
- concat = bm.CreateTerm(BVCONCAT, concat.GetValueWidth() + concatVec[i].GetValueWidth(),concatVec[i], concat);
-@@ -184,7 +184,7 @@ namespace BEEV
-
- topMutable->getAllUnconstrainedVariables(variable_array);
-
-- for (int i =0; i < variable_array.size() ; i++)
-+ for (size_t i =0; i < variable_array.size() ; i++)
- {
- // Don't make this is a reference. If the vector gets resized, it will point to
- // memory that no longer contains the object.
-@@ -208,7 +208,7 @@ namespace BEEV
- //nb. The children might be dirty. i.e. not have substitutions written through them yet.
- ASTVec children;
- children.reserve(mutable_children.size());
-- for (int j = 0; j <mutable_children.size(); j++ )
-+ for (size_t j = 0; j <mutable_children.size(); j++ )
- children.push_back(mutable_children[j]->n);
-
- const size_t numberOfChildren = children.size();
-@@ -242,7 +242,7 @@ namespace BEEV
- {
- int found = 0;
-
-- for (int i = 0; i < numberOfChildren; i++)
-+ for (size_t i = 0; i < numberOfChildren; i++)
- {
- if (children[i] == var)
- found++;
-@@ -429,7 +429,7 @@ namespace BEEV
- {
- ASTNodeSet already;
- ASTNode v =replaceParentWithFresh(muteParent, variable_array);
-- for (int i =0; i < numberOfChildren;i++)
-+ for (size_t i =0; i < numberOfChildren;i++)
- {
- /* to avoid problems with:
- 734:(AND
-@@ -464,7 +464,7 @@ namespace BEEV
- ASTNode v =replaceParentWithFresh(muteParent, variable_array);
-
- ASTVec others;
-- for (int i = 0; i < numberOfChildren; i++)
-+ for (size_t i = 0; i < numberOfChildren; i++)
- {
- if (children[i] !=var)
- others.push_back(mutable_children[i]->toASTNode(nf));
-@@ -617,7 +617,7 @@ namespace BEEV
- case BVPLUS:
- {
- ASTVec other;
-- for (int i = 0; i < children.size(); i++)
-+ for (size_t i = 0; i < children.size(); i++)
- if (children[i] != var)
- other.push_back(mutable_children[i]->toASTNode(nf));
-
---- ./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);
- }
-
-- for (int i = 0; i < n.Degree(); i++)
-+ for (size_t i = 0; i < n.Degree(); i++)
- {
- checkIfInSimplifyMap(n[i], visited);
- }
+diff --git a/src/simplifier/simplifier.cpp b/src/simplifier/simplifier.cpp
+index b309a8a..5bd000f 100644
+--- a/src/simplifier/simplifier.cpp
++++ b/src/simplifier/simplifier.cpp
@@ -523,6 +523,7 @@ namespace BEEV
return getConstantBit(n[0], i);
@@ -881,163 +128,10 @@
}
ASTNode
-@@ -1302,7 +1303,7 @@ namespace BEEV
- else
- {
- ASTVec newC;
-- for (int i = 0; i < a.GetChildren().size(); i++)
-+ for (size_t i = 0; i < a.GetChildren().size(); i++)
- {
- newC.push_back(SimplifyFormula(a[i], false, VarConstMap));
- }
-@@ -1664,9 +1665,9 @@ namespace BEEV
- assert(BVMULT == k || SBVDIV == k || BVPLUS ==k);
- const int inputValueWidth = output.GetValueWidth();
-
-- int lengthA = output.GetChildren()[0][0].GetValueWidth();
-- int lengthB = output.GetChildren()[1][0].GetValueWidth();
-- int maxLength;
-+ unsigned int lengthA = output.GetChildren()[0][0].GetValueWidth();
-+ unsigned int lengthB = output.GetChildren()[1][0].GetValueWidth();
-+ unsigned int maxLength;
- if (BVMULT == output.GetKind())
- maxLength = lengthA + lengthB;
- else if (BVPLUS == output.GetKind() || SBVDIV == output.GetKind())
-@@ -1694,7 +1695,7 @@ namespace BEEV
- {
- const ASTNode a = children[0];
- const ASTNode b = children[1];
-- const int width = children[0].GetValueWidth();
-+ const unsigned int width = children[0].GetValueWidth();
- ASTNode output;
-
- assert(b.isConstant());
-@@ -1725,7 +1726,7 @@ namespace BEEV
- {
- const ASTNode a = children[0];
- const ASTNode b = children[1];
-- const int width = children[0].GetValueWidth();
-+ const unsigned int width = children[0].GetValueWidth();
- ASTNode output;
-
- assert(b.isConstant());
-@@ -1906,7 +1907,7 @@ namespace BEEV
- //I haven't measured if this is worth the expense.
- {
- bool notSimplified = false;
-- for (int i = 0; i < inputterm.Degree(); i++)
-+ for (size_t i = 0; i < inputterm.Degree(); i++)
- if (inputterm[i].GetType() != ARRAY_TYPE)
- if (!hasBeenSimplified(inputterm[i]))
- {
-@@ -2658,7 +2659,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.
-@@ -2680,13 +2681,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;
-@@ -2703,7 +2704,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/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
+diff --git a/src/to-sat/ASTNode/ToSAT.cpp b/src/to-sat/ASTNode/ToSAT.cpp
+index 0b01b77..05ba88d 100644
+--- a/src/to-sat/ASTNode/ToSAT.cpp
++++ b/src/to-sat/ASTNode/ToSAT.cpp
@@ -53,7 +53,7 @@ namespace BEEV
// Copies the symbol into the map that is used to build the counter example.
@@ -1047,71 +141,3 @@
{
const ASTNode& symbol = n.GetKind() == BOOLEXTRACT ? n[0] : n;
const unsigned index = n.GetKind() == BOOLEXTRACT ? n[1].GetUnsignedConst() : 0;
-@@ -313,7 +313,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/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());
- assert(ms->r.getWidth() == (int)ms->bitWidth);
-- }
-
-- for (int i = 0; i < n.GetValueWidth(); i++)
-- if (ms->sumH[i] == 0)
-- highestZero = i;
-+ for (unsigned int i = 0; i < n.GetValueWidth(); i++)
-+ if (ms->sumH[i] == 0)
-+ highestZero = i;
-
-- return ms;
-+ return ms;
-+ }
- }
-
- return NULL;
-@@ -1831,22 +1831,24 @@ namespace BEEV
- for (int i = 0; i < b->getWidth(); i++)
- {
- if (b->isFixed(i))
-- if (b->getValue(i))
-- {
-- assert(v[i]== BBTrue);
-- }
-- else
-- {
-- if (v[i] != BBFalse)
-+ {
-+ if (b->getValue(i))
- {
-- cerr << *b;
-- cerr << i << endl;
-- cerr << n;
-- cerr << (v[i] == BBTrue) << endl;
-+ assert(v[i]== BBTrue);
- }
-+ else
-+ {
-+ if (v[i] != BBFalse)
-+ {
-+ cerr << *b;
-+ cerr << i << endl;
-+ cerr << n;
-+ cerr << (v[i] == BBTrue) << endl;
-+ }
-
-- assert(v[i]== BBFalse);
-- }
-+ assert(v[i]== BBFalse);
-+ }
-+ }
- }
- }
- }
diff --git a/stp.spec b/stp.spec
index 5f68439..e3d3433 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 20140402
-%global gittag f8a392dea3e6942897e2213e13f23cf99d323ef4
+%global gitdate 20140619
+%global gittag 44de620db195122e812e81940c8edef947c18765
%global shorttag %(cut -b -7 <<< %{gittag})
%global user stp
Name: stp
Version: 0.1
-Release: 22.%{gitdate}git.%{shorttag}%{?dist}
+Release: 23.%{gitdate}git.%{shorttag}%{?dist}
Summary: Constraint solver/decision procedure
Group: Applications/Engineering
@@ -20,8 +20,6 @@ Patch0: %{name}-unbundle.patch
# This patch has not yet been sent upstream. Fix a bunch of compiler warnings
# that may indicate miscompiled code.
Patch1: %{name}-warning.patch
-# This patch has not yet been sent upstream. Eliminate undefined symbols.
-Patch2: %{name}-undefined.patch
BuildRequires: bison
BuildRequires: boost-devel
@@ -62,7 +60,6 @@ or automated prover). Provides a static library.
%setup -q -n %{user}-%{name}-%{shorttag}
%patch0 -p1
%patch1 -p1
-%patch2 -p1
# Make sure nothing uses the shipped cryptominisat sources
rm -fr src/sat/cryptominisat2
@@ -71,18 +68,18 @@ rm -fr src/sat/cryptominisat2
sed -i "s/-Wno-deprecated/& -Wno-reorder/" CMakeLists.txt
%build
-%cmake
+%cmake -DALSO_BUILD_STATIC_LIB=0
make %{?_smp_mflags}
%install
make install DESTDIR=%{buildroot}
# Fix up the libdir install on 64-bit targets
-if [ %{__isa_bits} = "64" ]; then
- mkdir %{buildroot}%{_libdir}
- mv %{buildroot}%{_prefix}/lib/cmake %{buildroot}%{_libdir}
- mv %{buildroot}%{_prefix}/lib/libstp.so %{buildroot}%{_libdir}
-fi
+%if %{__isa_bits} == 64
+mkdir %{buildroot}%{_libdir}
+mv %{buildroot}%{_prefix}/lib/cmake %{buildroot}%{_libdir}
+mv %{buildroot}%{_prefix}/lib/libstp.so %{buildroot}%{_libdir}
+%endif
%files
%{_bindir}/*
@@ -94,6 +91,10 @@ fi
%{_libdir}/cmake/STP/
%changelog
+* Wed Jun 18 2014 Jerry James <loganjerry at gmail.com> - 0.1-23.20140619git.44de620
+- Update to recent git snapshot
+- Drop upstreamed -undefined patch
+
* Sun Jun 08 2014 Fedora Release Engineering <rel-eng at lists.fedoraproject.org> - 0.1-22.20140402git.f8a392d
- Rebuilt for https://fedoraproject.org/wiki/Fedora_21_Mass_Rebuild
More information about the scm-commits
mailing list