This should fix the debian build fails:

   * removed bvpicosat directory as it is currently not used

Cleared some of the flurry of warnings my previous merge caused in src/prop/

1 files changed, 19 insertions, 125 deletions

diff --git a/src/prop/sat_module.h b/src/prop/sat_module.h
index 94e39e5c6..320dfe09b 100644
--- a/src/prop/sat_module.h
+++ b/src/prop/sat_module.h
@@ -24,17 +24,24 @@
 #include <stdint.h> 
 #include "util/options.h"
 #include "util/stats.h"
-
+#include "context/cdlist.h"
 
 // DPLLT Minisat
-#include "prop/minisat/core/Solver.h"
 #include "prop/minisat/core/SolverTypes.h"
-#include "prop/minisat/simp/SimpSolver.h"
 
 // BV Minisat
-#include "prop/bvminisat/core/Solver.h"
 #include "prop/bvminisat/core/SolverTypes.h"
-#include "prop/bvminisat/simp/SimpSolver.h"
+
+
+namespace Minisat{
+class Solver;
+class SimpSolver; 
+}
+
+namespace BVMinisat{
+class Solver;
+class SimpSolver; 
+}
 
 
 namespace CVC4 {
@@ -155,7 +162,7 @@ class MinisatSatSolver: public BVSatSolverInterface {
 
   MinisatSatSolver();
 public:
-  ~MinisatSatSolver() {delete d_minisat;}
+  ~MinisatSatSolver();
   void addClause(SatClause& clause, bool removable);
 
   SatVariable newVar(bool theoryAtom = false);
@@ -188,7 +195,6 @@ public:
   static void  toMinisatClause(SatClause& clause, BVMinisat::vec<BVMinisat::Lit>& minisat_clause);
   static void  toSatClause    (BVMinisat::vec<BVMinisat::Lit>& clause, SatClause& sat_clause); 
 
-
   class Statistics {
   public:
     ReferenceStat<uint64_t> d_statStarts, d_statDecisions;
@@ -197,54 +203,9 @@ public:
     ReferenceStat<uint64_t> d_statLearntsLiterals,  d_statMaxLiterals;
     ReferenceStat<uint64_t> d_statTotLiterals;
     ReferenceStat<int> d_statEliminatedVars;
-    Statistics() :
-      d_statStarts("theory::bv::bvminisat::starts"),
-      d_statDecisions("theory::bv::bvminisat::decisions"),
-      d_statRndDecisions("theory::bv::bvminisat::rnd_decisions"),
-      d_statPropagations("theory::bv::bvminisat::propagations"),
-      d_statConflicts("theory::bv::bvminisat::conflicts"),
-      d_statClausesLiterals("theory::bv::bvminisat::clauses_literals"),
-      d_statLearntsLiterals("theory::bv::bvminisat::learnts_literals"),
-      d_statMaxLiterals("theory::bv::bvminisat::max_literals"),
-      d_statTotLiterals("theory::bv::bvminisat::tot_literals"),
-      d_statEliminatedVars("theory::bv::bvminisat::eliminated_vars")
-    {
-      StatisticsRegistry::registerStat(&d_statStarts);
-      StatisticsRegistry::registerStat(&d_statDecisions);
-      StatisticsRegistry::registerStat(&d_statRndDecisions);
-      StatisticsRegistry::registerStat(&d_statPropagations);
-      StatisticsRegistry::registerStat(&d_statConflicts);
-      StatisticsRegistry::registerStat(&d_statClausesLiterals);
-      StatisticsRegistry::registerStat(&d_statLearntsLiterals);
-      StatisticsRegistry::registerStat(&d_statMaxLiterals);
-      StatisticsRegistry::registerStat(&d_statTotLiterals);
-      StatisticsRegistry::registerStat(&d_statEliminatedVars);
-    }
-    ~Statistics() {
-      StatisticsRegistry::unregisterStat(&d_statStarts);
-      StatisticsRegistry::unregisterStat(&d_statDecisions);
-      StatisticsRegistry::unregisterStat(&d_statRndDecisions);
-      StatisticsRegistry::unregisterStat(&d_statPropagations);
-      StatisticsRegistry::unregisterStat(&d_statConflicts);
-      StatisticsRegistry::unregisterStat(&d_statClausesLiterals);
-      StatisticsRegistry::unregisterStat(&d_statLearntsLiterals);
-      StatisticsRegistry::unregisterStat(&d_statMaxLiterals);
-      StatisticsRegistry::unregisterStat(&d_statTotLiterals);
-      StatisticsRegistry::unregisterStat(&d_statEliminatedVars);
-    }
-    
-    void init(BVMinisat::SimpSolver* minisat){
-      d_statStarts.setData(minisat->starts);
-      d_statDecisions.setData(minisat->decisions);
-      d_statRndDecisions.setData(minisat->rnd_decisions);
-      d_statPropagations.setData(minisat->propagations);
-      d_statConflicts.setData(minisat->conflicts);
-      d_statClausesLiterals.setData(minisat->clauses_literals);
-      d_statLearntsLiterals.setData(minisat->learnts_literals);
-      d_statMaxLiterals.setData(minisat->max_literals);
-      d_statTotLiterals.setData(minisat->tot_literals);
-      d_statEliminatedVars.setData(minisat->eliminated_vars);
-    }
+    Statistics();
+    ~Statistics();
+    void init(BVMinisat::SimpSolver* minisat);
   };
   
   Statistics d_statistics;
@@ -252,31 +213,6 @@ public:
 }; 
 
 
-// class PicosatSatSolver: public SatSolverInterface {
-  
-// public:
-//   PicosatSatSolver();
-  
-//   void addClause(SatClause& clause, bool removable);
-
-//   SatVariable newVar(bool theoryAtom = false);
-
-//   void markUnremovable(SatLiteral lit); 
-  
-//   SatLiteralValue solve(unsigned long& resource = 0);
-  
-//   SatLiteralValue solve(const std::vector<SatLiteral>& assumptions); 
-
-//   void interrupt();
-
-//   SatLiteralValue value(SatLiteral l);
-
-//   SatLiteralValue modelValue(SatLiteral l);
-  
-// };
-
-
-
 class DPLLMinisatSatSolver : public DPLLSatSolverInterface {
 
   /** The SatSolver used */
@@ -338,49 +274,9 @@ public:
     ReferenceStat<uint64_t> d_statLearntsLiterals,  d_statMaxLiterals;
     ReferenceStat<uint64_t> d_statTotLiterals;
   public:
-    Statistics() :
-      d_statStarts("sat::starts"),
-      d_statDecisions("sat::decisions"),
-      d_statRndDecisions("sat::rnd_decisions"),
-      d_statPropagations("sat::propagations"),
-      d_statConflicts("sat::conflicts"),
-      d_statClausesLiterals("sat::clauses_literals"),
-      d_statLearntsLiterals("sat::learnts_literals"),
-      d_statMaxLiterals("sat::max_literals"),
-      d_statTotLiterals("sat::tot_literals")
-    {
-      StatisticsRegistry::registerStat(&d_statStarts);
-      StatisticsRegistry::registerStat(&d_statDecisions);
-      StatisticsRegistry::registerStat(&d_statRndDecisions);
-      StatisticsRegistry::registerStat(&d_statPropagations);
-      StatisticsRegistry::registerStat(&d_statConflicts);
-      StatisticsRegistry::registerStat(&d_statClausesLiterals);
-      StatisticsRegistry::registerStat(&d_statLearntsLiterals);
-      StatisticsRegistry::registerStat(&d_statMaxLiterals);
-      StatisticsRegistry::registerStat(&d_statTotLiterals);
-    }
-    ~Statistics() {
-      StatisticsRegistry::unregisterStat(&d_statStarts);
-      StatisticsRegistry::unregisterStat(&d_statDecisions);
-      StatisticsRegistry::unregisterStat(&d_statRndDecisions);
-      StatisticsRegistry::unregisterStat(&d_statPropagations);
-      StatisticsRegistry::unregisterStat(&d_statConflicts);
-      StatisticsRegistry::unregisterStat(&d_statClausesLiterals);
-      StatisticsRegistry::unregisterStat(&d_statLearntsLiterals);
-      StatisticsRegistry::unregisterStat(&d_statMaxLiterals);
-      StatisticsRegistry::unregisterStat(&d_statTotLiterals);
-    }
-    void init(Minisat::SimpSolver* d_minisat){
-      d_statStarts.setData(d_minisat->starts);
-      d_statDecisions.setData(d_minisat->decisions);
-      d_statRndDecisions.setData(d_minisat->rnd_decisions);
-      d_statPropagations.setData(d_minisat->propagations);
-      d_statConflicts.setData(d_minisat->conflicts);
-      d_statClausesLiterals.setData(d_minisat->clauses_literals);
-      d_statLearntsLiterals.setData(d_minisat->learnts_literals);
-      d_statMaxLiterals.setData(d_minisat->max_literals);
-      d_statTotLiterals.setData(d_minisat->tot_literals);
-    }
+    Statistics();
+    ~Statistics();
+    void init(Minisat::SimpSolver* d_minisat);
   };
   Statistics d_statistics;
 
@@ -391,8 +287,6 @@ class SatSolverFactory {
 public:
   static  MinisatSatSolver*      createMinisat();
   static  DPLLMinisatSatSolver*  createDPLLMinisat(); 
-  //static  PicosatSatSolver*      createPicosat();
-  //static  DPLLPicosatSatSolver*      createDPLLPicosat(context::Context* context); 
 }; 
 
 }/* prop namespace */