moving minisat implementation into their respective directories (regular and bv)

1 files changed, 35 insertions, 149 deletions

diff --git a/src/prop/sat_solver.h b/src/prop/sat_solver.h
index 56c6c2783..3b8e1ccbf 100644
--- a/src/prop/sat_solver.h
+++ b/src/prop/sat_solver.h
@@ -26,24 +26,6 @@
 #include "util/stats.h"
 #include "context/cdlist.h"
 
-// DPLLT Minisat
-#include "prop/minisat/core/SolverTypes.h"
-
-// BV Minisat
-#include "prop/bvminisat/core/SolverTypes.h"
-
-
-namespace Minisat{
-class Solver;
-class SimpSolver; 
-}
-
-namespace BVMinisat{
-class Solver;
-class SimpSolver; 
-}
-
-
 namespace CVC4 {
 namespace prop {
 
@@ -55,7 +37,6 @@ enum SatLiteralValue {
   SatValFalse 
 };
 
-
 typedef uint64_t SatVariable; 
 // special constant
 const SatVariable undefSatVariable = SatVariable(-1); 
@@ -154,144 +135,49 @@ public:
 
 }; 
 
-// toodo add ifdef
-
-
-class MinisatSatSolver: public BVSatSolverInterface {
-  BVMinisat::SimpSolver* d_minisat; 
-
-  MinisatSatSolver();
+class SatSolverFactory {
 public:
-  ~MinisatSatSolver();
-  void addClause(SatClause& clause, bool removable);
-
-  SatVariable newVar(bool theoryAtom = false);
-
-  void markUnremovable(SatLiteral lit); 
- 
-  void interrupt();
-
-  SatLiteralValue solve();
-  SatLiteralValue solve(long unsigned int&);
-  SatLiteralValue solve(const context::CDList<SatLiteral> & assumptions);
-  void getUnsatCore(SatClause& unsatCore); 
-  
-  SatLiteralValue value(SatLiteral l);
-  SatLiteralValue modelValue(SatLiteral l);
-
-  void unregisterVar(SatLiteral lit);
-  void renewVar(SatLiteral lit, int level = -1);
-  int getAssertionLevel() const;
-
-
-  // helper methods for converting from the internal Minisat representation
-
-  static SatVariable     toSatVariable(BVMinisat::Var var); 
-  static BVMinisat::Lit    toMinisatLit(SatLiteral lit);
-  static SatLiteral      toSatLiteral(BVMinisat::Lit lit);
-  static SatLiteralValue toSatLiteralValue(bool res);
-  static SatLiteralValue toSatLiteralValue(BVMinisat::lbool res);
- 
-  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;
-    ReferenceStat<uint64_t> d_statRndDecisions, d_statPropagations;
-    ReferenceStat<uint64_t> d_statConflicts, d_statClausesLiterals;
-    ReferenceStat<uint64_t> d_statLearntsLiterals,  d_statMaxLiterals;
-    ReferenceStat<uint64_t> d_statTotLiterals;
-    ReferenceStat<int> d_statEliminatedVars;
-    Statistics();
-    ~Statistics();
-    void init(BVMinisat::SimpSolver* minisat);
-  };
-  
-  Statistics d_statistics;
-  friend class SatSolverFactory;
+  static  BVSatSolverInterface*      createMinisat();
+  static  DPLLSatSolverInterface*  createDPLLMinisat();
 }; 
 
+}/* prop namespace */
 
-class DPLLMinisatSatSolver : public DPLLSatSolverInterface {
-
-  /** The SatSolver used */
-  Minisat::SimpSolver* d_minisat;
-  
-
-  /** The SatSolver uses this to communicate with the theories */ 
-  TheoryProxy* d_theoryProxy;
-
-  /** Context we will be using to synchronzie the sat solver */
-  context::Context* d_context;
-
-  DPLLMinisatSatSolver ();
-  
-public:
-
-  ~DPLLMinisatSatSolver(); 
-  static SatVariable     toSatVariable(Minisat::Var var); 
-  static Minisat::Lit    toMinisatLit(SatLiteral lit);
-  static SatLiteral      toSatLiteral(Minisat::Lit lit);
-  static SatLiteralValue toSatLiteralValue(bool res);
-  static SatLiteralValue toSatLiteralValue(Minisat::lbool res);
- 
-  static void  toMinisatClause(SatClause& clause, Minisat::vec<Minisat::Lit>& minisat_clause);
-  static void  toSatClause    (Minisat::vec<Minisat::Lit>& clause, SatClause& sat_clause); 
-  
-  void initialize(context::Context* context, TheoryProxy* theoryProxy); 
-  
-  void addClause(SatClause& clause, bool removable);
-
-  SatVariable newVar(bool theoryAtom = false);
-
-  SatLiteralValue solve();
-  SatLiteralValue solve(long unsigned int&); 
-
-  void interrupt();
-
-  SatLiteralValue value(SatLiteral l);
-
-  SatLiteralValue modelValue(SatLiteral l);
-
-  bool properExplanation(SatLiteral lit, SatLiteral expl) const;
-
-  /** Incremental interface */ 
-  
-  int getAssertionLevel() const;
-  
-  void push();
-
-  void pop();
-
-  void unregisterVar(SatLiteral lit);
-
-  void renewVar(SatLiteral lit, int level = -1);
+inline std::ostream& operator <<(std::ostream& out, prop::SatLiteral lit) {
+  out << lit.toString();
+  return out;
+}
 
-  class Statistics {
-  private:
-    ReferenceStat<uint64_t> d_statStarts, d_statDecisions;
-    ReferenceStat<uint64_t> d_statRndDecisions, d_statPropagations;
-    ReferenceStat<uint64_t> d_statConflicts, d_statClausesLiterals;
-    ReferenceStat<uint64_t> d_statLearntsLiterals,  d_statMaxLiterals;
-    ReferenceStat<uint64_t> d_statTotLiterals;
-  public:
-    Statistics();
-    ~Statistics();
-    void init(Minisat::SimpSolver* d_minisat);
-  };
-  Statistics d_statistics;
+inline std::ostream& operator <<(std::ostream& out, const prop::SatClause& clause) {
+  out << "clause:";
+  for(unsigned i = 0; i < clause.size(); ++i) {
+    out << " " << clause[i];
+  }
+  out << ";";
+  return out;
+}
 
-  friend class SatSolverFactory;   
-}; 
+inline std::ostream& operator <<(std::ostream& out, prop::SatLiteralValue val) {
+  std::string str;
+  switch(val) {
+  case prop::SatValUnknown:
+    str = "_";
+    break;
+  case prop::SatValTrue:
+    str = "1";
+    break;
+  case prop::SatValFalse:
+    str = "0";
+    break;
+  default:
+    str = "Error";
+    break;
+  }
 
-class SatSolverFactory {
-public:
-  static  MinisatSatSolver*      createMinisat();
-  static  DPLLMinisatSatSolver*  createDPLLMinisat(); 
-}; 
+  out << str;
+  return out;
+}
 
-}/* prop namespace */
 }/* CVC4 namespace */
 
 #endif /* __CVC4__PROP__SAT_MODULE_H */