Minor updates/fix to --cbqi-recurse

3 files changed, 30 insertions, 13 deletions

diff --git a/contrib/run-script-cascj7-fnt b/contrib/run-script-cascj7-fnt
index 5d51381da..073a9f297 100755
--- a/contrib/run-script-cascj7-fnt
+++ b/contrib/run-script-cascj7-fnt
@@ -2,16 +2,15 @@
 
 cvc4=cvc4
 bench="$1"
-let "to = $2 - 70"
 
 file=${bench##*/}
 filename=${file%.*}
 
-echo "Run $bench at $2"
+echo "------- cvc4-fnt $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
+# to attempt a run.  If an SZS ontology result is printed, then
+# the run script terminates immediately.  Otherwise, this
 # function returns normally.
 function trywith {
   limit=$1; shift;
@@ -24,9 +23,14 @@ function trywith {
   esac; exit 1)
   if [ ${PIPESTATUS[1]} -eq 0 ]; then exit 0; fi
 }
+function finishwith {
+  echo "--- Run $@ at $limit...";
+  $cvc4 --no-checking --no-interactive --dump-models --produce-models "$@" $bench
+}
 
 trywith 30 --finite-model-find --sort-inference --uf-ss-fair
 trywith 30 --finite-model-find --mbqi=gen-ev --uf-ss-totality --decision=internal --sort-inference --uf-ss-fair
 trywith 10 --finite-model-find --disable-uf-ss-min-model --sort-inference --uf-ss-fair
-trywith $to --finite-model-find --mbqi=abs --pre-skolem-quant --sort-inference --uf-ss-fair
+trywith 30 --finite-model-find --mbqi=abs --pre-skolem-quant --sort-inference --uf-ss-fair
+finishwith --finite-model-find --mbqi=abs --pre-skolem-quant --sort-inference --uf-ss-fair --mbqi-one-inst-per-round
 echo "% SZS status" "GaveUp for $filename"
diff --git a/contrib/run-script-cascj7-fof b/contrib/run-script-cascj7-fof
index eb0478e24..582a14952 100755
--- a/contrib/run-script-cascj7-fof
+++ b/contrib/run-script-cascj7-fof
@@ -2,14 +2,15 @@
 
 cvc4=cvc4
 bench="$1"
-let "to = $2 - 85"
 
 file=${bench##*/}
 filename=${file%.*}
 
+echo "------- cvc4-fof $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
+# to attempt a run.  If an SZS ontology result is printed, then
+# the run script terminates immediately.  Otherwise, this
 # function returns normally.
 function trywith {
   limit=$1; shift;
@@ -22,10 +23,16 @@ function trywith {
   esac; exit 1)
   if [ ${PIPESTATUS[1]} -eq 0 ]; then exit 0; fi
 }
+function finishwith {
+  echo "--- Run $@ at $limit...";
+  $cvc4 --no-checking --no-interactive --dump-instantiations "$@" $bench
+}
 
 trywith 30 --full-saturate-quant
-trywith 10 --decision=internal --full-saturate-quant
+trywith 15 --decision=internal --full-saturate-quant
 trywith 30 --finite-model-find --fmf-inst-engine --mbqi=gen-ev
+trywith 30 --relevant-triggers --full-saturate-quant
 trywith 15 --finite-model-find --decision=justification-stoponly
-trywith $to --quant-cf --full-saturate-quant
+trywith 30 --pre-skolem-quant --full-saturate-quant
+finishwith --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
index 893b69572..8033bed1f 100755
--- a/contrib/run-script-cascj7-tff
+++ b/contrib/run-script-cascj7-tff
@@ -2,11 +2,12 @@
 
 cvc4=cvc4
 bench="$1"
-let "to = $2 - 170"
 
 file=${bench##*/}
 filename=${file%.*}
 
+echo "------- cvc4-tff $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
@@ -22,11 +23,16 @@ function trywith {
   esac; exit 1)
   if [ ${PIPESTATUS[1]} -eq 0 ]; then exit 0; fi
 }
+function finishwith {
+  echo "--- Run $@ at $limit...";
+  $cvc4 --no-checking --no-interactive --dump-instantiations "$@" $bench
+}
 
 trywith 15 --cbqi-recurse --full-saturate-quant
 trywith 15 --decision=internal --full-saturate-quant
 trywith 30 --quant-cf --qcf-tconstraint --full-saturate-quant
 trywith 20 --finite-model-find
-trywith 90 --full-saturate-quant
-trywith $to --cbqi-recurse --full-saturate-quant --pre-skolem-quant
+trywith 30 --full-saturate-quant
+trywith 60 --quant-cf --full-saturate-quant
+finishwith --cbqi-recurse --full-saturate-quant --pre-skolem-quant
 echo "% SZS status" "GaveUp for $filename"