diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2013-05-20 11:06:02 -0500 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2013-05-20 11:06:02 -0500 |
commit | dcda4b10c3dd0dbbfd41203d4bbdaca6990ef0a8 (patch) | |
tree | 6b78991522b86b78b4baa051b749c84e6d9ad139 /contrib/run-script-casc24-fnt-no-models | |
parent | 6c407fa61d5a6ceaa3adef39d88e186823b28dbc (diff) |
Possible final version of run scripts for casc.
Diffstat (limited to 'contrib/run-script-casc24-fnt-no-models')
-rwxr-xr-x | contrib/run-script-casc24-fnt-no-models | 36 |
1 files changed, 36 insertions, 0 deletions
diff --git a/contrib/run-script-casc24-fnt-no-models b/contrib/run-script-casc24-fnt-no-models new file mode 100755 index 000000000..a189c10bd --- /dev/null +++ b/contrib/run-script-casc24-fnt-no-models @@ -0,0 +1,36 @@ +#!/bin/bash + +cvc4=./cvc4 +bench="$1" +let "to = $2 - 60" + +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 Satisfiable for $filename"; exit 0;; + unsat) echo "% SZS Unsatisfiable for $filename"; exit 0;; + conjecture-sat) echo "% SZS CounterSatisfiable for $filename"; exit 0;; + conjecture-unsat) echo "% SZS 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 Satisfiable for $filename"; exit 0;; + unsat) echo "% SZS Unsatisfiable for $filename"; exit 0;; + conjecture-sat) echo "% SZS CounterSatisfiable for $filename"; exit 0;; + conjecture-unsat) echo "% SZS Theorem for $filename"; exit 0;; + esac +} + +trywith 30 --finite-model-find --uf-ss-totality +trywith 30 --finite-model-find --decision=justification --fmf-fmc +trywith $to --finite-model-find --decision=justification +echo "% SZS GaveUp for $filename"
\ No newline at end of file |