Preliminary draft of changes for SMT comp 2021 (#6522)

Covers improvements to quantifiers.

diff --git a/contrib/competitions/smt-comp/run-script-smtcomp-current b/contrib/competitions/smt-comp/run-script-smtcomp-current
index 715f3fc6c6628fe60eb20baeed9d7834bc10ed52..e891cf8cf1801ee2587bc45a819351ae5521b90c 100755 (executable)
--- 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
   ;;