diff options
| author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-05-08 16:51:54 -0400 |
|---|---|---|
| committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-05-08 16:52:20 -0400 |
| commit | a2c0fd92782ce942a6f25f2561a4918fb2c5b020 (patch) | |
| tree | c976291b6aa9cc76244bb761c3db68cf7856a217 | |
| parent | 3f8927c16764151ed217b509a60e22336a2981de (diff) | |
final updates for smt-eval script
| -rwxr-xr-x | contrib/run-script-smteval2013 | 11 | ||||
| -rw-r--r-- | 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); |