diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2013-05-14 16:42:23 -0500 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2013-05-14 16:42:36 -0500 |
commit | b48a369333f077fa7cce117976f760cd6332691a (patch) | |
tree | acd6e9e9068deca14b8380b50bf7bbc5464fa105 /contrib/run-script-casc24-fof | |
parent | 99d5e608b1e1a7541406e86d16b8e3bf6e7e8f0a (diff) |
Update casc24-fnt run script. Add casc24-fof run script.
Diffstat (limited to 'contrib/run-script-casc24-fof')
-rwxr-xr-x | contrib/run-script-casc24-fof | 37 |
1 files changed, 37 insertions, 0 deletions
diff --git a/contrib/run-script-casc24-fof b/contrib/run-script-casc24-fof new file mode 100755 index 000000000..eb8e91310 --- /dev/null +++ b/contrib/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 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 +trywith 15 --finite-model-find --fmf-inst-engine +trywith 30 --finite-model-find --decision=justification --fmf-fmc +trywith $to --decision=justification +echo "SZS GaveUp for $filename"
\ No newline at end of file |