From 38216791c43f9be4afecbc700548d1dbba63acb0 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 10 May 2013 15:18:20 -0500 Subject: Update casc run script. Work on compliance for SZS output. --- contrib/run-script-casc24-fnt | 24 ++++++++++++++++-------- 1 file changed, 16 insertions(+), 8 deletions(-) (limited to 'contrib/run-script-casc24-fnt') 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 -- cgit v1.2.3