diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-04-01 23:26:46 -0400 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-04-01 23:29:13 -0400 |
commit | 2f195e4babef016e9b02faeb80cd79f0177a3f05 (patch) | |
tree | a9d22f73971bef8196fe7ffba748c1a17115b2b4 /contrib/run-script-smteval2013 | |
parent | f51b6e9a9dc853156ee392c26f40494d91f345e9 (diff) |
Adjust release Makefile rules, new run script
Diffstat (limited to 'contrib/run-script-smteval2013')
-rwxr-xr-x | contrib/run-script-smteval2013 | 55 |
1 files changed, 55 insertions, 0 deletions
diff --git a/contrib/run-script-smteval2013 b/contrib/run-script-smteval2013 new file mode 100755 index 000000000..3c71b28e7 --- /dev/null +++ b/contrib/run-script-smteval2013 @@ -0,0 +1,55 @@ +#!/bin/bash + +cat >bench-$$.smt2 +trap 'rm bench-$$.smt2' EXIT + +logic=$(expr "$(head -n 1 bench-$$.smt2)" : ' *(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. +function trywith { + result="$(./cvc4 -L smt2 --no-checking --no-interactive "$@" bench-$$.smt2)" + case "$result" in + sat|unsat) echo "$result"; exit 0;; + esac +} + +# use: finishwith [params..] +# to run cvc4 and let it output whatever it will to stdout. +function finishwith { + ./cvc4 -L smt2 --no-checking --no-interactive "$@" bench-$$.smt2 +} + +case "$logic" in + +QF_LRA) + # 3 minutes with default decision heuristic + trywith --tlimit-per=180000 + # switch to internal decision heuristic + finishwith --decision=internal + ;; +AUFLIA) + # 60 seconds with default decision heuristic + trywith --tlimit-per=60000 + # try simplification for 60 seconds, default decision heuristic + trywith --simplification=batch --tlimit-per=60000 + # switch to internal decision heuristic + finishwith --decision=internal + ;; +QF_AUFBV) + trywith --tlimit-per=600000 + finishwith --decision=justification-stoponly + ;; +QF_AX) + trywith --tlimit-per=2000 + finishwith --no-arrays-model-based + ;; +*) + # just run the default + finishwith + ;; + +esac + |