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

Update to recent subversion snapshot. 

Do not build bundled cryptominisat.
This commit is contained in:
Jerry James 2012-08-10 16:37:03 -06:00
parent cd5519131f
commit 5f844b447d
5 changed files with 2184 additions and 1917 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
sources
View File

@ -1 +1 @@
e23ce5a6ef6cc34ce289c2d4eb948efe stp-0.1.tar.xz
23ee46548b338443fd741ba2e50000e3 stp-0.1.tar.xz

25
stp-gcc47.patch
View File

@ -1,25 +0,0 @@
--- ./src/sat/mtl/Map.h.orig 2010-11-27 19:45:43.000000000 -0700
+++ ./src/sat/mtl/Map.h 2012-01-10 16:30:55.918767977 -0700
@@ -29,17 +29,17 @@ namespace Minisat {
// Default hash/equals functions
//
+static inline uint32_t hash(uint32_t x){ return x; }
+static inline uint32_t hash(uint64_t x){ return (uint32_t)x; }
+static inline uint32_t hash(int32_t x) { return (uint32_t)x; }
+static inline uint32_t hash(int64_t x) { return (uint32_t)x; }
+
template<class K> struct Hash { uint32_t operator()(const K& k) const { return hash(k); } };
template<class K> struct Equal { bool operator()(const K& k1, const K& k2) const { return k1 == k2; } };
template<class K> struct DeepHash { uint32_t operator()(const K* k) const { return hash(*k); } };
template<class K> struct DeepEqual { bool operator()(const K* k1, const K* k2) const { return *k1 == *k2; } };
-static inline uint32_t hash(uint32_t x){ return x; }
-static inline uint32_t hash(uint64_t x){ return (uint32_t)x; }
-static inline uint32_t hash(int32_t x) { return (uint32_t)x; }
-static inline uint32_t hash(int64_t x) { return (uint32_t)x; }
-
//=================================================================================================
// Some primes

394
stp-unbundle.patch Normal file
View File

@ -0,0 +1,394 @@
--- ./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 @@
#include "../AST/AST.h"
#include "../STPManager/STPManager.h"
-#include "../boost/noncopyable.hpp"
+#include <boost/noncopyable.hpp>
namespace BEEV
{
--- ./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>
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>
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 @@
#undef l_Undef
-#include "cryptominisat2/Solver.h"
-#include "cryptominisat2/SolverTypes.h"
+#include <cmsat/Solver/Solver.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 +40,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])));
s->addClause(v);
}
@@ -63,7 +73,7 @@ namespace BEEV
int 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
@@ -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();
--- ./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>
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
{

3646
stp-warning.patch
View File

File diff suppressed because it is too large Load Diff

34
stp.spec
View File

@ -1,11 +1,11 @@
# Upstream occasionally releases a subversion snapshot, but no "regular"
# releases since the 0.1 release.
%global svnver 1493
%global svntim 20120109svn
%global svnver 1666
%global svntim 20120615svn
Name: stp
Version: 0.1
Release: 10.%{svntim}%{?dist}
Release: 11.%{svntim}%{?dist}
Summary: Constraint solver/decision procedure
Group: Applications/Engineering
@ -19,12 +19,12 @@ URL: http://sourceforge.net/projects/stp-fast-prover/
# 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
# This patch has not yet been sent upstream. Fix a bunch of compiler warnings
# that may indicate miscompiled code.
Patch0: stp-warning.patch
# This patch has not yet been sent upstream. Deal with new C++ declaration
# ordering rules in GCC 4.7.
Patch1: stp-gcc47.patch
Patch1: stp-warning.patch
BuildRequires: bison
BuildRequires: boost-devel
@ -77,20 +77,26 @@ or automated prover). Provides a static library.
%patch0
%patch1
# Make sure nothing uses the shipped boost sources
rm -fr src/boost
# Make sure nothing uses the shipped boost or cryptominisat sources
rm -fr src/boost src/sat/cryptominisat2
# We do not want to know about the order of member initializers
sed -i "s/\(-Wno-deprecated\)/\1 -Wno-reorder/" scripts/Makefile.common
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 \$(TOP)\`|%{svnver}|" src/main/Makefile
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
%build
scripts/configure --with-prefix=%{_prefix}
# DO NOT use _smp_mflags; build will fail.
make all OPTIMIZE="%{optflags} -DNDEBUG" LIB_DIR=%{_libdir}
make all OPTIMIZE="%{optflags} -DNDEBUG" LIB_DIR=%{_libdir} \
LDFLAGS="$RPM_LD_FLAGS -lcryptominisat"
# Currently the valgrind tests are failing, because valgrind reports the use
# of uninitialized variables deep within libdl. All other tests pass, so
@ -116,6 +122,10 @@ make install PREFIX=%{buildroot}%{_prefix} LIB_DIR=%{buildroot}%{_libdir}
%{_includedir}/stp/
%changelog
* Tue Aug 7 2012 Jerry James <loganjerry@gmail.com> - 0.1-11.20120615svn
- Update to recent subversion snapshot
- Do not build bundled cryptominisat
* Sat Jul 21 2012 Fedora Release Engineering <rel-eng@lists.fedoraproject.org> - 0.1-10.20120109svn
- Rebuilt for https://fedoraproject.org/wiki/Fedora_18_Mass_Rebuild