From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Mon, 4 Jun 2018 19:30:28 +0000 (-0700)
Subject: [SMT-COMP] Add new logics to run-scripts (#2022)
X-Git-Tag: cvc5-1.0.0~4979
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=cd170ce1ce9883aac0ed4ccadd85b66111d14bed;p=cvc5.git

[SMT-COMP] Add new logics to run-scripts (#2022)
---

diff --git a/contrib/run-script-smtcomp2018 b/contrib/run-script-smtcomp2018
index 6bcc5f3d3..ff06fb933 100644
--- a/contrib/run-script-smtcomp2018
+++ b/contrib/run-script-smtcomp2018
@@ -51,7 +51,7 @@ 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)
+ALIA|AUFLIA|AUFLIRA|AUFNIRA|UF|UFIDL|UFLIA|UFLRA|UFNIA|UFDT|UFDTLIA|AUFDTLIA|AUFBVDTLIA|AUFNIA)
   # the following is designed for a run time of 20 min.
   # initial runs 1min
   trywith 30 --simplification=none --full-saturate-quant
@@ -82,6 +82,9 @@ ALIA|AUFLIA|AUFLIRA|AUFNIRA|UF|UFIDL|UFLIA|UFLRA|UFNIA|UFDT|UFDTLIA|AUFDTLIA|AUF
   trywith 240 --finite-model-find --decision=internal
   finishwith --full-saturate-quant
   ;;
+ABVFP|BVFP|FP)
+  finishwith --full-saturate-quant
+  ;;
 UFBV)
   # most problems in UFBV are essentially BV
   trywith 300 --full-saturate-quant --decision=internal
@@ -136,6 +139,15 @@ QF_SLIA)
   trywith 500 --strings-exp --rewrite-divk --lang=smt2.6.1
   finishwith --strings-exp --rewrite-divk --lang=smt2.6.1 --strings-fmf
   ;;
+QF_ABVFP)
+  finishwith
+  ;;
+QF_BVFP)
+  finishwith
+  ;;
+QF_FP)
+  finishwith
+  ;;
 *)
   # just run the default
   finishwith
diff --git a/contrib/run-script-smtcomp2018-application b/contrib/run-script-smtcomp2018-application
index 4bf2f6b91..58db84d36 100755
--- a/contrib/run-script-smtcomp2018-application
+++ b/contrib/run-script-smtcomp2018-application
@@ -49,6 +49,33 @@ QF_BV)
 QF_LIA)
   runcvc4 --tear-down-incremental=1 --unconstrained-simp
   ;;
+QF_UFBV)
+  runcvc4 --incremental
+  ;;
+QF_UF)
+  runcvc4 --incremental
+  ;;
+QF_AUFBV)
+  runcvc4 --incremental
+  ;;
+QF_ABV)
+  runcvc4 --incremental
+  ;;
+ABVFP)
+  runcvc4 --incremental
+  ;;
+BVFP)
+  runcvc4 --incremental
+  ;;
+QF_ABVFP)
+  runcvc4 --incremental
+  ;;
+QF_BVFP)
+  runcvc4 --incremental
+  ;;
+QF_FP)
+  runcvc4 --incremental
+  ;;
 *)
   # just run the default
   runcvc4 --incremental
diff --git a/contrib/run-script-smtcomp2018-unsat-cores b/contrib/run-script-smtcomp2018-unsat-cores
index 24933cf40..1454e7a8a 100644
--- a/contrib/run-script-smtcomp2018-unsat-cores
+++ b/contrib/run-script-smtcomp2018-unsat-cores
@@ -26,7 +26,7 @@ QF_NRA)
   finishwith --nl-ext --nl-ext-tplanes
   ;;
 # 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)
+ALIA|AUFLIA|AUFLIRA|AUFNIRA|UF|UFIDL|UFLIA|UFLRA|UFNIA|UFDT|UFDTLIA|AUFDTLIA|AUFBVDTLIA|AUFNIA|ABVFP|BVFP|FP)
   finishwith --full-saturate-quant
   ;;
 UFBV)
@@ -65,6 +65,15 @@ QF_AUFNIA)
 QF_ALIA)
   finishwith --decision=justification-stoponly --no-arrays-eager-index --arrays-eager-lemmas
   ;;
+QF_ABVFP)
+  finishwith
+  ;;
+QF_BVFP)
+  finishwith
+  ;;
+QF_FP)
+  finishwith
+  ;;
 *)
   # just run the default
   finishwith