new implementation of lemmas on demand

comparison <http://goedel.cims.nyu.edu/regress-results/compare_jobs.php?job_id=2673&&p=5&reference_id=2637>

1 files changed, 2 insertions, 27 deletions

diff --git a/src/prop/sat.cpp b/src/prop/sat.cpp
index f34699e2b..62558cac1 100644
--- a/src/prop/sat.cpp
+++ b/src/prop/sat.cpp
@@ -27,33 +27,8 @@
 namespace CVC4 {
 namespace prop {
 
-void SatSolver::theoryCheck(theory::Theory::Effort effort, SatClause& conflict) {
-  Assert(conflict.size() == 0);
-  // Try theory propagation
-  bool ok = d_theoryEngine->check(effort);
-  // If in conflict construct the conflict clause
-  if (!ok) {
-    // We have a conflict, get it
-    Node conflictNode = d_theoryEngine->getConflict();
-    Debug("prop") << "SatSolver::theoryCheck() => conflict: " << conflictNode << std::endl;
-    if(conflictNode.getKind() == kind::AND) {
-      // Go through the literals and construct the conflict clause
-      Node::const_iterator literal_it = conflictNode.begin();
-      Node::const_iterator literal_end = conflictNode.end();
-      while (literal_it != literal_end) {
-        // Get the literal corresponding to the node
-        SatLiteral l = d_cnfStream->getLiteral(*literal_it);
-        // Add the negation to the conflict clause and continue
-        conflict.push(~l);
-        literal_it ++;
-      }
-    } else { // unit conflict
-      // Get the literal corresponding to the node
-      SatLiteral l = d_cnfStream->getLiteral(conflictNode);
-      // construct the unit conflict clause
-      conflict.push(~l);
-    }
-  }
+void SatSolver::theoryCheck(theory::Theory::Effort effort) {
+  d_theoryEngine->check(effort);
 }
 
 void SatSolver::theoryPropagate(std::vector<SatLiteral>& output) {