stp/stp-unbundle.patch

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