Update competition scripts (#4715)

This PR creates a "current" sygus comp scripts, similar to what we have been doing for SMT COMP. It updates these scripts to fix the option names, as many have changed recently.

This also copies the SMT COMP current scripts to 2020, since they were used in the current state. @4tXJ7f let me know if this is not the case.

1 files changed, 75 insertions, 0 deletions

diff --git a/contrib/competitions/smt-comp/run-script-smtcomp2020-incremental b/contrib/competitions/smt-comp/run-script-smtcomp2020-incremental
new file mode 100644
index 000000000..7861a4c85
--- /dev/null
+++ b/contrib/competitions/smt-comp/run-script-smtcomp2020-incremental
@@ -0,0 +1,75 @@
+#!/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-type-checking --no-interactive "$@" <&0-
+}
+
+case "$logic" in
+
+ALIA|ANIA|AUFNIRA|LIA|LRA|QF_ALIA|QF_ANIA|QF_AUFBVLIA|QF_AUFBVNIA|QF_LIA|QF_LRA|QF_NIA|QF_UFBVLIA|QF_UFLIA|QF_UFLRA|QF_UFNIA|UFLRA)
+  runcvc4 --tear-down-incremental=1
+  ;;
+QF_AUFLIA)
+  runcvc4 --tear-down-incremental=1 --no-arrays-eager-index --arrays-eager-lemmas
+  ;;
+QF_BV)
+  runcvc4 --incremental --bitblast=eager --bv-sat-solver=cadical
+  ;;
+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