By default, ONLY enable symmetry breaker ONLY for QF_UF (both SMT-LIBv1
authorMorgan Deters <mdeters@gmail.com>
Mon, 20 Feb 2012 13:44:50 +0000 (13:44 +0000)
committerMorgan Deters <mdeters@gmail.com>
Mon, 20 Feb 2012 13:44:50 +0000 (13:44 +0000)
commit96240c3cbc2a25e2d9ab14d1048ffda82a83ded2
tree609bae884c1a02b396b62ac0cc7e7e7ce4c5d944
parent1632d0cad718fd07e9a987cd14d5fc29a1b450c4
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."
src/main/main.cpp
src/smt/smt_engine.cpp
src/util/options.cpp
src/util/options.h