Add model-producing run script for casc.

1 files changed, 38 insertions, 0 deletions

diff --git a/contrib/run-script-casc24-fnt-models b/contrib/run-script-casc24-fnt-models
new file mode 100755
index 000000000..fce320201
--- /dev/null
+++ b/contrib/run-script-casc24-fnt-models
@@ -0,0 +1,38 @@
+#!/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