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, 24 insertions, 2 deletions

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