adding runscripts for syguscomp2019 (#3118)

11 files changed, 317 insertions, 0 deletions

diff --git a/contrib/run-script-sygusComp2019-CLIA b/contrib/run-script-sygusComp2019-CLIA
new file mode 100755
index 000000000..97bb2175b
--- /dev/null
+++ b/contrib/run-script-sygusComp2019-CLIA
@@ -0,0 +1,37 @@
+#!/bin/bash
+
+cvc4=./cvc4
+bench="$1"
+
+function runl {
+  limit=$1; shift;
+  ulimit -S -t "$limit";$cvc4 --lang=sygus2 --no-checking --no-interactive --default-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-checking --no-interactive --default-dag-thresh=0 "$@" $bench 2>/dev/null |
+  (read result w1;
+  case "$result" in
+  unsat) echo "$w1";cat;exit 0;;
+  esac)
+}
+
+trywith 120 --cegqi-si=all --cegqi-si-abort --cbqi --cbqi-prereg-inst
+trywith 10 --cegqi-si=none --sygus-repair-const
+finishwith --cegqi-si=none
diff --git a/contrib/run-script-sygusComp2019-GENERAL-auto b/contrib/run-script-sygusComp2019-GENERAL-auto
new file mode 100755
index 000000000..36afb0790
--- /dev/null
+++ b/contrib/run-script-sygusComp2019-GENERAL-auto
@@ -0,0 +1,37 @@
+#!/bin/bash
+
+cvc4=./cvc4
+bench="$1"
+
+function runl {
+  limit=$1; shift;
+  ulimit -S -t "$limit";$cvc4 --lang=sygus2 --no-checking --no-interactive --default-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-checking --no-interactive --default-dag-thresh=0 "$@" $bench 2>/dev/null |
+  (read result w1;
+  case "$result" in
+  unsat) echo "$w1";cat;exit 0;;
+  esac)
+}
+
+trywith 120 --cegqi-si=all --cegqi-si-abort --cbqi --cbqi-prereg-inst
+trywith 5 --cegqi-si=none --sygus-crepair-abort --sygus-repair-const
+finishwith --cegqi-si=none
diff --git a/contrib/run-script-sygusComp2019-GENERAL-f b/contrib/run-script-sygusComp2019-GENERAL-f
new file mode 100755
index 000000000..5c5e5e9e7
--- /dev/null
+++ b/contrib/run-script-sygusComp2019-GENERAL-f
@@ -0,0 +1,36 @@
+#!/bin/bash
+
+cvc4=./cvc4
+bench="$1"
+
+function runl {
+  limit=$1; shift;
+  ulimit -S -t "$limit";$cvc4 --lang=sygus2 --no-checking --no-interactive --default-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-checking --no-interactive --default-dag-thresh=0 "$@" $bench 2>/dev/null |
+  (read result w1;
+  case "$result" in
+  unsat) echo "$w1";cat;exit 0;;
+  esac)
+}
+
+trywith 5 --sygus-active-gen=enum --cegqi-si=none --sygus-crepair-abort --sygus-repair-const
+finishwith --sygus-active-gen=enum --cegqi-si=none
diff --git a/contrib/run-script-sygusComp2019-GENERAL-s b/contrib/run-script-sygusComp2019-GENERAL-s
new file mode 100755
index 000000000..2a19a14b5
--- /dev/null
+++ b/contrib/run-script-sygusComp2019-GENERAL-s
@@ -0,0 +1,36 @@
+#!/bin/bash
+
+cvc4=./cvc4
+bench="$1"
+
+function runl {
+  limit=$1; shift;
+  ulimit -S -t "$limit";$cvc4 --lang=sygus2 --no-checking --no-interactive --default-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-checking --no-interactive --default-dag-thresh=0 "$@" $bench 2>/dev/null |
+  (read result w1;
+  case "$result" in
+  unsat) echo "$w1";cat;exit 0;;
+  esac)
+}
+
+trywith 5 --sygus-active-gen=none --cegqi-si=none --sygus-crepair-abort --sygus-repair-const
+finishwith --sygus-active-gen=none --cegqi-si=none
diff --git a/contrib/run-script-sygusComp2019-INV-f b/contrib/run-script-sygusComp2019-INV-f
new file mode 100755
index 000000000..21120c0a4
--- /dev/null
+++ b/contrib/run-script-sygusComp2019-INV-f
@@ -0,0 +1,37 @@
+#!/bin/bash
+
+cvc4=./cvc4
+bench="$1"
+
+function runl {
+  limit=$1; shift;
+  ulimit -S -t "$limit";$cvc4 --lang=sygus2 --no-checking --no-interactive --default-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-checking --no-interactive --default-dag-thresh=0 "$@" $bench 2>/dev/null |
+  (read result w1;
+  case "$result" in
+  unsat) echo "$w1";cat;exit 0;;
+  esac)
+}
+
+trywith 10 --sygus-active-gen=enum --sygus-repair-const
+trywith 120 --sygus-unif
+finishwith --sygus-active-gen=enum
diff --git a/contrib/run-script-sygusComp2019-INV-s b/contrib/run-script-sygusComp2019-INV-s
new file mode 100755
index 000000000..e835ba91a
--- /dev/null
+++ b/contrib/run-script-sygusComp2019-INV-s
@@ -0,0 +1,37 @@
+#!/bin/bash
+
+cvc4=./cvc4
+bench="$1"
+
+function runl {
+  limit=$1; shift;
+  ulimit -S -t "$limit";$cvc4 --lang=sygus2 --no-checking --no-interactive --default-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-checking --no-interactive --default-dag-thresh=0 "$@" $bench 2>/dev/null |
+  (read result w1;
+  case "$result" in
+  unsat) echo "$w1";cat;exit 0;;
+  esac)
+}
+
+trywith 10 --sygus-active-gen=none --sygus-repair-const
+trywith 120 --sygus-unif
+finishwith --sygus-active-gen=none
diff --git a/contrib/run-script-sygusComp2019-INV-su b/contrib/run-script-sygusComp2019-INV-su
new file mode 100755
index 000000000..b3e056d7c
--- /dev/null
+++ b/contrib/run-script-sygusComp2019-INV-su
@@ -0,0 +1,37 @@
+#!/bin/bash
+
+cvc4=./cvc4
+bench="$1"
+
+function runl {
+  limit=$1; shift;
+  ulimit -S -t "$limit";$cvc4 --lang=sygus2 --no-checking --no-interactive --default-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-checking --no-interactive --default-dag-thresh=0 "$@" $bench 2>/dev/null |
+  (read result w1;
+  case "$result" in
+  unsat) echo "$w1";cat;exit 0;;
+  esac)
+}
+
+trywith 30 --sygus-unif-boolean-heuristic-dt --sygus-active-gen=var-agnostic --sygus-add-const-grammar --decision=justification
+trywith 10 --sygus-active-gen=none --sygus-repair-const
+finishwith --sygus-active-gen=none
diff --git a/contrib/run-script-sygusComp2019-PBE_BitVec-f b/contrib/run-script-sygusComp2019-PBE_BitVec-f
new file mode 100755
index 000000000..7fd203238
--- /dev/null
+++ b/contrib/run-script-sygusComp2019-PBE_BitVec-f
@@ -0,0 +1,15 @@
+#!/bin/bash
+
+cvc4=./cvc4
+bench="$1"
+
+function finishwith {
+  ($cvc4 --lang=sygus2 --no-checking --no-interactive --default-dag-thresh=0 "$@" $bench) 2>/dev/null |
+  (read result w1;
+  case "$result" in
+  unsat) echo "$w1";cat;exit 0;;
+  esac; exit 1)
+  if [ ${PIPESTATUS[1]} -eq 0 ]; then exit 0; fi
+}
+
+finishwith --cegqi-si=none
diff --git a/contrib/run-script-sygusComp2019-PBE_BitVec-s b/contrib/run-script-sygusComp2019-PBE_BitVec-s
new file mode 100755
index 000000000..27d72f7a0
--- /dev/null
+++ b/contrib/run-script-sygusComp2019-PBE_BitVec-s
@@ -0,0 +1,15 @@
+#!/bin/bash
+
+cvc4=./cvc4
+bench="$1"
+
+function finishwith {
+  ($cvc4 --lang=sygus2 --no-checking --no-interactive --default-dag-thresh=0 "$@" $bench) 2>/dev/null |
+  (read result w1;
+  case "$result" in
+  unsat) echo "$w1";cat;exit 0;;
+  esac; exit 1)
+  if [ ${PIPESTATUS[1]} -eq 0 ]; then exit 0; fi
+}
+
+finishwith --sygus-active-gen=none --cegqi-si=none
diff --git a/contrib/run-script-sygusComp2019-PBE_Strings-f b/contrib/run-script-sygusComp2019-PBE_Strings-f
new file mode 100755
index 000000000..f60263e05
--- /dev/null
+++ b/contrib/run-script-sygusComp2019-PBE_Strings-f
@@ -0,0 +1,15 @@
+#!/bin/bash
+
+cvc4=./cvc4
+bench="$1"
+
+function finishwith {
+  ($cvc4 --lang=sygus2 --no-checking --no-interactive --default-dag-thresh=0 "$@" $bench) 2>/dev/null |
+  (read result w1;
+  case "$result" in
+  unsat) echo "$w1";cat;exit 0;;
+  esac; exit 1)
+  if [ ${PIPESTATUS[1]} -eq 0 ]; then exit 0; fi
+}
+
+finishwith --cegqi-si=none --sygus-fair=direct
diff --git a/contrib/run-script-sygusComp2019-PBE_Strings-s b/contrib/run-script-sygusComp2019-PBE_Strings-s
new file mode 100755
index 000000000..42c7c40e7
--- /dev/null
+++ b/contrib/run-script-sygusComp2019-PBE_Strings-s
@@ -0,0 +1,15 @@
+#!/bin/bash
+
+cvc4=./cvc4
+bench="$1"
+
+function finishwith {
+  ($cvc4 --lang=sygus2 --no-checking --no-interactive --default-dag-thresh=0 "$@" $bench) 2>/dev/null |
+  (read result w1;
+  case "$result" in
+  unsat) echo "$w1";cat;exit 0;;
+  esac; exit 1)
+  if [ ${PIPESTATUS[1]} -eq 0 ]; then exit 0; fi
+}
+
+finishwith --sygus-active-gen=none --cegqi-si=none --sygus-fair=direct