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, 37 insertions, 0 deletions

diff --git a/contrib/competitions/sygus-comp/run-script-sygusComp-current-CLIA b/contrib/competitions/sygus-comp/run-script-sygusComp-current-CLIA
new file mode 100755
index 000000000..d9864f651
--- /dev/null
+++ b/contrib/competitions/sygus-comp/run-script-sygusComp-current-CLIA
@@ -0,0 +1,37 @@
+#!/bin/bash
+
+cvc4=./cvc4
+bench="$1"
+
+function runl {
+  limit=$1; shift;
+  ulimit -S -t "$limit";$cvc4 --lang=sygus2 --no-type-checking --no-interactive --dag-thresh=0 "$@" $bench 2>/dev/null
+}
+
+function trywith {
+  sol=$(runl $@)
+  status=$?
+  if [ $status -ne 134 ]; then
+    echo $sol |&
+    (read result w1 w2;
+    case "$result" in
+    unsat)
+      case "$w1" in
+        "(define-fun") echo "$w1 $w2";cat;exit 0;;
+        esac; exit 1;;
+    esac; exit 1)
+    if [ ${PIPESTATUS[1]} -eq 0 ]; then exit 0; fi
+  fi
+}
+
+function finishwith {
+  $cvc4 --lang=sygus2 --no-type-checking --no-interactive --dag-thresh=0 "$@" $bench 2>/dev/null |
+  (read result w1;
+  case "$result" in
+  unsat) echo "$w1";cat;exit 0;;
+  esac)
+}
+
+trywith 120 --sygus-si=all --sygus-si-abort --ceqqi-prereg-inst
+trywith 10 --sygus-si=none --sygus-repair-const
+finishwith --sygus-si=none