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.

4 files changed, 77 insertions, 80 deletions

diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index a1d57af66..3760e233d 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -1109,65 +1109,63 @@ Node flattenAnd(Node n){
 }
 
 void TheoryArith::propagate(Effort e) {
-  if(quickCheckOrMore(e)){
-    bool propagated = false;
-    if(Options::current()->arithPropagation && hasAnyUpdates()){
-      propagateCandidates();
-    }else{
-      clearUpdates();
-    }
+  bool propagated = false;
+  if(Options::current()->arithPropagation && hasAnyUpdates()){
+    propagateCandidates();
+  }else{
+    clearUpdates();
+  }
 
-    while(d_propManager.hasMorePropagations()){
-      const PropManager::PropUnit next = d_propManager.getNextPropagation();
-      bool flag = next.flag;
-      TNode toProp = next.consequent;
-
-      TNode atom = (toProp.getKind() == kind::NOT) ? toProp[0] : toProp;
-
-      Debug("arith::propagate") << "propagate  @" << getContext()->getLevel() <<" flag: "<< flag << " " << toProp << endl;
-
-      if(flag) {
-        //Currently if the flag is set this came from an equality detected by the
-        //equality engine in the the difference manager.
-        if(toProp.getKind() == kind::EQUAL){
-          Node normalized = Rewriter::rewrite(toProp);
-          Node notNormalized = normalized.notNode();
-
-          if(d_diseq.find(notNormalized) == d_diseq.end()){
-            d_out->propagate(toProp);
-            propagated = true;
-          }else{
-            Node exp = d_differenceManager.explain(toProp);
-            Node lp = flattenAnd(exp.andNode(notNormalized));
-            Debug("arith::propagate") << "propagate conflict" <<  lp << endl;
-            d_out->conflict(lp);
-
-            propagated = true;
-            break;
-          }
-        }else{
+  while(d_propManager.hasMorePropagations()){
+    const PropManager::PropUnit next = d_propManager.getNextPropagation();
+    bool flag = next.flag;
+    TNode toProp = next.consequent;
+
+    TNode atom = (toProp.getKind() == kind::NOT) ? toProp[0] : toProp;
+
+    Debug("arith::propagate") << "propagate  @" << getContext()->getLevel() <<" flag: "<< flag << " " << toProp << endl;
+
+    if(flag) {
+      //Currently if the flag is set this came from an equality detected by the
+      //equality engine in the the difference manager.
+      if(toProp.getKind() == kind::EQUAL){
+        Node normalized = Rewriter::rewrite(toProp);
+        Node notNormalized = normalized.notNode();
+
+        if(d_diseq.find(notNormalized) == d_diseq.end()){
           d_out->propagate(toProp);
           propagated = true;
+        }else{
+          Node exp = d_differenceManager.explain(toProp);
+          Node lp = flattenAnd(exp.andNode(notNormalized));
+          Debug("arith::propagate") << "propagate conflict" <<  lp << endl;
+          d_out->conflict(lp);
+
+          propagated = true;
+          break;
         }
-      }else if(inContextAtom(atom)){
-        Node satValue = d_valuation.getSatValue(toProp);
-        AlwaysAssert(satValue.isNull());
-        propagated = true;
-        d_out->propagate(toProp);
       }else{
-        //Not clear if this is a good time to do this or not...
-        Debug("arith::propagate") << "Atom is not in context" << toProp << endl;
-#warning "enable remove atom in database"
-        //d_atomDatabase.removeAtom(atom);
+        d_out->propagate(toProp);
+        propagated = true;
       }
+    }else if(inContextAtom(atom)){
+      Node satValue = d_valuation.getSatValue(toProp);
+      AlwaysAssert(satValue.isNull());
+      propagated = true;
+      d_out->propagate(toProp);
+    }else{
+      //Not clear if this is a good time to do this or not...
+      Debug("arith::propagate") << "Atom is not in context" << toProp << endl;
+#warning "enable remove atom in database"
+      //d_atomDatabase.removeAtom(atom);
     }
+  }
 
-    if(!propagated){
-      //Opportunistically export previous conflicts
-      while(d_simplex.hasMoreLemmas()){
-        Node lemma = d_simplex.popLemma();
-        d_out->lemma(lemma);
-      }
+  if(!propagated){
+    //Opportunistically export previous conflicts
+    while(d_simplex.hasMoreLemmas()){
+      Node lemma = d_simplex.popLemma();
+      d_out->lemma(lemma);
     }
   }
 }
@@ -1387,7 +1385,7 @@ void TheoryArith::presolve(){
   }
 
   d_learner.clear();
-  check(FULL_EFFORT);
+  check(EFFORT_FULL);
 }
 
 EqualityStatus TheoryArith::getEqualityStatus(TNode a, TNode b) {
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 174513c72..6e0d45948 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -228,7 +228,7 @@ void TheoryDatatypes::check(Effort e) {
     }
   }
 
-  if( e == FULL_EFFORT ) {
+  if( e == EFFORT_FULL ) {
     Debug("datatypes-split") << "Check for splits " << e << endl;
     //do splitting
     for( EqLists::iterator i = d_labels.begin(); i != d_labels.end(); i++ ) {
diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp
index 76aabeb1f..0404bda3b 100644
--- a/src/theory/theory.cpp
+++ b/src/theory/theory.cpp
@@ -31,14 +31,12 @@ TheoryId Theory::s_uninterpretedSortOwner = THEORY_UF;
 
 std::ostream& operator<<(std::ostream& os, Theory::Effort level){
   switch(level){
-  case Theory::MIN_EFFORT:
-    os << "MIN_EFFORT"; break;
-  case Theory::QUICK_CHECK:
-    os << "QUICK_CHECK"; break;
-  case Theory::STANDARD:
-    os << "STANDARD"; break;
-  case Theory::FULL_EFFORT:
-    os << "FULL_EFFORT"; break;
+  case Theory::EFFORT_STANDARD:
+    os << "EFFORT_STANDARD"; break;
+  case Theory::EFFORT_FULL:
+    os << "EFFORT_FULL"; break;
+  case Theory::EFFORT_COMBINATION:
+    os << "EFFORT_COMBINATION"; break;
   default:
       Unreachable();
   }
diff --git a/src/theory/theory.h b/src/theory/theory.h
index 35c81239f..1451568ab 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -241,7 +241,7 @@ public:
    * Returns the ID of the theory responsible for the given node.
    */
   static inline TheoryId theoryOf(TNode node) {
-    Trace("theory") << "theoryOf(" << node << ")" << std::endl;
+    Trace("theory::internal") << "theoryOf(" << node << ")" << std::endl;
     // Constants, variables, 0-ary constructors
     if (node.getMetaKind() == kind::metakind::VARIABLE || node.getMetaKind() == kind::metakind::CONSTANT) {
       return theoryOf(node.getType());
@@ -298,28 +298,29 @@ public:
    * with FULL_EFFORT.
    */
   enum Effort {
-    MIN_EFFORT = 0,
-    QUICK_CHECK = 10,
-    STANDARD = 50,
-    FULL_EFFORT = 100,
-    COMBINATION = 150
+    /**
+     * Standard effort where theory need not do anything
+     */
+    EFFORT_STANDARD = 50,
+    /**
+     * Full effort requires the theory make sure its assertions are satisfiable or not
+     */
+    EFFORT_FULL = 100,
+    /**
+     * Combination effort means that the individual theories are already satisfied, and
+     * it is time to put some effort into propagation of shared term equalities
+     */
+    EFFORT_COMBINATION = 150
   };/* enum Effort */
 
-  // simple, useful predicates for effort values
-  static inline bool minEffortOnly(Effort e) CVC4_CONST_FUNCTION
-    { return e == MIN_EFFORT; }
-  static inline bool quickCheckOrMore(Effort e) CVC4_CONST_FUNCTION
-    { return e >= QUICK_CHECK; }
-  static inline bool quickCheckOnly(Effort e) CVC4_CONST_FUNCTION
-    { return e >= QUICK_CHECK && e <  STANDARD; }
   static inline bool standardEffortOrMore(Effort e) CVC4_CONST_FUNCTION
-    { return e >= STANDARD; }
+    { return e >= EFFORT_STANDARD; }
   static inline bool standardEffortOnly(Effort e) CVC4_CONST_FUNCTION
-    { return e >= STANDARD && e <  FULL_EFFORT; }
+    { return e >= EFFORT_STANDARD && e <  EFFORT_FULL; }
   static inline bool fullEffort(Effort e) CVC4_CONST_FUNCTION
-    { return e == FULL_EFFORT; }
+    { return e == EFFORT_FULL; }
   static inline bool combination(Effort e) CVC4_CONST_FUNCTION 
-    { return e == COMBINATION; }
+    { return e == EFFORT_COMBINATION; }
 
   /**
    * Get the id for this Theory.
@@ -409,12 +410,12 @@ public:
    * - throw an exception
    * - or call get() until done() is true.
    */
-  virtual void check(Effort level = FULL_EFFORT) { }
+  virtual void check(Effort level = EFFORT_FULL) { }
 
   /**
    * T-propagate new literal assignments in the current context.
    */
-  virtual void propagate(Effort level = FULL_EFFORT) { }
+  virtual void propagate(Effort level = EFFORT_FULL) { }
 
   /**
    * Return an explanation for the literal represented by parameter n