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

10 files changed, 694 insertions, 618 deletions

diff --git a/src/prop/bvminisat/Makefile.am b/src/prop/bvminisat/Makefile.am
index 480e4e83c..685dfac7d 100644
--- a/src/prop/bvminisat/Makefile.am
+++ b/src/prop/bvminisat/Makefile.am
@@ -22,7 +22,9 @@ libbvminisat_la_SOURCES = \
 	mtl/Sort.h \
 	mtl/Vec.h \
 	mtl/XAlloc.h \
-	utils/Options.h 
+	utils/Options.h \
+	bvminisat.h \
+	bvminisat.cpp
 
 EXTRA_DIST = \
 	core/Main.cc \
diff --git a/src/prop/bvminisat/bvminisat.cpp b/src/prop/bvminisat/bvminisat.cpp
new file mode 100644
index 000000000..d4e123489
--- /dev/null
+++ b/src/prop/bvminisat/bvminisat.cpp
@@ -0,0 +1,232 @@
+/*********************                                                        */
+/*! \file bvminisat.cpp
+ ** \verbatim
+ ** Original author: dejan
+ ** Major contributors:
+ ** Minor contributors (to current version):
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief SAT Solver.
+ **
+ ** Implementation of the minisat for cvc4 (bitvectors).
+ **/
+
+#include "prop/bvminisat/bvminisat.h"
+#include "prop/bvminisat/simp/SimpSolver.h"
+
+using namespace CVC4;
+using namespace prop;
+
+MinisatSatSolver::MinisatSatSolver() :
+  d_minisat(new BVMinisat::SimpSolver())
+{
+  d_statistics.init(d_minisat);
+}
+
+MinisatSatSolver::~MinisatSatSolver() {
+  delete d_minisat;
+}
+
+void MinisatSatSolver::addClause(SatClause& clause, bool removable) {
+  Debug("sat::minisat") << "Add clause " << clause <<"\n";
+  BVMinisat::vec<BVMinisat::Lit> minisat_clause;
+  toMinisatClause(clause, minisat_clause);
+  // for(unsigned i = 0; i < minisat_clause.size(); ++i) {
+  //   d_minisat->setFrozen(BVMinisat::var(minisat_clause[i]), true);
+  // }
+  d_minisat->addClause(minisat_clause);
+}
+
+SatVariable MinisatSatSolver::newVar(bool freeze){
+  return d_minisat->newVar(true, true, freeze);
+}
+
+void MinisatSatSolver::markUnremovable(SatLiteral lit){
+  d_minisat->setFrozen(BVMinisat::var(toMinisatLit(lit)), true);
+}
+
+void MinisatSatSolver::interrupt(){
+  d_minisat->interrupt();
+}
+
+SatLiteralValue MinisatSatSolver::solve(){
+  return toSatLiteralValue(d_minisat->solve());
+}
+
+SatLiteralValue MinisatSatSolver::solve(long unsigned int& resource){
+  Trace("limit") << "MinisatSatSolver::solve(): have limit of " << resource << " conflicts" << std::endl;
+  if(resource == 0) {
+    d_minisat->budgetOff();
+  } else {
+    d_minisat->setConfBudget(resource);
+  }
+  BVMinisat::vec<BVMinisat::Lit> empty;
+  unsigned long conflictsBefore = d_minisat->conflicts;
+  SatLiteralValue result = toSatLiteralValue(d_minisat->solveLimited(empty));
+  d_minisat->clearInterrupt();
+  resource = d_minisat->conflicts - conflictsBefore;
+  Trace("limit") << "<MinisatSatSolver::solve(): it took " << resource << " conflicts" << std::endl;
+  return result;
+}
+
+SatLiteralValue MinisatSatSolver::solve(const context::CDList<SatLiteral> & assumptions){
+  Debug("sat::minisat") << "Solve with assumptions ";
+  context::CDList<SatLiteral>::const_iterator it = assumptions.begin();
+  BVMinisat::vec<BVMinisat::Lit> assump;
+  for(; it!= assumptions.end(); ++it) {
+    SatLiteral lit = *it;
+    Debug("sat::minisat") << lit <<" ";
+    assump.push(toMinisatLit(lit));
+  }
+  Debug("sat::minisat") <<"\n";
+
+ SatLiteralValue result = toSatLiteralValue(d_minisat->solve(assump));
+ return result;
+}
+
+
+void MinisatSatSolver::getUnsatCore(SatClause& unsatCore) {
+  // TODO add assertion to check the call was after an unsat call
+  for (int i = 0; i < d_minisat->conflict.size(); ++i) {
+    unsatCore.push_back(toSatLiteral(d_minisat->conflict[i]));
+  }
+}
+
+SatLiteralValue MinisatSatSolver::value(SatLiteral l){
+    Unimplemented();
+    return SatValUnknown;
+}
+
+SatLiteralValue MinisatSatSolver::modelValue(SatLiteral l){
+    Unimplemented();
+    return SatValUnknown;
+}
+
+void MinisatSatSolver::unregisterVar(SatLiteral lit) {
+  // this should only be called when user context is implemented
+  // in the BVSatSolver
+  Unreachable();
+}
+
+void MinisatSatSolver::renewVar(SatLiteral lit, int level) {
+  // this should only be called when user context is implemented
+  // in the BVSatSolver
+
+  Unreachable();
+}
+
+int MinisatSatSolver::getAssertionLevel() const {
+  // we have no user context implemented so far
+  return 0;
+}
+
+// converting from internal Minisat representation
+
+SatVariable MinisatSatSolver::toSatVariable(BVMinisat::Var var) {
+  if (var == var_Undef) {
+    return undefSatVariable;
+  }
+  return SatVariable(var);
+}
+
+BVMinisat::Lit MinisatSatSolver::toMinisatLit(SatLiteral lit) {
+  if (lit == undefSatLiteral) {
+    return BVMinisat::lit_Undef;
+  }
+  return BVMinisat::mkLit(lit.getSatVariable(), lit.isNegated());
+}
+
+SatLiteral MinisatSatSolver::toSatLiteral(BVMinisat::Lit lit) {
+  if (lit == BVMinisat::lit_Undef) {
+    return undefSatLiteral;
+  }
+
+  return SatLiteral(SatVariable(BVMinisat::var(lit)),
+                    BVMinisat::sign(lit));
+}
+
+SatLiteralValue MinisatSatSolver::toSatLiteralValue(bool res) {
+  if(res) return SatValTrue;
+  else return SatValFalse;
+}
+
+SatLiteralValue MinisatSatSolver::toSatLiteralValue(BVMinisat::lbool res) {
+  if(res == (BVMinisat::lbool((uint8_t)0))) return SatValTrue;
+  if(res == (BVMinisat::lbool((uint8_t)2))) return SatValUnknown;
+  Assert(res == (BVMinisat::lbool((uint8_t)1)));
+  return SatValFalse;
+}
+
+void MinisatSatSolver::toMinisatClause(SatClause& clause,
+                                           BVMinisat::vec<BVMinisat::Lit>& minisat_clause) {
+  for (unsigned i = 0; i < clause.size(); ++i) {
+    minisat_clause.push(toMinisatLit(clause[i]));
+  }
+  Assert(clause.size() == (unsigned)minisat_clause.size());
+}
+
+void MinisatSatSolver::toSatClause(BVMinisat::vec<BVMinisat::Lit>& clause,
+                                       SatClause& sat_clause) {
+  for (int i = 0; i < clause.size(); ++i) {
+    sat_clause.push_back(toSatLiteral(clause[i]));
+  }
+  Assert((unsigned)clause.size() == sat_clause.size());
+}
+
+
+// Satistics for MinisatSatSolver
+
+MinisatSatSolver::Statistics::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);
+}
+
+MinisatSatSolver::Statistics::~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 MinisatSatSolver::Statistics::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);
+}
diff --git a/src/prop/bvminisat/bvminisat.h b/src/prop/bvminisat/bvminisat.h
new file mode 100644
index 000000000..7c12fcbd0
--- /dev/null
+++ b/src/prop/bvminisat/bvminisat.h
@@ -0,0 +1,87 @@
+/*********************                                                        */
+/*! \file bvminisat.h
+ ** \verbatim
+ ** Original author: dejan
+ ** Major contributors:
+ ** Minor contributors (to current version):
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief SAT Solver.
+ **
+ ** Implementation of the minisat for cvc4 (bitvectors).
+ **/
+
+#pragma once
+
+#include "prop/sat_solver.h"
+#include "prop/bvminisat/simp/SimpSolver.h"
+
+namespace CVC4 {
+namespace prop {
+
+class MinisatSatSolver: public BVSatSolverInterface {
+  BVMinisat::SimpSolver* d_minisat;
+
+  MinisatSatSolver();
+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;
+};
+
+}
+}
+
+
+
+
diff --git a/src/prop/minisat/Makefile.am b/src/prop/minisat/Makefile.am
index 6e003c248..045cc3616 100644
--- a/src/prop/minisat/Makefile.am
+++ b/src/prop/minisat/Makefile.am
@@ -22,7 +22,9 @@ libminisat_la_SOURCES = \
 	mtl/Sort.h \
 	mtl/Vec.h \
 	mtl/XAlloc.h \
-	utils/Options.h 
+	utils/Options.h \
+	minisat.cpp \
+	minisat.h
 
 EXTRA_DIST = \
 	core/Main.cc \
diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index e5a6d32e1..d75421e25 100644
--- a/src/prop/minisat/core/Solver.cc
+++ b/src/prop/minisat/core/Solver.cc
@@ -26,7 +26,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include "prop/minisat/core/Solver.h"
 
 #include "prop/theory_proxy.h"
-#include "prop/sat_solver.h"
+#include "prop/minisat/minisat.h"
 #include "util/output.h"
 #include "expr/command.h"
 #include "proof/proof_manager.h"
diff --git a/src/prop/minisat/minisat.cpp b/src/prop/minisat/minisat.cpp
new file mode 100644
index 000000000..bc611a097
--- /dev/null
+++ b/src/prop/minisat/minisat.cpp
@@ -0,0 +1,228 @@
+/*********************                                                        */
+/*! \file minisat.cpp
+ ** \verbatim
+ ** Original author: dejan
+ ** Major contributors:
+ ** Minor contributors (to current version):
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief SAT Solver.
+ **
+ ** Implementation of the minisat for cvc4.
+ **/
+
+#include "prop/minisat/minisat.h"
+#include "prop/minisat/simp/SimpSolver.h"
+
+using namespace CVC4;
+using namespace CVC4::prop;
+
+//// DPllMinisatSatSolver
+
+DPLLMinisatSatSolver::DPLLMinisatSatSolver() :
+  d_minisat(NULL),
+  d_theoryProxy(NULL),
+  d_context(NULL)
+{}
+
+DPLLMinisatSatSolver::~DPLLMinisatSatSolver() {
+  delete d_minisat;
+}
+
+SatVariable DPLLMinisatSatSolver::toSatVariable(Minisat::Var var) {
+  if (var == var_Undef) {
+    return undefSatVariable;
+  }
+  return SatVariable(var);
+}
+
+Minisat::Lit DPLLMinisatSatSolver::toMinisatLit(SatLiteral lit) {
+  if (lit == undefSatLiteral) {
+    return Minisat::lit_Undef;
+  }
+  return Minisat::mkLit(lit.getSatVariable(), lit.isNegated());
+}
+
+SatLiteral DPLLMinisatSatSolver::toSatLiteral(Minisat::Lit lit) {
+  if (lit == Minisat::lit_Undef) {
+    return undefSatLiteral;
+  }
+
+  return SatLiteral(SatVariable(Minisat::var(lit)),
+                    Minisat::sign(lit));
+}
+
+SatLiteralValue DPLLMinisatSatSolver::toSatLiteralValue(bool res) {
+  if(res) return SatValTrue;
+  else return SatValFalse;
+}
+
+SatLiteralValue DPLLMinisatSatSolver::toSatLiteralValue(Minisat::lbool res) {
+  if(res == (Minisat::lbool((uint8_t)0))) return SatValTrue;
+  if(res == (Minisat::lbool((uint8_t)2))) return SatValUnknown;
+  Assert(res == (Minisat::lbool((uint8_t)1)));
+  return SatValFalse;
+}
+
+
+void DPLLMinisatSatSolver::toMinisatClause(SatClause& clause,
+                                           Minisat::vec<Minisat::Lit>& minisat_clause) {
+  for (unsigned i = 0; i < clause.size(); ++i) {
+    minisat_clause.push(toMinisatLit(clause[i]));
+  }
+  Assert(clause.size() == (unsigned)minisat_clause.size());
+}
+
+void DPLLMinisatSatSolver::toSatClause(Minisat::vec<Minisat::Lit>& clause,
+                                       SatClause& sat_clause) {
+  for (int i = 0; i < clause.size(); ++i) {
+    sat_clause.push_back(toSatLiteral(clause[i]));
+  }
+  Assert((unsigned)clause.size() == sat_clause.size());
+}
+
+
+void DPLLMinisatSatSolver::initialize(context::Context* context, TheoryProxy* theoryProxy)
+{
+
+  d_context = context;
+
+  // Create the solver
+  d_minisat = new Minisat::SimpSolver(theoryProxy, d_context,
+                                      Options::current()->incrementalSolving);
+  // Setup the verbosity
+  d_minisat->verbosity = (Options::current()->verbosity > 0) ? 1 : -1;
+
+  // Setup the random decision parameters
+  d_minisat->random_var_freq = Options::current()->satRandomFreq;
+  d_minisat->random_seed = Options::current()->satRandomSeed;
+  // Give access to all possible options in the sat solver
+  d_minisat->var_decay = Options::current()->satVarDecay;
+  d_minisat->clause_decay = Options::current()->satClauseDecay;
+  d_minisat->restart_first = Options::current()->satRestartFirst;
+  d_minisat->restart_inc = Options::current()->satRestartInc;
+
+  d_statistics.init(d_minisat);
+}
+
+void DPLLMinisatSatSolver::addClause(SatClause& clause, bool removable) {
+  Minisat::vec<Minisat::Lit> minisat_clause;
+  toMinisatClause(clause, minisat_clause);
+  d_minisat->addClause(minisat_clause, removable);
+}
+
+SatVariable DPLLMinisatSatSolver::newVar(bool theoryAtom) {
+  return d_minisat->newVar(true, true, theoryAtom);
+}
+
+
+SatLiteralValue DPLLMinisatSatSolver::solve(unsigned long& resource) {
+  Trace("limit") << "SatSolver::solve(): have limit of " << resource << " conflicts" << std::endl;
+  if(resource == 0) {
+    d_minisat->budgetOff();
+  } else {
+    d_minisat->setConfBudget(resource);
+  }
+  Minisat::vec<Minisat::Lit> empty;
+  unsigned long conflictsBefore = d_minisat->conflicts;
+  SatLiteralValue result = toSatLiteralValue(d_minisat->solveLimited(empty));
+  d_minisat->clearInterrupt();
+  resource = d_minisat->conflicts - conflictsBefore;
+  Trace("limit") << "SatSolver::solve(): it took " << resource << " conflicts" << std::endl;
+  return result;
+}
+
+SatLiteralValue DPLLMinisatSatSolver::solve() {
+  d_minisat->budgetOff();
+  return toSatLiteralValue(d_minisat->solve());
+}
+
+
+void DPLLMinisatSatSolver::interrupt() {
+  d_minisat->interrupt();
+}
+
+SatLiteralValue DPLLMinisatSatSolver::value(SatLiteral l) {
+  return toSatLiteralValue(d_minisat->value(toMinisatLit(l)));
+}
+
+SatLiteralValue DPLLMinisatSatSolver::modelValue(SatLiteral l){
+  return toSatLiteralValue(d_minisat->modelValue(toMinisatLit(l)));
+}
+
+bool DPLLMinisatSatSolver::properExplanation(SatLiteral lit, SatLiteral expl) const {
+  return true;
+}
+
+/** Incremental interface */
+
+int DPLLMinisatSatSolver::getAssertionLevel() const {
+  return d_minisat->getAssertionLevel();
+}
+
+void DPLLMinisatSatSolver::push() {
+  d_minisat->push();
+}
+
+void DPLLMinisatSatSolver::pop(){
+  d_minisat->pop();
+}
+
+void DPLLMinisatSatSolver::unregisterVar(SatLiteral lit) {
+  d_minisat->unregisterVar(toMinisatLit(lit));
+}
+
+void DPLLMinisatSatSolver::renewVar(SatLiteral lit, int level) {
+  d_minisat->renewVar(toMinisatLit(lit), level);
+}
+
+/// Statistics for DPLLMinisatSatSolver
+
+DPLLMinisatSatSolver::Statistics::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);
+}
+DPLLMinisatSatSolver::Statistics::~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 DPLLMinisatSatSolver::Statistics::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);
+}
diff --git a/src/prop/minisat/minisat.h b/src/prop/minisat/minisat.h
new file mode 100644
index 000000000..81a12c491
--- /dev/null
+++ b/src/prop/minisat/minisat.h
@@ -0,0 +1,101 @@
+/*********************                                                        */
+/*! \file minisat.h
+ ** \verbatim
+ ** Original author: dejan
+ ** Major contributors:
+ ** Minor contributors (to current version):
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief SAT Solver.
+ **
+ ** Implementation of the minisat for cvc4.
+ **/
+
+#pragma once
+
+#include "prop/sat_solver.h"
+#include "prop/minisat/simp/SimpSolver.h"
+
+namespace CVC4 {
+namespace prop {
+
+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);
+
+  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;
+
+  friend class SatSolverFactory;
+};
+
+} // prop namespace
+} // cvc4 namespace
+
diff --git a/src/prop/sat_solver.cpp b/src/prop/sat_solver.cpp
index 13f2498f2..d3710b617 100644
--- a/src/prop/sat_solver.cpp
+++ b/src/prop/sat_solver.cpp
@@ -24,12 +24,8 @@
 #include "expr/expr_stream.h"
 #include "prop/theory_proxy.h"
 
-// DPLLT Minisat
-#include "prop/minisat/simp/SimpSolver.h"
-
-// BV Minisat
-#include "prop/bvminisat/simp/SimpSolver.h"
-
+#include "prop/minisat/minisat.h"
+#include "prop/bvminisat/bvminisat.h"
 
 using namespace std; 
 
@@ -42,434 +38,11 @@ string SatLiteral::toString() {
   return os.str(); 
 }
 
-MinisatSatSolver::MinisatSatSolver() :
-  d_minisat(new BVMinisat::SimpSolver())
-{
-  d_statistics.init(d_minisat); 
-}
-
-MinisatSatSolver::~MinisatSatSolver() {
-  delete d_minisat; 
-}
-
-void MinisatSatSolver::addClause(SatClause& clause, bool removable) {
-  Debug("sat::minisat") << "Add clause " << clause <<"\n"; 
-  BVMinisat::vec<BVMinisat::Lit> minisat_clause;
-  toMinisatClause(clause, minisat_clause);
-  // for(unsigned i = 0; i < minisat_clause.size(); ++i) {
-  //   d_minisat->setFrozen(BVMinisat::var(minisat_clause[i]), true); 
-  // }
-  d_minisat->addClause(minisat_clause);
-}
-
-SatVariable MinisatSatSolver::newVar(bool freeze){
-  return d_minisat->newVar(true, true, freeze);
-}
-
-void MinisatSatSolver::markUnremovable(SatLiteral lit){
-  d_minisat->setFrozen(BVMinisat::var(toMinisatLit(lit)), true);
-}
- 
-void MinisatSatSolver::interrupt(){
-  d_minisat->interrupt(); 
-}
-
-SatLiteralValue MinisatSatSolver::solve(){
-  return toSatLiteralValue(d_minisat->solve()); 
-}
-
-SatLiteralValue MinisatSatSolver::solve(long unsigned int& resource){
-  Trace("limit") << "MinisatSatSolver::solve(): have limit of " << resource << " conflicts" << std::endl;
-  if(resource == 0) {
-    d_minisat->budgetOff();
-  } else {
-    d_minisat->setConfBudget(resource);
-  }
-  BVMinisat::vec<BVMinisat::Lit> empty;
-  unsigned long conflictsBefore = d_minisat->conflicts;
-  SatLiteralValue result = toSatLiteralValue(d_minisat->solveLimited(empty));
-  d_minisat->clearInterrupt();
-  resource = d_minisat->conflicts - conflictsBefore;
-  Trace("limit") << "<MinisatSatSolver::solve(): it took " << resource << " conflicts" << std::endl;
-  return result;
-}
-
-SatLiteralValue MinisatSatSolver::solve(const context::CDList<SatLiteral> & assumptions){
-  Debug("sat::minisat") << "Solve with assumptions ";
-  context::CDList<SatLiteral>::const_iterator it = assumptions.begin();
-  BVMinisat::vec<BVMinisat::Lit> assump; 
-  for(; it!= assumptions.end(); ++it) {
-    SatLiteral lit = *it;
-    Debug("sat::minisat") << lit <<" "; 
-    assump.push(toMinisatLit(lit)); 
-  }
-  Debug("sat::minisat") <<"\n";
-  
- SatLiteralValue result = toSatLiteralValue(d_minisat->solve(assump));
- return result;
-}
-
-
-void MinisatSatSolver::getUnsatCore(SatClause& unsatCore) {
-  // TODO add assertion to check the call was after an unsat call
-  for (int i = 0; i < d_minisat->conflict.size(); ++i) {
-    unsatCore.push_back(toSatLiteral(d_minisat->conflict[i])); 
-  }
-}
-
-SatLiteralValue MinisatSatSolver::value(SatLiteral l){
-    Unimplemented();
-    return SatValUnknown; 
-}
-
-SatLiteralValue MinisatSatSolver::modelValue(SatLiteral l){
-    Unimplemented();
-    return SatValUnknown; 
-}
-
-void MinisatSatSolver::unregisterVar(SatLiteral lit) {
-  // this should only be called when user context is implemented
-  // in the BVSatSolver 
-  Unreachable();
-}
-
-void MinisatSatSolver::renewVar(SatLiteral lit, int level) {
-  // this should only be called when user context is implemented
-  // in the BVSatSolver 
-
-  Unreachable(); 
-}
-
-int MinisatSatSolver::getAssertionLevel() const {
-  // we have no user context implemented so far
-  return 0;
-}
-
-// converting from internal Minisat representation
-
-SatVariable MinisatSatSolver::toSatVariable(BVMinisat::Var var) {
-  if (var == var_Undef) {
-    return undefSatVariable; 
-  }
-  return SatVariable(var);
-}
-
-BVMinisat::Lit MinisatSatSolver::toMinisatLit(SatLiteral lit) {
-  if (lit == undefSatLiteral) {
-    return BVMinisat::lit_Undef;
-  }
-  return BVMinisat::mkLit(lit.getSatVariable(), lit.isNegated()); 
-}
-
-SatLiteral MinisatSatSolver::toSatLiteral(BVMinisat::Lit lit) {
-  if (lit == BVMinisat::lit_Undef) {
-    return undefSatLiteral; 
-  }
-  
-  return SatLiteral(SatVariable(BVMinisat::var(lit)),
-                    BVMinisat::sign(lit)); 
-}
-
-SatLiteralValue MinisatSatSolver::toSatLiteralValue(bool res) {
-  if(res) return SatValTrue;
-  else return SatValFalse; 
-}
-
-SatLiteralValue MinisatSatSolver::toSatLiteralValue(BVMinisat::lbool res) {
-  if(res == (BVMinisat::lbool((uint8_t)0))) return SatValTrue;
-  if(res == (BVMinisat::lbool((uint8_t)2))) return SatValUnknown;
-  Assert(res == (BVMinisat::lbool((uint8_t)1)));
-  return SatValFalse; 
-}
-
-void MinisatSatSolver::toMinisatClause(SatClause& clause,
-                                           BVMinisat::vec<BVMinisat::Lit>& minisat_clause) {
-  for (unsigned i = 0; i < clause.size(); ++i) {
-    minisat_clause.push(toMinisatLit(clause[i])); 
-  }
-  Assert(clause.size() == (unsigned)minisat_clause.size()); 
-}
-
-void MinisatSatSolver::toSatClause(BVMinisat::vec<BVMinisat::Lit>& clause,
-                                       SatClause& sat_clause) {
-  for (int i = 0; i < clause.size(); ++i) {
-    sat_clause.push_back(toSatLiteral(clause[i])); 
-  }
-  Assert((unsigned)clause.size() == sat_clause.size()); 
-}
-
-
-// Satistics for MinisatSatSolver
-
-MinisatSatSolver::Statistics::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);
-}
-
-MinisatSatSolver::Statistics::~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 MinisatSatSolver::Statistics::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);
-}
-
-
-
-//// DPllMinisatSatSolver
-
-DPLLMinisatSatSolver::DPLLMinisatSatSolver() :
-  d_minisat(NULL), 
-  d_theoryProxy(NULL),
-  d_context(NULL)
-{}
-
-DPLLMinisatSatSolver::~DPLLMinisatSatSolver() {
-  delete d_minisat; 
-}
-
-SatVariable DPLLMinisatSatSolver::toSatVariable(Minisat::Var var) {
-  if (var == var_Undef) {
-    return undefSatVariable; 
-  }
-  return SatVariable(var);
-}
-
-Minisat::Lit DPLLMinisatSatSolver::toMinisatLit(SatLiteral lit) {
-  if (lit == undefSatLiteral) {
-    return Minisat::lit_Undef;
-  }
-  return Minisat::mkLit(lit.getSatVariable(), lit.isNegated()); 
-}
-
-SatLiteral DPLLMinisatSatSolver::toSatLiteral(Minisat::Lit lit) {
-  if (lit == Minisat::lit_Undef) {
-    return undefSatLiteral; 
-  }
-  
-  return SatLiteral(SatVariable(Minisat::var(lit)),
-                    Minisat::sign(lit)); 
-}
-
-SatLiteralValue DPLLMinisatSatSolver::toSatLiteralValue(bool res) {
-  if(res) return SatValTrue;
-  else return SatValFalse; 
-}
-
-SatLiteralValue DPLLMinisatSatSolver::toSatLiteralValue(Minisat::lbool res) {
-  if(res == (Minisat::lbool((uint8_t)0))) return SatValTrue;
-  if(res == (Minisat::lbool((uint8_t)2))) return SatValUnknown;
-  Assert(res == (Minisat::lbool((uint8_t)1)));
-  return SatValFalse; 
-}
-
-
-void DPLLMinisatSatSolver::toMinisatClause(SatClause& clause,
-                                           Minisat::vec<Minisat::Lit>& minisat_clause) {
-  for (unsigned i = 0; i < clause.size(); ++i) {
-    minisat_clause.push(toMinisatLit(clause[i])); 
-  }
-  Assert(clause.size() == (unsigned)minisat_clause.size()); 
-}
-
-void DPLLMinisatSatSolver::toSatClause(Minisat::vec<Minisat::Lit>& clause,
-                                       SatClause& sat_clause) {
-  for (int i = 0; i < clause.size(); ++i) {
-    sat_clause.push_back(toSatLiteral(clause[i])); 
-  }
-  Assert((unsigned)clause.size() == sat_clause.size()); 
-}
-
-
-void DPLLMinisatSatSolver::initialize(context::Context* context, TheoryProxy* theoryProxy)
-{
-
-  d_context = context;
-  
-  // Create the solver
-  d_minisat = new Minisat::SimpSolver(theoryProxy, d_context,
-                                      Options::current()->incrementalSolving);
-  // Setup the verbosity
-  d_minisat->verbosity = (Options::current()->verbosity > 0) ? 1 : -1;
-
-  // Setup the random decision parameters
-  d_minisat->random_var_freq = Options::current()->satRandomFreq;
-  d_minisat->random_seed = Options::current()->satRandomSeed;
-  // Give access to all possible options in the sat solver
-  d_minisat->var_decay = Options::current()->satVarDecay;
-  d_minisat->clause_decay = Options::current()->satClauseDecay;
-  d_minisat->restart_first = Options::current()->satRestartFirst;
-  d_minisat->restart_inc = Options::current()->satRestartInc;
-
-  d_statistics.init(d_minisat);
-}
-
-void DPLLMinisatSatSolver::addClause(SatClause& clause, bool removable) {
-  Minisat::vec<Minisat::Lit> minisat_clause;
-  toMinisatClause(clause, minisat_clause); 
-  d_minisat->addClause(minisat_clause, removable);
-}
-
-SatVariable DPLLMinisatSatSolver::newVar(bool theoryAtom) {
-  return d_minisat->newVar(true, true, theoryAtom);
-}
-
-  
-SatLiteralValue DPLLMinisatSatSolver::solve(unsigned long& resource) {
-  Trace("limit") << "SatSolver::solve(): have limit of " << resource << " conflicts" << std::endl;
-  if(resource == 0) {
-    d_minisat->budgetOff();
-  } else {
-    d_minisat->setConfBudget(resource);
-  }
-  Minisat::vec<Minisat::Lit> empty;
-  unsigned long conflictsBefore = d_minisat->conflicts;
-  SatLiteralValue result = toSatLiteralValue(d_minisat->solveLimited(empty));
-  d_minisat->clearInterrupt();
-  resource = d_minisat->conflicts - conflictsBefore;
-  Trace("limit") << "SatSolver::solve(): it took " << resource << " conflicts" << std::endl;
-  return result;
-}
-
-SatLiteralValue DPLLMinisatSatSolver::solve() {
-  d_minisat->budgetOff();
-  return toSatLiteralValue(d_minisat->solve()); 
-}
-
-
-void DPLLMinisatSatSolver::interrupt() {
-  d_minisat->interrupt();
-}
-
-SatLiteralValue DPLLMinisatSatSolver::value(SatLiteral l) {
-  return toSatLiteralValue(d_minisat->value(toMinisatLit(l)));
-}
-
-SatLiteralValue DPLLMinisatSatSolver::modelValue(SatLiteral l){
-  return toSatLiteralValue(d_minisat->modelValue(toMinisatLit(l)));
-}
-
-bool DPLLMinisatSatSolver::properExplanation(SatLiteral lit, SatLiteral expl) const {
-  return true;
-}
-
-/** Incremental interface */ 
-  
-int DPLLMinisatSatSolver::getAssertionLevel() const {
-  return d_minisat->getAssertionLevel(); 
-}
-  
-void DPLLMinisatSatSolver::push() {
-  d_minisat->push();
-}
-
-void DPLLMinisatSatSolver::pop(){
-  d_minisat->pop();
-}
-
-void DPLLMinisatSatSolver::unregisterVar(SatLiteral lit) {
-  d_minisat->unregisterVar(toMinisatLit(lit));
-}
-
-void DPLLMinisatSatSolver::renewVar(SatLiteral lit, int level) {
-  d_minisat->renewVar(toMinisatLit(lit), level);
-}
-
-/// Statistics for DPLLMinisatSatSolver
-
-DPLLMinisatSatSolver::Statistics::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);
-}
-DPLLMinisatSatSolver::Statistics::~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 DPLLMinisatSatSolver::Statistics::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);
-}
-
-
-/*
-  
-  SatSolverFactory
-  
- */
-
-MinisatSatSolver* SatSolverFactory::createMinisat() {
+BVSatSolverInterface* SatSolverFactory::createMinisat() {
   return new MinisatSatSolver(); 
 }
 
-DPLLMinisatSatSolver* SatSolverFactory::createDPLLMinisat(){
+DPLLSatSolverInterface* SatSolverFactory::createDPLLMinisat(){
   return new DPLLMinisatSatSolver(); 
 } 
 
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 */
diff --git a/src/prop/theory_proxy.h b/src/prop/theory_proxy.h
index 2934bcad9..8b585710f 100644
--- a/src/prop/theory_proxy.h
+++ b/src/prop/theory_proxy.h
@@ -123,41 +123,6 @@ inline TheoryProxy::TheoryProxy(PropEngine* propEngine,
 
 }/* CVC4::prop namespace */
 
-inline std::ostream& operator <<(std::ostream& out, prop::SatLiteral lit) {
-  out << lit.toString(); 
-  return out;
-}
-
-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;
-}
-
-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;
-  }
-
-  out << str;
-  return out;
-}
-
 }/* CVC4 namespace */
 
 #endif /* __CVC4__PROP__SAT_H */