From 826d0abd7fe3043ca4304efa7639ee6a99210581 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Fri, 4 Sep 2015 10:14:38 -0600 Subject: [PATCH] Update to recent git snapshot. --- .gitignore | 1 + sources | 2 +- stp-unbundle.patch | 213 --------------------------------------------- stp-warning.patch | 143 ------------------------------ stp.spec | 70 +++++++++------ 5 files changed, 47 insertions(+), 382 deletions(-) delete mode 100644 stp-unbundle.patch delete mode 100644 stp-warning.patch diff --git a/.gitignore b/.gitignore index 3569748..c9ca4c9 100644 --- a/.gitignore +++ b/.gitignore @@ -1 +1,2 @@ /stp-stp-44de620.tar.gz +/stp-stp-5405af4.tar.gz diff --git a/sources b/sources index db2a34f..db254aa 100644 --- a/sources +++ b/sources @@ -1 +1 @@ -3744bde4e5a1d5108506adf1c929563d stp-stp-44de620.tar.gz +9cfefa8cda293105506e5a8f3ed7c6b2 stp-stp-5405af4.tar.gz diff --git a/stp-unbundle.patch b/stp-unbundle.patch deleted file mode 100644 index 6b1f268..0000000 --- a/stp-unbundle.patch +++ /dev/null @@ -1,213 +0,0 @@ -diff --git a/CMakeLists.txt b/CMakeLists.txt -index a43eb68..c0db102 100644 ---- a/CMakeLists.txt -+++ b/CMakeLists.txt -@@ -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_GNUCPP11) -@@ -219,6 +220,7 @@ include_directories(${Boost_INCLUDE_DIRS}) - - find_package(BISON REQUIRED) - find_package(FLEX REQUIRED) -+find_package(Cryptominisat REQUIRED) - - # ----------------------------------------------------------------------------- - # Setup library build path (this is **not** the library install path) -diff --git a/cmake/modules/FindCryptominisat.cmake b/cmake/modules/FindCryptominisat.cmake -new file mode 100644 -index 0000000..e900145 ---- /dev/null -+++ b/cmake/modules/FindCryptominisat.cmake -@@ -0,0 +1,32 @@ -+# - Find cryptominisat -+# Find the cryptominisat library -+# -+# This module defines the following variables: -+# CRYPTOMINISAT_FOUND - True if _INCLUDE_DIR & _LIBRARY are found -+# CRYPTOMINISAT_LIBRARIES - Set when CRYPTOMINISAT_LIBRARY is found -+# CRYPTOMINISAT_INCLUDE_DIRS - Set when CRYPTOMINISAT_INCLUDE_DIR is found -+# -+# CRYPTOMINISAT_INCLUDE_DIR - where to find Solver.h, etc. -+# CRYPTOMINISAT_LIBRARY - the cryptominisat library -+# -+ -+find_path(CRYPTOMINISAT_INCLUDE_DIR NAMES cmsat/Solver.h -+ DOC "The cryptominisat include directory" -+) -+ -+find_library(CRYPTOMINISAT_LIBRARY NAMES cryptominisat -+ DOC "The cryptominisat library" -+) -+ -+# handle the QUIETLY and REQUIRED arguments and set CRYPTOMINISAT_FOUND to -+# TRUE if all listed variables are TRUE -+find_package_handle_standard_args(CRYPTOMINISAT DEFAULT_MSG -+ CRYPTOMINISAT_LIBRARY -+ CRYPTOMINISAT_INCLUDE_DIR) -+ -+if(CRYPTOMINISAT_FOUND) -+ set( CRYPTOMINISAT_LIBRARIES ${CRYPTOMINISAT_LIBRARY} ) -+ set( CRYPTOMINISAT_INCLUDE_DIRS ${CRYPTOMINISAT_INCLUDE_DIR} ) -+endif() -+ -+mark_as_advanced(CRYPTOMINISAT_INCLUDE_DIR CRYPTOMINISAT_LIBRARY) -diff --git a/src/AST/RunTimes.cpp b/src/AST/RunTimes.cpp -index 7912aeb..cf646b4 100644 ---- a/src/AST/RunTimes.cpp -+++ b/src/AST/RunTimes.cpp -@@ -13,7 +13,7 @@ - #include - #include - #include "RunTimes.h" --#include "../sat/cryptominisat2/time_mem.h" -+#include - - // BE VERY CAREFUL> Update the Category Names to match. - std::string RunTimes::CategoryNames[] = { "Transforming", "Simplifying", "Parsing", "CNF Conversion", "Bit Blasting", "SAT Solving", "Bitvector Solving","Variable Elimination", "Sending to SAT Solver", "Counter Example Generation","SAT Simplification", "Constant Bit Propagation","Array Read Refinement", "Applying Substitutions", "Removing Unconstrained", "Pure Literals" , "ITE Contexts", "AIG core simplification", "Interval Propagation", "Always True"}; -@@ -67,7 +67,7 @@ void RunTimes::print() - std::cerr.precision(2); - std::cerr << "Statistics Total: " << ((double)cummulative_ms)/1000 << "s" << std::endl; - std::cerr << "CPU Time Used : " << cpuTime() << "s" << std::endl; -- std::cerr << "Peak Memory Used: " << memUsedPeak()/(1024.0*1024.0) << "MB" << std::endl; -+ std::cerr << "Peak Memory Used: " << memUsed()/(1024.0*1024.0) << "MB" << std::endl; - - clear(); - -diff --git a/src/AST/RunTimes.h b/src/AST/RunTimes.h -index 191711e..9a44acd 100644 ---- a/src/AST/RunTimes.h -+++ b/src/AST/RunTimes.h -@@ -18,7 +18,7 @@ - #include - #include - #include --#include "../sat/cryptominisat2/time_mem.h" -+#include - - class RunTimes : boost::noncopyable - { -diff --git a/src/libstp/CMakeLists.txt b/src/libstp/CMakeLists.txt -index 8ad9ccb..045b8ac 100644 ---- a/src/libstp/CMakeLists.txt -+++ b/src/libstp/CMakeLists.txt -@@ -13,7 +13,6 @@ set(stp_lib_targets - tosat - sat - minisat2 -- cryptominisat2 - simplifier - constantbv - abc -@@ -74,7 +73,7 @@ endif() - # Clients of libstp that don't use CMake will have to link the Boost libraries - # in manually. - # ----------------------------------------------------------------------------- --target_link_libraries(libstp ${Boost_LIBRARIES}) -+target_link_libraries(libstp ${Boost_LIBRARIES} cryptominisat) - - - # ----------------------------------------------------------------------------- -diff --git a/src/sat/CMakeLists.txt b/src/sat/CMakeLists.txt -index 4749a77..ffb169e 100644 ---- a/src/sat/CMakeLists.txt -+++ b/src/sat/CMakeLists.txt -@@ -1,4 +1,3 @@ --add_subdirectory(cryptominisat2) - add_subdirectory(minisat) - - add_library(sat OBJECT -diff --git a/src/sat/CryptoMinisat.cpp b/src/sat/CryptoMinisat.cpp -index 8646824..0d77ff5 100644 ---- a/src/sat/CryptoMinisat.cpp -+++ b/src/sat/CryptoMinisat.cpp -@@ -7,15 +7,26 @@ - #undef l_Undef - - --#include "cryptominisat2/Solver.h" --#include "cryptominisat2/SolverTypes.h" -+#include -+#include - - namespace BEEV - { -+ class CryptoMinisatSolver : public CMSat::Solver -+ { -+ public: -+ uint64_t getConflicts() const { return conflicts; } -+ uint64_t getDecisions() const { return decisions; } -+ uint64_t getMaxLiterals() const { return max_literals; } -+ uint64_t getPropagations() const { return propagations; } -+ uint64_t getRndDecisions() const { return rnd_decisions; } -+ uint64_t getStarts() const { return starts; } -+ uint64_t getTotLiterals() const { return tot_literals; } -+ }; - - CryptoMinisat::CryptoMinisat() - { -- s = new MINISAT::Solver(); -+ s = new CryptoMinisatSolver(); - } - - CryptoMinisat::~CryptoMinisat() -@@ -30,9 +41,9 @@ namespace BEEV - // Cryptominisat uses a slightly different Lit class too. - - // VERY SLOW> -- MINISAT::vec v; -+ CMSat::vec v; - for (int i =0; iaddClause(v); - } -@@ -63,7 +74,7 @@ namespace BEEV - - void CryptoMinisat::setVerbosity(int v) - { -- s->verbosity = v; -+ s->conf.verbosity = v; - } - - int CryptoMinisat::nVars() -diff --git a/src/sat/CryptoMinisat.h b/src/sat/CryptoMinisat.h -index 76e7a47..9ecb5b6 100644 ---- a/src/sat/CryptoMinisat.h -+++ b/src/sat/CryptoMinisat.h -@@ -6,16 +6,13 @@ - - #include "SATSolver.h" - --namespace MINISAT --{ -- class Solver; --} -- - namespace BEEV - { -+ class CryptoMinisatSolver; -+ - class CryptoMinisat : public SATSolver - { -- MINISAT::Solver* s; -+ CryptoMinisatSolver* s; - - public: - CryptoMinisat(); -diff --git a/tests/api/C/CMakeLists.txt b/tests/api/C/CMakeLists.txt -index dcdcc3d..e0146a8 100644 ---- a/tests/api/C/CMakeLists.txt -+++ b/tests/api/C/CMakeLists.txt -@@ -1,4 +1,6 @@ - AddGTestSuite(C-api-tests) -+find_library(cryptominisat) -+find_library(m) - - # ----------------------------------------------------------------------------- - # Find the public headers associated with libstp diff --git a/stp-warning.patch b/stp-warning.patch deleted file mode 100644 index 468f1e4..0000000 --- a/stp-warning.patch +++ /dev/null @@ -1,143 +0,0 @@ -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; - } -- else if (v_a.size() == 0 ^ v_b.size() == 0) -+ else if ((v_a.size() == 0) ^ (v_b.size() == 0)) - { - ASTNode constant = a.isConstant() ? a : b; - vector vec = v_a.size() == 0 ? v_b : v_a; -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_ --{ -- 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 -+ }; -+ unsigned int edgeInt; - }; - - typedef struct Kit_Node_t_ Kit_Node_t; -@@ -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 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_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 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; } -@@ -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( unsigned * pTruth, int nVars, int iVar ) - /// FUNCTION DECLARATIONS /// - //////////////////////////////////////////////////////////////////////// - -+extern Kit_Graph_t * Kit_GraphCreateConst0( void ); -+extern Kit_Graph_t * Kit_GraphCreateConst1( void ); -+extern void Kit_GraphFree( Kit_Graph_t * ); -+extern Kit_Graph_t * Kit_SopFactor( Vec_Int_t *, int, int, Vec_Int_t * ); -+extern void Kit_TruthCofactor0( unsigned *, int, int ); -+extern void Kit_TruthCofactor1( unsigned *, int, int ); -+extern int Kit_TruthIsop( unsigned *, int, Vec_Int_t *, int ); -+extern void Kit_TruthShrink( unsigned *, unsigned *, int, int, unsigned, int ); -+extern void Kit_TruthStretch( unsigned *, unsigned *, int, int, unsigned, int ); -+extern Kit_Graph_t * Kit_TruthToGraph( unsigned *, int, Vec_Int_t * ); -+extern int Kit_TruthVarInSupport( unsigned *, int, int ); -+ - #if 0 - - /*=== kitBdd.c ==========================================================*/ -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); - - 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; - } -+ return true; - } - - -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); - - assert(false); -+ return -1; - } - - ASTNode -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. - // For boolean we create a vector of size 1. -- if (n.GetKind() == BOOLEXTRACT && n[0].GetKind() == SYMBOL || (n.GetKind() == SYMBOL && !isTseitinVariable(n))) -+ if ((n.GetKind() == BOOLEXTRACT && n[0].GetKind() == SYMBOL) || (n.GetKind() == SYMBOL && !isTseitinVariable(n))) - { - const ASTNode& symbol = n.GetKind() == BOOLEXTRACT ? n[0] : n; - const unsigned index = n.GetKind() == BOOLEXTRACT ? n[1].GetUnsignedConst() : 0; diff --git a/stp.spec b/stp.spec index 6864256..a134bf5 100644 --- a/stp.spec +++ b/stp.spec @@ -1,32 +1,30 @@ -# Upstream occasionally releases a subversion snapshot, but no "regular" -# releases since the 0.1 release. -%global gitdate 20140619 -%global gittag 44de620db195122e812e81940c8edef947c18765 +# Upstream occasionally releases a git snapshot, but no "regular" releases +# since the 0.1 release. +%global gitdate 20150904 +%global gittag 5405af464b79800b49a14f3151f082ff4ad714ba %global shorttag %(cut -b -7 <<< %{gittag}) %global user stp Name: stp -Version: 0.1 -Release: 30.%{gitdate}git.%{shorttag}%{?dist} +Version: 2.1.0 +Release: 1.%{gitdate}git.%{shorttag}%{?dist} Summary: Constraint solver/decision procedure -Group: Applications/Engineering License: MIT -URL: http://stp.github.io/stp/ +URL: http://stp.github.io/ Source0: https://github.com/%{user}/%{name}/tarball/%{gittag}/%{user}-%{name}-%{shorttag}.tar.gz -# This patch is specific to Fedora. Use the existing cryptominisat library -# instead of the bundled version. -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 BuildRequires: bison BuildRequires: boost-devel BuildRequires: cmake +BuildRequires: cryptominisat BuildRequires: cryptominisat-devel +BuildRequires: cryptominisat4 +BuildRequires: cryptominisat4-devel +BuildRequires: minisat2-devel BuildRequires: flex -BuildRequires: python2 +BuildRequires: perl(Getopt::Long) +BuildRequires: python2-devel %description STP (Simple Theorem Prover) is a constraint solver (also referred to as @@ -48,7 +46,6 @@ Additional information can be found at: %package devel Summary: Development files for STP constraint solver/decision procedure -Group: Applications/Engineering Requires: %{name}%{?_isa} = %{version}-%{release} %description devel @@ -56,20 +53,36 @@ Development files for the STP (Simple Theorem Prover), a constraint solver (also referred to as a decision procedure or automated prover). Provides a static library. +%package -n python-%{name} +Summary: Python 2 interface to STP +Requires: %{name} = %{version}-%{release} +BuildArch: noarch + +%description -n python-%{name} +Python 2 interface to STP. + %prep %setup -q -n %{user}-%{name}-%{shorttag} -%patch0 -p1 -%patch1 -p1 -# Make sure nothing uses the shipped cryptominisat sources -rm -fr src/sat/cryptominisat2 +# We do not want to know about the order of member initializers, and add the +# minisat include directory +sed -e "s/-Wno-deprecated/-Wno-reorder/" \ + -e 's,\${PROJECT_SOURCE_DIR}/lib/Sat,&\n %{_includedir}/minisat,' \ + -i CMakeLists.txt -# We do not want to know about the order of member initializers -sed -i "s/-Wno-deprecated/& -Wno-reorder/" CMakeLists.txt +# Prevent a clash between minisat and cryptominisat4 definitions +sed '/SATSolver.h/a#undef var_Undef\n#undef l_True\n#undef l_False\n#undef l_Undef' \ + -i.orig include/stp/Sat/CryptoMinisat4.h +touch -r include/stp/Sat/CryptoMinisat4.h.orig include/stp/Sat/CryptoMinisat4.h +rm -f include/stp/Sat/CryptoMinisat4.h.orig %build +export CFLAGS="%{optflags} -I %{_includedir}/minisat" +export CXXFLAGS="%{optflags} -I %{_includedir}/minisat" +export LDFLAGS="-Wl,--as-needed $RPM_LD_FLAGS" %cmake -DALSO_BUILD_STATIC_LIB=0 -make %{?_smp_mflags} +# FIXME: %%{?_smp_mflags} doesn't work due to running genkinds.pl too late +make %install make install DESTDIR=%{buildroot} @@ -78,20 +91,27 @@ make install DESTDIR=%{buildroot} if [ "%{_libdir}" != "%{_prefix}/lib" ]; then mkdir %{buildroot}%{_libdir} mv %{buildroot}%{_prefix}/lib/cmake %{buildroot}%{_libdir} - mv %{buildroot}%{_prefix}/lib/libstp.so %{buildroot}%{_libdir} + mv %{buildroot}%{_prefix}/lib/libstp.so* %{buildroot}%{_libdir} fi %files %{_bindir}/* -%{_libdir}/libstp.so +%{_libdir}/libstp.so.* %doc AUTHORS README.markdown papers %license LICENSE LICENSE_COMPONENTS %files devel %{_includedir}/stp/ %{_libdir}/cmake/STP/ +%{_libdir}/libstp.so + +%files -n python-%{name} +%{python2_sitelib}/%{name}/ %changelog +* Fri Sep 4 2015 Jerry James - 2.1.0-1.20150904git.5405af4 +- Update to recent git snapshot + * Wed Jul 29 2015 Fedora Release Engineering - 0.1-30.20140619git.44de620 - Rebuilt for https://fedoraproject.org/wiki/Changes/F23Boost159