From e9d650f668bf044b2baad5328d80e64522454c50 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Wed, 9 Jun 2021 09:40:10 -0700 Subject: [PATCH] Update options for SMT-COMP (#6704) This commit removes obsolete options for BV and strings logics, and updates QF_NIA to spend more time on our best configuration. Co-authored-by: Gereon Kremer nafur42@gmail.com Co-authored-by: Mathias Preiner mathias.preiner@gmail.com --- .../smt-comp/run-script-smtcomp-current | 33 +++++++++---------- .../run-script-smtcomp-current-incremental | 2 +- ...un-script-smtcomp-current-model-validation | 2 +- .../run-script-smtcomp-current-unsat-cores | 8 ++--- 4 files changed, 21 insertions(+), 24 deletions(-) diff --git a/contrib/competitions/smt-comp/run-script-smtcomp-current b/contrib/competitions/smt-comp/run-script-smtcomp-current index ea3b2dde1..db72b3a6b 100755 --- a/contrib/competitions/smt-comp/run-script-smtcomp-current +++ b/contrib/competitions/smt-comp/run-script-smtcomp-current @@ -56,23 +56,23 @@ 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 --unconstrained-simp --use-soi --pb-rewrites --ite-simp --simp-ite-compress ;; QF_NIA) - trywith 480 --nl-ext-tplanes --decision=internal - trywith 60 --nl-ext-tplanes --decision=justification + trywith 420 --nl-ext-tplanes --decision=justification + trywith 60 --nl-ext-tplanes --decision=internal + trywith 60 --nl-ext-tplanes --decision=justification-old trywith 60 --no-nl-ext-tplanes --decision=internal trywith 60 --no-arith-brab --nl-ext-tplanes --decision=internal # this totals up to more than 20 minutes, although notice that smaller bit-widths may quickly fail - trywith 300 --solve-int-as-bv=2 --bitblast=eager --bv-sat-solver=cadical --no-bv-abstraction - trywith 300 --solve-int-as-bv=4 --bitblast=eager --bv-sat-solver=cadical --no-bv-abstraction - trywith 300 --solve-int-as-bv=8 --bitblast=eager --bv-sat-solver=cadical --no-bv-abstraction - trywith 300 --solve-int-as-bv=16 --bitblast=eager --bv-sat-solver=cadical --no-bv-abstraction - trywith 600 --solve-int-as-bv=32 --bitblast=eager --bv-sat-solver=cadical --no-bv-abstraction + trywith 300 --solve-int-as-bv=2 --bitblast=eager + trywith 300 --solve-int-as-bv=4 --bitblast=eager + trywith 300 --solve-int-as-bv=8 --bitblast=eager + trywith 300 --solve-int-as-bv=16 --bitblast=eager + trywith 600 --solve-int-as-bv=32 --bitblast=eager finishwith --nl-ext-tplanes --decision=internal ;; QF_NRA) - trywith 300 --nl-ext-tplanes --decision=internal - trywith 300 --nl-ext-tplanes --decision=justification --no-nl-ext-factor - trywith 30 --nl-ext-tplanes --decision=internal --solve-real-as-int - finishwith --nl-ext-tplanes --decision=justification + trywith 600 --decision=justification + trywith 300 --decision=internal --no-nl-cad --nl-ext=full --nl-ext-tplanes + 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) @@ -140,13 +140,10 @@ QF_ABV) finishwith --ite-simp --simp-with-care --repeat-simp --arrays-weak-equiv ;; QF_UFBV) - # Benchmarks with uninterpreted sorts cannot be solved with eager - # bit-blasting currently - trywith 1200 --bitblast=eager --bv-sat-solver=cadical - finishwith + finishwith --bitblast=eager ;; QF_BV) - finishwith --bv-div-zero-const --bitblast=eager --bv-sat-solver=cadical --no-bv-abstraction + finishwith --bitblast=eager --bv-assert-input ;; QF_AUFLIA) finishwith --no-arrays-eager-index --arrays-eager-lemmas --decision=justification @@ -162,8 +159,8 @@ QF_ALIA) finishwith --decision=justification-stoponly --no-arrays-eager-index --arrays-eager-lemmas ;; QF_S|QF_SLIA) - trywith 300 --strings-exp --rewrite-divk --strings-fmf --no-jh-rlv-order - finishwith --strings-exp --rewrite-divk --no-jh-rlv-order + trywith 300 --strings-exp --strings-fmf --no-jh-rlv-order + finishwith --strings-exp --no-jh-rlv-order ;; QF_ABVFP|QF_ABVFPLRA) finishwith --fp-exp diff --git a/contrib/competitions/smt-comp/run-script-smtcomp-current-incremental b/contrib/competitions/smt-comp/run-script-smtcomp-current-incremental index e0b51bc46..c6901ff5b 100755 --- a/contrib/competitions/smt-comp/run-script-smtcomp-current-incremental +++ b/contrib/competitions/smt-comp/run-script-smtcomp-current-incremental @@ -38,7 +38,7 @@ QF_AUFLIA) runcvc5 --tear-down-incremental=1 --no-arrays-eager-index --arrays-eager-lemmas ;; QF_BV) - runcvc5 --incremental --bitblast=eager --bv-sat-solver=cadical + runcvc5 --incremental --bitblast=eager --bv-assert-input ;; QF_UFBV) runcvc5 --incremental 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 b5df43b72..fe8d4ae44 100755 --- a/contrib/competitions/smt-comp/run-script-smtcomp-current-model-validation +++ b/contrib/competitions/smt-comp/run-script-smtcomp-current-model-validation @@ -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-sat-solver=cadical --no-bv-abstraction + finishwith --bitblast=eager --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 d87e83257..e9753781d 100755 --- a/contrib/competitions/smt-comp/run-script-smtcomp-current-unsat-cores +++ b/contrib/competitions/smt-comp/run-script-smtcomp-current-unsat-cores @@ -17,7 +17,7 @@ QF_LRA) finishwith --no-restrict-pivots --use-soi --new-prop ;; 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 --ite-simp --simp-ite-compress + 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 @@ -42,16 +42,16 @@ NIA|NRA) finishwith --full-saturate-quant --cegqi-nested-qe --decision=internal ;; QF_AUFBV) - finishwith --decision=justification-stoponly --ite-simp + finishwith --decision=justification-stoponly ;; QF_ABV) - finishwith --ite-simp --simp-with-care --arrays-weak-equiv + finishwith --arrays-weak-equiv ;; QF_UFBV) finishwith ;; QF_BV) - finishwith --no-bv-abstraction + finishwith ;; QF_AUFLIA) finishwith --no-arrays-eager-index --arrays-eager-lemmas --decision=justification -- 2.30.2