diff options
Diffstat (limited to 'contrib/competitions/smt-comp/run-script-smtcomp2020-incremental')
-rw-r--r-- | contrib/competitions/smt-comp/run-script-smtcomp2020-incremental | 75 |
1 files changed, 75 insertions, 0 deletions
diff --git a/contrib/competitions/smt-comp/run-script-smtcomp2020-incremental b/contrib/competitions/smt-comp/run-script-smtcomp2020-incremental new file mode 100644 index 000000000..7861a4c85 --- /dev/null +++ b/contrib/competitions/smt-comp/run-script-smtcomp2020-incremental @@ -0,0 +1,75 @@ +#!/bin/bash + +cvc4=./cvc4 + +line="" +while [[ -z "$line" ]]; do + read line +done +if [ "$line" != '(set-option :print-success true)' ]; then + echo 'ERROR: first line supposed to be set-option :print-success, but got: "'"$line"'"' >&2 + exit 1 +fi +echo success +line="" +while [[ -z "$line" ]]; do + read line +done +logic=$(expr "$line" : ' *(set-logic *\([A-Z_]*\) *) *$') +if [ -z "$logic" ]; then + echo 'ERROR: second line supposed to be set-logic, but got: "'"$line"'"' >&2 + exit 1 +fi +echo success + +function runcvc4 { + # we run in this way for line-buffered input, otherwise memory's a + # concern (plus it mimics what we'll end up getting from an + # application-track trace runner?) + $cvc4 --force-logic="$logic" -L smt2.6 --print-success --no-type-checking --no-interactive "$@" <&0- +} + +case "$logic" in + +ALIA|ANIA|AUFNIRA|LIA|LRA|QF_ALIA|QF_ANIA|QF_AUFBVLIA|QF_AUFBVNIA|QF_LIA|QF_LRA|QF_NIA|QF_UFBVLIA|QF_UFLIA|QF_UFLRA|QF_UFNIA|UFLRA) + runcvc4 --tear-down-incremental=1 + ;; +QF_AUFLIA) + runcvc4 --tear-down-incremental=1 --no-arrays-eager-index --arrays-eager-lemmas + ;; +QF_BV) + runcvc4 --incremental --bitblast=eager --bv-sat-solver=cadical + ;; +QF_UFBV) + runcvc4 --incremental + ;; +QF_UF) + runcvc4 --incremental + ;; +QF_AUFBV) + runcvc4 --incremental + ;; +QF_ABV) + runcvc4 --incremental + ;; +ABVFP) + runcvc4 --incremental + ;; +BVFP) + runcvc4 --incremental + ;; +QF_ABVFP) + runcvc4 --incremental + ;; +QF_BVFP) + runcvc4 --incremental + ;; +QF_FP) + runcvc4 --incremental + ;; +*) + # just run the default + runcvc4 --incremental + ;; + +esac |