diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2011-09-15 06:53:33 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2011-09-15 06:53:33 +0000 |
commit | 72f552ead344b13d90832222157b970ae3dec8ff (patch) | |
tree | b02854356d5c5f98b3873f858f38b6762135bdc1 /src/prop | |
parent | 62a50760346e130345b24e8a14ad0dac0dca5d38 (diff) |
additional stuff for sharing,
Diffstat (limited to 'src/prop')
-rw-r--r-- | src/prop/minisat/core/Solver.cc | 4 | ||||
-rw-r--r-- | src/prop/sat.cpp | 16 | ||||
-rw-r--r-- | src/prop/sat.h | 2 |
3 files changed, 5 insertions, 17 deletions
diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc index e160e1ef5..770433489 100644 --- a/src/prop/minisat/core/Solver.cc +++ b/src/prop/minisat/core/Solver.cc @@ -665,12 +665,10 @@ CRef Solver::propagate(TheoryCheckType type) void Solver::propagateTheory() { std::vector<Lit> propagatedLiterals; proxy->theoryPropagate(propagatedLiterals); - const unsigned i_end = propagatedLiterals.size(); - for (unsigned i = 0; i < i_end; ++ i) { + for (unsigned i = 0, i_end = propagatedLiterals.size(); i < i_end; ++ i) { Debug("minisat") << "Theory propagated: " << propagatedLiterals[i] << std::endl; uncheckedEnqueue(propagatedLiterals[i], CRef_Lazy); } - proxy->clearPropagatedLiterals(); } /*_________________________________________________________________________________________________ diff --git a/src/prop/sat.cpp b/src/prop/sat.cpp index 8bda0fd1e..386fb5aad 100644 --- a/src/prop/sat.cpp +++ b/src/prop/sat.cpp @@ -36,16 +36,12 @@ void SatSolver::theoryCheck(theory::Theory::Effort effort) { } void SatSolver::theoryPropagate(std::vector<SatLiteral>& output) { - // Propagate - d_theoryEngine->propagate(); // Get the propagated literals - const std::vector<TNode>& outputNodes = d_theoryEngine->getPropagatedLiterals(); - // If any literals, make a clause - const unsigned i_end = outputNodes.size(); - for (unsigned i = 0; i < i_end; ++ i) { + std::vector<TNode> outputNodes; + d_theoryEngine->getPropagatedLiterals(outputNodes); + for (unsigned i = 0, i_end = outputNodes.size(); i < i_end; ++ i) { Debug("prop-explain") << "theoryPropagate() => " << outputNodes[i].toString() << std::endl; - SatLiteral l = d_cnfStream->getLiteral(outputNodes[i]); - output.push_back(l); + output.push_back(d_cnfStream->getLiteral(outputNodes[i])); } } @@ -67,10 +63,6 @@ void SatSolver::explainPropagation(SatLiteral l, SatClause& explanation) { } } -void SatSolver::clearPropagatedLiterals() { - d_theoryEngine->clearPropagatedLiterals(); -} - void SatSolver::enqueueTheoryLiteral(const SatLiteral& l) { Node literalNode = d_cnfStream->getNode(l); Debug("prop") << "enqueueing theory literal " << l << " " << literalNode << std::endl; diff --git a/src/prop/sat.h b/src/prop/sat.h index 39977a96b..ee3978555 100644 --- a/src/prop/sat.h +++ b/src/prop/sat.h @@ -226,8 +226,6 @@ public: void theoryPropagate(std::vector<SatLiteral>& output); - void clearPropagatedLiterals(); - void enqueueTheoryLiteral(const SatLiteral& l); void setCnfStream(CnfStream* cnfStream); |