From 41d07960fd817d0d98b6bf65b2b3c2687837e46c Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Mon, 14 Jun 2021 16:45:17 -0700 Subject: [PATCH] Final update to SMT-COMP 2021 options (#6739) This commit: - Disables `--tear-down-incremental=X` for the competition since it currently does not work correctly on master and a fixed version did not show significant benefits. - Changes the occurrences of `--nl-ext` to `--nl-ext=full` because it is now a mode option. - Removes the use of `--bv-assert-input` because the option currently has some issues in incremental mode (#6738) - Removes the use of `--bitblast=eager` for the model validation track because it produces invalid models (#6741) --- .../smt-comp/run-script-smtcomp-current | 12 +++--- .../run-script-smtcomp-current-incremental | 40 +++---------------- ...un-script-smtcomp-current-model-validation | 4 +- .../run-script-smtcomp-current-unsat-cores | 7 +--- 4 files changed, 15 insertions(+), 48 deletions(-) diff --git a/contrib/competitions/smt-comp/run-script-smtcomp-current b/contrib/competitions/smt-comp/run-script-smtcomp-current index ecc6ce5fe..9b4f534b0 100755 --- a/contrib/competitions/smt-comp/run-script-smtcomp-current +++ b/contrib/competitions/smt-comp/run-script-smtcomp-current @@ -1,6 +1,6 @@ #!/bin/bash -cvc5=./cvc5 +cvc5=$(dirname "$(readlink -f "$0")")/cvc5 bench="$1" # Output other than "sat"/"unsat" is either written to stderr or to "err.log" @@ -75,7 +75,7 @@ QF_NRA) finishwith --decision=internal --nl-ext=none ;; # all logics with UF + quantifiers should either fall under this or special cases below -ALIA|AUFLIA|AUFLIRA|AUFNIRA|UF|UFIDL|UFLIA|UFLRA|UFNIA|UFDT|UFDTLIA|AUFDTLIA|AUFBVDTLIA|AUFNIA|UFFPDTLIRA|UFFPDTNIRA) +ALIA|AUFLIA|AUFLIRA|AUFNIRA|UF|UFBVLIA|UFIDL|UFLIA|UFLRA|UFNIA|UFDT|UFDTLIA|AUFDTLIA|AUFBV|AUFBVDTLIA|AUFBVFP|AUFNIA|UFFPDTLIRA|UFFPDTNIRA) # initial runs 1 min trywith 30 --simplification=none --full-saturate-quant trywith 30 --no-e-matching --full-saturate-quant @@ -112,7 +112,7 @@ UFBV) trywith 30 --full-saturate-quant --no-cegqi-innermost --global-negate finishwith --finite-model-find ;; -BV) +ABV|BV) trywith 120 --full-saturate-quant trywith 120 --sygus-inst trywith 300 --full-saturate-quant --cegqi-nested-qe --decision=internal @@ -121,7 +121,7 @@ BV) # finish 10min finishwith --full-saturate-quant --no-cegqi-innermost --global-negate ;; -ABVFP|BVFP|FP|NIA|NRA) +ABVFP|ABVFPLRA|BVFP|FP|NIA|NRA) trywith 300 --full-saturate-quant --nl-ext-tplanes --fp-exp finishwith --sygus-inst --fp-exp ;; @@ -131,8 +131,8 @@ LIA|LRA) finishwith --full-saturate-quant --cegqi-nested-qe --decision=internal ;; QF_AUFBV) - trywith 600 --ite-simp - finishwith --decision=justification-stoponly --ite-simp + trywith 600 + finishwith --decision=justification-stoponly ;; QF_ABV) trywith 50 --ite-simp --simp-with-care --repeat-simp --arrays-weak-equiv diff --git a/contrib/competitions/smt-comp/run-script-smtcomp-current-incremental b/contrib/competitions/smt-comp/run-script-smtcomp-current-incremental index 21bb2f6e0..79df91d69 100755 --- a/contrib/competitions/smt-comp/run-script-smtcomp-current-incremental +++ b/contrib/competitions/smt-comp/run-script-smtcomp-current-incremental @@ -1,6 +1,6 @@ #!/bin/bash -cvc5=./cvc5 +cvc5=$(dirname "$(readlink -f "$0")")/cvc5 line="" while [[ -z "$line" ]]; do @@ -26,50 +26,20 @@ function runcvc5 { # 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?) - $cvc5 --force-logic="$logic" -L smt2.6 --print-success --no-type-checking --no-interactive "$@" <&0- + $cvc5 --incremental --force-logic="$logic" -L smt2.6 --print-success --no-type-checking --no-interactive "$@" <&0- } case "$logic" in -ALIA|ANIA|AUFNIRA|LIA|LRA|QF_ALIA|QF_ANIA|QF_AUFBVLIA|QF_AUFBVNIA|QF_LIA|QF_LRA|QF_NIA|QF_UFBVLIA|QF_UFLIA|QF_UFLRA|QF_UFNIA|UFLRA) - runcvc5 --tear-down-incremental=1 - ;; QF_AUFLIA) - runcvc5 --tear-down-incremental=1 --no-arrays-eager-index --arrays-eager-lemmas + runcvc5 --no-arrays-eager-index --arrays-eager-lemmas ;; QF_BV) - runcvc5 --incremental --bitblast=eager --bv-assert-input - ;; -QF_UFBV) - runcvc5 --incremental --bv-assert-input - ;; -QF_UF) - runcvc5 --incremental - ;; -QF_AUFBV) - runcvc5 --incremental --bv-assert-input - ;; -QF_ABV) - runcvc5 --incremental --bv-assert-input - ;; -ABVFP) - runcvc5 --incremental - ;; -BVFP) - runcvc5 --incremental - ;; -QF_ABVFP) - runcvc5 --incremental - ;; -QF_BVFP) - runcvc5 --incremental - ;; -QF_FP) - runcvc5 --incremental + runcvc5 --bitblast=eager ;; *) # just run the default - runcvc5 --incremental + runcvc5 ;; esac diff --git a/contrib/competitions/smt-comp/run-script-smtcomp-current-model-validation b/contrib/competitions/smt-comp/run-script-smtcomp-current-model-validation index fe8d4ae44..0998e9949 100755 --- a/contrib/competitions/smt-comp/run-script-smtcomp-current-model-validation +++ b/contrib/competitions/smt-comp/run-script-smtcomp-current-model-validation @@ -1,6 +1,6 @@ #!/bin/bash -cvc5=./cvc5 +cvc5=$(dirname "$(readlink -f "$0")")/cvc5 bench="$1" logic=$(expr "$(grep -m1 '^[^;]*set-logic' "$bench")" : ' *(set-logic *\([A-Z_]*\) *) *$') @@ -20,7 +20,7 @@ QF_LIA) finishwith --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 --use-soi --pb-rewrites --ite-simp --simp-ite-compress ;; QF_BV) - finishwith --bitblast=eager --bv-assert-input + finishwith --bv-assert-input ;; *) # just run the default diff --git a/contrib/competitions/smt-comp/run-script-smtcomp-current-unsat-cores b/contrib/competitions/smt-comp/run-script-smtcomp-current-unsat-cores index e9753781d..75e3bfc82 100755 --- a/contrib/competitions/smt-comp/run-script-smtcomp-current-unsat-cores +++ b/contrib/competitions/smt-comp/run-script-smtcomp-current-unsat-cores @@ -1,6 +1,6 @@ #!/bin/bash -cvc5=./cvc5 +cvc5=$(dirname "$(readlink -f "$0")")/cvc5 bench="$1" logic=$(expr "$(grep -m1 '^[^;]*set-logic' "$bench")" : ' *(set-logic *\([A-Z_]*\) *) *$') @@ -20,10 +20,7 @@ QF_LIA) finishwith --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 --use-soi ;; QF_NIA) - finishwith --nl-ext --nl-ext-tplanes - ;; -QF_NRA) - finishwith --nl-ext --nl-ext-tplanes + finishwith --nl-ext-tplanes ;; # all logics with UF + quantifiers should either fall under this or special cases below ALIA|AUFLIA|AUFLIRA|AUFNIRA|UF|UFIDL|UFLIA|UFLRA|UFNIA|UFDT|UFDTLIA|AUFDTLIA|AUFBVDTLIA|AUFNIA|ABVFP|BVFP|FP) -- 2.30.2