Some initial changes to allow for lemmas on demand.

To be done:
* Add erasable map Clause* to bool to minisat (backtracks with the solver)
* Add map from Clause* to Node (clauses that came from a node)
* Add reference counting Literal -> Node to CNFManager
* If Literal -> Node refcount goes to zero, the clauses of Node can be erased (if eresable)
* If clause is erased for each L in clause L -> Node refcount goes down

2 files changed, 23 insertions, 10 deletions

diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 6ca447ea5..bdc32ab21 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -130,8 +130,8 @@ void TheoryArith::registerTerm(TNode tn){
 
           Node slackEqLeft = NodeManager::currentNM()->mkNode(EQUAL,slack,left);
           slackEqLeft.setAttribute(TheoryArithPropagated(), true);
-          //TODO this has to be wrong no?
-          d_out->lemma(slackEqLeft);
+          //TODO this has to be wrong no? YES (dejan)
+          // d_out->lemma(slackEqLeft);
 
           d_tableau.addRow(slackEqLeft);
 
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index c8b93e8b4..e85e66e99 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -22,6 +22,7 @@
 #include "theory/theory.h"
 #include "theory/theoryof_table.h"
 
+#include "prop/prop_engine.h"
 #include "theory/booleans/theory_bool.h"
 #include "theory/uf/theory_uf.h"
 #include "theory/arith/theory_arith.h"
@@ -30,8 +31,6 @@
 
 namespace CVC4 {
 
-class SmtEngine;
-
 // In terms of abstraction, this is below (and provides services to)
 // PropEngine.
 
@@ -43,8 +42,8 @@ class SmtEngine;
  */
 class TheoryEngine {
 
-  /** Associated SMT engine */
-  SmtEngine* d_smt;
+  /** Associated PropEngine engine */
+  prop::PropEngine* d_propEngine;
 
   /** A table of Kinds to pointers to Theory */
   theory::TheoryOfTable d_theoryOfTable;
@@ -80,7 +79,8 @@ class TheoryEngine {
     void propagate(TNode, bool) throw(theory::Interrupted) {
     }
 
-    void lemma(TNode, bool) throw(theory::Interrupted) {
+    void lemma(TNode node, bool) throw(theory::Interrupted) {
+      d_engine->newLemma(node);
     }
 
     void explanation(TNode, bool) throw(theory::Interrupted) {
@@ -171,8 +171,8 @@ public:
   /**
    * Construct a theory engine.
    */
-  TheoryEngine(SmtEngine* smt, context::Context* ctxt) :
-    d_smt(smt),
+  TheoryEngine(context::Context* ctxt) :
+    d_propEngine(NULL),
     d_theoryOut(this, ctxt),
     d_bool(ctxt, d_theoryOut),
     d_uf(ctxt, d_theoryOut),
@@ -187,6 +187,12 @@ public:
     d_theoryOfTable.registerTheory(&d_bv);
   }
 
+  void setPropEngine(prop::PropEngine* propEngine)
+  {
+    Assert(d_propEngine == NULL);
+    d_propEngine = propEngine;
+  }
+
   /**
    * This is called at shutdown time by the SmtEngine, just before
    * destruction.  It is important because there are destruction
@@ -263,8 +269,10 @@ public:
    * Check all (currently-active) theories for conflicts.
    * @param effort the effort level to use
    */
-  inline bool check(theory::Theory::Effort effort) {
+  inline bool check(theory::Theory::Effort effort)
+  {
     d_theoryOut.d_conflictNode = Node::null();
+    // Do the checking
     try {
       //d_bool.check(effort);
       d_uf.check(effort);
@@ -274,9 +282,14 @@ public:
     } catch(const theory::Interrupted&) {
       Debug("theory") << "TheoryEngine::check() => conflict" << std::endl;
     }
+    // Return wheather we have a conflict
     return d_theoryOut.d_conflictNode.get().isNull();
   }
 
+  inline void newLemma(TNode node) {
+    d_propEngine->assertLemma(node);
+  }
+
   /**
    * Returns the last conflict (if any).
    */