stp/stp-unbundle.patch

395 lines
13 KiB
Diff
Raw Normal View History

--- ./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.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
{