diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-02-20 13:44:50 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-02-20 13:44:50 +0000 |
commit | 96240c3cbc2a25e2d9ab14d1048ffda82a83ded2 (patch) | |
tree | 609bae884c1a02b396b62ac0cc7e7e7ce4c5d944 /src/util | |
parent | 1632d0cad718fd07e9a987cd14d5fc29a1b450c4 (diff) |
By default, ONLY enable symmetry breaker ONLY for QF_UF (both SMT-LIBv1
and SMT-LIBv2).
There are --enable-symmetry-breaker and --disable-symmetry-breaker
options that are always respected regardless of this default.
Expected performance impact: positive
New default (UF only) compared to old default (always on):
http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=3594&reference_id=3595&p=5
Symmetry breaker remains a big win on UF:
http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=3594&reference_id=3596&p=5
The last link to results looks at first that the symmetry breaker should
always be turned off, since its use loses more regressions than it gains.
*However*, the lost ones are only our "QF_SAT" benchmarks. For these, we
should indeed turn off the symmetry breaker, but that's impossible for
now because we tag them internally with the logic "QF_UF."
Diffstat (limited to 'src/util')
-rw-r--r-- | src/util/options.cpp | 13 | ||||
-rw-r--r-- | src/util/options.h | 6 |
2 files changed, 17 insertions, 2 deletions
diff --git a/src/util/options.cpp b/src/util/options.cpp index e5f185d24..d33064c73 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(false), + ufSymmetryBreakerSetByUser(false), dioSolver(true) { } @@ -158,7 +159,8 @@ Additional CVC4 options:\n\ --random-seed=S sets the random seed for the sat solver\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\ + --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\ "; @@ -327,6 +329,7 @@ enum OptionValue { ARITHMETIC_PIVOT_THRESHOLD, ARITHMETIC_PROP_MAX_LENGTH, ARITHMETIC_DIO_SOLVER, + ENABLE_SYMMETRY_BREAKER, DISABLE_SYMMETRY_BREAKER, TIME_LIMIT, TIME_LIMIT_PER, @@ -409,6 +412,7 @@ static struct option cmdlineOptions[] = { { "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 }, + { "enable-symmetry-breaker", no_argument, NULL, ENABLE_SYMMETRY_BREAKER }, { "disable-symmetry-breaker", no_argument, NULL, DISABLE_SYMMETRY_BREAKER }, { "tlimit" , required_argument, NULL, TIME_LIMIT }, { "tlimit-per" , required_argument, NULL, TIME_LIMIT_PER }, @@ -746,8 +750,13 @@ throw(OptionException) { dioSolver = false; break; + case ENABLE_SYMMETRY_BREAKER: + ufSymmetryBreaker = true; + ufSymmetryBreakerSetByUser = true; + break; case DISABLE_SYMMETRY_BREAKER: ufSymmetryBreaker = false; + ufSymmetryBreakerSetByUser = true; break; case TIME_LIMIT: diff --git a/src/util/options.h b/src/util/options.h index 32d26c750..d04947b02 100644 --- a/src/util/options.h +++ b/src/util/options.h @@ -209,6 +209,12 @@ struct CVC4_PUBLIC Options { bool ufSymmetryBreaker; /** + * Whether the user explicitly requested that the symmetry + * breaker be enabled or disabled. + */ + bool ufSymmetryBreakerSetByUser; + + /** * Whether to do the linear diophantine equation solver * in Arith as described by Griggio JSAT 2012 (on by default). */ |