diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-04-23 15:11:44 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-04-23 15:11:44 -0500 |
commit | d59314199fc72fa299ed536937a2184c54f0fc98 (patch) | |
tree | bbc150972b1524b09ddc6836a3c5629c1ee6728c /contrib | |
parent | 28e9077fad9d5c61c61a1762e7cf021c226cb9c2 (diff) |
Draft smt comp 2018 for quantifiers and non-linear (#1808)
Diffstat (limited to 'contrib')
-rw-r--r-- | contrib/run-script-smtcomp2018 | 80 | ||||
-rwxr-xr-x | contrib/run-script-smtcomp2018-application | 4 | ||||
-rw-r--r-- | contrib/run-script-smtcomp2018-unsat-cores | 6 |
3 files changed, 43 insertions, 47 deletions
diff --git a/contrib/run-script-smtcomp2018 b/contrib/run-script-smtcomp2018 index a0e793c2e..403f6c8a8 100644 --- a/contrib/run-script-smtcomp2018 +++ b/contrib/run-script-smtcomp2018 @@ -35,23 +35,25 @@ QF_LIA) ;; QF_NIA) trywith 300 --nl-ext --nl-ext-tplanes --decision=internal - trywith 1800 --solve-int-as-bv=2 --bitblast=eager --bv-sat-solver=cryptominisat - trywith 1800 --solve-int-as-bv=4 --bitblast=eager --bv-sat-solver=cryptominisat - trywith 1800 --solve-int-as-bv=8 --bitblast=eager --bv-sat-solver=cryptominisat - trywith 1800 --solve-int-as-bv=16 --bitblast=eager --bv-sat-solver=cryptominisat + # 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=cryptominisat + trywith 300 --solve-int-as-bv=4 --bitblast=eager --bv-sat-solver=cryptominisat + trywith 300 --solve-int-as-bv=8 --bitblast=eager --bv-sat-solver=cryptominisat + trywith 300 --solve-int-as-bv=16 --bitblast=eager --bv-sat-solver=cryptominisat finishwith --solve-int-as-bv=32 --bitblast=eager --bv-sat-solver=cryptominisat ;; QF_NRA) - trywith 300 --nl-ext --nl-ext-tplanes --decision=justification - finishwith --nl-ext --nl-ext-tplanes + trywith 300 --nl-ext --nl-ext-tplanes --decision=internal + trywith 300 --nl-ext --nl-ext-tplanes --decision=justification --no-nl-ext-factor + trywith 30 --nl-ext --nl-ext-tplanes --decision=internal --solve-real-as-int + finishwith --nl-ext --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) - # the following is designed for a run time of 2400s (40 min). + # the following is designed for a run time of 20 min. # initial runs 1min - trywith 20 --simplification=none --full-saturate-quant - trywith 20 --no-e-matching --full-saturate-quant - trywith 20 --fs-interleave --decision=internal --full-saturate-quant + trywith 30 --simplification=none --full-saturate-quant + trywith 30 --no-e-matching --full-saturate-quant # trigger selections 3min trywith 30 --relevant-triggers --full-saturate-quant trywith 30 --trigger-sel=max --full-saturate-quant @@ -59,52 +61,46 @@ ALIA|AUFLIA|AUFLIRA|AUFNIRA|UF|UFIDL|UFLIA|UFLRA|UFNIA|UFDT|UFDTLIA|AUFDTLIA|AUF trywith 30 --multi-trigger-when-single --multi-trigger-priority --full-saturate-quant trywith 30 --multi-trigger-cache --full-saturate-quant trywith 30 --no-multi-trigger-linear --full-saturate-quant - # other 3min + # other 4min trywith 30 --pre-skolem-quant --full-saturate-quant trywith 30 --inst-when=full --full-saturate-quant trywith 30 --no-e-matching --no-quant-cf --full-saturate-quant - trywith 30 --nl-ext --full-saturate-quant trywith 30 --full-saturate-quant --quant-ind - trywith 60 --decision=internal --simplification=none --no-inst-no-entail --no-quant-cf --full-saturate-quant - # finite model find 2min - trywith 20 --finite-model-find --mbqi=none - trywith 20 --finite-model-find - trywith 20 --finite-model-find --uf-ss=no-minimal + 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 --term-db-mode=relevant --full-saturate-quant + trywith 30 --fs-interleave --full-saturate-quant + # finite model find 3min + 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 20min - trywith 200 --decision=internal --full-saturate-quant - trywith 200 --term-db-mode=relevant --full-saturate-quant - trywith 200 --fs-interleave --full-saturate-quant - trywith 600 --finite-model-find --decision=internal - # finite model find 1min - trywith 30 --finite-model-find --fmf-bound-int - trywith 30 --finite-model-find --sort-inference - # finish 10min + # long runs 9min + trywith 240 --finite-model-find --decision=internal finishwith --full-saturate-quant ;; UFBV) # most problems in UFBV are essentially BV - trywith 300 --full-saturate-quant - trywith 300 --full-saturate-quant --no-cbqi - trywith 300 --full-saturate-quant --cbqi --decision=internal + trywith 300 --full-saturate-quant --decision=internal + trywith 300 --full-saturate-quant --cbqi-nested-qe --decision=internal + trywith 30 --full-saturate-quant --cbqi-no-innermost --global-negate finishwith --finite-model-find ;; BV) - trywith 300 --full-saturate-quant - trywith 300 --full-saturate-quant --no-cbqi - finishwith --full-saturate-quant --cbqi --decision=internal - ;; -LIA|LRA) - trywith 30 --full-saturate-quant - trywith 300 --full-saturate-quant --cbqi-midpoint - trywith 300 --full-saturate-quant --cbqi-nested-qe - finishwith --full-saturate-quant --cbqi --cbqi-nested-qe --decision=internal + trywith 120 --full-saturate-quant + trywith 120 --full-saturate-quant --cbqi-no-innermost + trywith 300 --full-saturate-quant --cbqi-nested-qe --decision=internal + trywith 30 --full-saturate-quant --no-cbqi-bv + trywith 30 --full-saturate-quant --cbqi-bv-ineq=eq-slack + # finish 10min + finishwith --full-saturate-quant --cbqi-no-innermost --global-negate ;; -NIA|NRA) - trywith 30 --full-saturate-quant - trywith 300 --full-saturate-quant --nl-ext +LIA|LRA|NIA|NRA) + trywith 30 --full-saturate-quant --nl-ext-tplanes + trywith 300 --full-saturate-quant --cbqi-no-innermost trywith 300 --full-saturate-quant --cbqi-nested-qe - finishwith --full-saturate-quant --cbqi --cbqi-nested-qe --decision=internal + finishwith --full-saturate-quant --cbqi-nested-qe --decision=internal ;; QF_AUFBV) trywith 600 diff --git a/contrib/run-script-smtcomp2018-application b/contrib/run-script-smtcomp2018-application index 8a8ea7786..4bf2f6b91 100755 --- a/contrib/run-script-smtcomp2018-application +++ b/contrib/run-script-smtcomp2018-application @@ -35,10 +35,10 @@ ALIA|QF_ALIA|QF_LRA|QF_UFLIA|QF_UFLRA|UFLRA) runcvc4 --incremental ;; ANIA|QF_ANIA|QF_NIA|QF_UFNIA|QF_NRA) - runcvc4 --nl-ext --tear-down-incremental=1 + runcvc4 --tear-down-incremental=1 ;; LIA|LRA) - runcvc4 --incremental --cbqi + runcvc4 --incremental ;; QF_AUFLIA) runcvc4 --no-arrays-eager-index --arrays-eager-lemmas --incremental diff --git a/contrib/run-script-smtcomp2018-unsat-cores b/contrib/run-script-smtcomp2018-unsat-cores index 19dc45885..24933cf40 100644 --- a/contrib/run-script-smtcomp2018-unsat-cores +++ b/contrib/run-script-smtcomp2018-unsat-cores @@ -33,13 +33,13 @@ UFBV) finishwith --finite-model-find ;; BV) - finishwith --full-saturate-quant --cbqi --decision=internal + finishwith --full-saturate-quant --decision=internal ;; LIA|LRA) - finishwith --full-saturate-quant --cbqi --cbqi-nested-qe --decision=internal + finishwith --full-saturate-quant --cbqi-nested-qe --decision=internal ;; NIA|NRA) - finishwith --full-saturate-quant --cbqi --cbqi-nested-qe --decision=internal + finishwith --full-saturate-quant --cbqi-nested-qe --decision=internal ;; QF_AUFBV) finishwith --decision=justification-stoponly |