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/options.h | |
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/options.h')
-rw-r--r-- | src/util/options.h | 6 |
1 files changed, 6 insertions, 0 deletions
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). */ |