Update run scripts for SMT-COMP 2020 (#4454)

This commit adds additional options for the model validation track and
makes sure that non-"sat"/"unsat" outputs from the sequential porfolio
approaches are written to a file instead of stderr when running on
StarExec.

diff --git a/contrib/competitions/smt-comp/run-script-smtcomp-current b/contrib/competitions/smt-comp/run-script-smtcomp-current
index 506eb56b731da68dcd284c5b9f0b2ff34f92e6fb..bdc94b0bcedb0265c38ea45b5dd0cb7bc6c39e26 100755 (executable)
--- a/contrib/competitions/smt-comp/run-script-smtcomp-current
+++ b/contrib/competitions/smt-comp/run-script-smtcomp-current
@@ -3,25 +3,38 @@
 cvc4=./cvc4
 bench="$1"
 
+# Output other than "sat"/"unsat" is either written to stderr or to "err.log"
+# in the directory specified by $2 if it has been set (e.g. when running on
+# StarExec).
+out_file=/dev/stderr
+if [ -n "$2" ]; then
+  out_file="$2/err.log"
+fi
+
 logic=$(expr "$(grep -m1 '^[^;]*set-logic' "$bench")" : ' *(set-logic  *\([A-Z_]*\) *) *$')
 
 # 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 and prints the output of the solver to stderr.
+# returns normally and prints the output of the solver to $out_file.
 function trywith {
   limit=$1; shift;
-  result="$(ulimit -S -t "$limit";$cvc4 -L smt2.6 --no-incremental --no-type-checking --no-interactive "$@" $bench)"
+  result="$({ ulimit -S -t "$limit"; $cvc4 -L smt2.6 --no-incremental --no-type-checking --no-interactive "$@" $bench; } 2>&1)"
   case "$result" in
     sat|unsat) echo "$result"; exit 0;;
-    *)         echo "$result" >&2;;
+    *)         echo "$result" &> "$out_file";;
   esac
 }
 
 # use: finishwith [params..]
-# to run cvc4 and let it output whatever it will to stdout.
+# to run cvc4. Only "sat" or "unsat" are output. Other outputs are written to
+# $out_file.
 function finishwith {
-  $cvc4 -L smt2.6 --no-incremental --no-type-checking --no-interactive "$@" $bench
+  result="$({ $cvc4 -L smt2.6 --no-incremental --no-type-checking --no-interactive "$@" $bench; } 2>&1)"
+  case "$result" in
+    sat|unsat) echo "$result"; exit 0;;
+    *)         echo "$result" &> "$out_file";;
+  esac
 }
 
 # the following is designed for a run time of 20 min.

diff --git a/contrib/competitions/smt-comp/run-script-smtcomp-current-model-validation b/contrib/competitions/smt-comp/run-script-smtcomp-current-model-validation
index 385a845e7071341714357f86c3a5414ee05e5530..9982a9e29d9465fb1b5fb23fdfdb5383095237aa 100755 (executable)
--- a/contrib/competitions/smt-comp/run-script-smtcomp-current-model-validation
+++ b/contrib/competitions/smt-comp/run-script-smtcomp-current-model-validation
@@ -13,6 +13,12 @@ function finishwith {
 
 case "$logic" in
 
+QF_LRA)
+  finishwith --no-restrict-pivots --use-soi --new-prop
+  ;;
+QF_LIA)
+  finishwith --miplib-trick --miplib-trick-subs=4 --use-approx --lemmas-on-replay-failure --replay-early-close-depth=4 --replay-lemma-reject-cut=128 --replay-reject-cut=512 --use-soi --pb-rewrites --ite-simp --simp-ite-compress
+  ;;
 QF_BV)
   finishwith --bv-div-zero-const --bitblast=eager --bv-sat-solver=cadical --no-bv-abstraction
   ;;
@@ -22,4 +28,3 @@ QF_BV)
   ;;
 
 esac
-