From: Morgan Deters <mdeters@gmail.com>
Date: Mon, 20 Feb 2012 13:44:50 +0000 (+0000)
Subject: By default, ONLY enable symmetry breaker ONLY for QF_UF (both SMT-LIBv1
X-Git-Tag: cvc5-1.0.0~8326
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=96240c3cbc2a25e2d9ab14d1048ffda82a83ded2;p=cvc5.git

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 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;
     }
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 7ea22ce8f..f8667fb71 100644
--- 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 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:
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
@@ -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).