additional stuff for sharing,

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);