diff options
Diffstat (limited to 'src/prop/sat.cpp')
-rw-r--r-- | src/prop/sat.cpp | 49 |
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(); } |