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

diff --git a/contrib/run-script-smtcomp2018 b/contrib/run-script-smtcomp2018
index 6bcc5f3d3b0faca49d5add2db3bfcae859575d24..ff06fb9331b77a5a78f9dc5fd0945f25ccab77ec 100644 (file)
--- 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 4bf2f6b918bc043c673764d40d7eaafdbc4ea31f..58db84d36cbc96d94767a18db7fc919fa5771d0f 100755 (executable)
--- 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 24933cf4054fa0dd22bd3c1bf9499cb1f139e3a0..1454e7a8a47e3d70fd62287c60b5c96aac2ff157 100644 (file)
--- 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