diff options
| author | Morgan Deters <mdeters@gmail.com> | 2012-06-14 17:25:22 +0000 |
|---|---|---|
| committer | Morgan Deters <mdeters@gmail.com> | 2012-06-14 17:25:22 +0000 |
| commit | 69693d7c8e5ca84b76fa807cb0797823058caa9a (patch) | |
| tree | f6d21d86d8e5df93519b5a2f45d56d897bded6ef /src/smt | |
| parent | da66d47ddff4315db54bbcd3b8f46cf1040d5fd0 (diff) | |
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
Diffstat (limited to 'src/smt')
| -rw-r--r-- | src/smt/smt_engine.cpp | 7 |
1 files 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 |