diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-05-12 09:38:59 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-05-12 14:38:59 +0000 |
| commit | b016f603f2a3709faaf90008a09f2567d7283ff3 (patch) | |
| tree | 77c2d4a2b5ebdf8576d62e8d2a9dbbd211bbb8e2 /contrib | |
| parent | 111f98a41b488b8124fbecd28dba17465ea30786 (diff) | |
Preliminary draft of changes for SMT comp 2021 (#6522)
Covers improvements to quantifiers.
Diffstat (limited to 'contrib')
| -rwxr-xr-x | contrib/competitions/smt-comp/run-script-smtcomp-current | 22 |
1 files changed, 11 insertions, 11 deletions
diff --git a/contrib/competitions/smt-comp/run-script-smtcomp-current b/contrib/competitions/smt-comp/run-script-smtcomp-current index 715f3fc6c..e891cf8cf 100755 --- a/contrib/competitions/smt-comp/run-script-smtcomp-current +++ b/contrib/competitions/smt-comp/run-script-smtcomp-current @@ -75,10 +75,11 @@ QF_NRA) finishwith --nl-ext-tplanes --decision=justification ;; # 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) +ALIA|AUFLIA|AUFLIRA|AUFNIRA|UF|UFIDL|UFLIA|UFLRA|UFNIA|UFDT|UFDTLIA|AUFDTLIA|AUFBVDTLIA|AUFNIA|UFFPDTLIRA|UFFPDTNIRA) # initial runs 1 min trywith 30 --simplification=none --full-saturate-quant trywith 30 --no-e-matching --full-saturate-quant + trywith 30 --no-e-matching --full-saturate-quant --fs-sum # trigger selections 3 min trywith 30 --relevant-triggers --full-saturate-quant trywith 30 --trigger-sel=max --full-saturate-quant @@ -92,41 +93,40 @@ ALIA|AUFLIA|AUFLIRA|AUFNIRA|UF|UFIDL|UFLIA|UFLRA|UFNIA|UFDT|UFDTLIA|AUFDTLIA|AUF trywith 30 --no-e-matching --no-quant-cf --full-saturate-quant trywith 30 --full-saturate-quant --quant-ind trywith 30 --decision=internal --simplification=none --no-inst-no-entail --no-quant-cf --full-saturate-quant - trywith 30 --decision=internal --full-saturate-quant + trywith 30 --decision=internal --full-saturate-quant --fs-sum trywith 30 --term-db-mode=relevant --full-saturate-quant trywith 30 --fs-interleave --full-saturate-quant # finite model find 3 min trywith 30 --finite-model-find --mbqi=none trywith 30 --finite-model-find --decision=internal trywith 30 --finite-model-find --macros-quant --macros-quant-mode=all - trywith 30 --finite-model-find --uf-ss=no-minimal trywith 60 --finite-model-find --fmf-inst-engine # long runs 4 min trywith 240 --finite-model-find --decision=internal finishwith --full-saturate-quant ;; -ABVFP|BVFP|FP|UFFPDTLIRA|UFFPDTNIRA) - finishwith --full-saturate-quant --fp-exp - ;; UFBV) # most problems in UFBV are essentially BV - trywith 300 --full-saturate-quant --decision=internal + trywith 300 --sygus-inst trywith 300 --full-saturate-quant --cegqi-nested-qe --decision=internal trywith 30 --full-saturate-quant --no-cegqi-innermost --global-negate finishwith --finite-model-find ;; BV) trywith 120 --full-saturate-quant - trywith 120 --full-saturate-quant --no-cegqi-innermost + trywith 120 --sygus-inst trywith 300 --full-saturate-quant --cegqi-nested-qe --decision=internal trywith 30 --full-saturate-quant --no-cegqi-bv trywith 30 --full-saturate-quant --cegqi-bv-ineq=eq-slack # finish 10min finishwith --full-saturate-quant --no-cegqi-innermost --global-negate ;; -LIA|LRA|NIA|NRA) - trywith 30 --full-saturate-quant --nl-ext-tplanes - trywith 300 --full-saturate-quant --no-cegqi-innermost +ABVFP|BVFP|FP|NIA|NRA) + trywith 300 --full-saturate-quant --nl-ext-tplanes --fp-exp + finishwith --sygus-inst --fp-exp + ;; +LIA|LRA) + trywith 30 --full-saturate-quant trywith 300 --full-saturate-quant --cegqi-nested-qe finishwith --full-saturate-quant --cegqi-nested-qe --decision=internal ;; |