From 69693d7c8e5ca84b76fa807cb0797823058caa9a Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Thu, 14 Jun 2012 17:25:22 +0000 Subject: [PATCH] making --simplification=none the default for quantified logics; this a request from andy. evidence of performance improvement: http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=4516&reference_id=4475&p=5 --- src/smt/smt_engine.cpp | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 75d306663..91c43a1de 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -455,11 +455,12 @@ void SmtEngine::setLogicInternal() throw(AssertionException) { Trace("smt") << "setting uf symmetry breaker to " << qf_uf << std::endl; NodeManager::currentNM()->getOptions()->ufSymmetryBreaker = qf_uf; } - // by default, nonclausal simplification is off for QF_SAT + // by default, nonclausal simplification is off for QF_SAT and for quantifiers if(! Options::current()->simplificationModeSetByUser) { bool qf_sat = d_logic.isPure(theory::THEORY_BOOL) && !d_logic.isQuantified(); - Trace("smt") << "setting simplification mode to <" << d_logic.getLogicString() << "> " << (!qf_sat) << std::endl; - NodeManager::currentNM()->getOptions()->simplificationMode = (qf_sat ? Options::SIMPLIFICATION_MODE_NONE : Options::SIMPLIFICATION_MODE_BATCH); + bool quantifiers = d_logic.isQuantified(); + Trace("smt") << "setting simplification mode to <" << d_logic.getLogicString() << "> " << (!qf_sat && !quantifiers) << std::endl; + NodeManager::currentNM()->getOptions()->simplificationMode = (qf_sat || quantifiers ? Options::SIMPLIFICATION_MODE_NONE : Options::SIMPLIFICATION_MODE_BATCH); } // If in arrays, set the UF handler to arrays -- 2.30.2