diff options
| -rw-r--r-- | src/main/main.cpp | 8 | ||||
| -rw-r--r-- | src/smt/smt_engine.cpp | 6 | ||||
| -rw-r--r-- | src/util/options.cpp | 13 | ||||
| -rw-r--r-- | src/util/options.h | 6 |
4 files changed, 30 insertions, 3 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; } 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 @@ -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). */ |