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

Update to recent git snapshot, now hosted on github. 

Build now uses cmake.
Tests now need boolector, which has license problems.  Disable %%check for
now unless we can find something useful to do.
This commit is contained in:
Jerry James 2014-03-19 17:09:33 -06:00
parent e611f6d776
commit 5a3a024fae
6 changed files with 1141 additions and 2372 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
.gitignore vendored
View File

@ -1 +1 @@
/stp-0.1.tar.xz
/stp-stp-fe766c9.tar.gz

2
sources
View File

@ -1 +1 @@
4a44259e06e7d18ccc6615ca65dbc426 stp-0.1.tar.xz
3104c3fcb6e89da91f766e9b61dd87d9 stp-stp-fe766c9.tar.gz

463
stp-unbundle.patch
View File

@ -1,67 +1,138 @@
--- ./src/to-sat/ToSATBase.h.orig 2012-01-23 05:43:59.000000000 -0700
+++ ./src/to-sat/ToSATBase.h 2012-08-07 16:22:05.823811600 -0600
@@ -3,7 +3,7 @@
diff --git a/CMakeLists.txt b/CMakeLists.txt
index cc5bb76..169c064 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -69,6 +69,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()
#include "../AST/AST.h"
#include "../STPManager/STPManager.h"
-#include "../boost/noncopyable.hpp"
+#include <boost/noncopyable.hpp>
check_cxx_compiler_flag("-std=gnu++11" HAVE_FLAG_STD_GNUPP11)
@@ -179,6 +180,7 @@ include_directories(${Boost_INCLUDE_DIRS})
namespace BEEV
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
{
--- ./src/to-sat/AIG/ToCNFAIG.h.orig 2012-01-23 15:51:23.000000000 -0700
+++ ./src/to-sat/AIG/ToCNFAIG.h 2012-08-07 16:22:05.823811600 -0600
@@ -6,7 +6,7 @@
#include "../../extlib-abc/dar.h"
#include "../ToSATBase.h"
#include "BBNodeManagerAIG.h"
-#include "../../boost/noncopyable.hpp"
+#include <boost/noncopyable.hpp>
diff --git a/src/libstp/CMakeLists.txt b/src/libstp/CMakeLists.txt
index eabc0d6..8cc3bc7 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
@@ -58,7 +57,7 @@ set_target_properties(libstp PROPERTIES
# 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)
namespace BEEV {
--- ./src/to-sat/ASTNode/ToCNF.h.orig 2012-01-27 21:08:17.000000000 -0700
+++ ./src/to-sat/ASTNode/ToCNF.h 2012-08-07 16:22:05.823811600 -0600
@@ -15,7 +15,7 @@
#include "../../AST/AST.h"
#include "../../STPManager/STPManager.h"
#include "ClauseList.h"
-#include "../../boost/noncopyable.hpp"
+#include <boost/noncopyable.hpp>
# -----------------------------------------------------------------------------
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)
namespace BEEV
{
--- ./src/to-sat/BitBlaster.h.orig 2012-04-09 07:21:26.000000000 -0600
+++ ./src/to-sat/BitBlaster.h 2012-08-07 16:22:05.824811583 -0600
@@ -14,7 +14,7 @@
#include <cassert>
#include <map>
#include "../STPManager/STPManager.h"
-#include "../boost/noncopyable.hpp"
+#include <boost/noncopyable.hpp>
#include <list>
#include "../simplifier/constantBitP/MultiplicationStats.h"
--- ./src/absrefine_counterexample/AbsRefine_CounterExample.h.orig 2012-04-25 07:40:33.000000000 -0600
+++ ./src/absrefine_counterexample/AbsRefine_CounterExample.h 2012-08-07 16:22:05.825811565 -0600
@@ -15,7 +15,7 @@
#include "../simplifier/simplifier.h"
#include "../AST/ArrayTransformer.h"
#include "../to-sat/ToSATBase.h"
-#include "../boost/noncopyable.hpp"
+#include <boost/noncopyable.hpp>
namespace BEEV
{
--- ./src/sat/CryptoMinisat.cpp.orig 2010-08-20 06:07:42.000000000 -0600
+++ ./src/sat/CryptoMinisat.cpp 2012-08-07 16:22:39.477306573 -0600
@@ -7,15 +7,25 @@
add_library(sat OBJECT
diff --git a/src/sat/CryptoMinisat.cpp b/src/sat/CryptoMinisat.cpp
index 27f372d..93e9b85 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
{
@ -84,7 +155,7 @@
}
CryptoMinisat::~CryptoMinisat()
@@ -30,9 +40,9 @@ namespace BEEV
@@ -30,9 +41,9 @@ namespace BEEV
// Cryptominisat uses a slightly different Lit class too.
// VERY SLOW>
@ -94,64 +165,21 @@
- v.push(MINISAT::Lit(var(ps[i]), sign(ps[i])));
+ v.push(CMSat::Lit(var(ps[i]), sign(ps[i])));
s->addClause(v);
return s->addClause(v);
}
@@ -63,7 +73,7 @@ namespace BEEV
@@ -63,7 +74,7 @@ namespace BEEV
int CryptoMinisat::setVerbosity(int v)
void CryptoMinisat::setVerbosity(int v)
{
- s->verbosity = v;
+ s->conf.verbosity = v;
}
int CryptoMinisat::nVars()
@@ -73,11 +83,11 @@ namespace BEEV
{
double cpu_time = Minisat::cpuTime();
double mem_used = Minisat::memUsedPeak();
- printf("restarts : %"PRIu64"\n", s->starts);
- printf("conflicts : %-12"PRIu64" (%.0f /sec)\n", s->conflicts , s->conflicts /cpu_time);
- printf("decisions : %-12"PRIu64" (%4.2f %% random) (%.0f /sec)\n", s->decisions, (float)s->rnd_decisions*100 / (float)s->decisions, s->decisions /cpu_time);
- printf("propagations : %-12"PRIu64" (%.0f /sec)\n", s->propagations, s->propagations/cpu_time);
- printf("conflict literals : %-12"PRIu64" (%4.2f %% deleted)\n", s->tot_literals, (s->max_literals - s->tot_literals)*100 / (double)s->max_literals);
+ printf("restarts : %"PRIu64"\n", s->getStarts());
+ printf("conflicts : %-12"PRIu64" (%.0f /sec)\n", s->getConflicts(), s->getConflicts()/cpu_time);
+ printf("decisions : %-12"PRIu64" (%4.2f %% random) (%.0f /sec)\n", s->getDecisions(), (float)s->getRndDecisions()*100 / (float)s->getDecisions(), s->getDecisions()/cpu_time);
+ printf("propagations : %-12"PRIu64" (%.0f /sec)\n", s->getPropagations(), s->getPropagations()/cpu_time);
+ printf("conflict literals : %-12"PRIu64" (%4.2f %% deleted)\n", s->getTotLiterals(), (s->getMaxLiterals() - s->getTotLiterals())*100 / (double)s->getMaxLiterals());
if (mem_used != 0) printf("Memory used : %.2f MB\n", mem_used);
printf("CPU time : %g s\n", cpu_time);
}
--- ./src/sat/Makefile.orig 2011-11-27 19:55:18.000000000 -0700
+++ ./src/sat/Makefile 2012-08-07 16:22:05.826811547 -0600
@@ -13,7 +13,7 @@ export COPTIMIZE=$(CFLAGS_M32) $(CFLAGS_
core: $(LIB)
# $(LIB) depends on */lib_release.a and will be rebuilt only if they have been updated
-$(LIB): core/lib_release.a core_prop/lib_release.a simp/lib_release.a utils/lib_release.a cryptominisat2/libminisat.a $(OBJS)
+$(LIB): core/lib_release.a core_prop/lib_release.a simp/lib_release.a utils/lib_release.a $(OBJS)
$(RM) $@
$(call arcat,$@,$(filter %.a,$^))
$(AR) qcs $@ $(filter %.o,$^)
@@ -26,8 +26,6 @@ simp/lib_release.a: FORCE
$(MAKE) -C simp libr
utils/lib_release.a: FORCE
$(MAKE) -C utils libr
-cryptominisat2/libminisat.a: FORCE
- $(MAKE) -C cryptominisat2 lib all
FORCE:
.PHONY: clean
@@ -37,6 +35,5 @@ clean:
$(MAKE) -C core_prop clean
$(MAKE) -C simp clean
$(MAKE) -C utils clean
- $(MAKE) -C cryptominisat2 clean
-CryptoMinisat.o: CFLAGS += -Icryptominisat2/mtl -Imtl -I$(TOP)/src
+CryptoMinisat.o: CFLAGS += -I/usr/include/cmsat/mtl -Imtl -I$(TOP)/src
--- ./src/sat/CryptoMinisat.h.orig 2012-01-09 21:59:09.000000000 -0700
+++ ./src/sat/CryptoMinisat.h 2012-08-07 16:22:05.826811547 -0600
diff --git a/src/sat/CryptoMinisat.h b/src/sat/CryptoMinisat.h
index 9c11c1d..50d55fc 100644
--- a/src/sat/CryptoMinisat.h
+++ b/src/sat/CryptoMinisat.h
@@ -6,16 +6,13 @@
#include "SATSolver.h"
@ -172,223 +200,14 @@
public:
CryptoMinisat();
--- ./src/STPManager/STP.h.orig 2012-03-15 06:38:21.000000000 -0600
+++ ./src/STPManager/STP.h 2012-08-07 16:22:05.827811530 -0600
@@ -19,7 +19,7 @@
#include "../parser/LetMgr.h"
#include "../absrefine_counterexample/AbsRefine_CounterExample.h"
#include "../simplifier/PropagateEqualities.h"
-#include "../boost/noncopyable.hpp"
+#include <boost/noncopyable.hpp>
diff --git a/tests/api/C/CMakeLists.txt b/tests/api/C/CMakeLists.txt
index 99c1478..2a490ff 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)
namespace BEEV
{
--- ./src/STPManager/NodeIterator.h.orig 2012-01-23 05:43:59.000000000 -0700
+++ ./src/STPManager/NodeIterator.h 2012-08-07 16:22:05.827811530 -0600
@@ -2,7 +2,7 @@
#define NODEITERATOR_H_
#include <stack>
-#include "../boost/noncopyable.hpp"
+#include <boost/noncopyable.hpp>
namespace BEEV
{
--- ./src/STPManager/UserDefinedFlags.h.orig 2012-04-06 18:20:57.000000000 -0600
+++ ./src/STPManager/UserDefinedFlags.h 2012-08-07 16:22:05.827811530 -0600
@@ -14,7 +14,7 @@
#include <assert.h>
#include <iostream>
#include <set>
-#include "../boost/noncopyable.hpp"
+#include <boost/noncopyable.hpp>
namespace BEEV
{
--- ./src/STPManager/STPManager.h.orig 2012-01-25 22:04:55.000000000 -0700
+++ ./src/STPManager/STPManager.h 2012-08-07 16:22:05.828811513 -0600
@@ -14,7 +14,7 @@
#include "../AST/AST.h"
#include "../AST/NodeFactory/HashingNodeFactory.h"
#include "../sat/SATSolver.h"
-#include "../boost/noncopyable.hpp"
+#include <boost/noncopyable.hpp>
namespace BEEV
{
--- ./src/STPManager/DifficultyScore.h.orig 2012-01-23 05:43:59.000000000 -0700
+++ ./src/STPManager/DifficultyScore.h 2012-08-07 16:22:05.828811513 -0600
@@ -6,7 +6,7 @@
#include "../AST/ASTKind.h"
#include <list>
#include "../STPManager/NodeIterator.h"
-#include "../boost/noncopyable.hpp"
+#include <boost/noncopyable.hpp>
// estimate how difficult that input is to solve based on some simple rules.
--- ./src/simplifier/SubstitutionMap.h.orig 2012-03-19 21:59:03.000000000 -0600
+++ ./src/simplifier/SubstitutionMap.h 2012-08-07 16:22:05.829811496 -0600
@@ -5,7 +5,7 @@
#include "../STPManager/STPManager.h"
#include "../AST/NodeFactory/SimplifyingNodeFactory.h"
#include "VariablesInExpression.h"
-#include "../boost/noncopyable.hpp"
+#include <boost/noncopyable.hpp>
namespace BEEV
{
--- ./src/simplifier/simplifier.h.orig 2012-03-19 21:59:03.000000000 -0600
+++ ./src/simplifier/simplifier.h 2012-08-07 16:22:05.829811496 -0600
@@ -14,7 +14,7 @@
#include "../STPManager/STPManager.h"
#include "../AST/NodeFactory/SimplifyingNodeFactory.h"
#include "SubstitutionMap.h"
-#include "../boost/noncopyable.hpp"
+#include <boost/noncopyable.hpp>
namespace BEEV
{
--- ./src/simplifier/UseITEContext.h.orig 2012-03-19 21:59:03.000000000 -0600
+++ ./src/simplifier/UseITEContext.h 2012-08-07 16:22:05.829811496 -0600
@@ -13,7 +13,7 @@
#include "../AST/AST.h"
#include "../STPManager/STPManager.h"
-#include "../boost/noncopyable.hpp"
+#include <boost/noncopyable.hpp>
namespace BEEV
{
--- ./src/simplifier/AIGSimplifyPropositionalCore.h.orig 2012-03-19 21:59:03.000000000 -0600
+++ ./src/simplifier/AIGSimplifyPropositionalCore.h 2012-08-07 16:22:05.830811479 -0600
@@ -18,7 +18,7 @@
#include "../extlib-abc/dar.h"
#include "../to-sat/AIG/BBNodeManagerAIG.h"
#include "../to-sat/BitBlaster.h"
-#include "../boost/noncopyable.hpp"
+#include <boost/noncopyable.hpp>
namespace BEEV
{
--- ./src/simplifier/FindPureLiterals.h.orig 2012-01-23 05:43:59.000000000 -0700
+++ ./src/simplifier/FindPureLiterals.h 2012-08-07 16:22:05.830811479 -0600
@@ -21,7 +21,7 @@
#include "../AST/AST.h"
#include "../STPManager/STPManager.h"
#include "../simplifier/simplifier.h"
-#include "../boost/noncopyable.hpp"
+#include <boost/noncopyable.hpp>
namespace BEEV
{
--- ./src/simplifier/Symbols.h.orig 2012-01-23 05:43:59.000000000 -0700
+++ ./src/simplifier/Symbols.h 2012-08-07 16:22:05.831811462 -0600
@@ -1,7 +1,7 @@
#ifndef SYMBOLS_H
#define SYMBOLS_H
-#include "../boost/noncopyable.hpp"
+#include <boost/noncopyable.hpp>
// Each node is either: empty, an ASTNode, or a vector of more than one child nodes.
--- ./src/simplifier/AlwaysTrue.h.orig 2012-01-23 05:43:59.000000000 -0700
+++ ./src/simplifier/AlwaysTrue.h 2012-08-07 16:22:05.831811462 -0600
@@ -7,7 +7,7 @@
#include "../AST/AST.h"
#include "../STPManager/STPManager.h"
#include "../simplifier/simplifier.h"
-#include "../boost/noncopyable.hpp"
+#include <boost/noncopyable.hpp>
namespace BEEV
{
--- ./src/simplifier/RemoveUnconstrained.h.orig 2012-03-19 21:59:03.000000000 -0600
+++ ./src/simplifier/RemoveUnconstrained.h 2012-08-07 16:22:05.832811445 -0600
@@ -11,7 +11,7 @@
#include "constantBitP/Dependencies.h"
#include "simplifier.h"
#include "MutableASTNode.h"
-#include "../boost/noncopyable.hpp"
+#include <boost/noncopyable.hpp>
namespace BEEV
--- ./src/simplifier/bvsolver.h.orig 2012-03-19 21:59:03.000000000 -0600
+++ ./src/simplifier/bvsolver.h 2012-08-07 16:22:05.832811445 -0600
@@ -13,7 +13,7 @@
#include "simplifier.h"
#include "Symbols.h"
#include "VariablesInExpression.h"
-#include "../boost/noncopyable.hpp"
+#include <boost/noncopyable.hpp>
namespace BEEV
{
--- ./src/simplifier/VariablesInExpression.h.orig 2012-01-23 05:43:59.000000000 -0700
+++ ./src/simplifier/VariablesInExpression.h 2012-08-07 16:22:05.833811428 -0600
@@ -8,7 +8,7 @@
#include "../AST/AST.h"
#include "Symbols.h"
-#include "../boost/noncopyable.hpp"
+#include <boost/noncopyable.hpp>
namespace BEEV
{
--- ./src/simplifier/PropagateEqualities.h.orig 2012-01-23 05:43:59.000000000 -0700
+++ ./src/simplifier/PropagateEqualities.h 2012-08-07 16:22:05.833811428 -0600
@@ -4,7 +4,7 @@
#include "../AST/AST.h"
#include "../STPManager/STPManager.h"
#include "../simplifier/simplifier.h"
-#include "../boost/noncopyable.hpp"
+#include <boost/noncopyable.hpp>
//This finds conjuncts which are one of: (= SYMBOL BVCONST), (= BVCONST (READ SYMBOL BVCONST)),
// (IFF SYMBOL TRUE), (IFF SYMBOL FALSE), (IFF SYMBOL SYMBOL), (=SYMBOL SYMBOL)
--- ./src/simplifier/EstablishIntervals.h.orig 2012-03-19 21:59:03.000000000 -0600
+++ ./src/simplifier/EstablishIntervals.h 2012-08-07 16:22:05.834811411 -0600
@@ -8,7 +8,7 @@
#include "../STPManager/STPManager.h"
#include "simplifier.h"
#include "../AST/NodeFactory/SimplifyingNodeFactory.h"
-#include "../boost/noncopyable.hpp"
+#include <boost/noncopyable.hpp>
namespace BEEV
{
--- ./src/AST/NodeFactory/NodeFactory.h.orig 2012-03-19 21:59:03.000000000 -0600
+++ ./src/AST/NodeFactory/NodeFactory.h 2012-08-07 16:22:05.834811411 -0600
@@ -4,7 +4,7 @@
#include <vector>
#include "../ASTKind.h"
-#include "../../boost/noncopyable.hpp"
+#include <boost/noncopyable.hpp>
namespace BEEV
{
--- ./src/AST/ArrayTransformer.h.orig 2012-05-11 20:18:08.000000000 -0600
+++ ./src/AST/ArrayTransformer.h 2012-08-07 16:22:05.834811411 -0600
@@ -13,7 +13,7 @@
#include "AST.h"
#include "../STPManager/STPManager.h"
#include "../AST/NodeFactory/SimplifyingNodeFactory.h"
-#include "../boost/noncopyable.hpp"
+#include <boost/noncopyable.hpp>
namespace BEEV
{
--- ./src/AST/RunTimes.h.orig 2012-01-23 05:43:59.000000000 -0700
+++ ./src/AST/RunTimes.h 2012-08-07 16:22:05.835811395 -0600
@@ -15,7 +15,7 @@
#include <string>
#include "../sat/utils/System.h"
#include <iomanip>
-#include "../boost/noncopyable.hpp"
+#include <boost/noncopyable.hpp>
class RunTimes : boost::noncopyable
{
# -----------------------------------------------------------------------------
# Find the public headers associated with libstp

80
stp-undefined.patch Normal file
View File

@ -0,0 +1,80 @@
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 ///
////////////////////////////////////////////////////////////////////////

2850
stp-warning.patch
View File

File diff suppressed because it is too large Load Diff

116
stp.spec
View File

@ -1,38 +1,34 @@
# Upstream occasionally releases a subversion snapshot, but no "regular"
# releases since the 0.1 release.
%global svnver 1673
%global svntim 20130223svn
%global gitdate 20140319
%global gittag fe766c9add6f80453ec14f4a3b4d5cf3a0385551
%global shorttag %(echo %{gittag} | cut -b -7)
%global user stp
Name: stp
Version: 0.1
Release: 18.%{svntim}%{?dist}
Release: 19.%{gitdate}git.%{shorttag}%{?dist}
Summary: Constraint solver/decision procedure
Group: Applications/Engineering
License: MIT
URL: http://sourceforge.net/projects/stp-fast-prover/
# The source for this package was pulled from upstream's subversion repository.
# Use the following commands to generate the tarball:
#
# svn export -r %%{svnver} \
# https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp \
# stp-0.1
# tar cvJf stp-0.1.tar.xz stp-0.1
Source0: stp-%{version}.tar.xz
# This patch is specific to Fedora. Use the existing cryptominisat and boost
# libraries instead of the bundled versions.
Patch0: stp-unbundle.patch
URL: http://stp.github.io/stp/
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: stp-warning.patch
Patch1: %{name}-warning.patch
# This patch has not yet been sent upstream. Eliminate undefined symbols.
Patch2: %{name}-undefined.patch
BuildRequires: bison
BuildRequires: boost-devel
BuildRequires: cmake
BuildRequires: cryptominisat-devel
BuildRequires: flex
BuildRequires: time
BuildRequires: valgrind
BuildRequires: zlib-devel
BuildRequires: python2
%description
STP (Simple Theorem Prover) is a constraint solver (also referred to as
@ -56,85 +52,53 @@ Additional information can be found at:
Summary: Development files for STP constraint solver/decision procedure
Group: Applications/Engineering
Requires: %{name}%{?_isa} = %{version}-%{release}
Provides: %{name}-static = %{version}-%{release}
# This "devel" package provides a static (not dynamic) library because:
# 1. This is the normal usage mode when linking this as a library;
# it's what upstream and existing programs that use this program expect.
# 2. This speeds execution. In this library, speed matters.
# There's a speed penalty for .so files, and this program is much
# like a chess program - it's essentially an inner loop that searches
# a massive space of possibilities.
# A dynamic .so version could be create using:
# gcc -shared -Wl,-soname,libstp.so.1 -o libstp.so.1.0.1 libstp.a
# but this would require -fpic to compile (slowing the results).
# See my document:
# http://www.dwheeler.com/program-library/Program-Library-HOWTO/
%description devel
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.
%prep
%setup -q
%patch0
%patch1
%setup -q -n %{user}-%{name}-%{shorttag}
%patch0 -p1
%patch1 -p1
%patch2 -p1
# Make sure nothing uses the shipped boost or cryptominisat sources
rm -fr src/boost src/sat/cryptominisat2
# 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
sed -i "s/-Wno-deprecated/& -Wno-reorder/" scripts/Makefile.common
# Avoid a BR on subversion, as well as subversion version hell
sed -i "s|\`svnversion -c \$(TOP)\`|%{svnver}|" src/main/Makefile
# Fix Makefile bugs
sed -e "s/^\.PHONY:.*/& depend/" -e "s/^depend:.*/& ASTKind.h/" \
-i src/AST/Makefile
sed -i "s/^\.PHONY:.*/& depend/" src/main/Makefile
# Fix underlinked tests
sed -i 's/^LIBS=.*/& -lcryptominisat -lm/' tests/c-api-tests/Makefile
sed -i "s/-Wno-deprecated/& -Wno-reorder/" CMakeLists.txt
%build
scripts/configure --with-prefix=%{_prefix}
# DO NOT use _smp_mflags; build will fail.
make all OPTIMIZE="%{optflags} -DNDEBUG" LIB_DIR=%{_libdir} \
LDFLAGS="$RPM_LD_FLAGS -lcryptominisat"
%cmake
%install
mkdir -p %{buildroot}%{_bindir}
mkdir -p %{buildroot}%{_includedir}/stp
mkdir -p %{buildroot}%{_libdir}
make install DESTDIR=%{buildroot}
# This "make install" doesn't support DESTDIR=%%{buildroot}.
# We'll rig PREFIX/LIB_DIR, since that happens to work for this makefile.
make install PREFIX=%{buildroot}%{_prefix} LIB_DIR=%{buildroot}%{_libdir}
%check
# Most of the tests are broken. Run the ones that aren't.
export PATH=$PATH:%{buildroot}%{_bindir}
make check
%ifarch %{ix86} x86_64
# On non-x86 architectures, the memory leak tests tend to fail, because
# valgrind finds problems in glibc itself. Also, the non-valgrind tests
# tend to fail because they time out. Until valgrind works and I can figure
# out how to adapt the timeout estimates for such architectures, skip these
# tests.
make regressstp
make regresscapi
%endif
# 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
%files
%{_bindir}/*
%doc AUTHORS README LICENSE LICENSE_COMPONENTS papers
%{_libdir}/libstp.so
%doc AUTHORS README.markdown LICENSE LICENSE_COMPONENTS papers
%files devel
%{_libdir}/libstp*.a
%{_includedir}/stp/
%{_libdir}/cmake/STP/
%changelog
* Wed Mar 19 2014 Jerry James <loganjerry@gmail.com> - 0.1-19.20140319git.6110a49
- Update to recent git snapshot, now hosted on github
- Build now uses cmake
- Tests now need boolector, which has license problems. Disable %%check for
now unless we can find something useful to do.
* Wed Oct 9 2013 Jerry James <loganjerry@gmail.com> - 0.1-18.20130223svn
- Really rebuild for cryptominisat 2.9.8