From 96240c3cbc2a25e2d9ab14d1048ffda82a83ded2 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Mon, 20 Feb 2012 13:44:50 +0000 Subject: 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/smt/smt_engine.cpp | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) (limited to 'src/smt') 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); } } -- cgit v1.2.3