diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-08-27 17:27:57 +0200 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-08-27 17:27:57 +0200 |
| commit | 0ddf1b9c74f2b2a78e0960b710c2edbdc5f8d02d (patch) | |
| tree | 523a7c7ec9bfefd4297c5d8f56ef0ff474045d73 /contrib/run-script-syguscomp2015 | |
| parent | d4a7b0cf0500e971c9c01e7628f3c1b567715059 (diff) | |
Do ITE term bookkeeping when solving Sygus inputs. Add missing script from Sygus comp 2015. Fix bug 665 regarding strings rewriter for contains.
Diffstat (limited to 'contrib/run-script-syguscomp2015')
| -rw-r--r-- | contrib/run-script-syguscomp2015 | 17 |
1 files changed, 17 insertions, 0 deletions
diff --git a/contrib/run-script-syguscomp2015 b/contrib/run-script-syguscomp2015 new file mode 100644 index 000000000..aab6851e1 --- /dev/null +++ b/contrib/run-script-syguscomp2015 @@ -0,0 +1,17 @@ +#!/bin/bash + +cvc4=./cvc4 +bench="$1" + +function trywith { + ($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 +} + +trywith --cegqi --cegqi-si-multi-inst-abort --cegqi-si-abort --decision=internal +trywith --cegqi --no-cegqi-si + |