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, 6 insertions, 29 deletions

diff --git a/test/regress/regress0/arith/integers/Makefile.am b/test/regress/regress0/arith/integers/Makefile.am
index ccfeb51f1..d55e12fbc 100644
--- a/test/regress/regress0/arith/integers/Makefile.am
+++ b/test/regress/regress0/arith/integers/Makefile.am
@@ -18,7 +18,6 @@ TESTS =	\
 	arith-int-013.cvc \
 	arith-int-022.cvc \
 	arith-int-024.cvc \
-	arith-int-041.cvc \
 	arith-int-042.cvc \
 	arith-int-042.min.cvc \
 	arith-int-047.cvc \
@@ -66,6 +65,7 @@ EXTRA_DIST = $(TESTS) \
 	arith-int-038.cvc \
 	arith-int-039.cvc \
 	arith-int-040.cvc \
+	arith-int-041.cvc \
 	arith-int-043.cvc \
 	arith-int-044.cvc \
 	arith-int-045.cvc \
diff --git a/test/unit/theory/theory_arith_white.h b/test/unit/theory/theory_arith_white.h
index 4787dfd21..41d370aac 100644
--- a/test/unit/theory/theory_arith_white.h
+++ b/test/unit/theory/theory_arith_white.h
@@ -64,7 +64,7 @@ class TheoryArithWhite : public CxxTest::TestSuite {
 
 public:
 
-  TheoryArithWhite() : d_level(Theory::FULL_EFFORT), d_zero(0), d_one(1), debug(false) {}
+  TheoryArithWhite() : d_level(Theory::EFFORT_FULL), d_zero(0), d_one(1), debug(false) {}
 
   void fakeTheoryEnginePreprocess(TNode inp){
     Node rewrite = inp; //FIXME this needs to enforce that inp is fully rewritten already!
diff --git a/test/unit/theory/theory_black.h b/test/unit/theory/theory_black.h
index 76385219d..a737772ed 100644
--- a/test/unit/theory/theory_black.h
+++ b/test/unit/theory/theory_black.h
@@ -181,38 +181,15 @@ public:
   }
 
   void testEffort(){
-    Theory::Effort m = Theory::MIN_EFFORT;
-    Theory::Effort q = Theory::QUICK_CHECK;
-    Theory::Effort s = Theory::STANDARD;
-    Theory::Effort f = Theory::FULL_EFFORT;
-
-    TS_ASSERT( Theory::minEffortOnly(m));
-    TS_ASSERT(!Theory::minEffortOnly(q));
-    TS_ASSERT(!Theory::minEffortOnly(s));
-    TS_ASSERT(!Theory::minEffortOnly(f));
-
-    TS_ASSERT(!Theory::quickCheckOnly(m));
-    TS_ASSERT( Theory::quickCheckOnly(q));
-    TS_ASSERT(!Theory::quickCheckOnly(s));
-    TS_ASSERT(!Theory::quickCheckOnly(f));
-
-    TS_ASSERT(!Theory::standardEffortOnly(m));
-    TS_ASSERT(!Theory::standardEffortOnly(q));
+    Theory::Effort s = Theory::EFFORT_STANDARD;
+    Theory::Effort f = Theory::EFFORT_FULL;
+
     TS_ASSERT( Theory::standardEffortOnly(s));
     TS_ASSERT(!Theory::standardEffortOnly(f));
 
-    TS_ASSERT(!Theory::fullEffort(m));
-    TS_ASSERT(!Theory::fullEffort(q));
     TS_ASSERT(!Theory::fullEffort(s));
     TS_ASSERT( Theory::fullEffort(f));
 
-    TS_ASSERT(!Theory::quickCheckOrMore(m));
-    TS_ASSERT( Theory::quickCheckOrMore(q));
-    TS_ASSERT( Theory::quickCheckOrMore(s));
-    TS_ASSERT( Theory::quickCheckOrMore(f));
-
-    TS_ASSERT(!Theory::standardEffortOrMore(m));
-    TS_ASSERT(!Theory::standardEffortOrMore(q));
     TS_ASSERT( Theory::standardEffortOrMore(s));
     TS_ASSERT( Theory::standardEffortOrMore(f));
   }
@@ -225,7 +202,7 @@ public:
 
     TS_ASSERT(!d_dummy->doneWrapper());
 
-    d_dummy->check(Theory::FULL_EFFORT);
+    d_dummy->check(Theory::EFFORT_FULL);
 
     TS_ASSERT(d_dummy->doneWrapper());
   }