rpms/stp
3
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Update to recent git snapshot.

Browse Source
This commit is contained in:
Jerry James 2015-09-04 10:14:38 -06:00
parent 10c7533b48
commit 826d0abd7f
5 changed files with 47 additions and 382 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
.gitignore vendored
View File

@ -1 +1,2 @@
/stp-stp-44de620.tar.gz
/stp-stp-5405af4.tar.gz

2
sources
View File

@ -1 +1 @@
3744bde4e5a1d5108506adf1c929563d stp-stp-44de620.tar.gz
9cfefa8cda293105506e5a8f3ed7c6b2 stp-stp-5405af4.tar.gz

213
stp-unbundle.patch
View File

@ -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 <iostream>
#include <utility>
#include "RunTimes.h"
-#include "../sat/cryptominisat2/time_mem.h"
+#include <cmsat/time_mem.h>
// 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 <boost/utility.hpp>
#include <iostream>
#include <sstream>
-#include "../sat/cryptominisat2/time_mem.h"
+#include <cmsat/time_mem.h>
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 <cmsat/Solver.h>
+#include <cmsat/SolverTypes.h>
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<MINISAT::Lit> v;
+ CMSat::vec<CMSat::Lit> v;
for (int i =0; i<ps.size();i++)
- v.push(MINISAT::Lit(var(ps[i]), sign(ps[i])));
+ v.push(CMSat::Lit(var(ps[i]), sign(ps[i])));
return s->addClause(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

143
stp-warning.patch
View File

@ -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<unsigned> 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;

70
stp.spec
View File

@ -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 <loganjerry@gmail.com> - 2.1.0-1.20150904git.5405af4
- Update to recent git snapshot
* Wed Jul 29 2015 Fedora Release Engineering <rel-eng@lists.fedoraproject.org> - 0.1-30.20140619git.44de620
- Rebuilt for https://fedoraproject.org/wiki/Changes/F23Boost159