From dcda4b10c3dd0dbbfd41203d4bbdaca6990ef0a8 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 20 May 2013 11:06:02 -0500 Subject: [PATCH] Possible final version of run scripts for casc. --- contrib/run-script-casc24-fnt | 34 +++++++++++----------- contrib/run-script-casc24-fnt-models | 38 ------------------------- contrib/run-script-casc24-fnt-no-models | 36 +++++++++++++++++++++++ contrib/run-script-casc24-fof | 18 ++++++------ 4 files changed, 63 insertions(+), 63 deletions(-) delete mode 100755 contrib/run-script-casc24-fnt-models create mode 100755 contrib/run-script-casc24-fnt-no-models diff --git a/contrib/run-script-casc24-fnt b/contrib/run-script-casc24-fnt index 5376bfd72..2a10c5347 100755 --- a/contrib/run-script-casc24-fnt +++ b/contrib/run-script-casc24-fnt @@ -12,25 +12,27 @@ filename=${file%.*} # 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)" + limit=$1; shift; + (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"; 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 + sat) echo "% SZS Satisfiable for $filename"; + echo "% SZS output start FiniteModel for $filename"; + cat; + 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"; + cat; + echo "% SZS output end FiniteModel for $filename"; + exit 0;; + conjecture-unsat) echo "% SZS Theorem for $filename"; exit 0;; + esac; exit 1) + if [ ${PIPESTATUS[1]} -eq 0 ]; then exit 0; fi } 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 GaveUp for $filename" \ No newline at end of file diff --git a/contrib/run-script-casc24-fnt-models b/contrib/run-script-casc24-fnt-models deleted file mode 100755 index fce320201..000000000 --- a/contrib/run-script-casc24-fnt-models +++ /dev/null @@ -1,38 +0,0 @@ -#!/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 { - limit=$1; shift; - (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"; - cat; - 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"; - cat; - echo "SZS output end FiniteModel for $filename"; - exit 0;; - conjecture-unsat) echo "SZS Theorem for $filename"; exit 0;; - esac; exit 1) - if [ ${PIPESTATUS[1]} -eq 0 ]; then exit 0; fi -} - -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 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 diff --git a/contrib/run-script-casc24-fof b/contrib/run-script-casc24-fof index eb8e91310..940e26946 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 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;; + 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 } @@ -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 GaveUp for $filename" \ No newline at end of file -- 2.30.2