From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Mon, 20 May 2013 16:06:02 +0000 (-0500)
Subject: Possible final version of run scripts for casc.
X-Git-Tag: cvc5-1.0.0~7287^2~113^2~1
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=dcda4b10c3dd0dbbfd41203d4bbdaca6990ef0a8;p=cvc5.git

Possible final version of run scripts for casc.
---

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