diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-06-18 21:33:00 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-06-18 21:33:00 +0000 |
commit | 09590d6e174d810cde3c223da375ac798901aa3d (patch) | |
tree | 87f258c90a243d906ed8367b97ad97e382bf7d94 /contrib | |
parent | 8adb4e13c5c28059ed9271522137daf341942a75 (diff) |
final sources (?) for competition
Diffstat (limited to 'contrib')
-rw-r--r-- | contrib/Makefile.am | 1 | ||||
-rwxr-xr-x | contrib/run-script-smtcomp2012 | 51 |
2 files changed, 52 insertions, 0 deletions
diff --git a/contrib/Makefile.am b/contrib/Makefile.am index 815c3377d..facf5a21c 100644 --- a/contrib/Makefile.am +++ b/contrib/Makefile.am @@ -11,6 +11,7 @@ EXTRA_DIST = \ configure-in-place \ depgraph \ get-antlr-3.4 \ + run-script-smtcomp2012 \ theoryskel/kinds \ theoryskel/Makefile \ theoryskel/Makefile.am \ diff --git a/contrib/run-script-smtcomp2012 b/contrib/run-script-smtcomp2012 new file mode 100755 index 000000000..bad8482c2 --- /dev/null +++ b/contrib/run-script-smtcomp2012 @@ -0,0 +1,51 @@ +#!/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) + # 10 minutes with default decision heuristic + trywith --tlimit-per=600000 + # 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 + ;; +*) + # just run the default + finishwith + ;; + +esac + |