Removing QUICK_CHECK, and other unused ones, from the Theory::Effort.

Seems to be working better <http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=3749&category=&p=5&reference_id=3739>, and should fix the failing cases in the regressions.

Removing one test case from the integer regress0.

3 files changed, 35 insertions, 49 deletions

diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index 678fe28dc..9f3285fff 100644
--- a/src/prop/minisat/core/Solver.cc
+++ b/src/prop/minisat/core/Solver.cc
@@ -248,7 +248,7 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable)
             Debug("minisat") << "got new unit " << ps[0] << " at assertion level " << assertionLevel << std::endl;
             trail_user.push(ps[0]);
           }
-          return ok = (propagate(CHECK_WITHOUTH_PROPAGATION_QUICK) == CRef_Undef);
+          return ok = (propagate(CHECK_WITHOUTH_THEORY) == CRef_Undef);
         } else return ok;
       } else {
         CRef cr = ca.alloc(assertionLevel, ps, false);
@@ -654,8 +654,8 @@ CRef Solver::propagate(TheoryCheckType type)
 
     ScopedBool scoped_bool(minisat_busy, true);
 
-    // If we are not in the quick mode add the lemmas that were left begind
-    if (type != CHECK_WITHOUTH_PROPAGATION_QUICK && lemmas.size() > 0) {
+    // If we are not in the quick mode add the lemmas that were left behind
+    if (type != CHECK_WITHOUTH_THEORY && lemmas.size() > 0) {
       confl = updateLemmas();
       if (confl != CRef_Undef) {
         return confl;
@@ -664,9 +664,9 @@ CRef Solver::propagate(TheoryCheckType type)
 
     // If this is the final check, no need for Boolean propagation and
     // theory propagation
-    if (type == CHECK_WITHOUTH_PROPAGATION_FINAL) {
+    if (type == CHECK_FINAL) {
       // Do the theory check
-      theoryCheck(CVC4::theory::Theory::FULL_EFFORT);
+      theoryCheck(CVC4::theory::Theory::EFFORT_FULL);
       // If there are lemmas (or conflicts) update them
       if (lemmas.size() > 0) {
         recheck = true;
@@ -677,38 +677,24 @@ CRef Solver::propagate(TheoryCheckType type)
       }
     }
 
-    // The effort we will be using to theory check
-    CVC4::theory::Theory::Effort effort = type == CHECK_WITHOUTH_PROPAGATION_QUICK ?
-    		CVC4::theory::Theory::QUICK_CHECK : 
-    		CVC4::theory::Theory::STANDARD;
-
     // Keep running until we have checked everything, we
     // have no conflict and no new literals have been asserted
-    do {
-        do {
-          // Propagate on the clauses
-          confl = propagateBool();
-
-          // If no conflict, do the theory check
-          if (confl == CRef_Undef) {
-              // Do the theory check
-              theoryCheck(effort);
-              // If there are lemmas (or conflicts) update them
-              if (lemmas.size() > 0) {
-                  confl = updateLemmas();
-              }
-          }
-        } while (confl == CRef_Undef && qhead < trail.size());
-
-        // If still consistent do some theory propagation
-        if (confl == CRef_Undef && type == CHECK_WITH_PROPAGATION_STANDARD) {
-          propagateTheory();
-          if (lemmas.size() > 0) {
-              confl = updateLemmas();
-          }
+      do {
+        // Propagate on the clauses
+        confl = propagateBool();
+
+        // If no conflict, do the theory check
+        if (confl == CRef_Undef && type != CHECK_WITHOUTH_THEORY) {
+            // Do the theory check
+            theoryCheck(CVC4::theory::Theory::EFFORT_STANDARD);
+            // Pick up the theory propagated literals
+            propagateTheory();
+            // If there are lemmas (or conflicts) update them
+            if (lemmas.size() > 0) {
+                confl = updateLemmas();
+            }
         }
-
-    } while (confl == CRef_Undef && qhead < trail.size());
+      } while (confl == CRef_Undef && qhead < trail.size());
 
     return confl;
 }
@@ -931,7 +917,7 @@ bool Solver::simplify()
 {
     assert(decisionLevel() == 0);
 
-    if (!ok || propagate(CHECK_WITHOUTH_PROPAGATION_QUICK) != CRef_Undef)
+    if (!ok || propagate(CHECK_WITHOUTH_THEORY) != CRef_Undef)
         return ok = false;
 
     if (nAssigns() == simpDB_assigns || (simpDB_props > 0))
@@ -972,7 +958,7 @@ lbool Solver::search(int nof_conflicts)
     vec<Lit>    learnt_clause;
     starts++;
 
-    TheoryCheckType check_type = CHECK_WITH_PROPAGATION_STANDARD;
+    TheoryCheckType check_type = CHECK_WITH_THEORY;
     for (;;) {
 
         // Propagate and call the theory solvers
@@ -1025,14 +1011,14 @@ lbool Solver::search(int nof_conflicts)
             }
 
              // We have a conflict so, we are going back to standard checks
-            check_type = CHECK_WITH_PROPAGATION_STANDARD;
+            check_type = CHECK_WITH_THEORY;
         } else {
 
 	    // If this was a final check, we are satisfiable
-            if (check_type == CHECK_WITHOUTH_PROPAGATION_FINAL) {
+            if (check_type == CHECK_FINAL) {
               // Unless a lemma has added more stuff to the queues
               if (!order_heap.empty() || qhead < trail.size()) {
-                check_type = CHECK_WITH_PROPAGATION_STANDARD;
+                check_type = CHECK_WITH_THEORY;
                 continue;
               } else if (recheck) {
                 // There some additional stuff added, so we go for another full-check
@@ -1086,7 +1072,7 @@ lbool Solver::search(int nof_conflicts)
 
                 if (next == lit_Undef) {
                     // We need to do a full theory check to confirm
-                    check_type = CHECK_WITHOUTH_PROPAGATION_FINAL;
+                    check_type = CHECK_FINAL;
                     continue;
                 }
 
diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h
index c0dd00166..8a5472725 100644
--- a/src/prop/minisat/core/Solver.h
+++ b/src/prop/minisat/core/Solver.h
@@ -303,12 +303,12 @@ protected:
     vec<bool>           theory;           // Is the variable representing a theory atom
 
     enum TheoryCheckType {
-      // Quick check, but don't perform theory propagation
-      CHECK_WITHOUTH_PROPAGATION_QUICK,
-      // Check and perform theory propagation
-      CHECK_WITH_PROPAGATION_STANDARD,
-      // The SAT problem is satisfiable, perform a full theory check
-      CHECK_WITHOUTH_PROPAGATION_FINAL
+      // Quick check, but don't perform theory reasoning
+      CHECK_WITHOUTH_THEORY,
+      // Check and perform theory reasoning
+      CHECK_WITH_THEORY,
+      // The SAT abstraction of the problem is satisfiable, perform a full theory check
+      CHECK_FINAL
     };
 
     // Temporaries (to reduce allocation overhead). Each variable is prefixed by the method in which it is
diff --git a/src/prop/minisat/simp/SimpSolver.cc b/src/prop/minisat/simp/SimpSolver.cc
index 2b5468186..2cacfbcc0 100644
--- a/src/prop/minisat/simp/SimpSolver.cc
+++ b/src/prop/minisat/simp/SimpSolver.cc
@@ -214,7 +214,7 @@ bool SimpSolver::strengthenClause(CRef cr, Lit l)
         updateElimHeap(var(l));
     }
 
-    return c.size() == 1 ? enqueue(c[0]) && propagate(CHECK_WITHOUTH_PROPAGATION_QUICK) == CRef_Undef : true;
+    return c.size() == 1 ? enqueue(c[0]) && propagate(CHECK_WITHOUTH_THEORY) == CRef_Undef : true;
 }
 
 
@@ -321,7 +321,7 @@ bool SimpSolver::implied(const vec<Lit>& c)
             uncheckedEnqueue(~c[i]);
         }
 
-    bool result = propagate(CHECK_WITHOUTH_PROPAGATION_QUICK) != CRef_Undef;
+    bool result = propagate(CHECK_WITHOUTH_THEORY) != CRef_Undef;
     cancelUntil(0);
     return result;
 }
@@ -410,7 +410,7 @@ bool SimpSolver::asymm(Var v, CRef cr)
         else
             l = c[i];
 
-    if (propagate(CHECK_WITHOUTH_PROPAGATION_QUICK) != CRef_Undef){
+    if (propagate(CHECK_WITHOUTH_THEORY) != CRef_Undef){
         cancelUntil(0);
         asymm_lits++;
         if (!strengthenClause(cr, l))