diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-07-10 09:52:01 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-07-10 09:52:01 -0500 |
commit | 246f3c6d2f11e788ced562c1fc1f8def4628baf2 (patch) | |
tree | 2ae403e2c732d356367084d915c2ab9640858e0a /contrib/competitions/sygus-comp/run-script-sygusComp-current-GENERAL-auto | |
parent | ba7cda7a9cb02a38b1cf8fd9fbd85304a9056a5e (diff) |
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.
Diffstat (limited to 'contrib/competitions/sygus-comp/run-script-sygusComp-current-GENERAL-auto')
-rwxr-xr-x | contrib/competitions/sygus-comp/run-script-sygusComp-current-GENERAL-auto | 37 |
1 files changed, 37 insertions, 0 deletions
diff --git a/contrib/competitions/sygus-comp/run-script-sygusComp-current-GENERAL-auto b/contrib/competitions/sygus-comp/run-script-sygusComp-current-GENERAL-auto new file mode 100755 index 000000000..f69398bed --- /dev/null +++ b/contrib/competitions/sygus-comp/run-script-sygusComp-current-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-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 --cegqi-prereg-inst +trywith 5 --sygus-si=none --sygus-crepair-abort --sygus-repair-const +finishwith --sygus-si=none |