Changes to Solver and PropEngine to support lemmasOnDemand during solve but not yet...

diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index a2477258175717060c895be1ad189ffd4313370f..4817ec1f572f3824ed794f7785f8b289d5f6dcbc 100644 (file)
--- a/src/prop/minisat/core/Solver.cc
+++ b/src/prop/minisat/core/Solver.cc
@@ -56,7 +56,7 @@ Solver::Solver(CVC4::prop::SatSolver* proxy, CVC4::context::Context* context, bo
   , assertionLevel(0)
   , enable_incremental(enable_incremental)
   , problem_extended(false)
-  , in_propagate(false)
+  , in_solve(false)
     // Parameters (user settable):
     //
   , verbosity        (0)
@@ -135,7 +135,7 @@ Var Solver::newVar(bool sign, bool dvar, bool theoryAtom)
     theory   .push(theoryAtom);
 
     // We have extended the problem
-    if (in_propagate) {
+    if (in_solve) {
       problem_extended = true;
       insertVarOrder(v);
     }
@@ -256,7 +256,7 @@ bool Solver::addClause_(vec<Lit>& ps, ClauseType type)
         }
     }
 
-    if (in_propagate && type == CLAUSE_LEMMA) {
+    if (type == CLAUSE_LEMMA) {
       problem_extended = true;
     }
 
@@ -620,15 +620,12 @@ void Solver::uncheckedEnqueue(Lit p, CRef from)
 
 CRef Solver::propagate(TheoryCheckType type)
 {
-    in_propagate = true;
-
     CRef confl = CRef_Undef;
 
     // If this is the final check, no need for Boolean propagation and
     // theory propagation
     if (type == CHECK_WITHOUTH_PROPAGATION_FINAL) {
       confl = theoryCheck(CVC4::theory::Theory::FULL_EFFORT);
-      in_propagate = false;
       return confl;
     }
 
@@ -655,8 +652,6 @@ CRef Solver::propagate(TheoryCheckType type)
         }
     } while (new_assertions);
 
-    in_propagate = false;
-
     return confl;
 }
 
@@ -916,7 +911,26 @@ lbool Solver::search(int nof_conflicts)
 
     TheoryCheckType check_type = CHECK_WITH_PROPAGATION_STANDARD;
     for (;;){
-        problem_extended = false;
+
+        // If we have more assertions from lemmas, we continue
+        if (problem_extended) {
+
+          Debug("minisat::lemmas") << "Problem extended with lemmas, adding propagations." << endl;
+
+          for (int i = 0, i_end = lemma_propagated_literals.size(); i < i_end; ++ i) {
+            if (value(var(lemma_propagated_literals[i])) == l_Undef) {
+              Debug("minisat::lemmas") << "Lemma propagating: " << proxy->getNode(lemma_propagated_literals[i]) << endl;
+              uncheckedEnqueue(lemma_propagated_literals[i], lemma_propagated_reasons[i]);
+            }
+          }
+
+          lemma_propagated_literals.clear();
+          lemma_propagated_reasons.clear();
+
+          check_type = CHECK_WITH_PROPAGATION_STANDARD;
+          problem_extended = false;
+        }
+
         CRef confl = propagate(check_type);
         if (confl != CRef_Undef){
             // CONFLICT
@@ -959,27 +973,10 @@ lbool Solver::search(int nof_conflicts)
                    // We have a conflict so, we are going back to standard checks
             check_type = CHECK_WITH_PROPAGATION_STANDARD;
         }else{
-            // NO CONFLICT
-
-            // If we have more assertions from lemmas, we continue
-            if (problem_extended) {
-
-              Debug("minisat::lemmas") << "Problem extended with lemmas, adding propagations." << endl;
-
-              for (int i = 0, i_end = lemma_propagated_literals.size(); i < i_end; ++ i) {
-                if (value(var(lemma_propagated_literals[i])) == l_Undef) {
-                  Debug("minisat::lemmas") << "Lemma propagating: " << proxy->getNode(lemma_propagated_literals[i]) << endl;
-                  uncheckedEnqueue(lemma_propagated_literals[i], lemma_propagated_reasons[i]);
-                }
-              }
-
-              lemma_propagated_literals.clear();
-              lemma_propagated_reasons.clear();
-
-              check_type = CHECK_WITH_PROPAGATION_STANDARD;
 
+            // NO CONFLICT
+            if (problem_extended)
               continue;
-            }
 
            // If this was a final check, we are satisfiable
             if (check_type == CHECK_WITHOUTH_PROPAGATION_FINAL)
@@ -1082,9 +1079,14 @@ lbool Solver::solve_()
 {
     Debug("minisat") << "nvars = " << nVars() << endl;
 
+    in_solve = true;
+
     model.clear();
     conflict.clear();
-    if (!ok) return l_False;
+    if (!ok){
+      in_solve = false;
+      return l_False;
+    }
 
     solves++;
 
@@ -1126,6 +1128,8 @@ lbool Solver::solve_()
     // Cancel the trail downto previous push
     popTrail();
 
+    in_solve = false;
+
     return status;
 }
 

diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h
index 7050f2d101be9b8f5fd3972603cb841e40cc450a..5c0f0f9a33e54c111325ffc90cd4c71666d9018e 100644 (file)
--- a/src/prop/minisat/core/Solver.h
+++ b/src/prop/minisat/core/Solver.h
@@ -79,8 +79,8 @@ protected:
   /** Shrink 'cs' to contain only clauses below given level */
   void removeClausesAboveLevel(vec<CRef>& cs, int level); 
 
-  /** True if we are inside the propagate method */
-  bool in_propagate;
+  /** True if we are currently solving. */
+  bool in_solve;
 
 public:
 

diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index f3caead8b2eebb60050d33e4d86fa18515d6450a..ab1afceba6293e3ba1716e63b0cb05c1543b1c01 100644 (file)
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -81,19 +81,14 @@ void PropEngine::assertFormula(TNode node) {
 }
 
 void PropEngine::assertLemma(TNode node) {
-  Assert(d_inCheckSat, "Sat solver should be in solve()!");
+  //Assert(d_inCheckSat, "Sat solver should be in solve()!");
   Debug("prop::lemmas") << "assertLemma(" << node << ")" << endl;
+
+  //TODO This comment is now false
   // Assert as removable
   d_cnfStream->convertAndAssert(node, true, false);
 }
 
-void PropEngine::assertSafeLemma(TNode node) {
-  if(d_inCheckSat){
-    assertLemma(node);
-  }else{
-    assertFormula(node);
-  }
-}
 
 void PropEngine::printSatisfyingAssignment(){
   const CnfStream::TranslationCache& transCache =

diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h
index c0483e943eae4d8ef6332269c5f3e934a89eed1b..b43c2d85981ed15f45dca76f828ab054ae75756f 100644 (file)
--- a/src/prop/prop_engine.h
+++ b/src/prop/prop_engine.h
@@ -103,7 +103,6 @@ public:
    * @param node the formula to assert
    */
   void assertLemma(TNode node);
-  void assertSafeLemma(TNode node);
 
   /**
    * Checks the current context for satisfiability.

diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 813b38d9367b3b86dd024c4e6e3e19da3bb5109e..7958d977ee67e8a1933cca3a11bf28342a1fbd1f 100644 (file)
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -318,7 +318,7 @@ public:
   }
 
   inline void newLemma(TNode node) {
-    d_propEngine->assertSafeLemma(preprocess(node));
+    d_propEngine->assertLemma(preprocess(node));
   }
 
   /**