diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2017-06-21 10:24:11 -0500 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2017-06-21 10:24:39 -0500 |
commit | cdf019f8be3b4affdb582ceb95054b327006521c (patch) | |
tree | 48f7091d06d1eea5abe9f4773b26a18a0bf7c8fa /contrib/run-script-sygusComp2017-INV | |
parent | 89e41ba0f27c6f2c8aceb1884df7392a6ef577c7 (diff) |
Update casc and sygus comp scripts.
Diffstat (limited to 'contrib/run-script-sygusComp2017-INV')
-rwxr-xr-x | contrib/run-script-sygusComp2017-INV | 27 |
1 files changed, 22 insertions, 5 deletions
diff --git a/contrib/run-script-sygusComp2017-INV b/contrib/run-script-sygusComp2017-INV index a25a5f5c8..a21792fb9 100755 --- a/contrib/run-script-sygusComp2017-INV +++ b/contrib/run-script-sygusComp2017-INV @@ -3,14 +3,31 @@ cvc4=./cvc4 bench="$1" +function runl { + limit=$1; shift; + ulimit -S -t "$limit";$cvc4 --lang=sygus --no-checking --no-interactive --dump-synth --default-dag-thresh=0 "$@" $bench +} + function trywith { - ($cvc4 --lang=sygus --no-checking --no-interactive --dump-synth --default-dag-thresh=0 "$@" $bench) 2>/dev/null | + sol=$(runl $@) + status=$? + if [ $status -ne 134 ]; then + echo $sol | + (read result w1; + case "$result" in + unsat) echo "$w1";cat;exit 0;; + esac; exit 1) + if [ ${PIPESTATUS[1]} -eq 0 ]; then exit 0; fi + fi +} + +function finishwith { + $cvc4 --lang=sygus --no-checking --no-interactive --dump-synth --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 + esac) } -trywith --sygus-inv-templ=post - +trywith 60 --sygus-inv-templ=pre +finishwith --sygus-inv-templ=post |