From: Morgan Deters <mdeters@gmail.com>
Date: Thu, 14 Jun 2012 17:25:22 +0000 (+0000)
Subject: making --simplification=none the default for quantified logics; this a request from... 
X-Git-Tag: cvc5-1.0.0~8016
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=69693d7c8e5ca84b76fa807cb0797823058caa9a;p=cvc5.git

making --simplification=none the default for quantified logics; this a request from andy.  evidence of performance improvement: church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=4516&reference_id=4475&p=5
---

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