1 files changed, 16 insertions, 15 deletions

diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index 3430fd7c6..7d0353122 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -19,9 +19,10 @@
 #include "prop/cnf_stream.h"
 #include "prop/prop_engine.h"
 #include "prop/sat.h"
+#include "prop/sat_module.h"
 
 #include "theory/theory_engine.h"
-#include "theory/registrar.h"
+#include "theory/theory_registrar.h"
 #include "util/Assert.h"
 #include "util/options.h"
 #include "util/output.h"
@@ -70,12 +71,12 @@ PropEngine::PropEngine(TheoryEngine* te, Context* context) :
 
   Debug("prop") << "Constructing the PropEngine" << endl;
 
-  d_satSolver = new SatSolver(this, d_theoryEngine, d_context);
+  d_satSolver = SatSolverFactory::createDPLLMinisat(); 
 
-  theory::Registrar registrar(d_theoryEngine);
+  theory::TheoryRegistrar* registrar = new theory::TheoryRegistrar(d_theoryEngine);
   d_cnfStream = new CVC4::prop::TseitinCnfStream(d_satSolver, registrar, Options::current()->threads > 1);
 
-  d_satSolver->setCnfStream(d_cnfStream);
+  d_satSolver->initialize(d_context, new TheoryProxy(this, d_theoryEngine, d_context, d_cnfStream));
 }
 
 PropEngine::~PropEngine() {
@@ -118,7 +119,7 @@ void PropEngine::printSatisfyingAssignment(){
       ++i) {
     pair<Node, CnfStream::TranslationInfo> curr = *i;
     SatLiteral l = curr.second.literal;
-    if(!sign(l)) {
+    if(!l.isNegated()) {
       Node n = curr.first;
       SatLiteralValue value = d_satSolver->modelValue(l);
       Debug("prop-value") << "'" << l << "' " << value << " " << n << endl;
@@ -153,22 +154,22 @@ Result PropEngine::checkSat(unsigned long& millis, unsigned long& resource) {
 
   millis = d_satTimer.elapsed();
 
-  if( result == l_Undef ) {
+  if( result == SatValUnknown ) {
     Result::UnknownExplanation why =
       d_satTimer.expired() ? Result::TIMEOUT :
         (d_interrupted ? Result::INTERRUPTED : Result::RESOURCEOUT);
     return Result(Result::SAT_UNKNOWN, why);
   }
 
-  if( result == l_True && Debug.isOn("prop") ) {
+  if( result == SatValTrue && Debug.isOn("prop") ) {
     printSatisfyingAssignment();
   }
 
   Debug("prop") << "PropEngine::checkSat() => " << result << endl;
-  if(result == l_True && d_theoryEngine->isIncomplete()) {
+  if(result == SatValTrue && d_theoryEngine->isIncomplete()) {
     return Result(Result::SAT_UNKNOWN, Result::INCOMPLETE);
   }
-  return Result(result == l_True ? Result::SAT : Result::UNSAT);
+  return Result(result == SatValTrue ? Result::SAT : Result::UNSAT);
 }
 
 Node PropEngine::getValue(TNode node) const {
@@ -178,12 +179,12 @@ Node PropEngine::getValue(TNode node) const {
   SatLiteral lit = d_cnfStream->getLiteral(node);
 
   SatLiteralValue v = d_satSolver->value(lit);
-  if(v == l_True) {
+  if(v == SatValTrue) {
     return NodeManager::currentNM()->mkConst(true);
-  } else if(v == l_False) {
+  } else if(v == SatValFalse) {
     return NodeManager::currentNM()->mkConst(false);
   } else {
-    Assert(v == l_Undef);
+    Assert(v == SatValUnknown);
     return Node::null();
   }
 }
@@ -203,14 +204,14 @@ bool PropEngine::hasValue(TNode node, bool& value) const {
   SatLiteral lit = d_cnfStream->getLiteral(node);
 
   SatLiteralValue v = d_satSolver->value(lit);
-  if(v == l_True) {
+  if(v == SatValTrue) {
     value = true;
     return true;
-  } else if(v == l_False) {
+  } else if(v == SatValFalse) {
     value = false;
     return true;
   } else {
-    Assert(v == l_Undef);
+    Assert(v == SatValUnknown);
     return false;
   }
 }