summaryrefslogtreecommitdiff
path: root/contrib/run-script-sygusComp2017-PBE_Strings
diff options
context:
space:
mode:
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>2019-08-08 15:16:41 -0500
committerGitHub <noreply@github.com>2019-08-08 15:16:41 -0500
commita56575f413499d256e81f6ca1a64ffe1413ed3c7 (patch)
tree03ea560fb5b45eb0877e1df4bdfe410ea9de79dd /contrib/run-script-sygusComp2017-PBE_Strings
parent63a6e17196d849ad6e57bce7490eafb5b7f7f3ec (diff)
Add subdirectories to contrib for competition scripts (#3164)
Diffstat (limited to 'contrib/run-script-sygusComp2017-PBE_Strings')
-rwxr-xr-xcontrib/run-script-sygusComp2017-PBE_Strings16
1 files changed, 0 insertions, 16 deletions
diff --git a/contrib/run-script-sygusComp2017-PBE_Strings b/contrib/run-script-sygusComp2017-PBE_Strings
deleted file mode 100755
index 849835b28..000000000
--- a/contrib/run-script-sygusComp2017-PBE_Strings
+++ /dev/null
@@ -1,16 +0,0 @@
-#!/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-si=none --sygus-fair=direct
-
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback