From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 9 May 2014 21:53:57 +0000 (-0500)
Subject: Initial draft of run scripts for CASC j7
X-Git-Tag: cvc5-1.0.0~6917
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=3dece37c42b37cde370108c0cf405eb0c8274da8;p=cvc5.git

Initial draft of run scripts for CASC j7
---

diff --git a/contrib/run-script-cascj7-fnt b/contrib/run-script-cascj7-fnt
new file mode 100755
index 000000000..11133cd0f
--- /dev/null
+++ b/contrib/run-script-cascj7-fnt
@@ -0,0 +1,32 @@
+#!/bin/bash
+
+cvc4=cvc4
+bench="$1"
+let "to = $2 - 70"
+
+file=${bench##*/}
+filename=${file%.*}
+
+echo "Run $bench at $2"
+
+# 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;
+  echo "--- Run $@ at $limit...";
+  (ulimit -t "$limit";$cvc4 --no-checking --no-interactive --dump-models --produce-models "$@" $bench) 2>/dev/null |
+  (read w1 w2 w3 result w4 w5;
+  case "$result" in
+  Satisfiable) echo "$w1 $w2 $w3 $result $w4 $w5";cat;exit 0;;
+  CounterSatisfiable) echo "$w1 $w2 $w3 $result $w4 $w5";cat;exit 0;;
+  esac; exit 1)
+  if [ ${PIPESTATUS[1]} -eq 0 ]; then exit 0; fi
+}
+
+trywith 30 --finite-model-find 
+trywith 30 --finite-model-find --mbqi=gen-ev --uf-ss-totality --decision=internal
+trywith 10 --finite-model-find --disable-uf-ss-min-model
+trywith $to --finite-model-find --mbqi=abs --pre-skolem-quant
+echo "% SZS status" "GaveUp for $filename"
diff --git a/contrib/run-script-cascj7-fof b/contrib/run-script-cascj7-fof
new file mode 100755
index 000000000..bfaaf722f
--- /dev/null
+++ b/contrib/run-script-cascj7-fof
@@ -0,0 +1,33 @@
+#!/bin/bash
+
+cvc4=cvc4
+bench="$1"
+let "to = $2 - 85"
+
+file=${bench##*/}
+filename=${file%.*}
+
+echo "Run $bench at $2"
+
+# 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;
+  echo "--- Run $@ at $limit...";
+  (ulimit -t "$limit";$cvc4 --no-checking --no-interactive "$@" $bench) 2>/dev/null |
+  (read w1 w2 w3 result w4 w5;
+  case "$result" in
+  Unsatisfiable) echo "$w1 $w2 $w3 $result $w4 $w5";cat;exit 0;;
+  Theorem) echo "$w1 $w2 $w3 $result $w4 $w5";cat;exit 0;;
+  esac; exit 1)
+  if [ ${PIPESTATUS[1]} -eq 0 ]; then exit 0; fi
+}
+
+trywith 30 
+trywith 10 --decision=internal
+trywith 30 --finite-model-find --fmf-inst-engine --mbqi=gen-ev
+trywith 15 --finite-model-find --decision=justification-stoponly
+trywith $to --quant-cf
+echo "% SZS status" "GaveUp for $filename"