diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2013-05-10 15:18:20 -0500 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2013-05-10 15:18:20 -0500 |
commit | 38216791c43f9be4afecbc700548d1dbba63acb0 (patch) | |
tree | 60f7b525ca01980f954350f2312563eb57d30679 /contrib/run-script-casc24-fnt | |
parent | f84120cd5311450de2075a91356524d4e20d457c (diff) |
Update casc run script. Work on compliance for SZS output.
Diffstat (limited to 'contrib/run-script-casc24-fnt')
-rwxr-xr-x | contrib/run-script-casc24-fnt | 24 |
1 files changed, 16 insertions, 8 deletions
diff --git a/contrib/run-script-casc24-fnt b/contrib/run-script-casc24-fnt index 0230b8e13..ef3cd4b65 100755 --- a/contrib/run-script-casc24-fnt +++ b/contrib/run-script-casc24-fnt @@ -11,17 +11,25 @@ filename=${file%.*} # which case this run script terminates immediately. Otherwise, this # function returns normally. function trywith { - result="$($cvc4 -L tptp --no-checking --no-interactive "$@" $bench)" + 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 --finite-model-find --uf-ss-totality --tlimit-per=10000 -trywith --finite-model-find --decision=justification --tlimit-per=10000 -trywith --finite-model-find --decision=justification --fmf-fmc -;; - - +trywith 15 --finite-model-find --uf-ss-totality +trywith 15 --finite-model-find --decision=justification --fmf-fmc +finishwith --finite-model-find --decision=justification +echo "SZS GaveUp for $filename"
\ No newline at end of file |