From: Morgan Deters Date: Thu, 12 Jun 2014 17:43:06 +0000 (-0400) Subject: New application track script, new heuristics and all --tear-down-incremental. Not... X-Git-Tag: cvc5-1.0.0~6829^2 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=ed402af3aaf578a55df6fa225b7b7a5455486a05;p=cvc5.git New application track script, new heuristics and all --tear-down-incremental. Not yet tested. --- 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