summaryrefslogtreecommitdiff
path: root/contrib/run-script-sygusComp2018-PBE_BitVec
diff options
context:
space:
mode:
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>2018-06-26 18:59:28 -0500
committerAndres Noetzli <andres.noetzli@gmail.com>2018-06-26 16:59:28 -0700
commita236ade3242599d4916fd9ee676c2c68c7c004b1 (patch)
tree8e3061156672bd19fe1386e7ccc7924c553ecc76 /contrib/run-script-sygusComp2018-PBE_BitVec
parent81bb4147ad681641dc99a62fc1a8605f99c05f2d (diff)
sygusComp2018: add scripts. (#2103)
Diffstat (limited to 'contrib/run-script-sygusComp2018-PBE_BitVec')
-rw-r--r--contrib/run-script-sygusComp2018-PBE_BitVec16
1 files changed, 16 insertions, 0 deletions
diff --git a/contrib/run-script-sygusComp2018-PBE_BitVec b/contrib/run-script-sygusComp2018-PBE_BitVec
new file mode 100644
index 000000000..ee5035e59
--- /dev/null
+++ b/contrib/run-script-sygusComp2018-PBE_BitVec
@@ -0,0 +1,16 @@
+#!/bin/bash
+
+cvc4=./cvc4
+bench="$1"
+
+function finishwith {
+ ($cvc4 --lang=sygus --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
+
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback