From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 12 May 2021 14:38:59 +0000 (-0500)
Subject: Preliminary draft of changes for SMT comp 2021 (#6522)
X-Git-Tag: cvc5-1.0.0~1771
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=b016f603f2a3709faaf90008a09f2567d7283ff3;p=cvc5.git

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 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
   ;;