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

1 files changed, 6 insertions, 2 deletions

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