From a2c0fd92782ce942a6f25f2561a4918fb2c5b020 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Wed, 8 May 2013 16:51:54 -0400 Subject: [PATCH] final updates for smt-eval script --- contrib/run-script-smteval2013 | 11 +++++++---- src/smt/smt_engine.cpp | 5 ++--- 2 files changed, 9 insertions(+), 7 deletions(-) diff --git a/contrib/run-script-smteval2013 b/contrib/run-script-smteval2013 index fbdf4e039..2212f71c7 100755 --- a/contrib/run-script-smteval2013 +++ b/contrib/run-script-smteval2013 @@ -27,13 +27,16 @@ case "$logic" in QF_LRA) finishwith --no-restrict-pivots --enable-miplib-trick --miplib-trick-subs=2 --fc-penalties --collect-pivot-stats --use-soi --new-prop --dio-decomps --unconstrained-simp --fancy-final ;; -AUFLIA) +AUFLIA|AUFLIRA|AUFNIRA|UFLRA|UFNIA) # 60 seconds with default decision heuristic - trywith --tlimit-per=60000 + trywith --simplification=none --tlimit-per=60000 # try simplification for 60 seconds, default decision heuristic - trywith --simplification=batch --tlimit-per=60000 + trywith --tlimit-per=60000 # switch to internal decision heuristic - finishwith --decision=internal + finishwith --simplification=none --decision=internal + ;; +LRA) + finishwith --enable-cbqi ;; QF_AUFBV) trywith --tlimit-per=600000 diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 75cffefc2..0bfc6e634 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -848,11 +848,10 @@ void SmtEngine::setLogicInternal() throw() { Trace("smt") << "setting uf symmetry breaker to " << qf_uf << endl; options::ufSymmetryBreaker.set(qf_uf); } - // by default, nonclausal simplification is off for QF_SAT and for quantifiers + // by default, nonclausal simplification is off for QF_SAT if(! options::simplificationMode.wasSetByUser()) { bool qf_sat = d_logic.isPure(THEORY_BOOL) && !d_logic.isQuantified(); - bool quantifiers = d_logic.isQuantified(); - Trace("smt") << "setting simplification mode to <" << d_logic.getLogicString() << "> " << (!qf_sat && !quantifiers) << endl; + Trace("smt") << "setting simplification mode to <" << d_logic.getLogicString() << "> " << (!qf_sat) << endl; //simplification=none works better for SMT LIB benchmarks with quantifiers, not others //options::simplificationMode.set(qf_sat || quantifiers ? SIMPLIFICATION_MODE_NONE : SIMPLIFICATION_MODE_BATCH); options::simplificationMode.set(qf_sat ? SIMPLIFICATION_MODE_NONE : SIMPLIFICATION_MODE_BATCH); -- 2.30.2