1 files changed, 23 insertions, 26 deletions

diff --git a/src/prop/sat.cpp b/src/prop/sat.cpp
index 559467922..ab8be39eb 100644
--- a/src/prop/sat.cpp
+++ b/src/prop/sat.cpp
@@ -28,15 +28,15 @@
 namespace CVC4 {
 namespace prop {
 
-void SatSolver::variableNotify(SatVariable var) {
-  d_theoryEngine->preRegister(getNode(variableToLiteral(var)));
+void TheoryProxy::variableNotify(SatVariable var) {
+  d_theoryEngine->preRegister(getNode(SatLiteral(var)));
 }
 
-void SatSolver::theoryCheck(theory::Theory::Effort effort) {
+void TheoryProxy::theoryCheck(theory::Theory::Effort effort) {
   d_theoryEngine->check(effort);
 }
 
-void SatSolver::theoryPropagate(std::vector<SatLiteral>& output) {
+void TheoryProxy::theoryPropagate(std::vector<SatLiteral>& output) {
   // Get the propagated literals
   std::vector<TNode> outputNodes;
   d_theoryEngine->getPropagatedLiterals(outputNodes);
@@ -46,7 +46,7 @@ void SatSolver::theoryPropagate(std::vector<SatLiteral>& output) {
   }
 }
 
-void SatSolver::explainPropagation(SatLiteral l, SatClause& explanation) {
+void TheoryProxy::explainPropagation(SatLiteral l, SatClause& explanation) {
   TNode lNode = d_cnfStream->getNode(l);
   Debug("prop-explain") << "explainPropagation(" << lNode << ")" << std::endl;
   Node theoryExplanation = d_theoryEngine->getExplanation(lNode);
@@ -54,45 +54,41 @@ void SatSolver::explainPropagation(SatLiteral l, SatClause& explanation) {
   if (theoryExplanation.getKind() == kind::AND) {
     Node::const_iterator it = theoryExplanation.begin();
     Node::const_iterator it_end = theoryExplanation.end();
-    explanation.push(l);
+    explanation.push_back(l);
     for (; it != it_end; ++ it) {
-      explanation.push(~d_cnfStream->getLiteral(*it));
+      explanation.push_back(~d_cnfStream->getLiteral(*it));
     }
   } else {
-    explanation.push(l);
-    explanation.push(~d_cnfStream->getLiteral(theoryExplanation));
+    explanation.push_back(l);
+    explanation.push_back(~d_cnfStream->getLiteral(theoryExplanation));
   }
 }
 
-void SatSolver::enqueueTheoryLiteral(const SatLiteral& l) {
+void TheoryProxy::enqueueTheoryLiteral(const SatLiteral& l) {
   Node literalNode = d_cnfStream->getNode(l);
   Debug("prop") << "enqueueing theory literal " << l << " " << literalNode << std::endl;
   Assert(!literalNode.isNull());
   d_theoryEngine->assertFact(literalNode);
 }
 
-SatLiteral SatSolver::getNextDecisionRequest() {
+SatLiteral TheoryProxy::getNextDecisionRequest() {
   TNode n = d_theoryEngine->getNextDecisionRequest();
-  return n.isNull() ? Minisat::lit_Undef : d_cnfStream->getLiteral(n);
+  return n.isNull() ? undefSatLiteral : d_cnfStream->getLiteral(n);
 }
 
-bool SatSolver::theoryNeedCheck() const {
+bool TheoryProxy::theoryNeedCheck() const {
   return d_theoryEngine->needCheck();
 }
 
-void SatSolver::setCnfStream(CnfStream* cnfStream) {
-  d_cnfStream = cnfStream;
-}
-
-void SatSolver::removeClausesAboveLevel(int level) {
+void TheoryProxy::removeClausesAboveLevel(int level) {
   d_cnfStream->removeClausesAboveLevel(level);
 }
 
-TNode SatSolver::getNode(SatLiteral lit) {
+TNode TheoryProxy::getNode(SatLiteral lit) {
   return d_cnfStream->getNode(lit);
 }
 
-void SatSolver::notifyRestart() {
+void TheoryProxy::notifyRestart() {
   d_propEngine->checkTime();
   d_theoryEngine->notifyRestart();
 
@@ -123,7 +119,7 @@ void SatSolver::notifyRestart() {
   }
 }
 
-void SatSolver::notifyNewLemma(SatClause& lemma) {
+void TheoryProxy::notifyNewLemma(SatClause& lemma) {
   Assert(lemma.size() > 0);
   if(Options::current()->lemmaOutputChannel != NULL) {
     if(lemma.size() == 1) {
@@ -146,7 +142,7 @@ void SatSolver::notifyNewLemma(SatClause& lemma) {
   }
 }
 
-SatLiteral SatSolver::getNextReplayDecision() {
+SatLiteral TheoryProxy::getNextReplayDecision() {
 #ifdef CVC4_REPLAY
   if(Options::current()->replayStream != NULL) {
     Expr e = Options::current()->replayStream->nextExpr();
@@ -156,19 +152,20 @@ SatLiteral SatSolver::getNextReplayDecision() {
     }
   }
 #endif /* CVC4_REPLAY */
-  return Minisat::lit_Undef;
+  //FIXME!
+  return undefSatLiteral;
 }
 
-void SatSolver::logDecision(SatLiteral lit) {
+void TheoryProxy::logDecision(SatLiteral lit) {
 #ifdef CVC4_REPLAY
   if(Options::current()->replayLog != NULL) {
-    Assert(lit != Minisat::lit_Undef, "logging an `undef' decision ?!");
+    Assert(lit != undefSatLiteral, "logging an `undef' decision ?!");
     *Options::current()->replayLog << d_cnfStream->getNode(lit) << std::endl;
   }
 #endif /* CVC4_REPLAY */
 }
 
-void SatSolver::checkTime() {
+void TheoryProxy::checkTime() {
   d_propEngine->checkTime();
 }