Final update to SMT-COMP 2021 options (#6739)

This commit:

- Disables `--tear-down-incremental=X` for the competition since
  it currently does not work correctly on master and a fixed version did
  not show significant benefits.
- Changes the occurrences of `--nl-ext` to `--nl-ext=full` because it
  is now a mode option.
- Removes the use of `--bv-assert-input` because the option currently
  has some issues in incremental mode (#6738)
- Removes the use of `--bitblast=eager` for the model validation track
  because it produces invalid models (#6741)

diff --git a/contrib/competitions/smt-comp/run-script-smtcomp-current b/contrib/competitions/smt-comp/run-script-smtcomp-current
index ecc6ce5fe4f097384c5e48b31c663ed769c1a50c..9b4f534b017c0fe11dc62e3ad1dee89e95e4146b 100755 (executable)
--- a/contrib/competitions/smt-comp/run-script-smtcomp-current
+++ b/contrib/competitions/smt-comp/run-script-smtcomp-current
@@ -1,6 +1,6 @@
 #!/bin/bash
 
-cvc5=./cvc5
+cvc5=$(dirname "$(readlink -f "$0")")/cvc5
 bench="$1"
 
 # Output other than "sat"/"unsat" is either written to stderr or to "err.log"
@@ -75,7 +75,7 @@ QF_NRA)
   finishwith --decision=internal --nl-ext=none
   ;;
 # 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|UFFPDTLIRA|UFFPDTNIRA)
+ALIA|AUFLIA|AUFLIRA|AUFNIRA|UF|UFBVLIA|UFIDL|UFLIA|UFLRA|UFNIA|UFDT|UFDTLIA|AUFDTLIA|AUFBV|AUFBVDTLIA|AUFBVFP|AUFNIA|UFFPDTLIRA|UFFPDTNIRA)
   # initial runs 1 min
   trywith 30 --simplification=none --full-saturate-quant
   trywith 30 --no-e-matching --full-saturate-quant
@@ -112,7 +112,7 @@ UFBV)
   trywith 30 --full-saturate-quant --no-cegqi-innermost --global-negate
   finishwith --finite-model-find
   ;;
-BV)
+ABV|BV)
   trywith 120 --full-saturate-quant
   trywith 120 --sygus-inst
   trywith 300 --full-saturate-quant --cegqi-nested-qe --decision=internal
@@ -121,7 +121,7 @@ BV)
   # finish 10min
   finishwith --full-saturate-quant --no-cegqi-innermost --global-negate
   ;;
-ABVFP|BVFP|FP|NIA|NRA)
+ABVFP|ABVFPLRA|BVFP|FP|NIA|NRA)
   trywith 300 --full-saturate-quant --nl-ext-tplanes --fp-exp
   finishwith --sygus-inst --fp-exp
   ;;
@@ -131,8 +131,8 @@ LIA|LRA)
   finishwith --full-saturate-quant --cegqi-nested-qe --decision=internal
   ;;
 QF_AUFBV)
-  trywith 600 --ite-simp
-  finishwith --decision=justification-stoponly --ite-simp
+  trywith 600
+  finishwith --decision=justification-stoponly
   ;;
 QF_ABV)
   trywith 50 --ite-simp --simp-with-care --repeat-simp --arrays-weak-equiv

diff --git a/contrib/competitions/smt-comp/run-script-smtcomp-current-incremental b/contrib/competitions/smt-comp/run-script-smtcomp-current-incremental
index 21bb2f6e0b60cd87e6c8d8dabb1cfa6d4bbcd5e7..79df91d69cfd42e999d80f645f1c905f9528e015 100755 (executable)
--- a/contrib/competitions/smt-comp/run-script-smtcomp-current-incremental
+++ b/contrib/competitions/smt-comp/run-script-smtcomp-current-incremental
@@ -1,6 +1,6 @@
 #!/bin/bash
 
-cvc5=./cvc5
+cvc5=$(dirname "$(readlink -f "$0")")/cvc5
 
 line=""
 while [[ -z "$line" ]]; do
@@ -26,50 +26,20 @@ function runcvc5 {
   # we run in this way for line-buffered input, otherwise memory's a
   # concern (plus it mimics what we'll end up getting from an
   # application-track trace runner?)
-  $cvc5 --force-logic="$logic" -L smt2.6 --print-success --no-type-checking --no-interactive "$@" <&0-
+  $cvc5 --incremental --force-logic="$logic" -L smt2.6 --print-success --no-type-checking --no-interactive "$@" <&0-
 }
 
 case "$logic" in
 
-ALIA|ANIA|AUFNIRA|LIA|LRA|QF_ALIA|QF_ANIA|QF_AUFBVLIA|QF_AUFBVNIA|QF_LIA|QF_LRA|QF_NIA|QF_UFBVLIA|QF_UFLIA|QF_UFLRA|QF_UFNIA|UFLRA)
-  runcvc5 --tear-down-incremental=1
-  ;;
 QF_AUFLIA)
-  runcvc5 --tear-down-incremental=1 --no-arrays-eager-index --arrays-eager-lemmas
+  runcvc5 --no-arrays-eager-index --arrays-eager-lemmas
   ;;
 QF_BV)
-  runcvc5 --incremental --bitblast=eager --bv-assert-input
-  ;;
-QF_UFBV)
-  runcvc5 --incremental --bv-assert-input
-  ;;
-QF_UF)
-  runcvc5 --incremental
-  ;;
-QF_AUFBV)
-  runcvc5 --incremental --bv-assert-input
-  ;;
-QF_ABV)
-  runcvc5 --incremental --bv-assert-input
-  ;;
-ABVFP)
-  runcvc5 --incremental
-  ;;
-BVFP)
-  runcvc5 --incremental
-  ;;
-QF_ABVFP)
-  runcvc5 --incremental
-  ;;
-QF_BVFP)
-  runcvc5 --incremental
-  ;;
-QF_FP)
-  runcvc5 --incremental
+  runcvc5 --bitblast=eager
   ;;
 *)
   # just run the default
-  runcvc5 --incremental
+  runcvc5
   ;;
 
 esac

diff --git a/contrib/competitions/smt-comp/run-script-smtcomp-current-model-validation b/contrib/competitions/smt-comp/run-script-smtcomp-current-model-validation
index fe8d4ae440497b744cab7226a76579d04810b8b4..0998e99490a724e46f304c874ed98e7d99c2e7cf 100755 (executable)
--- a/contrib/competitions/smt-comp/run-script-smtcomp-current-model-validation
+++ b/contrib/competitions/smt-comp/run-script-smtcomp-current-model-validation
@@ -1,6 +1,6 @@
 #!/bin/bash
 
-cvc5=./cvc5
+cvc5=$(dirname "$(readlink -f "$0")")/cvc5
 bench="$1"
 
 logic=$(expr "$(grep -m1 '^[^;]*set-logic' "$bench")" : ' *(set-logic  *\([A-Z_]*\) *) *$')
@@ -20,7 +20,7 @@ QF_LIA)
   finishwith --miplib-trick --miplib-trick-subs=4 --use-approx --lemmas-on-replay-failure --replay-early-close-depth=4 --replay-lemma-reject-cut=128 --replay-reject-cut=512 --use-soi --pb-rewrites --ite-simp --simp-ite-compress
   ;;
 QF_BV)
-  finishwith --bitblast=eager --bv-assert-input
+  finishwith --bv-assert-input
   ;;
 *)
   # just run the default

diff --git a/contrib/competitions/smt-comp/run-script-smtcomp-current-unsat-cores b/contrib/competitions/smt-comp/run-script-smtcomp-current-unsat-cores
index e9753781dfe241421c71a84f38ccaf26cf4e3e2f..75e3bfc8270cd384dbc32608279cccc1ae90b115 100755 (executable)
--- a/contrib/competitions/smt-comp/run-script-smtcomp-current-unsat-cores
+++ b/contrib/competitions/smt-comp/run-script-smtcomp-current-unsat-cores
@@ -1,6 +1,6 @@
 #!/bin/bash
 
-cvc5=./cvc5
+cvc5=$(dirname "$(readlink -f "$0")")/cvc5
 bench="$1"
 
 logic=$(expr "$(grep -m1 '^[^;]*set-logic' "$bench")" : ' *(set-logic  *\([A-Z_]*\) *) *$')
@@ -20,10 +20,7 @@ QF_LIA)
   finishwith --miplib-trick --miplib-trick-subs=4 --use-approx --lemmas-on-replay-failure --replay-early-close-depth=4 --replay-lemma-reject-cut=128 --replay-reject-cut=512 --use-soi
   ;;
 QF_NIA)
-  finishwith --nl-ext --nl-ext-tplanes
-  ;;
-QF_NRA)
-  finishwith --nl-ext --nl-ext-tplanes
+  finishwith --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|AUFNIA|ABVFP|BVFP|FP)