[SMT-COMP 2019] Update run scripts to match tracks (#3018)

The "Application Track" has been renamed to "Incremental Track" this
year, so this commit renames the script accordingly and updates the name
of the CVC4 binary that the script calls to be just `cvc4`. The commit
also adds an initial script for the model validation track.

diff --git a/contrib/run-script-smtcomp2019 b/contrib/run-script-smtcomp2019
old mode 100644 (file)
new mode 100755 (executable)

diff --git a/contrib/run-script-smtcomp2019-application b/contrib/run-script-smtcomp2019-application
deleted file mode 100755 (executable)
index a7d4d98..0000000
--- a/contrib/run-script-smtcomp2019-application
+++ /dev/null
@@ -1,84 +0,0 @@
-#!/bin/bash
-
-cvc4=./cvc4-application
-
-line=""
-while [[ -z "$line" ]]; do
-  read line
-done
-if [ "$line" != '(set-option :print-success true)' ]; then
-  echo 'ERROR: first line supposed to be set-option :print-success, but got: "'"$line"'"' >&2
-  exit 1
-fi
-echo success
-line=""
-while [[ -z "$line" ]]; do
-  read line
-done
-logic=$(expr "$line" : ' *(set-logic  *\([A-Z_]*\) *) *$')
-if [ -z "$logic" ]; then
-  echo 'ERROR: second line supposed to be set-logic, but got: "'"$line"'"' >&2
-  exit 1
-fi
-echo success
-
-function runcvc4 {
-  # we run in this way for line-buffered input, otherwise memory's a
-  # concern (plus it mimics what we'll end up getting from an
-  # application-track trace runner?)
-  $cvc4 --force-logic="$logic" -L smt2.6 --print-success --no-checking --no-interactive "$@" <&0-
-}
-
-case "$logic" in
-
-ALIA|QF_ALIA|QF_LRA|QF_UFLIA|QF_UFLRA|UFLRA)
-  runcvc4 --incremental
-  ;;
-ANIA|QF_ANIA|QF_NIA|QF_UFNIA|QF_NRA)
-  runcvc4 --tear-down-incremental=1
-  ;;
-LIA|LRA)
-  runcvc4 --incremental
-  ;;
-QF_AUFLIA)
-  runcvc4 --no-arrays-eager-index --arrays-eager-lemmas --incremental
-  ;;
-QF_BV)
-  runcvc4 --incremental --bitblast=eager --bv-sat-solver=cadical
-  ;;
-QF_LIA)
-  runcvc4 --tear-down-incremental=1 --unconstrained-simp
-  ;;
-QF_UFBV)
-  runcvc4 --incremental
-  ;;
-QF_UF)
-  runcvc4 --incremental
-  ;;
-QF_AUFBV)
-  runcvc4 --incremental
-  ;;
-QF_ABV)
-  runcvc4 --incremental
-  ;;
-ABVFP)
-  runcvc4 --incremental
-  ;;
-BVFP)
-  runcvc4 --incremental
-  ;;
-QF_ABVFP)
-  runcvc4 --incremental
-  ;;
-QF_BVFP)
-  runcvc4 --incremental
-  ;;
-QF_FP)
-  runcvc4 --incremental
-  ;;
-*)
-  # just run the default
-  runcvc4 --incremental
-  ;;
-
-esac

diff --git a/contrib/run-script-smtcomp2019-incremental b/contrib/run-script-smtcomp2019-incremental
new file mode 100755 (executable)
index 0000000..12c91a0
--- /dev/null
+++ b/contrib/run-script-smtcomp2019-incremental
@@ -0,0 +1,84 @@
+#!/bin/bash
+
+cvc4=./cvc4
+
+line=""
+while [[ -z "$line" ]]; do
+  read line
+done
+if [ "$line" != '(set-option :print-success true)' ]; then
+  echo 'ERROR: first line supposed to be set-option :print-success, but got: "'"$line"'"' >&2
+  exit 1
+fi
+echo success
+line=""
+while [[ -z "$line" ]]; do
+  read line
+done
+logic=$(expr "$line" : ' *(set-logic  *\([A-Z_]*\) *) *$')
+if [ -z "$logic" ]; then
+  echo 'ERROR: second line supposed to be set-logic, but got: "'"$line"'"' >&2
+  exit 1
+fi
+echo success
+
+function runcvc4 {
+  # we run in this way for line-buffered input, otherwise memory's a
+  # concern (plus it mimics what we'll end up getting from an
+  # application-track trace runner?)
+  $cvc4 --force-logic="$logic" -L smt2.6 --print-success --no-checking --no-interactive "$@" <&0-
+}
+
+case "$logic" in
+
+ALIA|QF_ALIA|QF_LRA|QF_UFLIA|QF_UFLRA|UFLRA)
+  runcvc4 --incremental
+  ;;
+ANIA|QF_ANIA|QF_NIA|QF_UFNIA|QF_NRA)
+  runcvc4 --tear-down-incremental=1
+  ;;
+LIA|LRA)
+  runcvc4 --incremental
+  ;;
+QF_AUFLIA)
+  runcvc4 --no-arrays-eager-index --arrays-eager-lemmas --incremental
+  ;;
+QF_BV)
+  runcvc4 --incremental --bitblast=eager --bv-sat-solver=cadical
+  ;;
+QF_LIA)
+  runcvc4 --tear-down-incremental=1 --unconstrained-simp
+  ;;
+QF_UFBV)
+  runcvc4 --incremental
+  ;;
+QF_UF)
+  runcvc4 --incremental
+  ;;
+QF_AUFBV)
+  runcvc4 --incremental
+  ;;
+QF_ABV)
+  runcvc4 --incremental
+  ;;
+ABVFP)
+  runcvc4 --incremental
+  ;;
+BVFP)
+  runcvc4 --incremental
+  ;;
+QF_ABVFP)
+  runcvc4 --incremental
+  ;;
+QF_BVFP)
+  runcvc4 --incremental
+  ;;
+QF_FP)
+  runcvc4 --incremental
+  ;;
+*)
+  # just run the default
+  runcvc4 --incremental
+  ;;
+
+esac

diff --git a/contrib/run-script-smtcomp2019-model-validation b/contrib/run-script-smtcomp2019-model-validation
new file mode 100755 (executable)
index 0000000..f4b812f
--- /dev/null
+++ b/contrib/run-script-smtcomp2019-model-validation
@@ -0,0 +1,25 @@
+#!/bin/bash
+
+cvc4=./cvc4
+bench="$1"
+
+logic=$(expr "$(grep -m1 '^[^;]*set-logic' "$bench")" : ' *(set-logic  *\([A-Z_]*\) *) *$')
+
+# use: finishwith [params..]
+# to run cvc4 and let it output whatever it will to stdout.
+function finishwith {
+  $cvc4 -L smt2.6 --no-incremental --no-checking --no-interactive "$@" $bench
+}
+
+case "$logic" in
+
+QF_BV)
+  finishwith --bv-div-zero-const --bv-intro-pow2 --bitblast=eager --bv-sat-solver=cadical --bv-eq-slicer=auto --no-bv-abstraction
+  ;;
+*)
+  # just run the default
+  finishwith
+  ;;
+
+esac
+

diff --git a/contrib/run-script-smtcomp2019-unsat-cores b/contrib/run-script-smtcomp2019-unsat-cores
old mode 100644 (file)
new mode 100755 (executable)