summaryrefslogtreecommitdiff
path: root/src/util/options.cpp
diff options
context:
space:
mode:
authorMorgan Deters <mdeters@gmail.com>2012-02-20 13:44:50 +0000
committerMorgan Deters <mdeters@gmail.com>2012-02-20 13:44:50 +0000
commit96240c3cbc2a25e2d9ab14d1048ffda82a83ded2 (patch)
tree609bae884c1a02b396b62ac0cc7e7e7ce4c5d944 /src/util/options.cpp
parent1632d0cad718fd07e9a987cd14d5fc29a1b450c4 (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/options.cpp')
-rw-r--r--src/util/options.cpp13
1 files changed, 11 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:
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback