Add simplification option --fo-prop-quant. Add model support for new model-checking procedure. Add run script for casc24-fnt.

1 files changed, 27 insertions, 0 deletions

diff --git a/contrib/run-script-casc24-fnt b/contrib/run-script-casc24-fnt
new file mode 100755
index 000000000..0230b8e13
--- /dev/null
+++ b/contrib/run-script-casc24-fnt
@@ -0,0 +1,27 @@
+#!/bin/bash
+
+cvc4=cvc4
+bench="$1"
+
+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="$($cvc4 -L tptp --no-checking --no-interactive "$@" $bench)"
+  case "$result" in
+    sat) echo "SZS Satisfiable for $filename"; exit 0;;
+    unsat) echo "SZS Unsatisfiable for $filename"; exit 0;;
+  esac
+}
+
+
+trywith --finite-model-find --uf-ss-totality --tlimit-per=10000
+trywith --finite-model-find --decision=justification --tlimit-per=10000
+trywith --finite-model-find --decision=justification --fmf-fmc
+;;
+
+