From 4e32479206a1f890b5db7c814ded91fdcb770c65 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Mon, 3 Jun 2013 18:02:33 -0400 Subject: Updated CASC scripts, as provided to Geoff Sutcliffe --- contrib/run-script-casc24-fnt | 18 +++++++++--------- contrib/run-script-casc24-fnt-no-models | 18 +++++++++--------- contrib/run-script-casc24-fof | 18 +++++++++--------- 3 files changed, 27 insertions(+), 27 deletions(-) (limited to 'contrib') diff --git a/contrib/run-script-casc24-fnt b/contrib/run-script-casc24-fnt index 2a10c5347..b10d7324a 100755 --- a/contrib/run-script-casc24-fnt +++ b/contrib/run-script-casc24-fnt @@ -16,18 +16,18 @@ function trywith { (ulimit -t "$limit";$cvc4 -L tptp --szs-compliant --no-checking --no-interactive --dump-models --produce-models "$@" $bench) 2>/dev/null | (read result; case "$result" in - sat) echo "% SZS Satisfiable for $filename"; - echo "% SZS output start FiniteModel for $filename"; + sat) echo "% SZS status" "Satisfiable for $filename"; + echo "% SZS output" "start FiniteModel for $filename"; cat; - echo "% SZS output end FiniteModel for $filename"; + echo "% SZS output" "end FiniteModel for $filename"; exit 0;; - unsat) echo "% SZS Unsatisfiable for $filename"; exit 0;; - conjecture-sat) echo "% SZS CounterSatisfiable for $filename"; - echo "% SZS output start FiniteModel for $filename"; + unsat) echo "% SZS status" "Unsatisfiable for $filename"; exit 0;; + conjecture-sat) echo "% SZS status" "CounterSatisfiable for $filename"; + echo "% SZS output" "start FiniteModel for $filename"; cat; - echo "% SZS output end FiniteModel for $filename"; + echo "% SZS output" "end FiniteModel for $filename"; exit 0;; - conjecture-unsat) echo "% SZS Theorem for $filename"; exit 0;; + conjecture-unsat) echo "% SZS status" "Theorem for $filename"; exit 0;; esac; exit 1) if [ ${PIPESTATUS[1]} -eq 0 ]; then exit 0; fi } @@ -35,4 +35,4 @@ function trywith { 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 +echo "% SZS status" "GaveUp for $filename" diff --git a/contrib/run-script-casc24-fnt-no-models b/contrib/run-script-casc24-fnt-no-models index a189c10bd..3b4d5e320 100755 --- a/contrib/run-script-casc24-fnt-no-models +++ b/contrib/run-script-casc24-fnt-no-models @@ -14,23 +14,23 @@ filename=${file%.*} 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;; + 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 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;; + 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 --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 +echo "% SZS status" "GaveUp for $filename" diff --git a/contrib/run-script-casc24-fof b/contrib/run-script-casc24-fof index 940e26946..b3ede0dfa 100755 --- a/contrib/run-script-casc24-fof +++ b/contrib/run-script-casc24-fof @@ -14,19 +14,19 @@ filename=${file%.*} 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;; + 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 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;; + 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 } @@ -34,4 +34,4 @@ 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 +echo "% SZS status" "GaveUp for $filename" -- cgit v1.2.3