diff options
Diffstat (limited to 'contrib/competitions/smt-comp/run-script-smtcomp-current')
| -rwxr-xr-x | contrib/competitions/smt-comp/run-script-smtcomp-current | 23 |
1 files changed, 18 insertions, 5 deletions
diff --git a/contrib/competitions/smt-comp/run-script-smtcomp-current b/contrib/competitions/smt-comp/run-script-smtcomp-current index 506eb56b7..bdc94b0bc 100755 --- a/contrib/competitions/smt-comp/run-script-smtcomp-current +++ b/contrib/competitions/smt-comp/run-script-smtcomp-current @@ -3,25 +3,38 @@ cvc4=./cvc4 bench="$1" +# Output other than "sat"/"unsat" is either written to stderr or to "err.log" +# in the directory specified by $2 if it has been set (e.g. when running on +# StarExec). +out_file=/dev/stderr +if [ -n "$2" ]; then + out_file="$2/err.log" +fi + logic=$(expr "$(grep -m1 '^[^;]*set-logic' "$bench")" : ' *(set-logic *\([A-Z_]*\) *) *$') # use: trywith [params..] # to attempt a run. Only thing printed on stdout is "sat" or "unsat", in which # case this run script terminates immediately. Otherwise, this function -# returns normally and prints the output of the solver to stderr. +# returns normally and prints the output of the solver to $out_file. function trywith { limit=$1; shift; - result="$(ulimit -S -t "$limit";$cvc4 -L smt2.6 --no-incremental --no-type-checking --no-interactive "$@" $bench)" + result="$({ ulimit -S -t "$limit"; $cvc4 -L smt2.6 --no-incremental --no-type-checking --no-interactive "$@" $bench; } 2>&1)" case "$result" in sat|unsat) echo "$result"; exit 0;; - *) echo "$result" >&2;; + *) echo "$result" &> "$out_file";; esac } # use: finishwith [params..] -# to run cvc4 and let it output whatever it will to stdout. +# to run cvc4. Only "sat" or "unsat" are output. Other outputs are written to +# $out_file. function finishwith { - $cvc4 -L smt2.6 --no-incremental --no-type-checking --no-interactive "$@" $bench + result="$({ $cvc4 -L smt2.6 --no-incremental --no-type-checking --no-interactive "$@" $bench; } 2>&1)" + case "$result" in + sat|unsat) echo "$result"; exit 0;; + *) echo "$result" &> "$out_file";; + esac } # the following is designed for a run time of 20 min. |