Some renaming and refactoring in SAT

9 files changed, 268 insertions, 195 deletions

diff --git a/src/prop/Makefile.am b/src/prop/Makefile.am
index e505c168e..730df70aa 100644
--- a/src/prop/Makefile.am
+++ b/src/prop/Makefile.am
@@ -16,6 +16,7 @@ libprop_la_SOURCES = \
 	cnf_stream.h \
 	cnf_stream.cpp \
 	sat_solver.h \
+	sat_solver_types.h \	
 	sat_solver_factory.h \
 	sat_solver_factory.cpp \
 	sat_solver_registry.h \
diff --git a/src/prop/bvminisat/bvminisat.cpp b/src/prop/bvminisat/bvminisat.cpp
index c4c21e126..b32483cbe 100644
--- a/src/prop/bvminisat/bvminisat.cpp
+++ b/src/prop/bvminisat/bvminisat.cpp
@@ -22,17 +22,17 @@
 using namespace CVC4;
 using namespace prop;
 
-MinisatSatSolver::MinisatSatSolver() :
+BVMinisatSatSolver::BVMinisatSatSolver() :
   d_minisat(new BVMinisat::SimpSolver())
 {
   d_statistics.init(d_minisat);
 }
 
-MinisatSatSolver::~MinisatSatSolver() {
+BVMinisatSatSolver::~BVMinisatSatSolver() {
   delete d_minisat;
 }
 
-void MinisatSatSolver::addClause(SatClause& clause, bool removable) {
+void BVMinisatSatSolver::addClause(SatClause& clause, bool removable) {
   Debug("sat::minisat") << "Add clause " << clause <<"\n";
   BVMinisat::vec<BVMinisat::Lit> minisat_clause;
   toMinisatClause(clause, minisat_clause);
@@ -42,23 +42,23 @@ void MinisatSatSolver::addClause(SatClause& clause, bool removable) {
   d_minisat->addClause(minisat_clause);
 }
 
-SatVariable MinisatSatSolver::newVar(bool freeze){
+SatVariable BVMinisatSatSolver::newVar(bool freeze){
   return d_minisat->newVar(true, true, freeze);
 }
 
-void MinisatSatSolver::markUnremovable(SatLiteral lit){
+void BVMinisatSatSolver::markUnremovable(SatLiteral lit){
   d_minisat->setFrozen(BVMinisat::var(toMinisatLit(lit)), true);
 }
 
-void MinisatSatSolver::interrupt(){
+void BVMinisatSatSolver::interrupt(){
   d_minisat->interrupt();
 }
 
-SatValue MinisatSatSolver::solve(){
+SatValue BVMinisatSatSolver::solve(){
   return toSatLiteralValue(d_minisat->solve());
 }
 
-SatValue MinisatSatSolver::solve(long unsigned int& resource){
+SatValue BVMinisatSatSolver::solve(long unsigned int& resource){
   Trace("limit") << "MinisatSatSolver::solve(): have limit of " << resource << " conflicts" << std::endl;
   if(resource == 0) {
     d_minisat->budgetOff();
@@ -74,7 +74,7 @@ SatValue MinisatSatSolver::solve(long unsigned int& resource){
   return result;
 }
 
-SatValue MinisatSatSolver::solve(const context::CDList<SatLiteral> & assumptions){
+SatValue BVMinisatSatSolver::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;
@@ -90,58 +90,58 @@ SatValue MinisatSatSolver::solve(const context::CDList<SatLiteral> & assumptions
 }
 
 
-void MinisatSatSolver::getUnsatCore(SatClause& unsatCore) {
+void BVMinisatSatSolver::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]));
   }
 }
 
-SatValue MinisatSatSolver::value(SatLiteral l){
+SatValue BVMinisatSatSolver::value(SatLiteral l){
     Unimplemented();
     return SAT_VALUE_UNKNOWN;
 }
 
-SatValue MinisatSatSolver::modelValue(SatLiteral l){
+SatValue BVMinisatSatSolver::modelValue(SatLiteral l){
     Unimplemented();
     return SAT_VALUE_UNKNOWN;
 }
 
-void MinisatSatSolver::unregisterVar(SatLiteral lit) {
+void BVMinisatSatSolver::unregisterVar(SatLiteral lit) {
   // this should only be called when user context is implemented
   // in the BVSatSolver
   Unreachable();
 }
 
-void MinisatSatSolver::renewVar(SatLiteral lit, int level) {
+void BVMinisatSatSolver::renewVar(SatLiteral lit, int level) {
   // this should only be called when user context is implemented
   // in the BVSatSolver
 
   Unreachable();
 }
 
-unsigned MinisatSatSolver::getAssertionLevel() const {
+unsigned BVMinisatSatSolver::getAssertionLevel() const {
   // we have no user context implemented so far
   return 0;
 }
 
 // converting from internal Minisat representation
 
-SatVariable MinisatSatSolver::toSatVariable(BVMinisat::Var var) {
+SatVariable BVMinisatSatSolver::toSatVariable(BVMinisat::Var var) {
   if (var == var_Undef) {
     return undefSatVariable;
   }
   return SatVariable(var);
 }
 
-BVMinisat::Lit MinisatSatSolver::toMinisatLit(SatLiteral lit) {
+BVMinisat::Lit BVMinisatSatSolver::toMinisatLit(SatLiteral lit) {
   if (lit == undefSatLiteral) {
     return BVMinisat::lit_Undef;
   }
   return BVMinisat::mkLit(lit.getSatVariable(), lit.isNegated());
 }
 
-SatLiteral MinisatSatSolver::toSatLiteral(BVMinisat::Lit lit) {
+SatLiteral BVMinisatSatSolver::toSatLiteral(BVMinisat::Lit lit) {
   if (lit == BVMinisat::lit_Undef) {
     return undefSatLiteral;
   }
@@ -150,19 +150,19 @@ SatLiteral MinisatSatSolver::toSatLiteral(BVMinisat::Lit lit) {
                     BVMinisat::sign(lit));
 }
 
-SatValue MinisatSatSolver::toSatLiteralValue(bool res) {
+SatValue BVMinisatSatSolver::toSatLiteralValue(bool res) {
   if(res) return SAT_VALUE_TRUE;
   else return SAT_VALUE_FALSE;
 }
 
-SatValue MinisatSatSolver::toSatLiteralValue(BVMinisat::lbool res) {
+SatValue BVMinisatSatSolver::toSatLiteralValue(BVMinisat::lbool res) {
   if(res == (BVMinisat::lbool((uint8_t)0))) return SAT_VALUE_TRUE;
   if(res == (BVMinisat::lbool((uint8_t)2))) return SAT_VALUE_UNKNOWN;
   Assert(res == (BVMinisat::lbool((uint8_t)1)));
   return SAT_VALUE_FALSE;
 }
 
-void MinisatSatSolver::toMinisatClause(SatClause& clause,
+void BVMinisatSatSolver::toMinisatClause(SatClause& clause,
                                            BVMinisat::vec<BVMinisat::Lit>& minisat_clause) {
   for (unsigned i = 0; i < clause.size(); ++i) {
     minisat_clause.push(toMinisatLit(clause[i]));
@@ -170,7 +170,7 @@ void MinisatSatSolver::toMinisatClause(SatClause& clause,
   Assert(clause.size() == (unsigned)minisat_clause.size());
 }
 
-void MinisatSatSolver::toSatClause(BVMinisat::vec<BVMinisat::Lit>& clause,
+void BVMinisatSatSolver::toSatClause(BVMinisat::vec<BVMinisat::Lit>& clause,
                                        SatClause& sat_clause) {
   for (int i = 0; i < clause.size(); ++i) {
     sat_clause.push_back(toSatLiteral(clause[i]));
@@ -179,9 +179,9 @@ void MinisatSatSolver::toSatClause(BVMinisat::vec<BVMinisat::Lit>& clause,
 }
 
 
-// Satistics for MinisatSatSolver
+// Satistics for BVMinisatSatSolver
 
-MinisatSatSolver::Statistics::Statistics() :
+BVMinisatSatSolver::Statistics::Statistics() :
   d_statStarts("theory::bv::bvminisat::starts"),
   d_statDecisions("theory::bv::bvminisat::decisions"),
   d_statRndDecisions("theory::bv::bvminisat::rnd_decisions"),
@@ -205,7 +205,7 @@ MinisatSatSolver::Statistics::Statistics() :
   StatisticsRegistry::registerStat(&d_statEliminatedVars);
 }
 
-MinisatSatSolver::Statistics::~Statistics() {
+BVMinisatSatSolver::Statistics::~Statistics() {
   StatisticsRegistry::unregisterStat(&d_statStarts);
   StatisticsRegistry::unregisterStat(&d_statDecisions);
   StatisticsRegistry::unregisterStat(&d_statRndDecisions);
@@ -218,7 +218,7 @@ MinisatSatSolver::Statistics::~Statistics() {
   StatisticsRegistry::unregisterStat(&d_statEliminatedVars);
 }
 
-void MinisatSatSolver::Statistics::init(BVMinisat::SimpSolver* minisat){
+void BVMinisatSatSolver::Statistics::init(BVMinisat::SimpSolver* minisat){
   d_statStarts.setData(minisat->starts);
   d_statDecisions.setData(minisat->decisions);
   d_statRndDecisions.setData(minisat->rnd_decisions);
diff --git a/src/prop/bvminisat/bvminisat.h b/src/prop/bvminisat/bvminisat.h
index 86fbe4433..d192b34b7 100644
--- a/src/prop/bvminisat/bvminisat.h
+++ b/src/prop/bvminisat/bvminisat.h
@@ -25,12 +25,12 @@
 namespace CVC4 {
 namespace prop {
 
-class MinisatSatSolver: public BVSatSolverInterface {
+class BVMinisatSatSolver: public BVSatSolverInterface {
   BVMinisat::SimpSolver* d_minisat;
 
 public:
-  MinisatSatSolver();
-  ~MinisatSatSolver();
+  BVMinisatSatSolver();
+  ~BVMinisatSatSolver();
   void addClause(SatClause& clause, bool removable);
 
   SatVariable newVar(bool theoryAtom = false);
@@ -79,7 +79,7 @@ public:
   Statistics d_statistics;
 };
 
-template class SatSolverConstructor<MinisatSatSolver>;
+template class SatSolverConstructor<BVMinisatSatSolver>;
 
 }
 }
diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index d75421e25..3a16b0d19 100644
--- a/src/prop/minisat/core/Solver.cc
+++ b/src/prop/minisat/core/Solver.cc
@@ -179,9 +179,9 @@ CRef Solver::reason(Var x) {
 
     // Get the explanation from the theory
     SatClause explanation_cl;
-    proxy->explainPropagation(DPLLMinisatSatSolver::toSatLiteral(l), explanation_cl);
+    proxy->explainPropagation(MinisatSatSolver::toSatLiteral(l), explanation_cl);
     vec<Lit> explanation;
-    DPLLMinisatSatSolver::toMinisatClause(explanation_cl, explanation); 
+    MinisatSatSolver::toMinisatClause(explanation_cl, explanation); 
 
     // Sort the literals by trail index level
     lemma_lt lt(*this);
@@ -343,7 +343,7 @@ void Solver::cancelUntil(int level) {
         int currentLevel = decisionLevel();
         for(int i = variables_to_register.size() - 1; i >= 0 && variables_to_register[i].level > currentLevel; --i) {
           variables_to_register[i].level = currentLevel;
-          proxy->variableNotify(DPLLMinisatSatSolver::toSatVariable(variables_to_register[i].var));
+          proxy->variableNotify(MinisatSatSolver::toSatVariable(variables_to_register[i].var));
         }
     }
 }
@@ -361,7 +361,7 @@ Lit Solver::pickBranchLit()
     Lit nextLit;
 
 #ifdef CVC4_REPLAY
-    nextLit = DPLLMinisatSatSolver::toMinisatLit(proxy->getNextReplayDecision());
+    nextLit = MinisatSatSolver::toMinisatLit(proxy->getNextReplayDecision());
 
     if (nextLit != lit_Undef) {
       return nextLit;
@@ -369,7 +369,7 @@ Lit Solver::pickBranchLit()
 #endif /* CVC4_REPLAY */
 
     // Theory requests
-    nextLit = DPLLMinisatSatSolver::toMinisatLit(proxy->getNextDecisionRequest());
+    nextLit = MinisatSatSolver::toMinisatLit(proxy->getNextDecisionRequest());
     while (nextLit != lit_Undef) {
       if(value(var(nextLit)) == l_Undef) {
         Debug("propagateAsDecision") << "propagateAsDecision(): now deciding on " << nextLit << std::endl;
@@ -377,7 +377,7 @@ Lit Solver::pickBranchLit()
       } else {
         Debug("propagateAsDecision") << "propagateAsDecision(): would decide on " << nextLit << " but it already has an assignment" << std::endl;
       }
-      nextLit = DPLLMinisatSatSolver::toMinisatLit(proxy->getNextDecisionRequest());
+      nextLit = MinisatSatSolver::toMinisatLit(proxy->getNextDecisionRequest());
     }
 
     Var next = var_Undef;
@@ -642,7 +642,7 @@ void Solver::uncheckedEnqueue(Lit p, CRef from)
     }
     if (theory[var(p)]) {
       // Enqueue to the theory
-      proxy->enqueueTheoryLiteral(DPLLMinisatSatSolver::toSatLiteral(p));
+      proxy->enqueueTheoryLiteral(MinisatSatSolver::toSatLiteral(p));
     }
 }
 
@@ -708,7 +708,7 @@ void Solver::propagateTheory() {
   proxy->theoryPropagate(propagatedLiteralsClause);
 
   vec<Lit> propagatedLiterals;
-  DPLLMinisatSatSolver::toMinisatClause(propagatedLiteralsClause, propagatedLiterals); 
+  MinisatSatSolver::toMinisatClause(propagatedLiteralsClause, propagatedLiterals); 
 
   int oldTrailSize = trail.size();
   Debug("minisat") << "old trail size is " << oldTrailSize << ", propagating " << propagatedLiterals.size() << " lits..." << std::endl;
@@ -1079,7 +1079,7 @@ lbool Solver::search(int nof_conflicts)
                 }
 
 #ifdef CVC4_REPLAY
-                proxy->logDecision(DPLLMinisatSatSolver::toSatLiteral(next));
+                proxy->logDecision(MinisatSatSolver::toSatLiteral(next));
 #endif /* CVC4_REPLAY */
             }
 
diff --git a/src/prop/minisat/minisat.cpp b/src/prop/minisat/minisat.cpp
index 1ec81a4f6..c8d310992 100644
--- a/src/prop/minisat/minisat.cpp
+++ b/src/prop/minisat/minisat.cpp
@@ -24,31 +24,31 @@ using namespace CVC4::prop;
 
 //// DPllMinisatSatSolver
 
-DPLLMinisatSatSolver::DPLLMinisatSatSolver() :
+MinisatSatSolver::MinisatSatSolver() :
   d_minisat(NULL),
   d_theoryProxy(NULL),
   d_context(NULL)
 {}
 
-DPLLMinisatSatSolver::~DPLLMinisatSatSolver() {
+MinisatSatSolver::~MinisatSatSolver() {
   delete d_minisat;
 }
 
-SatVariable DPLLMinisatSatSolver::toSatVariable(Minisat::Var var) {
+SatVariable MinisatSatSolver::toSatVariable(Minisat::Var var) {
   if (var == var_Undef) {
     return undefSatVariable;
   }
   return SatVariable(var);
 }
 
-Minisat::Lit DPLLMinisatSatSolver::toMinisatLit(SatLiteral lit) {
+Minisat::Lit MinisatSatSolver::toMinisatLit(SatLiteral lit) {
   if (lit == undefSatLiteral) {
     return Minisat::lit_Undef;
   }
   return Minisat::mkLit(lit.getSatVariable(), lit.isNegated());
 }
 
-SatLiteral DPLLMinisatSatSolver::toSatLiteral(Minisat::Lit lit) {
+SatLiteral MinisatSatSolver::toSatLiteral(Minisat::Lit lit) {
   if (lit == Minisat::lit_Undef) {
     return undefSatLiteral;
   }
@@ -57,12 +57,12 @@ SatLiteral DPLLMinisatSatSolver::toSatLiteral(Minisat::Lit lit) {
                     Minisat::sign(lit));
 }
 
-SatValue DPLLMinisatSatSolver::toSatLiteralValue(bool res) {
+SatValue MinisatSatSolver::toSatLiteralValue(bool res) {
   if(res) return SAT_VALUE_TRUE;
   else return SAT_VALUE_FALSE;
 }
 
-SatValue DPLLMinisatSatSolver::toSatLiteralValue(Minisat::lbool res) {
+SatValue MinisatSatSolver::toSatLiteralValue(Minisat::lbool res) {
   if(res == (Minisat::lbool((uint8_t)0))) return SAT_VALUE_TRUE;
   if(res == (Minisat::lbool((uint8_t)2))) return SAT_VALUE_UNKNOWN;
   Assert(res == (Minisat::lbool((uint8_t)1)));
@@ -70,7 +70,7 @@ SatValue DPLLMinisatSatSolver::toSatLiteralValue(Minisat::lbool res) {
 }
 
 
-void DPLLMinisatSatSolver::toMinisatClause(SatClause& clause,
+void MinisatSatSolver::toMinisatClause(SatClause& clause,
                                            Minisat::vec<Minisat::Lit>& minisat_clause) {
   for (unsigned i = 0; i < clause.size(); ++i) {
     minisat_clause.push(toMinisatLit(clause[i]));
@@ -78,7 +78,7 @@ void DPLLMinisatSatSolver::toMinisatClause(SatClause& clause,
   Assert(clause.size() == (unsigned)minisat_clause.size());
 }
 
-void DPLLMinisatSatSolver::toSatClause(Minisat::vec<Minisat::Lit>& clause,
+void MinisatSatSolver::toSatClause(Minisat::vec<Minisat::Lit>& clause,
                                        SatClause& sat_clause) {
   for (int i = 0; i < clause.size(); ++i) {
     sat_clause.push_back(toSatLiteral(clause[i]));
@@ -87,7 +87,7 @@ void DPLLMinisatSatSolver::toSatClause(Minisat::vec<Minisat::Lit>& clause,
 }
 
 
-void DPLLMinisatSatSolver::initialize(context::Context* context, TheoryProxy* theoryProxy)
+void MinisatSatSolver::initialize(context::Context* context, TheoryProxy* theoryProxy)
 {
 
   d_context = context;
@@ -110,18 +110,18 @@ void DPLLMinisatSatSolver::initialize(context::Context* context, TheoryProxy* th
   d_statistics.init(d_minisat);
 }
 
-void DPLLMinisatSatSolver::addClause(SatClause& clause, bool removable) {
+void MinisatSatSolver::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) {
+SatVariable MinisatSatSolver::newVar(bool theoryAtom) {
   return d_minisat->newVar(true, true, theoryAtom);
 }
 
 
-SatValue DPLLMinisatSatSolver::solve(unsigned long& resource) {
+SatValue MinisatSatSolver::solve(unsigned long& resource) {
   Trace("limit") << "SatSolver::solve(): have limit of " << resource << " conflicts" << std::endl;
   if(resource == 0) {
     d_minisat->budgetOff();
@@ -137,53 +137,53 @@ SatValue DPLLMinisatSatSolver::solve(unsigned long& resource) {
   return result;
 }
 
-SatValue DPLLMinisatSatSolver::solve() {
+SatValue MinisatSatSolver::solve() {
   d_minisat->budgetOff();
   return toSatLiteralValue(d_minisat->solve());
 }
 
 
-void DPLLMinisatSatSolver::interrupt() {
+void MinisatSatSolver::interrupt() {
   d_minisat->interrupt();
 }
 
-SatValue DPLLMinisatSatSolver::value(SatLiteral l) {
+SatValue MinisatSatSolver::value(SatLiteral l) {
   return toSatLiteralValue(d_minisat->value(toMinisatLit(l)));
 }
 
-SatValue DPLLMinisatSatSolver::modelValue(SatLiteral l){
+SatValue MinisatSatSolver::modelValue(SatLiteral l){
   return toSatLiteralValue(d_minisat->modelValue(toMinisatLit(l)));
 }
 
-bool DPLLMinisatSatSolver::properExplanation(SatLiteral lit, SatLiteral expl) const {
+bool MinisatSatSolver::properExplanation(SatLiteral lit, SatLiteral expl) const {
   return true;
 }
 
 /** Incremental interface */
 
-unsigned DPLLMinisatSatSolver::getAssertionLevel() const {
+unsigned MinisatSatSolver::getAssertionLevel() const {
   return d_minisat->getAssertionLevel();
 }
 
-void DPLLMinisatSatSolver::push() {
+void MinisatSatSolver::push() {
   d_minisat->push();
 }
 
-void DPLLMinisatSatSolver::pop(){
+void MinisatSatSolver::pop(){
   d_minisat->pop();
 }
 
-void DPLLMinisatSatSolver::unregisterVar(SatLiteral lit) {
+void MinisatSatSolver::unregisterVar(SatLiteral lit) {
   d_minisat->unregisterVar(toMinisatLit(lit));
 }
 
-void DPLLMinisatSatSolver::renewVar(SatLiteral lit, int level) {
+void MinisatSatSolver::renewVar(SatLiteral lit, int level) {
   d_minisat->renewVar(toMinisatLit(lit), level);
 }
 
-/// Statistics for DPLLMinisatSatSolver
+/// Statistics for MinisatSatSolver
 
-DPLLMinisatSatSolver::Statistics::Statistics() :
+MinisatSatSolver::Statistics::Statistics() :
   d_statStarts("sat::starts"),
   d_statDecisions("sat::decisions"),
   d_statRndDecisions("sat::rnd_decisions"),
@@ -204,7 +204,7 @@ DPLLMinisatSatSolver::Statistics::Statistics() :
   StatisticsRegistry::registerStat(&d_statMaxLiterals);
   StatisticsRegistry::registerStat(&d_statTotLiterals);
 }
-DPLLMinisatSatSolver::Statistics::~Statistics() {
+MinisatSatSolver::Statistics::~Statistics() {
   StatisticsRegistry::unregisterStat(&d_statStarts);
   StatisticsRegistry::unregisterStat(&d_statDecisions);
   StatisticsRegistry::unregisterStat(&d_statRndDecisions);
@@ -215,7 +215,7 @@ DPLLMinisatSatSolver::Statistics::~Statistics() {
   StatisticsRegistry::unregisterStat(&d_statMaxLiterals);
   StatisticsRegistry::unregisterStat(&d_statTotLiterals);
 }
-void DPLLMinisatSatSolver::Statistics::init(Minisat::SimpSolver* d_minisat){
+void MinisatSatSolver::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);
diff --git a/src/prop/minisat/minisat.h b/src/prop/minisat/minisat.h
index 66aca717d..3bd690cc7 100644
--- a/src/prop/minisat/minisat.h
+++ b/src/prop/minisat/minisat.h
@@ -25,7 +25,7 @@
 namespace CVC4 {
 namespace prop {
 
-class DPLLMinisatSatSolver : public DPLLSatSolverInterface {
+class MinisatSatSolver : public DPLLSatSolverInterface {
 
   /** The SatSolver used */
   Minisat::SimpSolver* d_minisat;
@@ -39,8 +39,8 @@ class DPLLMinisatSatSolver : public DPLLSatSolverInterface {
 
 public:
 
-  DPLLMinisatSatSolver ();
-  ~DPLLMinisatSatSolver();
+  MinisatSatSolver ();
+  ~MinisatSatSolver();
 
   static SatVariable     toSatVariable(Minisat::Var var);
   static Minisat::Lit    toMinisatLit(SatLiteral lit);
@@ -96,7 +96,7 @@ public:
 
 };
 
-template class SatSolverConstructor<DPLLMinisatSatSolver>;
+template class SatSolverConstructor<MinisatSatSolver>;
 
 } // prop namespace
 } // cvc4 namespace
diff --git a/src/prop/sat_solver.h b/src/prop/sat_solver.h
index 61c67ed5f..f18335048 100644
--- a/src/prop/sat_solver.h
+++ b/src/prop/sat_solver.h
@@ -26,135 +26,13 @@
 #include "util/options.h"
 #include "util/stats.h"
 #include "context/cdlist.h"
+#include "prop/sat_solver_types.h"
 
 namespace CVC4 {
 namespace prop {
 
 class TheoryProxy; 
 
-/**
- * Boolean values of the SAT solver.
- */
-enum SatValue {
-  SAT_VALUE_UNKNOWN,
-  SAT_VALUE_TRUE, 
-  SAT_VALUE_FALSE 
-};
-
-/**
- * A variable of the SAT solver.
- */
-typedef uint64_t SatVariable; 
-
-/**
- * Undefined SAT solver variable.
- */
-const SatVariable undefSatVariable = SatVariable(-1); 
-
-/**
- * A SAT literal is a variable or an negated variable.
- */
-class SatLiteral {
-
-  /**
-   * The value holds the variable and a bit noting if the variable is negated.
-   */
-  uint64_t d_value;
-
-public:
-
-  /**
-   * Construct an undefined SAT literal.
-   */
-  SatLiteral()
-  : d_value(undefSatVariable)
-  {}
-  
-  /**
-   * Construct a literal given a possible negated variable.
-   */
-  SatLiteral(SatVariable var, bool negated = false) {
-    d_value = var + var + (int)negated;
-  }
-
-  /**
-   * Returns the variable of the literal.
-   */
-  SatVariable getSatVariable() const {
-    return d_value >> 1;
-  }
-
-  /**
-   * Returns true if the literal is a negated variable.
-   */
-  bool isNegated() const {
-    return d_value & 1;
-  }
-
-  /**
-   * Negate the given literal.
-   */
-  SatLiteral operator ~ () const {
-    return SatLiteral(getSatVariable(), !isNegated()); 
-  }
-
-  /**
-   * Compare two literals for equality.
-   */
-  bool operator == (const SatLiteral& other) const {
-    return d_value == other.d_value; 
-  }
-
-  /**
-   * Compare two literals for dis-equality.
-   */
-  bool operator != (const SatLiteral& other) const {
-    return !(*this == other); 
-  }
-
-  /**
-   * Returns a string representation of the literal.
-   */
-  std::string toString() const {
-    std::ostringstream os;
-    os << (isNegated()? "~" : "") << getSatVariable() << " ";
-    return os.str();
-  }
-
-  /**
-   * Returns the hash value of a literal.
-   */
-  size_t hash() const {
-    return (size_t)d_value;
-  }
-
-  /**
-   * Returns true if the literal is undefined.
-   */
-  bool isNull() const {
-    return getSatVariable() == undefSatVariable;
-  }
-};
-
-/**
- * A constant representing a undefined literal.
- */
-const SatLiteral undefSatLiteral = SatLiteral(undefSatVariable);  
-
-/**
- * Helper for hashing the literals.
- */
-struct SatLiteralHashFunction {
-  inline size_t operator() (const SatLiteral& literal) const {
-    return literal.hash();
-  }
-};
-
-/**
- * A SAT clause is a vector of literals.
- */
-typedef std::vector<SatLiteral> SatClause;
-
 class SatSolver {
 
 public:  
diff --git a/src/prop/sat_solver_factory.cpp b/src/prop/sat_solver_factory.cpp
index c5972d7bb..fa787451d 100644
--- a/src/prop/sat_solver_factory.cpp
+++ b/src/prop/sat_solver_factory.cpp
@@ -25,11 +25,11 @@ using namespace CVC4;
 using namespace prop;
 
 BVSatSolverInterface* SatSolverFactory::createMinisat() {
-  return new MinisatSatSolver();
+  return new BVMinisatSatSolver();
 }
 
 DPLLSatSolverInterface* SatSolverFactory::createDPLLMinisat() {
-  return new DPLLMinisatSatSolver();
+  return new MinisatSatSolver();
 }
 
 SatSolver* SatSolverFactory::create(const char* name) {
diff --git a/src/prop/sat_solver_types.h b/src/prop/sat_solver_types.h
new file mode 100644
index 000000000..406782468
--- /dev/null
+++ b/src/prop/sat_solver_types.h
@@ -0,0 +1,194 @@
+/*********************                                                        */
+/*! \file cnf_stream.h
+ ** \verbatim
+ ** Original author: taking
+ ** Major contributors: mdeters, dejan
+ ** Minor contributors (to current version): barrett, cconway
+ ** 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 This class transforms a sequence of formulas into clauses.
+ **
+ ** This class takes a sequence of formulas.
+ ** It outputs a stream of clauses that is propositionally
+ ** equi-satisfiable with the conjunction of the formulas.
+ ** This stream is maintained in an online fashion.
+ **
+ ** Unlike other parts of the system it is aware of the PropEngine's
+ ** internals such as the representation and translation of [??? -Chris]
+ **/
+
+#pragma once
+
+#include "cvc4_private.h"
+
+namespace CVC4 {
+namespace prop {
+
+/**
+ * Boolean values of the SAT solver.
+ */
+enum SatValue {
+  SAT_VALUE_UNKNOWN,
+  SAT_VALUE_TRUE,
+  SAT_VALUE_FALSE
+};
+
+/**
+ * A variable of the SAT solver.
+ */
+typedef uint64_t SatVariable;
+
+/**
+ * Undefined SAT solver variable.
+ */
+const SatVariable undefSatVariable = SatVariable(-1);
+
+/**
+ * A SAT literal is a variable or an negated variable.
+ */
+class SatLiteral {
+
+  /**
+   * The value holds the variable and a bit noting if the variable is negated.
+   */
+  uint64_t d_value;
+
+public:
+
+  /**
+   * Construct an undefined SAT literal.
+   */
+  SatLiteral()
+  : d_value(undefSatVariable)
+  {}
+
+  /**
+   * Construct a literal given a possible negated variable.
+   */
+  SatLiteral(SatVariable var, bool negated = false) {
+    d_value = var + var + (int)negated;
+  }
+
+  /**
+   * Returns the variable of the literal.
+   */
+  SatVariable getSatVariable() const {
+    return d_value >> 1;
+  }
+
+  /**
+   * Returns true if the literal is a negated variable.
+   */
+  bool isNegated() const {
+    return d_value & 1;
+  }
+
+  /**
+   * Negate the given literal.
+   */
+  SatLiteral operator ~ () const {
+    return SatLiteral(getSatVariable(), !isNegated());
+  }
+
+  /**
+   * Compare two literals for equality.
+   */
+  bool operator == (const SatLiteral& other) const {
+    return d_value == other.d_value;
+  }
+
+  /**
+   * Compare two literals for dis-equality.
+   */
+  bool operator != (const SatLiteral& other) const {
+    return !(*this == other);
+  }
+
+  /**
+   * Returns a string representation of the literal.
+   */
+  std::string toString() const {
+    std::ostringstream os;
+    os << (isNegated()? "~" : "") << getSatVariable() << " ";
+    return os.str();
+  }
+
+  /**
+   * Returns the hash value of a literal.
+   */
+  size_t hash() const {
+    return (size_t)d_value;
+  }
+
+  /**
+   * Returns true if the literal is undefined.
+   */
+  bool isNull() const {
+    return getSatVariable() == undefSatVariable;
+  }
+};
+
+/**
+ * A constant representing a undefined literal.
+ */
+const SatLiteral undefSatLiteral = SatLiteral(undefSatVariable);
+
+/**
+ * Helper for hashing the literals.
+ */
+struct SatLiteralHashFunction {
+  inline size_t operator() (const SatLiteral& literal) const {
+    return literal.hash();
+  }
+};
+
+/**
+ * A SAT clause is a vector of literals.
+ */
+typedef std::vector<SatLiteral> SatClause;
+
+/**
+ * Each object in the SAT solver, such as as variables and clauses, can be assigned a life span,
+ * so that the SAT solver can (or should) remove them when the lifespan is over.
+ */
+enum SatSolverLifespan
+{
+  /**
+   * The object should stay forever and never be removed
+   */
+  SAT_LIFESPAN_PERMANENT,
+  /**
+   * The object can be removed at any point when it becomes unnecessary.
+   */
+  SAT_LIFESPAN_REMOVABLE,
+  /**
+   * The object must be removed as soon as the SAT solver exits the search context
+   * where the object got introduced.
+   */
+  SAT_LIFESPAN_SEARCH_CONTEXT_STRICT,
+  /**
+   * The object can be removed when SAT solver exits the search context where the object
+   * got introduced, but can be kept at the solver discretion.
+   */
+  SAT_LIFESPAN_SEARCH_CONTEXT_LENIENT,
+  /**
+   * The object must be removed as soon as the SAT solver exits the user-level context where
+   * the object got introduced.
+   */
+  SAT_LIFESPAN_USER_CONTEXT_STRICT,
+  /**
+   * The object can be removed when the SAT solver exits the user-level context where
+   * the object got introduced.
+   */
+  SAT_LIFESPAN_USER_CONTEXT_LENIENT
+};
+
+}
+}
+
+