8 files changed, 15 insertions, 17 deletions
diff --git a/src/prop/Makefile.am b/src/prop/Makefile.am
index 02a6a4714..832255621 100644
--- a/src/prop/Makefile.am
+++ b/src/prop/Makefile.am
@@ -15,8 +15,8 @@ libprop_la_SOURCES = \
 	theory_proxy.cpp \
 	cnf_stream.h \
 	cnf_stream.cpp \
-	sat_module.h \
-	sat_module.cpp
+	sat_solver.h \
+	sat_solver.cpp
 
 SUBDIRS = minisat bvminisat
 
diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp
index 676cc4c49..3a4fa781a 100644
--- a/src/prop/cnf_stream.cpp
+++ b/src/prop/cnf_stream.cpp
@@ -44,7 +44,7 @@ namespace CVC4 {
 namespace prop {
 
 
-CnfStream::CnfStream(SatSolverInterface *satSolver, Registrar* registrar, bool fullLitToNodeMap) :
+CnfStream::CnfStream(SatSolver *satSolver, Registrar* registrar, bool fullLitToNodeMap) :
   d_satSolver(satSolver),
   d_fullLitToNodeMap(fullLitToNodeMap),
   d_registrar(registrar) {
@@ -66,7 +66,7 @@ void CnfStream::recordTranslation(TNode node, bool alwaysRecord) {
   }
 }
 
-TseitinCnfStream::TseitinCnfStream(SatSolverInterface* satSolver, Registrar* registrar, bool fullLitToNodeMap) :
+TseitinCnfStream::TseitinCnfStream(SatSolver* satSolver, Registrar* registrar, bool fullLitToNodeMap) :
   CnfStream(satSolver, registrar, fullLitToNodeMap) {
 }
 
diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h
index af2ff2fcd..f75e74d63 100644
--- a/src/prop/cnf_stream.h
+++ b/src/prop/cnf_stream.h
@@ -65,7 +65,7 @@ public:
 protected:
 
   /** The SAT solver we will be using */
-  SatSolverInterface *d_satSolver;
+  SatSolver *d_satSolver;
 
   TranslationCache d_translationCache;
   NodeCache d_nodeCache;
@@ -190,7 +190,7 @@ public:
    * @param fullLitToNodeMap maintain a full SAT-literal-to-Node mapping,
    * even for non-theory literals
    */
-  CnfStream(SatSolverInterface* satSolver, Registrar* registrar, bool fullLitToNodeMap = false);
+  CnfStream(SatSolver* satSolver, Registrar* registrar, bool fullLitToNodeMap = false);
 
   /**
    * Destructs a CnfStream.  This implementation does nothing, but we
@@ -290,7 +290,7 @@ public:
    * @param fullLitToNodeMap maintain a full SAT-literal-to-Node mapping,
    * even for non-theory literals
    */
-  TseitinCnfStream(SatSolverInterface* satSolver, Registrar* registrar, bool fullLitToNodeMap = false);
+  TseitinCnfStream(SatSolver* satSolver, Registrar* registrar, bool fullLitToNodeMap = false);
 
 private:
 
diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index 65ec025b1..e5a6d32e1 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_module.h"
+#include "prop/sat_solver.h"
 #include "util/output.h"
 #include "expr/command.h"
 #include "proof/proof_manager.h"
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index 9d6a2c8f6..0fa13dc04 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -19,7 +19,7 @@
 #include "prop/cnf_stream.h"
 #include "prop/prop_engine.h"
 #include "prop/theory_proxy.h"
-#include "prop/sat_module.h"
+#include "prop/sat_solver.h"
 
 #include "theory/theory_engine.h"
 #include "theory/theory_registrar.h"
diff --git a/src/prop/sat_module.cpp b/src/prop/sat_solver.cpp
index 5e5b78b44..13f2498f2 100644
--- a/src/prop/sat_module.cpp
+++ b/src/prop/sat_solver.cpp
@@ -18,7 +18,7 @@
  **/
 
 #include "prop/prop_engine.h"
-#include "prop/sat_module.h"
+#include "prop/sat_solver.h"
 #include "context/context.h"
 #include "theory/theory_engine.h"
 #include "expr/expr_stream.h"
diff --git a/src/prop/sat_module.h b/src/prop/sat_solver.h
index 9c49c7d67..56c6c2783 100644
--- a/src/prop/sat_module.h
+++ b/src/prop/sat_solver.h
@@ -96,12 +96,10 @@ struct SatLiteralHashFunction {
 
 typedef std::vector<SatLiteral> SatClause;
 
-
-
-class SatSolverInterface {
+class SatSolver {
 public:  
   /** Virtual destructor to make g++ happy */
-  virtual ~SatSolverInterface() { }
+  virtual ~SatSolver() { }
   
   /** Assert a clause in the solver. */
   virtual void addClause(SatClause& clause, bool removable) = 0;
@@ -134,7 +132,7 @@ public:
 };
 
 
-class BVSatSolverInterface: public SatSolverInterface {
+class BVSatSolverInterface: public SatSolver {
 public:
   virtual SatLiteralValue solve(const context::CDList<SatLiteral> & assumptions) = 0;
 
@@ -144,7 +142,7 @@ public:
 }; 
 
 
-class DPLLSatSolverInterface: public SatSolverInterface {
+class DPLLSatSolverInterface: public SatSolver {
 public:
   virtual void initialize(context::Context* context, prop::TheoryProxy* theoryProxy) = 0; 
   
diff --git a/src/prop/theory_proxy.h b/src/prop/theory_proxy.h
index 85dcae68b..2934bcad9 100644
--- a/src/prop/theory_proxy.h
+++ b/src/prop/theory_proxy.h
@@ -29,7 +29,7 @@
 #include "util/options.h"
 #include "util/stats.h"
 
-#include "prop/sat_module.h"
+#include "prop/sat_solver.h"
 
 namespace CVC4 {