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-undefined.patch b/stp-undefined.patch deleted file mode 100644 index a5f305e..0000000 --- a/stp-undefined.patch +++ /dev/null @@ -1,80 +0,0 @@ -diff --git a/src/extlib-abc/aig/aig/aigPart.c b/src/extlib-abc/aig/aig/aigPart.c -index a4cc116..c486a11 100644 ---- a/src/extlib-abc/aig/aig/aigPart.c -+++ b/src/extlib-abc/aig/aig/aigPart.c -@@ -871,10 +871,6 @@ Vec_Ptr_t * Aig_ManMiterPartitioned( Aig_Man_t * p1, Aig_Man_t * p2, int nPartSi - ***********************************************************************/ - Aig_Man_t * Aig_ManChoicePartitioned( Vec_Ptr_t * vAigs, int nPartSize ) - { -- extern int Cmd_CommandExecute( void * pAbc, char * sCommand ); -- extern void * Abc_FrameGetGlobalFrame(); -- extern Aig_Man_t * Fra_FraigChoice( Aig_Man_t * pManAig, int nConfMax ); -- - Vec_Ptr_t * vOutsTotal, * vOuts; - Aig_Man_t * pAigTotal, * pAigPart, * pAig; - Vec_Int_t * vPart, * vPartSupp; -@@ -898,8 +894,6 @@ Aig_Man_t * Aig_ManChoicePartitioned( Vec_Ptr_t * vAigs, int nPartSize ) - Aig_ManForEachPi( pAig, pObj, k ) - pObj->pNext = (Aig_Obj_t *)(long)k; - -- Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), "unset progressbar" ); -- - // create the total fraiged AIG - vPartSupp = Vec_IntAlloc( 100 ); // maps part PI num into total PI num - Vec_PtrForEachEntry( vParts, vPart, i ) -@@ -936,7 +930,7 @@ Aig_Man_t * Aig_ManChoicePartitioned( Vec_Ptr_t * vAigs, int nPartSize ) - i+1, Vec_PtrSize(vParts), Aig_ManPiNum(pAigPart), Aig_ManPoNum(pAigPart), - Aig_ManNodeNum(pAigPart), Aig_ManLevelNum(pAigPart) ); - // compute equivalence classes (to be stored in pNew->pReprs) -- pAig = Fra_FraigChoice( pAigPart, 1000 ); -+ pAig = NULL; - Aig_ManStop( pAig ); - // reset the pData pointers - Aig_ManForEachObj( pAigPart, pObj, k ) -@@ -951,8 +945,6 @@ Aig_Man_t * Aig_ManChoicePartitioned( Vec_Ptr_t * vAigs, int nPartSize ) - Vec_VecFree( (Vec_Vec_t *)vParts ); - Vec_IntFree( vPartSupp ); - -- Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), "set progressbar" ); -- - // clear the PI numbers - Vec_PtrForEachEntry( vAigs, pAig, i ) - Aig_ManForEachPi( pAig, pObj, k ) -diff --git a/src/extlib-abc/aig/aig/aigShow.c b/src/extlib-abc/aig/aig/aigShow.c -index a88f493..34b26ef 100644 ---- a/src/extlib-abc/aig/aig/aigShow.c -+++ b/src/extlib-abc/aig/aig/aigShow.c -@@ -328,7 +328,6 @@ void Aig_WriteDotAig( Aig_Man_t * pMan, char * pFileName, int fHaig, Vec_Ptr_t * - ***********************************************************************/ - void Aig_ManShow( Aig_Man_t * pMan, int fHaig, Vec_Ptr_t * vBold ) - { -- extern void Abc_ShowFile( char * FileNameDot ); - static int Counter = 0; - char FileNameDot[200]; - FILE * pFile; -@@ -344,8 +343,6 @@ void Aig_ManShow( Aig_Man_t * pMan, int fHaig, Vec_Ptr_t * vBold ) - fclose( pFile ); - // generate the file - Aig_WriteDotAig( pMan, FileNameDot, fHaig, vBold ); -- // visualize the file -- Abc_ShowFile( FileNameDot ); - } - - -diff --git a/src/extlib-abc/aig/kit/kitGraph.c b/src/extlib-abc/aig/kit/kitGraph.c -index 1ae5891..f6ea2ca 100644 ---- a/src/extlib-abc/aig/kit/kitGraph.c -+++ b/src/extlib-abc/aig/kit/kitGraph.c -@@ -20,6 +20,12 @@ - - #include "kit.h" - -+Kit_Graph_t *Kit_SopFactor( Vec_Int_t * vCover, int fCompl, int nVars, -+ Vec_Int_t * vMemory ) -+{ -+ return NULL; -+} -+ - //////////////////////////////////////////////////////////////////////// - /// DECLARATIONS /// - //////////////////////////////////////////////////////////////////////// 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 vec = v_a.size() == 0 ? v_b : v_a; -@@ -217,7 +217,7 @@ namespace BEEV - void - applyAxiomsToSolver(ToSATBase::ASTNodeToSATVar & satVar, vector & 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 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 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); +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); - // 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; - -- 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 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 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 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 variables; - -- for (int i =0; 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 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 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 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 - 0.1-23.20140619git.44de620 +- Update to recent git snapshot +- Drop upstreamed -undefined patch + * Sun Jun 08 2014 Fedora Release Engineering - 0.1-22.20140402git.f8a392d - Rebuilt for https://fedoraproject.org/wiki/Fedora_21_Mass_Rebuild