diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-08-08 15:16:41 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-08-08 15:16:41 -0500 |
commit | a56575f413499d256e81f6ca1a64ffe1413ed3c7 (patch) | |
tree | 03ea560fb5b45eb0877e1df4bdfe410ea9de79dd /contrib/competitions/casc/run-script-casc24-fof | |
parent | 63a6e17196d849ad6e57bce7490eafb5b7f7f3ec (diff) |
Add subdirectories to contrib for competition scripts (#3164)
Diffstat (limited to 'contrib/competitions/casc/run-script-casc24-fof')
-rwxr-xr-x | contrib/competitions/casc/run-script-casc24-fof | 37 |
1 files changed, 37 insertions, 0 deletions
diff --git a/contrib/competitions/casc/run-script-casc24-fof b/contrib/competitions/casc/run-script-casc24-fof new file mode 100755 index 000000000..b3ede0dfa --- /dev/null +++ b/contrib/competitions/casc/run-script-casc24-fof @@ -0,0 +1,37 @@ +#!/bin/bash + +cvc4=./cvc4 +bench="$1" +let "to = $2 - 75" + +file=${bench##*/} +filename=${file%.*} + +# use: trywith [params..] +# to attempt a run. Only thing printed on stdout is "sat" or "unsat", in +# which case this run script terminates immediately. Otherwise, this +# function returns normally. +function trywith { + result="$( ulimit -t "$1";shift;$cvc4 -L tptp --szs-compliant --no-checking --no-interactive "$@" $bench)" + case "$result" in + sat) echo "% SZS status" "Satisfiable for $filename"; exit 0;; + unsat) echo "% SZS status" "Unsatisfiable for $filename"; exit 0;; + conjecture-sat) echo "% SZS status" "CounterSatisfiable for $filename"; exit 0;; + conjecture-unsat) echo "% SZS status" "Theorem for $filename"; exit 0;; + esac +} +function finishwith { + result="$( $cvc4 -L tptp --szs-compliant --no-checking --no-interactive "$@" $bench)" + case "$result" in + sat) echo "% SZS status" "Satisfiable for $filename"; exit 0;; + unsat) echo "% SZS status" "Unsatisfiable for $filename"; exit 0;; + conjecture-sat) echo "% SZS status" "CounterSatisfiable for $filename"; exit 0;; + conjecture-unsat) echo "% SZS status" "Theorem for $filename"; exit 0;; + esac +} + +trywith 30 +trywith 15 --finite-model-find --fmf-inst-engine +trywith 30 --finite-model-find --decision=justification --fmf-fmc +trywith $to --decision=justification +echo "% SZS status" "GaveUp for $filename" |