1 files changed, 43 insertions, 2 deletions

diff --git a/src/prop/sat.cpp b/src/prop/sat.cpp
index 207bda4db..a7b536a57 100644
--- a/src/prop/sat.cpp
+++ b/src/prop/sat.cpp
@@ -26,9 +26,9 @@
 namespace CVC4 {
 namespace prop {
 
-void SatSolver::theoryCheck(SatClause& conflict) {
+void SatSolver::theoryCheck(theory::Theory::Effort effort, SatClause& conflict) {
   // Try theory propagation
-  bool ok = d_theoryEngine->check(theory::Theory::FULL_EFFORT);
+  bool ok = d_theoryEngine->check(effort);
   // If in conflict construct the conflict clause
   if (!ok) {
     // We have a conflict, get it
@@ -47,6 +47,47 @@ void SatSolver::theoryCheck(SatClause& conflict) {
   }
 }
 
+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) {
+    Debug("prop-explain") << "theoryPropagate() => " << outputNodes[i].toString() << endl;
+    // The second argument ("true") instructs the CNF stream to create
+    // a new literal mapping if it doesn't exist.  This can happen due
+    // to a circular dependence, if a SAT literal "a" is asserted as a
+    // unit to the SAT solver, a round of theory propagation can occur
+    // before all Nodes have SAT variable mappings.
+    SatLiteral l = d_cnfStream->getLiteral(outputNodes[i], true);
+    output.push_back(l);
+  }
+}
+
+void SatSolver::explainPropagation(SatLiteral l, SatClause& explanation) {
+  TNode lNode = d_cnfStream->getNode(l);
+  Debug("prop-explain") << "explainPropagation(" << lNode.toString() << ")" << endl;
+  Node theoryExplanation = d_theoryEngine->getExplanation(lNode);
+  Debug("prop-explain") << "explainPropagation() => " <<  theoryExplanation.toString() << endl;
+  if (lNode.getKind() == kind::AND) {
+    Node::const_iterator it = theoryExplanation.begin();
+    Node::const_iterator it_end = theoryExplanation.end();
+    explanation.push(l);
+    for (; it != it_end; ++ it) {
+      explanation.push(~d_cnfStream->getLiteral(*it));
+    }
+  } else {
+    explanation.push(l);
+    explanation.push(~d_cnfStream->getLiteral(theoryExplanation));
+  }
+}
+
+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;