diff options
Diffstat (limited to 'src/util/options.cpp')
| -rw-r--r-- | src/util/options.cpp | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/src/util/options.cpp b/src/util/options.cpp index b6956a31b..b6a306ee0 100644 --- a/src/util/options.cpp +++ b/src/util/options.cpp @@ -110,6 +110,7 @@ Options::Options() : ufSymmetryBreaker(false), ufSymmetryBreakerSetByUser(false), dioSolver(true), + arithRewriteEq(true), lemmaOutputChannel(NULL), lemmaInputChannel(NULL), threads(2),// default should be 1 probably, but say 2 for now @@ -183,6 +184,7 @@ Additional CVC4 options:\n\ --enable-symmetry-breaker turns on UF symmetry breaker (Deharbe et al., CADE 2011) [on by default only for QF_UF]\n\ --disable-symmetry-breaker turns off UF symmetry breaker\n\ --disable-dio-solver turns off Linear Diophantine Equation solver (Griggio, JSAT 2012)\n\ + --disable-arith-rewrite-equalities turns off the preprocessing rewrite turning equalities into a conjunction of inequalities.\n \ --threads=N sets the number of solver threads\n\ --threadN=string configures thread N (0..#threads-1)\n\ --filter-lemma-length=N don't share lemmas strictly longer than N\n\ @@ -356,6 +358,7 @@ enum OptionValue { ARITHMETIC_PIVOT_THRESHOLD, ARITHMETIC_PROP_MAX_LENGTH, ARITHMETIC_DIO_SOLVER, + ARITHMETIC_REWRITE_EQUALITIES, ENABLE_SYMMETRY_BREAKER, DISABLE_SYMMETRY_BREAKER, PARALLEL_THREADS, @@ -445,6 +448,7 @@ static struct option cmdlineOptions[] = { { "print-winner", no_argument , NULL, PRINT_WINNER }, { "disable-arithmetic-propagation", no_argument, NULL, ARITHMETIC_PROPAGATION }, { "disable-dio-solver", no_argument, NULL, ARITHMETIC_DIO_SOLVER }, + { "disable-arith-rewrite-equalities", no_argument, NULL, ARITHMETIC_REWRITE_EQUALITIES }, { "enable-symmetry-breaker", no_argument, NULL, ENABLE_SYMMETRY_BREAKER }, { "disable-symmetry-breaker", no_argument, NULL, DISABLE_SYMMETRY_BREAKER }, { "threads", required_argument, NULL, PARALLEL_THREADS }, @@ -796,6 +800,10 @@ throw(OptionException) { dioSolver = false; break; + case ARITHMETIC_REWRITE_EQUALITIES: + arithRewriteEq = false; + break; + case ENABLE_SYMMETRY_BREAKER: ufSymmetryBreaker = true; ufSymmetryBreakerSetByUser = true; |