diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2017-10-03 00:55:35 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2017-10-03 00:55:35 -0700 |
commit | df058b7fb79abaa4e6488449f2307ee29f47efdd (patch) | |
tree | 3ad8f6161cba83e78e5ac0f78ca53002762341dc /contrib/run-script-smtcomp2018-unsat-cores | |
parent | d0faa2b676130119c5d01e00851427fa97f44464 (diff) |
Add initial version of the SMTCOMP2018 run scripts (#1185)
This commit is a preparation step for removing the --thread-stack
option (and, ultimately, the dependency on Boost). It just copies the
2017 version of the scripts and changes the --fs-inst flag to
--fs-interleave, following the renaming in commit
7766f0ba088ad6d6c58ea9678477b255c9e52fee.
Diffstat (limited to 'contrib/run-script-smtcomp2018-unsat-cores')
-rw-r--r-- | contrib/run-script-smtcomp2018-unsat-cores | 74 |
1 files changed, 74 insertions, 0 deletions
diff --git a/contrib/run-script-smtcomp2018-unsat-cores b/contrib/run-script-smtcomp2018-unsat-cores new file mode 100644 index 000000000..f42f3ca30 --- /dev/null +++ b/contrib/run-script-smtcomp2018-unsat-cores @@ -0,0 +1,74 @@ +#!/bin/bash + +cvc4=./cvc4 +bench="$1" + +logic=$(expr "$(grep -m1 '^[^;]*set-logic' "$bench")" : ' *(set-logic *\([A-Z_]*\) *) *$') + +# use: finishwith [params..] +# to run cvc4 and let it output whatever it will to stdout. +function finishwith { + $cvc4 -L smt2.6 --no-incremental --no-checking --no-interactive "$@" $bench +} + +case "$logic" in + +QF_LRA) + finishwith --no-restrict-pivots --use-soi --new-prop --unconstrained-simp + ;; +QF_LIA) + finishwith --enable-miplib-trick --miplib-trick-subs=4 --use-approx --lemmas-on-replay-failure --replay-early-close-depth=4 --replay-lemma-reject-cut=128 --replay-reject-cut=512 --unconstrained-simp --use-soi + ;; +QF_NIA) + finishwith --solve-int-as-bv=32 --bitblast=eager --bv-sat-solver=cryptominisat + ;; +QF_NRA) + finishwith --nl-ext --nl-ext-tplanes + ;; +# all logics with UF + quantifiers should either fall under this or special cases below +ALIA|AUFLIA|AUFLIRA|AUFNIRA|UF|UFIDL|UFLIA|UFLRA|UFNIA|UFDT|UFDTLIA|AUFDTLIA|AUFBVDTLIA) + finishwith --full-saturate-quant + ;; +UFBV) + finishwith --finite-model-find + ;; +BV) + finishwith --full-saturate-quant --cbqi --decision=internal + ;; +LIA|LRA) + finishwith --full-saturate-quant --cbqi --cbqi-nested-qe --decision=internal + ;; +NIA|NRA) + finishwith --full-saturate-quant --cbqi --cbqi-nested-qe --decision=internal + ;; +QF_AUFBV) + finishwith --decision=justification-stoponly + ;; +QF_ABV) + finishwith --ite-simp --simp-with-care --arrays-weak-equiv + ;; +QF_UFBV) + finishwith --bitblast=eager --bv-sat-solver=cryptominisat + ;; +QF_BV) + finishwith --bv-div-zero-const --bv-eq-slicer=auto --no-bv-abstraction + ;; +QF_AUFLIA) + finishwith --no-arrays-eager-index --arrays-eager-lemmas --decision=justification + ;; +QF_AX) + finishwith --no-arrays-eager-index --arrays-eager-lemmas --decision=internal + ;; +QF_AUFNIA) + finishwith --decision=justification --no-arrays-eager-index --arrays-eager-lemmas + ;; +QF_ALIA) + finishwith --decision=justification-stoponly --no-arrays-eager-index --arrays-eager-lemmas + ;; +*) + # just run the default + finishwith + ;; + +esac + |