More cleaning up.

12 files changed, 252 insertions, 153 deletions

diff --git a/src/prop/Makefile.am b/src/prop/Makefile.am
index 832255621..c1dc3b828 100644
--- a/src/prop/Makefile.am
+++ b/src/prop/Makefile.am
@@ -16,7 +16,8 @@ libprop_la_SOURCES = \
 	cnf_stream.h \
 	cnf_stream.cpp \
 	sat_solver.h \
-	sat_solver.cpp
-
+	sat_solver_factory.h \
+	sat_solver_factory.cpp 
+	
 SUBDIRS = minisat bvminisat
 
diff --git a/src/prop/bvminisat/bvminisat.cpp b/src/prop/bvminisat/bvminisat.cpp
index 3d2d4c9ea..c4c21e126 100644
--- a/src/prop/bvminisat/bvminisat.cpp
+++ b/src/prop/bvminisat/bvminisat.cpp
@@ -54,11 +54,11 @@ void MinisatSatSolver::interrupt(){
   d_minisat->interrupt();
 }
 
-SatLiteralValue MinisatSatSolver::solve(){
+SatValue MinisatSatSolver::solve(){
   return toSatLiteralValue(d_minisat->solve());
 }
 
-SatLiteralValue MinisatSatSolver::solve(long unsigned int& resource){
+SatValue MinisatSatSolver::solve(long unsigned int& resource){
   Trace("limit") << "MinisatSatSolver::solve(): have limit of " << resource << " conflicts" << std::endl;
   if(resource == 0) {
     d_minisat->budgetOff();
@@ -67,14 +67,14 @@ SatLiteralValue MinisatSatSolver::solve(long unsigned int& resource){
   }
   BVMinisat::vec<BVMinisat::Lit> empty;
   unsigned long conflictsBefore = d_minisat->conflicts;
-  SatLiteralValue result = toSatLiteralValue(d_minisat->solveLimited(empty));
+  SatValue 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){
+SatValue 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;
@@ -85,7 +85,7 @@ SatLiteralValue MinisatSatSolver::solve(const context::CDList<SatLiteral> & assu
   }
   Debug("sat::minisat") <<"\n";
 
- SatLiteralValue result = toSatLiteralValue(d_minisat->solve(assump));
+ SatValue result = toSatLiteralValue(d_minisat->solve(assump));
  return result;
 }
 
@@ -97,14 +97,14 @@ void MinisatSatSolver::getUnsatCore(SatClause& unsatCore) {
   }
 }
 
-SatLiteralValue MinisatSatSolver::value(SatLiteral l){
+SatValue MinisatSatSolver::value(SatLiteral l){
     Unimplemented();
-    return SatValUnknown;
+    return SAT_VALUE_UNKNOWN;
 }
 
-SatLiteralValue MinisatSatSolver::modelValue(SatLiteral l){
+SatValue MinisatSatSolver::modelValue(SatLiteral l){
     Unimplemented();
-    return SatValUnknown;
+    return SAT_VALUE_UNKNOWN;
 }
 
 void MinisatSatSolver::unregisterVar(SatLiteral lit) {
@@ -150,16 +150,16 @@ SatLiteral MinisatSatSolver::toSatLiteral(BVMinisat::Lit lit) {
                     BVMinisat::sign(lit));
 }
 
-SatLiteralValue MinisatSatSolver::toSatLiteralValue(bool res) {
-  if(res) return SatValTrue;
-  else return SatValFalse;
+SatValue MinisatSatSolver::toSatLiteralValue(bool res) {
+  if(res) return SAT_VALUE_TRUE;
+  else return SAT_VALUE_FALSE;
 }
 
-SatLiteralValue MinisatSatSolver::toSatLiteralValue(BVMinisat::lbool res) {
-  if(res == (BVMinisat::lbool((uint8_t)0))) return SatValTrue;
-  if(res == (BVMinisat::lbool((uint8_t)2))) return SatValUnknown;
+SatValue MinisatSatSolver::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 SatValFalse;
+  return SAT_VALUE_FALSE;
 }
 
 void MinisatSatSolver::toMinisatClause(SatClause& clause,
diff --git a/src/prop/bvminisat/bvminisat.h b/src/prop/bvminisat/bvminisat.h
index ed164904e..043aa5d24 100644
--- a/src/prop/bvminisat/bvminisat.h
+++ b/src/prop/bvminisat/bvminisat.h
@@ -38,13 +38,13 @@ public:
 
   void interrupt();
 
-  SatLiteralValue solve();
-  SatLiteralValue solve(long unsigned int&);
-  SatLiteralValue solve(const context::CDList<SatLiteral> & assumptions);
+  SatValue solve();
+  SatValue solve(long unsigned int&);
+  SatValue solve(const context::CDList<SatLiteral> & assumptions);
   void getUnsatCore(SatClause& unsatCore);
 
-  SatLiteralValue value(SatLiteral l);
-  SatLiteralValue modelValue(SatLiteral l);
+  SatValue value(SatLiteral l);
+  SatValue modelValue(SatLiteral l);
 
   void unregisterVar(SatLiteral lit);
   void renewVar(SatLiteral lit, int level = -1);
@@ -56,8 +56,8 @@ public:
   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 SatValue toSatLiteralValue(bool res);
+  static SatValue 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);
diff --git a/src/prop/minisat/minisat.cpp b/src/prop/minisat/minisat.cpp
index ede18c585..1ec81a4f6 100644
--- a/src/prop/minisat/minisat.cpp
+++ b/src/prop/minisat/minisat.cpp
@@ -57,16 +57,16 @@ SatLiteral DPLLMinisatSatSolver::toSatLiteral(Minisat::Lit lit) {
                     Minisat::sign(lit));
 }
 
-SatLiteralValue DPLLMinisatSatSolver::toSatLiteralValue(bool res) {
-  if(res) return SatValTrue;
-  else return SatValFalse;
+SatValue DPLLMinisatSatSolver::toSatLiteralValue(bool res) {
+  if(res) return SAT_VALUE_TRUE;
+  else return SAT_VALUE_FALSE;
 }
 
-SatLiteralValue DPLLMinisatSatSolver::toSatLiteralValue(Minisat::lbool res) {
-  if(res == (Minisat::lbool((uint8_t)0))) return SatValTrue;
-  if(res == (Minisat::lbool((uint8_t)2))) return SatValUnknown;
+SatValue DPLLMinisatSatSolver::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)));
-  return SatValFalse;
+  return SAT_VALUE_FALSE;
 }
 
 
@@ -121,7 +121,7 @@ SatVariable DPLLMinisatSatSolver::newVar(bool theoryAtom) {
 }
 
 
-SatLiteralValue DPLLMinisatSatSolver::solve(unsigned long& resource) {
+SatValue DPLLMinisatSatSolver::solve(unsigned long& resource) {
   Trace("limit") << "SatSolver::solve(): have limit of " << resource << " conflicts" << std::endl;
   if(resource == 0) {
     d_minisat->budgetOff();
@@ -130,14 +130,14 @@ SatLiteralValue DPLLMinisatSatSolver::solve(unsigned long& resource) {
   }
   Minisat::vec<Minisat::Lit> empty;
   unsigned long conflictsBefore = d_minisat->conflicts;
-  SatLiteralValue result = toSatLiteralValue(d_minisat->solveLimited(empty));
+  SatValue 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() {
+SatValue DPLLMinisatSatSolver::solve() {
   d_minisat->budgetOff();
   return toSatLiteralValue(d_minisat->solve());
 }
@@ -147,11 +147,11 @@ void DPLLMinisatSatSolver::interrupt() {
   d_minisat->interrupt();
 }
 
-SatLiteralValue DPLLMinisatSatSolver::value(SatLiteral l) {
+SatValue DPLLMinisatSatSolver::value(SatLiteral l) {
   return toSatLiteralValue(d_minisat->value(toMinisatLit(l)));
 }
 
-SatLiteralValue DPLLMinisatSatSolver::modelValue(SatLiteral l){
+SatValue DPLLMinisatSatSolver::modelValue(SatLiteral l){
   return toSatLiteralValue(d_minisat->modelValue(toMinisatLit(l)));
 }
 
diff --git a/src/prop/minisat/minisat.h b/src/prop/minisat/minisat.h
index dc06753ab..549c0b679 100644
--- a/src/prop/minisat/minisat.h
+++ b/src/prop/minisat/minisat.h
@@ -44,8 +44,8 @@ public:
   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 SatValue toSatLiteralValue(bool res);
+  static SatValue 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);
@@ -56,14 +56,14 @@ public:
 
   SatVariable newVar(bool theoryAtom = false);
 
-  SatLiteralValue solve();
-  SatLiteralValue solve(long unsigned int&);
+  SatValue solve();
+  SatValue solve(long unsigned int&);
 
   void interrupt();
 
-  SatLiteralValue value(SatLiteral l);
+  SatValue value(SatLiteral l);
 
-  SatLiteralValue modelValue(SatLiteral l);
+  SatValue modelValue(SatLiteral l);
 
   bool properExplanation(SatLiteral lit, SatLiteral expl) const;
 
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index 0fa13dc04..7d4cb7b1c 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -20,6 +20,7 @@
 #include "prop/prop_engine.h"
 #include "prop/theory_proxy.h"
 #include "prop/sat_solver.h"
+#include "prop/sat_solver_factory.h"
 
 #include "theory/theory_engine.h"
 #include "theory/theory_registrar.h"
@@ -121,7 +122,7 @@ void PropEngine::printSatisfyingAssignment(){
     SatLiteral l = curr.second.literal;
     if(!l.isNegated()) {
       Node n = curr.first;
-      SatLiteralValue value = d_satSolver->modelValue(l);
+      SatValue value = d_satSolver->modelValue(l);
       Debug("prop-value") << "'" << l << "' " << value << " " << n << endl;
     }
   }
@@ -150,26 +151,26 @@ Result PropEngine::checkSat(unsigned long& millis, unsigned long& resource) {
   d_interrupted = false;
 
   // Check the problem
-  SatLiteralValue result = d_satSolver->solve(resource);
+  SatValue result = d_satSolver->solve(resource);
 
   millis = d_satTimer.elapsed();
 
-  if( result == SatValUnknown ) {
+  if( result == SAT_VALUE_UNKNOWN ) {
     Result::UnknownExplanation why =
       d_satTimer.expired() ? Result::TIMEOUT :
         (d_interrupted ? Result::INTERRUPTED : Result::RESOURCEOUT);
     return Result(Result::SAT_UNKNOWN, why);
   }
 
-  if( result == SatValTrue && Debug.isOn("prop") ) {
+  if( result == SAT_VALUE_TRUE && Debug.isOn("prop") ) {
     printSatisfyingAssignment();
   }
 
   Debug("prop") << "PropEngine::checkSat() => " << result << endl;
-  if(result == SatValTrue && d_theoryEngine->isIncomplete()) {
+  if(result == SAT_VALUE_TRUE && d_theoryEngine->isIncomplete()) {
     return Result(Result::SAT_UNKNOWN, Result::INCOMPLETE);
   }
-  return Result(result == SatValTrue ? Result::SAT : Result::UNSAT);
+  return Result(result == SAT_VALUE_TRUE ? Result::SAT : Result::UNSAT);
 }
 
 Node PropEngine::getValue(TNode node) const {
@@ -178,13 +179,13 @@ Node PropEngine::getValue(TNode node) const {
 
   SatLiteral lit = d_cnfStream->getLiteral(node);
 
-  SatLiteralValue v = d_satSolver->value(lit);
-  if(v == SatValTrue) {
+  SatValue v = d_satSolver->value(lit);
+  if(v == SAT_VALUE_TRUE) {
     return NodeManager::currentNM()->mkConst(true);
-  } else if(v == SatValFalse) {
+  } else if(v == SAT_VALUE_FALSE) {
     return NodeManager::currentNM()->mkConst(false);
   } else {
-    Assert(v == SatValUnknown);
+    Assert(v == SAT_VALUE_UNKNOWN);
     return Node::null();
   }
 }
@@ -203,15 +204,15 @@ bool PropEngine::hasValue(TNode node, bool& value) const {
 
   SatLiteral lit = d_cnfStream->getLiteral(node);
 
-  SatLiteralValue v = d_satSolver->value(lit);
-  if(v == SatValTrue) {
+  SatValue v = d_satSolver->value(lit);
+  if(v == SAT_VALUE_TRUE) {
     value = true;
     return true;
-  } else if(v == SatValFalse) {
+  } else if(v == SAT_VALUE_FALSE) {
     value = false;
     return true;
   } else {
-    Assert(v == SatValUnknown);
+    Assert(v == SAT_VALUE_UNKNOWN);
     return false;
   }
 }
diff --git a/src/prop/sat_solver.cpp b/src/prop/sat_solver.cpp
deleted file mode 100644
index d3710b617..000000000
--- a/src/prop/sat_solver.cpp
+++ /dev/null
@@ -1,51 +0,0 @@
-/*********************                                                        */
-/*! \file sat.cpp
- ** \verbatim
- ** Original author: cconway
- ** Major contributors: dejan, taking, mdeters, lianah
- ** Minor contributors (to current version): none
- ** 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 [[ Add one-line brief description here ]]
- **
- ** [[ Add lengthier description here ]]
- ** \todo document this file
- **/
-
-#include "prop/prop_engine.h"
-#include "prop/sat_solver.h"
-#include "context/context.h"
-#include "theory/theory_engine.h"
-#include "expr/expr_stream.h"
-#include "prop/theory_proxy.h"
-
-#include "prop/minisat/minisat.h"
-#include "prop/bvminisat/bvminisat.h"
-
-using namespace std; 
-
-namespace CVC4 {
-namespace prop {
-
-string SatLiteral::toString() {
-  ostringstream os;
-  os << (isNegated()? "~" : "") << getSatVariable() << " ";
-  return os.str(); 
-}
-
-BVSatSolverInterface* SatSolverFactory::createMinisat() {
-  return new MinisatSatSolver(); 
-}
-
-DPLLSatSolverInterface* SatSolverFactory::createDPLLMinisat(){
-  return new DPLLMinisatSatSolver(); 
-} 
-
-
-}/* CVC4::prop namespace */
-}/* CVC4 namespace */
diff --git a/src/prop/sat_solver.h b/src/prop/sat_solver.h
index e54f551fa..eb694852c 100644
--- a/src/prop/sat_solver.h
+++ b/src/prop/sat_solver.h
@@ -16,7 +16,7 @@
  ** SAT Solver.
  **/
 
-#include "cvc4_private.h"
+#include "cvc4_public.h"
 
 #ifndef __CVC4__PROP__SAT_MODULE_H
 #define __CVC4__PROP__SAT_MODULE_H
@@ -31,55 +31,134 @@ namespace prop {
 
 class TheoryProxy; 
 
-enum SatLiteralValue {
-  SatValUnknown,
-  SatValTrue, 
-  SatValFalse 
+/**
+ * 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; 
-// special constant
+
+/**
+ * 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:
-  SatLiteral() :
-    d_value(undefSatVariable)
+
+  /**
+   * Construct an undefined SAT literal.
+   */
+  SatLiteral()
+  : d_value(undefSatVariable)
   {}
   
-  SatLiteral(SatVariable var, bool negated = false) { d_value = var + var + (int)negated; }
-  SatLiteral operator~() {
+  /**
+   * 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()); 
   }
-  bool operator==(const SatLiteral& other) const {
+
+  /**
+   * Compare two literals for equality.
+   */
+  bool operator == (const SatLiteral& other) const {
     return d_value == other.d_value; 
   }
-  bool operator!=(const SatLiteral& other) const {
+
+  /**
+   * Compare two literals for dis-equality.
+   */
+  bool operator != (const SatLiteral& other) const {
     return !(*this == other); 
   }
-  std::string toString();
-  bool isNegated() const { return d_value & 1; }
-  size_t toHash() const {return (size_t)d_value; }
-  bool isNull() const { return d_value == (uint64_t)-1; }
-  SatVariable getSatVariable() const {return d_value >> 1; }
+
+  /**
+   * 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;
+  }
 };
 
-// special constant 
+/**
+ * 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.toHash();
+    return literal.hash();
   }
 };
 
+/**
+ * A SAT clause is a vector of literals.
+ */
 typedef std::vector<SatLiteral> SatClause;
 
 class SatSolver {
+
 public:  
-  /** Virtual destructor to make g++ happy */
+
+  /** Virtual destructor */
   virtual ~SatSolver() { }
   
   /** Assert a clause in the solver. */
@@ -90,19 +169,19 @@ public:
 
  
   /** Check the satisfiability of the added clauses */
-  virtual SatLiteralValue solve() = 0;
+  virtual SatValue solve() = 0;
 
   /** Check the satisfiability of the added clauses */
-  virtual SatLiteralValue solve(long unsigned int&) = 0;
+  virtual SatValue solve(long unsigned int&) = 0;
   
   /** Interrupt the solver */
   virtual void interrupt() = 0;
 
   /** Call value() during the search.*/
-  virtual SatLiteralValue value(SatLiteral l) = 0;
+  virtual SatValue value(SatLiteral l) = 0;
 
   /** Call modelValue() when the search is done.*/
-  virtual SatLiteralValue modelValue(SatLiteral l) = 0;
+  virtual SatValue modelValue(SatLiteral l) = 0;
 
   virtual void unregisterVar(SatLiteral lit) = 0;
   
@@ -115,7 +194,7 @@ public:
 
 class BVSatSolverInterface: public SatSolver {
 public:
-  virtual SatLiteralValue solve(const context::CDList<SatLiteral> & assumptions) = 0;
+  virtual SatValue solve(const context::CDList<SatLiteral> & assumptions) = 0;
 
   virtual void markUnremovable(SatLiteral lit) = 0;
 
@@ -135,12 +214,6 @@ public:
 
 }; 
 
-class SatSolverFactory {
-public:
-  static  BVSatSolverInterface*      createMinisat();
-  static  DPLLSatSolverInterface*  createDPLLMinisat();
-}; 
-
 }/* prop namespace */
 
 inline std::ostream& operator <<(std::ostream& out, prop::SatLiteral lit) {
@@ -157,16 +230,16 @@ inline std::ostream& operator <<(std::ostream& out, const prop::SatClause& claus
   return out;
 }
 
-inline std::ostream& operator <<(std::ostream& out, prop::SatLiteralValue val) {
+inline std::ostream& operator <<(std::ostream& out, prop::SatValue val) {
   std::string str;
   switch(val) {
-  case prop::SatValUnknown:
+  case prop::SAT_VALUE_UNKNOWN:
     str = "_";
     break;
-  case prop::SatValTrue:
+  case prop::SAT_VALUE_TRUE:
     str = "1";
     break;
-  case prop::SatValFalse:
+  case prop::SAT_VALUE_FALSE:
     str = "0";
     break;
   default:
diff --git a/src/prop/sat_solver_factory.cpp b/src/prop/sat_solver_factory.cpp
new file mode 100644
index 000000000..fbb244789
--- /dev/null
+++ b/src/prop/sat_solver_factory.cpp
@@ -0,0 +1,36 @@
+/*********************                                                        */
+/*! \file sat_solver_factory.h
+ ** \verbatim
+ ** Original author: lianah
+ ** 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 creation facility.
+ **
+ ** SAT Solver.
+ **/
+
+#include "prop/sat_solver_factory.h"
+#include "prop/minisat/minisat.h"
+#include "prop/bvminisat/bvminisat.h"
+
+using namespace CVC4;
+using namespace prop;
+
+BVSatSolverInterface* SatSolverFactory::createMinisat() {
+  return new MinisatSatSolver();
+}
+
+DPLLSatSolverInterface* SatSolverFactory::createDPLLMinisat() {
+  return new DPLLMinisatSatSolver();
+}
+
+
+
+
diff --git a/src/prop/sat_solver_factory.h b/src/prop/sat_solver_factory.h
new file mode 100644
index 000000000..09d66b8d4
--- /dev/null
+++ b/src/prop/sat_solver_factory.h
@@ -0,0 +1,38 @@
+/*********************                                                        */
+/*! \file sat_solver_factory.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.
+ **
+ ** SAT Solver creation facility
+ **/
+
+#pragma once
+
+#include "cvc4_public.h"
+
+#include "prop/sat_solver.h"
+
+namespace CVC4 {
+namespace prop {
+
+class SatSolverFactory {
+public:
+  static BVSatSolverInterface* createMinisat();
+  static DPLLSatSolverInterface* createDPLLMinisat();
+};
+
+}
+}
+
+
+
diff --git a/src/theory/bv/bv_sat.cpp b/src/theory/bv/bv_sat.cpp
index f580aee44..6f91335ce 100644
--- a/src/theory/bv/bv_sat.cpp
+++ b/src/theory/bv/bv_sat.cpp
@@ -22,6 +22,7 @@
 #include "theory/rewriter.h"
 #include "prop/cnf_stream.h"
 #include "prop/sat_solver.h"
+#include "prop/sat_solver_factory.h"
 
 using namespace std;
 
@@ -184,7 +185,7 @@ void Bitblaster::assertToSat(TNode lit) {
  
 bool Bitblaster::solve() {
   Trace("bitvector") << "Bitblaster::solve() asserted atoms " << d_assertedAtoms.size() <<"\n"; 
-  return SatValTrue == d_satSolver->solve(d_assertedAtoms); 
+  return SAT_VALUE_TRUE == d_satSolver->solve(d_assertedAtoms); 
 }
 
 void Bitblaster::getConflict(std::vector<TNode>& conflict) {
diff --git a/test/unit/prop/cnf_stream_black.h b/test/unit/prop/cnf_stream_black.h
index d1f79f6ab..5c20b534d 100644
--- a/test/unit/prop/cnf_stream_black.h
+++ b/test/unit/prop/cnf_stream_black.h
@@ -84,20 +84,20 @@ public:
   void interrupt() {
   }
   
-  SatLiteralValue solve() {
-    return SatValUnknown;
+  SatValue solve() {
+    return SAT_VALUE_UNKNOWN;
   }
 
-  SatLiteralValue solve(long unsigned int& resource) {
-    return SatValUnknown;
+  SatValue solve(long unsigned int& resource) {
+    return SAT_VALUE_UNKNOWN;
   }
 
-  SatLiteralValue value(SatLiteral l) {
-    return SatValUnknown;
+  SatValue value(SatLiteral l) {
+    return SAT_VALUE_UNKNOWN;
   }
 
-  SatLiteralValue modelValue(SatLiteral l) {
-    return SatValUnknown;
+  SatValue modelValue(SatLiteral l) {
+    return SAT_VALUE_UNKNOWN;
   }
 
   bool properExplanation(SatLiteral lit, SatLiteral expl) const {