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

diff --git a/src/main/main.cpp b/src/main/main.cpp
index df906380814f20c77eac440198d09028f01de219..ecef7e79f9dbf5f29e6bcbc81a25c2f0ad19965d 100644 (file)
--- 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;
     }

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 7ea22ce8f8b41158f2ffd31960567791f7af0501..f8667fb71830d454e8fadb6455e4721b5ba42afd 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -285,17 +285,21 @@ SmtEngine::~SmtEngine() {
 }
 
 void SmtEngine::setLogic(const std::string& s) throw(ModalException) {
+  NodeManagerScope nms(d_nodeManager);
+
   if(d_logic != "") {
     throw ModalException("logic already set");
   }
+
   if(Dump.isOn("benchmark")) {
     Dump("benchmark") << SetBenchmarkLogicCommand(s) << endl;
   }
+
   d_logic = s;
   d_theoryEngine->setLogic(s);
 
   // If in arrays, set the UF handler to arrays
-  if (s == "QF_AX") {
+  if(s == "QF_AX") {
     theory::Theory::setUninterpretedSortOwner(theory::THEORY_ARRAY);
   }
 }

diff --git a/src/util/options.cpp b/src/util/options.cpp
index e5f185d2413b26f3fc52d0cfc48ac5cb08fdd2a9..d33064c73d719eebc0fb46a715bb357c4ee30d6f 100644 (file)
--- 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 32d26c7503ecdd6ae0be5d938f0fbf1111ed52eb..d04947b028ce6e1ee5a1539e83296410fad01267 100644 (file)
--- a/src/util/options.h
+++ b/src/util/options.h
@@ -208,6 +208,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).