From: Dejan Jovanović <dejan.jovanovic@gmail.com>
Date: Tue, 25 May 2010 05:30:40 +0000 (+0000)
Subject: Some initial changes to allow for lemmas on demand.
X-Git-Tag: cvc5-1.0.0~9053
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=e87c14798b99ccb586751d291b0eeb3208265bd8;p=cvc5.git

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

diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp
index 31afa986c..51ae695cf 100644
--- a/src/prop/cnf_stream.cpp
+++ b/src/prop/cnf_stream.cpp
@@ -37,30 +37,30 @@ TseitinCnfStream::TseitinCnfStream(SatInputInterface* satSolver) :
   CnfStream(satSolver) {
 }
 
-void CnfStream::assertClause(SatClause& c) {
+void CnfStream::assertClause(TNode node, SatClause& c) {
   Debug("cnf") << "Inserting into stream " << c << endl;
-  d_satSolver->addClause(c);
+  d_satSolver->addClause(c, d_assertingLemma);
 }
 
-void CnfStream::assertClause(SatLiteral a) {
+void CnfStream::assertClause(TNode node, SatLiteral a) {
   SatClause clause(1);
   clause[0] = a;
-  assertClause(clause);
+  assertClause(node, clause);
 }
 
-void CnfStream::assertClause(SatLiteral a, SatLiteral b) {
+void CnfStream::assertClause(TNode node, SatLiteral a, SatLiteral b) {
   SatClause clause(2);
   clause[0] = a;
   clause[1] = b;
-  assertClause(clause);
+  assertClause(node, clause);
 }
 
-void CnfStream::assertClause(SatLiteral a, SatLiteral b, SatLiteral c) {
+void CnfStream::assertClause(TNode node, SatLiteral a, SatLiteral b, SatLiteral c) {
   SatClause clause(3);
   clause[0] = a;
   clause[1] = b;
   clause[2] = c;
-  assertClause(clause);
+  assertClause(node, clause);
 }
 
 bool CnfStream::isCached(TNode n) const {
@@ -74,7 +74,7 @@ SatLiteral CnfStream::lookupInCache(TNode n) const {
 
 void CnfStream::cacheTranslation(TNode node, SatLiteral lit) {
   Debug("cnf") << "caching translation " << node << " to " << lit << endl;
-  // We always cash bot the node and the negation at the same time
+  // We always cash both the node and the negation at the same time
   d_translationCache[node] = lit;
   d_translationCache[node.notNode()] = ~lit;
 }
@@ -125,9 +125,9 @@ SatLiteral TseitinCnfStream::handleAtom(TNode node) {
 
   if(node.getKind() == kind::CONST_BOOLEAN) {
     if(node.getConst<bool>()) {
-      assertClause(lit);
+      assertClause(node, lit);
     } else {
-      assertClause(~lit);
+      assertClause(node, ~lit);
     }
   }
 
@@ -144,10 +144,10 @@ SatLiteral TseitinCnfStream::handleXor(TNode xorNode) {
 
   SatLiteral xorLit = newLiteral(xorNode);
 
-  assertClause(a, b, ~xorLit);
-  assertClause(~a, ~b, ~xorLit);
-  assertClause(a, ~b, xorLit);
-  assertClause(~a, b, xorLit);
+  assertClause(xorNode, a, b, ~xorLit);
+  assertClause(xorNode, ~a, ~b, ~xorLit);
+  assertClause(xorNode, a, ~b, xorLit);
+  assertClause(xorNode, ~a, b, xorLit);
 
   return xorLit;
 }
@@ -175,14 +175,14 @@ SatLiteral TseitinCnfStream::handleOr(TNode orNode) {
   // lit | ~(a_1 | a_2 | a_3 | ... | a_n)
   // (lit | ~a_1) & (lit | ~a_2) & (lit & ~a_3) & ... & (lit & ~a_n)
   for(unsigned i = 0; i < n_children; ++i) {
-    assertClause(orLit, ~clause[i]);
+    assertClause(orNode, orLit, ~clause[i]);
   }
 
   // lit -> (a_1 | a_2 | a_3 | ... | a_n)
   // ~lit | a_1 | a_2 | a_3 | ... | a_n
   clause[n_children] = ~orLit;
   // This needs to go last, as the clause might get modified by the SAT solver
-  assertClause(clause);
+  assertClause(orNode, clause);
 
   // Return the literal
   return orLit;
@@ -211,7 +211,7 @@ SatLiteral TseitinCnfStream::handleAnd(TNode andNode) {
   // ~lit | (a_1 & a_2 & a_3 & ... & a_n)
   // (~lit | a_1) & (~lit | a_2) & ... & (~lit | a_n)
   for(unsigned i = 0; i < n_children; ++i) {
-    assertClause(~andLit, ~clause[i]);
+    assertClause(andNode, ~andLit, ~clause[i]);
   }
 
   // lit <- (a_1 & a_2 & a_3 & ... a_n)
@@ -219,7 +219,7 @@ SatLiteral TseitinCnfStream::handleAnd(TNode andNode) {
   // lit | ~a_1 | ~a_2 | ~a_3 | ... | ~a_n
   clause[n_children] = andLit;
   // This needs to go last, as the clause might get modified by the SAT solver
-  assertClause(clause);
+  assertClause(andNode, clause);
   return andLit;
 }
 
@@ -236,13 +236,13 @@ SatLiteral TseitinCnfStream::handleImplies(TNode impliesNode) {
 
   // lit -> (a->b)
   // ~lit | ~ a | b
-  assertClause(~impliesLit, ~a, b);
+  assertClause(impliesNode, ~impliesLit, ~a, b);
 
   // (a->b) -> lit
   // ~(~a | b) | lit
   // (a | l) & (~b | l)
-  assertClause(a, impliesLit);
-  assertClause(~b, impliesLit);
+  assertClause(impliesNode, a, impliesLit);
+  assertClause(impliesNode, ~b, impliesLit);
 
   return impliesLit;
 }
@@ -263,16 +263,16 @@ SatLiteral TseitinCnfStream::handleIff(TNode iffNode) {
   // lit -> ((a-> b) & (b->a))
   // ~lit | ((~a | b) & (~b | a))
   // (~a | b | ~lit) & (~b | a | ~lit)
-  assertClause(~a, b, ~iffLit);
-  assertClause(a, ~b, ~iffLit);
+  assertClause(iffNode, ~a, b, ~iffLit);
+  assertClause(iffNode, a, ~b, ~iffLit);
 
   // (a<->b) -> lit
   // ~((a & b) | (~a & ~b)) | lit
   // (~(a & b)) & (~(~a & ~b)) | lit
   // ((~a | ~b) & (a | b)) | lit
   // (~a | ~b | lit) & (a | b | lit)
-  assertClause(~a, ~b, iffLit);
-  assertClause(a, b, iffLit);
+  assertClause(iffNode, ~a, ~b, iffLit);
+  assertClause(iffNode, a, b, iffLit);
 
   return iffLit;
 }
@@ -309,9 +309,9 @@ SatLiteral TseitinCnfStream::handleIte(TNode iteNode) {
   // lit -> (t | e) & (b -> t) & (!b -> e)
   // lit -> (t | e) & (!b | t) & (b | e)
   // (!lit | t | e) & (!lit | !b | t) & (!lit | b | e)
-  assertClause(~iteLit, thenLit, elseLit);
-  assertClause(~iteLit, ~condLit, thenLit);
-  assertClause(~iteLit, condLit, elseLit);
+  assertClause(iteNode, ~iteLit, thenLit, elseLit);
+  assertClause(iteNode, ~iteLit, ~condLit, thenLit);
+  assertClause(iteNode, ~iteLit, condLit, elseLit);
 
   // If ITE is false then one of the branches is false and the condition
   // implies which one
@@ -319,9 +319,9 @@ SatLiteral TseitinCnfStream::handleIte(TNode iteNode) {
   // !lit -> (!t | !e) & (b -> !t) & (!b -> !e)
   // !lit -> (!t | !e) & (!b | !t) & (b | !e)
   // (lit | !t | !e) & (lit | !b | !t) & (lit | b | !e)
-  assertClause(iteLit, ~thenLit, ~elseLit);
-  assertClause(iteLit, ~condLit, ~thenLit);
-  assertClause(iteLit, condLit, ~elseLit);
+  assertClause(iteNode, iteLit, ~thenLit, ~elseLit);
+  assertClause(iteNode, iteLit, ~condLit, ~thenLit);
+  assertClause(iteNode, iteLit, condLit, ~elseLit);
 
   return iteLit;
 }
@@ -347,7 +347,7 @@ Node TseitinCnfStream::handleNonAtomicNode(TNode node) {
             nodeManager->mkNode(EQUAL, skolem, node[1]),
             nodeManager->mkNode(EQUAL, skolem, node[2]));
     nodeManager->setAttribute(node, IteRewriteAttr(), skolem);
-    convertAndAssert( newAssertion );
+    convertAndAssert(newAssertion, d_assertingLemma);
     return skolem;
   } else {
     std::vector<Node> newChildren;
@@ -403,15 +403,16 @@ SatLiteral TseitinCnfStream::toCNF(TNode node) {
   }
 }
 
-void TseitinCnfStream::convertAndAssert(TNode node) {
+void TseitinCnfStream::convertAndAssert(TNode node, bool lemma) {
   Debug("cnf") << "convertAndAssert(" << node << ")" << endl;
+  d_assertingLemma = lemma;
   if(node.getKind() == AND) {
     // If the node is a conjunction, we handle each conjunct separately
     for( TNode::const_iterator conjunct = node.begin(),
          node_end = node.end();
          conjunct != node_end;
          ++conjunct ) {
-      convertAndAssert(*conjunct);
+      convertAndAssert(*conjunct, lemma);
     }
   } else if(node.getKind() == OR) {
     // If the node is a disjunction, we construct a clause and assert it
@@ -423,10 +424,10 @@ void TseitinCnfStream::convertAndAssert(TNode node) {
       clause[i] = toCNF(*disjunct);
     }
     Assert( disjunct == node.end() );
-    assertClause(clause);
+    assertClause(node, clause);
   } else {
     // Otherwise, we just convert using the definitional transformation
-    assertClause(toCNF(node));
+    assertClause(node, toCNF(node));
   }
 }
 
diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h
index 7546a8880..1ea600322 100644
--- a/src/prop/cnf_stream.h
+++ b/src/prop/cnf_stream.h
@@ -39,7 +39,9 @@ class PropEngine;
  * @author Tim King <taking@cs.nyu.edu>
  */
 class CnfStream {
+
 public:
+
   /** Cache of what nodes have been registered to a literal. */
   typedef __gnu_cxx::hash_map<SatLiteral, Node, SatSolver::SatLiteralHashFunction> NodeCache;
 
@@ -56,24 +58,31 @@ private:
 
 protected:
 
+  /**
+   * Are we asserting a lemma (true) or a permanent clause (false).
+   * This is set at the begining of convertAndAssert so that it doesn't
+   * need to be passed on over the stack.
+   */
+  bool d_assertingLemma;
+
   /**
    * Asserts the given clause to the sat solver.
    * @param clause the clasue to assert
    */
-  void assertClause(SatClause& clause);
+  void assertClause(TNode node, SatClause& clause);
 
   /**
    * Asserts the unit clause to the sat solver.
    * @param a the unit literal of the clause
    */
-  void assertClause(SatLiteral a);
+  void assertClause(TNode node, SatLiteral a);
 
   /**
    * Asserts the binary clause to the sat solver.
    * @param a the first literal in the clause
    * @param b the second literal in the clause
    */
-  void assertClause(SatLiteral a, SatLiteral b);
+  void assertClause(TNode node, SatLiteral a, SatLiteral b);
 
   /**
    * Asserts the ternary clause to the sat solver.
@@ -81,7 +90,7 @@ protected:
    * @param b the second literal in the clause
    * @param c the thirs literal in the clause
    */
-  void assertClause(SatLiteral a, SatLiteral b, SatLiteral c);
+  void assertClause(TNode node, SatLiteral a, SatLiteral b, SatLiteral c);
 
   /**
    * Returns true if the node has been cashed in the translation cache.
@@ -137,7 +146,7 @@ public:
    * @param node node to convert and assert
    * @param whether the sat solver can choose to remove this clause
    */
-  virtual void convertAndAssert(TNode node) = 0;
+  virtual void convertAndAssert(TNode node, bool lemma = false) = 0;
 
   /**
    * Get the node that is represented by the given SatLiteral.
@@ -175,8 +184,9 @@ public:
   /**
    * Convert a given formula to CNF and assert it to the SAT solver.
    * @param node the formula to assert
+   * @param lemma is this a lemma that is erasable
    */
-  void convertAndAssert(TNode node);
+  void convertAndAssert(TNode node, bool lemma);
 
   /**
    * Constructs the stream to use the given sat solver.
diff --git a/src/prop/minisat/core/Solver.C b/src/prop/minisat/core/Solver.C
index a735cd46c..8533e191b 100644
--- a/src/prop/minisat/core/Solver.C
+++ b/src/prop/minisat/core/Solver.C
@@ -98,7 +98,7 @@ Var Solver::newVar(bool sign, bool dvar, bool theoryAtom)
 }
 
 
-bool Solver::addClause(vec<Lit>& ps)
+bool Solver::addClause(vec<Lit>& ps, ClauseType type)
 {
     assert(decisionLevel() == 0);
 
@@ -119,16 +119,19 @@ bool Solver::addClause(vec<Lit>& ps)
     if (ps.size() == 0)
         return ok = false;
     else if (ps.size() == 1){
+        assert(type != CLAUSE_LEMMA);
         assert(value(ps[0]) == l_Undef);
         uncheckedEnqueue(ps[0]);
         return ok = (propagate() == NULL);
     }else{
         Clause* c = Clause_new(ps, false);
         clauses.push(c);
+        if (type == CLAUSE_LEMMA) lemmas.push(c);
         attachClause(*c);
     }
 
     return true;
+
 }
 
 
@@ -181,6 +184,12 @@ void Solver::cancelUntil(int level) {
         qhead = trail_lim[level];
         trail.shrink(trail.size() - trail_lim[level]);
         trail_lim.shrink(trail_lim.size() - level);
+        // We can erase the lemmas now
+        for (int c = lemmas.size() - 1; c >= lemmas_lim[level]; c--) {
+          // TODO: can_erase[lemma[c]] = true;
+        }
+        lemmas.shrink(lemmas.size() - lemmas_lim[level]);
+        lemmas_lim.shrink(lemmas_lim.size() - level);
     }
 }
 
diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h
index bf2018338..312fe44d5 100644
--- a/src/prop/minisat/core/Solver.h
+++ b/src/prop/minisat/core/Solver.h
@@ -66,7 +66,18 @@ public:
     // Problem specification:
     //
     Var     newVar    (bool polarity = true, bool dvar = true, bool theoryAtom = false); // Add a new variable with parameters specifying variable mode.
-    bool    addClause (vec<Lit>& ps);                           // Add a clause to the solver. NOTE! 'ps' may be shrunk by this method!
+
+    // Types of clauses
+    enum ClauseType {
+      // Clauses defined by the problem
+      CLAUSE_PROBLEM,
+      // Lemma clauses added by the theories
+      CLAUSE_LEMMA,
+      // Conflict clauses
+      CLAUSE_CONFLICT
+    };
+
+    bool    addClause (vec<Lit>& ps, ClauseType type);                           // Add a clause to the solver. NOTE! 'ps' may be shrunk by this method!
 
     // Solving:
     //
@@ -148,9 +159,12 @@ protected:
     vec<char>           decision_var;     // Declares if a variable is eligible for selection in the decision heuristic.
     vec<Lit>            trail;            // Assignment stack; stores all assigments made in the order they were made.
     vec<int>            trail_lim;        // Separator indices for different decision levels in 'trail'.
+    vec<Clause*>        lemmas;           // List of lemmas we added (context dependent)
+    vec<int>            lemmas_lim;       // Separator indices for different decision levels in 'lemmas'.
     vec<Clause*>        reason;           // 'reason[var]' is the clause that implied the variables current value, or 'NULL' if none.
     vec<int>            level;            // 'level[var]' contains the level at which the assignment was made.
     int                 qhead;            // Head of queue (as index into the trail -- no more explicit propagation queue in MiniSat).
+    int                 lhead;            // Head of the lemma stack (for backtracking)
     int                 simpDB_assigns;   // Number of top-level assignments since last execution of 'simplify()'.
     int64_t             simpDB_props;     // Remaining number of propagations that must be made before next execution of 'simplify()'.
     vec<Lit>            assumptions;      // Current set of assumptions provided to solve by the user.
@@ -256,7 +270,7 @@ inline void Solver::claBumpActivity (Clause& c) {
 
 inline bool     Solver::enqueue         (Lit p, Clause* from)   { return value(p) != l_Undef ? value(p) != l_False : (uncheckedEnqueue(p, from), true); }
 inline bool     Solver::locked          (const Clause& c) const { return reason[var(c[0])] == &c && value(c[0]) == l_True; }
-inline void     Solver::newDecisionLevel()                      { trail_lim.push(trail.size()); context->push(); }
+inline void     Solver::newDecisionLevel()                      { trail_lim.push(trail.size()); lemmas_lim.push(lemmas.size()); context->push(); }
 
 inline int      Solver::decisionLevel ()      const   { return trail_lim.size(); }
 inline uint32_t Solver::abstractLevel (Var x) const   { return 1 << (level[x] & 31); }
diff --git a/src/prop/minisat/simp/SimpSolver.C b/src/prop/minisat/simp/SimpSolver.C
index 057dfdbe2..9aad6aea7 100644
--- a/src/prop/minisat/simp/SimpSolver.C
+++ b/src/prop/minisat/simp/SimpSolver.C
@@ -118,7 +118,7 @@ bool SimpSolver::solve(const vec<Lit>& assumps, bool do_simp, bool turn_off_simp
 
 
 
-bool SimpSolver::addClause(vec<Lit>& ps)
+bool SimpSolver::addClause(vec<Lit>& ps, ClauseType type)
 {
     for (int i = 0; i < ps.size(); i++)
         if (isEliminated(var(ps[i])))
@@ -129,7 +129,7 @@ bool SimpSolver::addClause(vec<Lit>& ps)
     if (redundancy_check && implied(ps))
         return true;
 
-    if (!Solver::addClause(ps))
+    if (!Solver::addClause(ps, type))
         return false;
 
     if (use_simplification && clauses.size() == nclauses + 1){
@@ -485,7 +485,7 @@ bool SimpSolver::eliminateVar(Var v, bool fail)
     vec<Lit> resolvent;
     for (int i = 0; i < pos.size(); i++)
         for (int j = 0; j < neg.size(); j++)
-            if (merge(*pos[i], *neg[j], v, resolvent) && !addClause(resolvent))
+            if (merge(*pos[i], *neg[j], v, resolvent) && !addClause(resolvent, CLAUSE_CONFLICT))
                 return false;
 
     // DEBUG: For checking that a clause set is saturated with respect to variable elimination.
@@ -527,7 +527,7 @@ void SimpSolver::remember(Var v)
             clause.push(c[j]);
 
         remembered_clauses++;
-        check(addClause(clause));
+        check(addClause(clause, CLAUSE_PROBLEM));
         free(&c);
     }
 
diff --git a/src/prop/minisat/simp/SimpSolver.h b/src/prop/minisat/simp/SimpSolver.h
index 38d51206d..3da574f6c 100644
--- a/src/prop/minisat/simp/SimpSolver.h
+++ b/src/prop/minisat/simp/SimpSolver.h
@@ -45,7 +45,7 @@ class SimpSolver : public Solver {
     // Problem specification:
     //
     Var     newVar    (bool polarity = true, bool dvar = true, bool theoryAtom = false);
-    bool    addClause (vec<Lit>& ps);
+    bool    addClause (vec<Lit>& ps, ClauseType type);
 
     // Variable mode:
     // 
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index ec0e2dfbc..b9fbd3ce6 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -33,6 +33,26 @@ using namespace CVC4::context;
 namespace CVC4 {
 namespace prop {
 
+/** Keeps a boolean flag scoped */
+class ScopedBool {
+
+private:
+
+  bool d_original;
+  bool& d_reference;
+
+public:
+
+  ScopedBool(bool& reference) :
+    d_reference(reference) {
+    d_original = reference;
+  }
+
+  ~ScopedBool() {
+    d_reference = d_original;
+  }
+};
+
 PropEngine::PropEngine(const Options* opts, DecisionEngine* de,
                        TheoryEngine* te, Context* context)
 : d_inCheckSat(false),
@@ -61,6 +81,7 @@ void PropEngine::assertFormula(TNode node) {
 }
 
 void PropEngine::assertLemma(TNode node) {
+  Assert(d_inCheckSat, "Sat solver should be in solve()!");
   Debug("prop") << "assertFormula(" << node << ")" << endl;
   // Assert as removable
   d_cnfStream->convertAndAssert(node);
@@ -89,12 +110,13 @@ void PropEngine::printSatisfyingAssignment(){
 Result PropEngine::checkSat() {
   Assert(!d_inCheckSat, "Sat solver in solve()!");
   Debug("prop") << "PropEngine::checkSat()" << endl;
+
   // Mark that we are in the checkSat
+  ScopedBool scopedBool(d_inCheckSat);
   d_inCheckSat = true;
+
   // Check the problem
   bool result = d_satSolver->solve();
-  // Not in checkSat any more
-  d_inCheckSat = false;
 
   if( result && debugTagIsOn("prop") ) {
     printSatisfyingAssignment();
diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h
index 4d25e9bc0..7d3656a32 100644
--- a/src/prop/prop_engine.h
+++ b/src/prop/prop_engine.h
@@ -23,9 +23,11 @@
 #include "util/result.h"
 #include "util/options.h"
 #include "util/decision_engine.h"
-#include "theory/theory_engine.h"
 
 namespace CVC4 {
+
+class TheoryEngine;
+
 namespace prop {
 
 class CnfStream;
@@ -96,7 +98,9 @@ public:
 
   /**
    * Converts the given formula to CNF and assert the CNF to the sat solver.
-   * The formula can be removed by the sat solver.
+   * The formula can be removed by the sat solver after backtracking lower
+   * than the (SAT and SMT) level at which it was asserted.
+   *
    * @param node the formula to assert
    */
   void assertLemma(TNode node);
diff --git a/src/prop/sat.cpp b/src/prop/sat.cpp
index 46d2182a9..df6eead4c 100644
--- a/src/prop/sat.cpp
+++ b/src/prop/sat.cpp
@@ -9,7 +9,9 @@ namespace prop {
 
 void SatSolver::theoryCheck(SatClause& conflict) {
   // Try theory propagation
-  if (!d_theoryEngine->check(theory::Theory::FULL_EFFORT)) {
+  bool ok = d_theoryEngine->check(theory::Theory::FULL_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;
diff --git a/src/prop/sat.h b/src/prop/sat.h
index 42f454820..f9d27d2ac 100644
--- a/src/prop/sat.h
+++ b/src/prop/sat.h
@@ -93,7 +93,7 @@ inline std::string stringOfLiteralValue(SatLiteralValue val) {
 class SatInputInterface {
 public:
   /** Assert a clause in the solver. */
-  virtual void addClause(SatClause& clause) = 0;
+  virtual void addClause(SatClause& clause, bool lemma) = 0;
   /** Create a new boolean variable in the solver. */
   virtual SatVariable newVar(bool theoryAtom = false) = 0;
 };
@@ -148,7 +148,7 @@ public:
 
   bool solve();
   
-  void addClause(SatClause& clause);
+  void addClause(SatClause& clause, bool lemma);
 
   SatVariable newVar(bool theoryAtom = false);
 
@@ -190,8 +190,8 @@ inline bool SatSolver::solve() {
   return d_minisat->solve();
 }
 
-inline void SatSolver::addClause(SatClause& clause) {
-  d_minisat->addClause(clause);
+inline void SatSolver::addClause(SatClause& clause, bool lemma) {
+  d_minisat->addClause(clause, lemma ? minisat::Solver::CLAUSE_LEMMA : minisat::Solver::CLAUSE_PROBLEM);
 }
 
 inline SatVariable SatSolver::newVar(bool theoryAtom) {
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index a55c146b8..3b003846c 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -20,6 +20,8 @@
 #include "util/exception.h"
 #include "util/options.h"
 #include "prop/prop_engine.h"
+#include "theory/theory_engine.h"
+
 
 using namespace CVC4::prop;
 using CVC4::context::Context;
@@ -72,8 +74,11 @@ SmtEngine::SmtEngine(ExprManager* em, const Options* opts) throw () :
   NodeManagerScope nms(d_nodeManager);
 
   d_decisionEngine = new DecisionEngine;
-  d_theoryEngine = new TheoryEngine(this, d_ctxt);
+  // We have mutual dependancy here, so we add the prop engine to the theory
+  // engine later (it is non-essential there)
+  d_theoryEngine = new TheoryEngine(d_ctxt);
   d_propEngine = new PropEngine(opts, d_decisionEngine, d_theoryEngine, d_ctxt);
+  d_theoryEngine->setPropEngine(d_propEngine);
 }
 
 void SmtEngine::shutdown() {
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).
    */