From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Mon, 6 Jun 2022 19:19:16 +0000 (-0500)
Subject: Add MBQI to SMT comp script (#8858)
X-Git-Tag: cvc5-1.0.1~67
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=a1c8064e3113849ecc759b659f2a70e377f873e3;p=cvc5.git

Add MBQI to SMT comp script (#8858)

Also fixes 2 existing issues in the script (that @nafur pointed out).
---

diff --git a/contrib/competitions/smt-comp/run-script-smtcomp-current b/contrib/competitions/smt-comp/run-script-smtcomp-current
index 01aa78ba4..6980d31f2 100755
--- a/contrib/competitions/smt-comp/run-script-smtcomp-current
+++ b/contrib/competitions/smt-comp/run-script-smtcomp-current
@@ -88,7 +88,7 @@ ALIA|AUFLIA|AUFLIRA|AUFNIRA|UF|UFBVLIA|UFIDL|UFLIA|UFLRA|UFNIA|UFDT|UFDTLIA|AUFD
   trywith 30 --multi-trigger-cache --enum-inst
   trywith 30 --no-multi-trigger-linear --enum-inst
   # other 4 min
-  trywith 30 --pre-skolem-quant --enum-inst
+  trywith 30 --pre-skolem-quant=on --enum-inst
   trywith 30 --inst-when=full --enum-inst
   trywith 30 --no-e-matching --no-cbqi --enum-inst
   trywith 30 --enum-inst --quant-ind
@@ -97,7 +97,7 @@ ALIA|AUFLIA|AUFLIRA|AUFNIRA|UF|UFBVLIA|UFIDL|UFLIA|UFLRA|UFNIA|UFDT|UFDTLIA|AUFD
   trywith 30 --term-db-mode=relevant --enum-inst
   trywith 30 --enum-inst-interleave --enum-inst
   # finite model find 3 min
-  trywith 30 --finite-model-find --mbqi=none
+  trywith 30 --finite-model-find --fmf-mbqi=none
   trywith 30 --finite-model-find --decision=internal
   trywith 30 --finite-model-find --macros-quant --macros-quant-mode=all
   trywith 60 --finite-model-find --e-matching
@@ -107,14 +107,16 @@ ALIA|AUFLIA|AUFLIRA|AUFNIRA|UF|UFBVLIA|UFIDL|UFLIA|UFLRA|UFNIA|UFDT|UFDTLIA|AUFD
   ;;
 UFBV)
   # most problems in UFBV are essentially BV
-  trywith 300 --sygus-inst
+  trywith 150 --sygus-inst
+  trywith 150 --mbqi --no-cegqi --no-sygus-inst
   trywith 300 --enum-inst --cegqi-nested-qe --decision=internal
   trywith 30 --enum-inst --no-cegqi-innermost --global-negate
   finishwith --finite-model-find
   ;;
 ABV|BV)
-  trywith 120 --enum-inst
-  trywith 120 --sygus-inst
+  trywith 80 --enum-inst
+  trywith 80 --sygus-inst
+  trywith 80 --mbqi --no-cegqi --no-sygus-inst
   trywith 300 --enum-inst --cegqi-nested-qe --decision=internal
   trywith 30 --enum-inst --no-cegqi-bv
   trywith 30 --enum-inst --cegqi-bv-ineq=eq-slack
@@ -123,11 +125,13 @@ ABV|BV)
   ;;
 ABVFP|ABVFPLRA|BVFP|FP|NIA|NRA)
   trywith 300 --enum-inst --nl-ext-tplanes --fp-exp
+  trywith 60 --mbqi --no-cegqi --no-sygus-inst
   finishwith --sygus-inst --fp-exp
   ;;
 LIA|LRA)
   trywith 30 --enum-inst
   trywith 300 --enum-inst --cegqi-nested-qe
+  trywith 60 --mbqi --no-cegqi --no-sygus-inst
   finishwith --enum-inst --cegqi-nested-qe --decision=internal
   ;;
 QF_AUFBV)