Possible final version of run scripts for casc.

diff --git a/contrib/run-script-casc24-fnt b/contrib/run-script-casc24-fnt
index 5376bfd724fc72b97c86c10f46eb43be667da789..2a10c53477c8143de3b26d8191ad7804a680543d 100755 (executable)
--- 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 (executable)
index fce3202..0000000
--- 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 (executable)
index 0000000..a189c10
--- /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 eb8e91310b6467f4d904b9ffed1c7236ee727557..940e26946468a798a2753088eaf44083489eff6b 100755 (executable)
--- 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