diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2014-06-12 13:43:06 -0400 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2014-06-12 13:43:06 -0400 |
commit | ed402af3aaf578a55df6fa225b7b7a5455486a05 (patch) | |
tree | a12b4ff65461bd3304dc1044c091491aaadb80bb /contrib | |
parent | a026ce1757679f19ae646221ac5c12058d449f28 (diff) |
New application track script, new heuristics and all --tear-down-incremental. Not yet tested.
Diffstat (limited to 'contrib')
-rwxr-xr-x | contrib/run-script-smtcomp2014-application | 36 |
1 files changed, 23 insertions, 13 deletions
diff --git a/contrib/run-script-smtcomp2014-application b/contrib/run-script-smtcomp2014-application index 94e80b940..3703dcd2f 100755 --- a/contrib/run-script-smtcomp2014-application +++ b/contrib/run-script-smtcomp2014-application @@ -5,24 +5,34 @@ bench="$1" logic=$(expr "$(grep -m1 '^[^;]*set-logic' "$bench")" : ' *(set-logic *\([A-Z_]*\) *) *$') -case "$logic" in - -QF_BV) - # run tear-down incremental - # +function runcvc4 { # we run in this way for line-buffered input, otherwise memory's a # concern (plus it mimics what we'll end up getting from an # application-track trace runner?) - cat "$bench" | $cvc4 -L smt2 --no-checking --no-interactive --tear-down-incremental - ;; + cat "$bench" | $cvc4 -L smt2 --no-checking --no-interactive --tear-down-incremental "$@" +} +case "$logic" in + +QF_LRA) + runcvc4 --enable-miplib-trick --miplib-trick-subs=4 --use-approx --lemmas-on-replay-failure --replay-early-close-depth=4 --replay-lemma-reject-cut=128 --replay-reject-cut=512 --unconstrained-simp --use-soi + ;; +QF_LIA) + # same as QF_LRA but add --pb-rewrites + runcvc4 --enable-miplib-trick --miplib-trick-subs=4 --use-approx --lemmas-on-replay-failure --replay-early-close-depth=4 --replay-lemma-reject-cut=128 --replay-reject-cut=512 --unconstrained-simp --use-soi --pb-rewrites + ;; +ALIA|AUFLIA|AUFLIRA|AUFNIRA|BV|UF|UFBV|UFIDL|UFLIA|UFLRA|UFNIA) + runcvc4 --simplification=none --decision=internal --full-saturate-quant + ;; +LIA|LRA|NIA|NRA) + runcvc4 --enable-cbqi --full-saturate-quant + ;; +QF_BV) + runcvc4 --bv-eq-slicer=auto --decision=justification + ;; *) - # just run the default --incremental - # - # we run in this way for line-buffered input, otherwise memory's a - # concern (plus it mimics what we'll end up getting from an - # application-track trace runner?) - cat "$bench" | $cvc4 -L smt2 --no-checking --no-interactive --incremental + # just run the default + runcvc4 ;; esac |