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."

1 files changed, 8 insertions, 0 deletions

diff --git a/src/main/main.cpp b/src/main/main.cpp
index df9063808..ecef7e79f 100644
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -373,6 +373,14 @@ static bool doCommand(SmtEngine& smt, Command* cmd) {
       status = doCommand(smt, *subcmd) && status;
     }
   } else {
+    // by default, symmetry breaker is on only for QF_UF
+    if(! options.ufSymmetryBreakerSetByUser) {
+      SetBenchmarkLogicCommand *logic = dynamic_cast<SetBenchmarkLogicCommand*>(cmd);
+      if(logic != NULL) {
+        options.ufSymmetryBreaker = (logic->getLogic() == "QF_UF");
+      }
+    }
+
     if(options.verbosity > 0) {
       *options.out << "Invoking: " << *cmd << endl;
     }