Draft smt comp 2018 for quantifiers and non-linear (#1808)

diff --git a/contrib/run-script-smtcomp2018 b/contrib/run-script-smtcomp2018
index a0e793c2e9bdb0b89e28697d1bfb1ccf8756ceb6..403f6c8a838c2a0d3bee326fc03bfe97ef16a15d 100644 (file)
--- 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 8a8ea77866e5c7c83e82380130735a59b2b02283..4bf2f6b918bc043c673764d40d7eaafdbc4ea31f 100755 (executable)
--- 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 19dc45885203ed785febd4295c617a4d6f10c317..24933cf4054fa0dd22bd3c1bf9499cb1f139e3a0 100644 (file)
--- 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