Bug fixes to CBQI. Add first draft of CASC j7 TFF script. Add regression, minor changes.

2 files changed, 32 insertions, 3 deletions

diff --git a/contrib/run-script-cascj7-fof b/contrib/run-script-cascj7-fof
index bfaaf722f..151413ac2 100755
--- a/contrib/run-script-cascj7-fof
+++ b/contrib/run-script-cascj7-fof
@@ -25,9 +25,9 @@ function trywith {
   if [ ${PIPESTATUS[1]} -eq 0 ]; then exit 0; fi
 }
 
-trywith 30 
-trywith 10 --decision=internal
+trywith 30 --full-saturate-quant
+trywith 10 --decision=internal --full-saturate-quant
 trywith 30 --finite-model-find --fmf-inst-engine --mbqi=gen-ev
 trywith 15 --finite-model-find --decision=justification-stoponly
-trywith $to --quant-cf
+trywith $to --quant-cf --full-saturate-quant
 echo "% SZS status" "GaveUp for $filename"
diff --git a/contrib/run-script-cascj7-tff b/contrib/run-script-cascj7-tff
new file mode 100755
index 000000000..445f7b08a
--- /dev/null
+++ b/contrib/run-script-cascj7-tff
@@ -0,0 +1,29 @@
+#!/bin/bash
+
+cvc4=./cvc4
+bench="$1"
+let "to = $2 - 150"
+
+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;
+  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
+  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 --full-saturate-quant
+trywith 120 --quant-cf --qcf-tconstraint --full-saturate-quant
+trywith $to --cbqi --cbqi-recurse --full-saturate-quant --flip-decision
+echo "% SZS status" "GaveUp for $filename"