Last commit accidentally lacked r2778 and r2779 from integer2. I have manually brought these changes over. Changed the tests used by test/regress/regress0/arith/integers/Makefile.am to be 15 of the more interesting tests. Did a bit of cleanup on TheoryArith to eliminate a warning and remove dead code.

1 files changed, 9 insertions, 1 deletions

diff --git a/src/util/options.cpp b/src/util/options.cpp
index 842bd84b2..e5f185d24 100644
--- a/src/util/options.cpp
+++ b/src/util/options.cpp
@@ -96,7 +96,8 @@ Options::Options() :
   pivotRule(MINIMUM),
   arithPivotThreshold(16),
   arithPropagateMaxLength(16),
-  ufSymmetryBreaker(true)
+  ufSymmetryBreaker(true),
+  dioSolver(true)
 {
 }
 
@@ -158,6 +159,7 @@ Additional CVC4 options:\n\
    --disable-variable-removal enable permanent removal of variables in arithmetic (UNSAFE! experts only)\n\
    --disable-arithmetic-propagation turns on arithmetic propagation\n\
    --disable-symmetry-breaker turns off UF symmetry breaker (Deharbe et al., CADE 2011)\n\
+   --disable-dio-solver   turns off Linear Diophantine Equation solver (Griggio, JSAT 2012)\n\
 ";
 
 #warning "Change CL options as --disable-variable-removal cannot do anything currently."
@@ -324,6 +326,7 @@ enum OptionValue {
   ARITHMETIC_PROPAGATION,
   ARITHMETIC_PIVOT_THRESHOLD,
   ARITHMETIC_PROP_MAX_LENGTH,
+  ARITHMETIC_DIO_SOLVER,
   DISABLE_SYMMETRY_BREAKER,
   TIME_LIMIT,
   TIME_LIMIT_PER,
@@ -405,6 +408,7 @@ static struct option cmdlineOptions[] = {
   { "random-seed" , required_argument, NULL, RANDOM_SEED  },
   { "disable-variable-removal", no_argument, NULL, ARITHMETIC_VARIABLE_REMOVAL },
   { "disable-arithmetic-propagation", no_argument, NULL, ARITHMETIC_PROPAGATION },
+  { "disable-dio-solver", no_argument, NULL, ARITHMETIC_DIO_SOLVER },
   { "disable-symmetry-breaker", no_argument, NULL, DISABLE_SYMMETRY_BREAKER },
   { "tlimit"     , required_argument, NULL, TIME_LIMIT  },
   { "tlimit-per" , required_argument, NULL, TIME_LIMIT_PER },
@@ -738,6 +742,10 @@ throw(OptionException) {
       arithPropagation = false;
       break;
 
+    case ARITHMETIC_DIO_SOLVER:
+      dioSolver = false;
+      break;
+
     case DISABLE_SYMMETRY_BREAKER:
       ufSymmetryBreaker = false;
       break;