2020 unsat core postprocessor update (#7)

* Updated process, added new verifying solvers, and updated old verifying solvers to 2020 final submissions

Unified starexec run script names

Updated the validation solvers in readme and the makefile.

* Fixed cvc4 version to correspond to starexec id 28798

Author: aehyvari

Makefile

@@ -13,7 +13,7 @@ POSTPROCESSORS = SMT-COMP-2020-single-query-post-processor.tar.gz \
 	SMT-COMP-2020-incremental-post-processor.tar.gz \
 	SMT-COMP-2020-unsat-core-post-processor.tar.gz \
 	SMT-COMP-2020-model-validation-post-processor.tar.gz
-VALIDATION_SOLVERS=cvc4 mathsat vampire yices z3
+VALIDATION_SOLVERS=alt-ergo bitwuzla cvc4 mathsat ultimateeliminator+mathsat vampire yices z3
 
 all: $(POSTPROCESSORS)
 

unsat-core-track/README.md

@@ -15,13 +15,12 @@ unsatisfiable using a set of validating solvers built into the script.
 
 ### Setup
 
-1. Unpack all [validation solvers](validation_solvesr) and ensure that they
+1. Unpack all [validation solvers](validation_solvers) and ensure that they
    are available at
 ```bash
 ./validation_solvers/<solver>/bin/<solver>
 ```
-The solvers currently required by the script are `CVC4`, `MathSAT`, `Z3`, and
-`Vampire`.
+The solvers currently required by the script are `alt-ergo`, `bitwuzla`, `cvc4`, `mathsat`, `ultimateeliminator+mathsat`, `vampire`, `yices`, and `z3`.
 
 2. Ensure that the [scrambler](https://github.com/SMT-COMP/scrambler) is in
 the current directory as a compiled binary.

unsat-core-track/process

@@ -56,44 +56,44 @@ set -u
 echo "ucpp-version=2019v0"
 
 # set validating solvers for each logic
-ABV="cvc4 z3"
-ABVFP="cvc4 z3"
-ABVFPLRA="cvc4"
+ABV="cvc4 z3 ultimateeliminator+mathsat"
+ABVFP="cvc4 ultimateeliminator+mathsat"
+ABVFPLRA="cvc4 ultimateeliminator+mathsat"
 ALIA="cvc4 vampire z3"
 #ANIA="cvc4 vampire z3"
 AUFBVDTLIA="cvc4 z3"
 AUFDTLIA="cvc4 vampire z3"
-AUFDTLIRA="cvc4 vampire"
-AUFDTNIRA="cvc4 vampire"
-AUFFPDTLIRA="cvc4"
+AUFDTLIRA="cvc4 vampire alt-ergo"
+AUFDTNIRA="cvc4 vampire alt-ergo"
+AUFFPDTLIRA="cvc4 ultimateeliminator+mathsat"
 AUFLIA="cvc4 vampire z3"
 AUFLIRA="cvc4 vampire z3"
 AUFNIA="cvc4 vampire z3"
 AUFNIRA="cvc4 vampire z3"
-BV="cvc4 z3"
-BVFP="cvc4 z3"
-BVFPLRA="cvc4"
-FP="cvc4 z3"
-FPLRA=""
-LIA="cvc4 vampire z3"
+BV="cvc4 z3 ultimateeliminator+mathsat"
+BVFP="cvc4 ultimateeliminator+mathsat"
+BVFPLRA="cvc4 ultimateeliminator+mathsat"
+FP="cvc4 z3 ultimateeliminator+mathsat"
+FPLRA="cvc4 ultimateeliminator+mathsat"
+LIA="cvc4 ultimateeliminator+mathsat z3"
 LRA="cvc4 vampire z3"
 NIA="cvc4 vampire z3"
 NRA="cvc4 vampire z3"
 QF_ABV="cvc4 z3 yices"
-QF_ABVFP="cvc4 z3"
-QF_ABVFPLRA="cvc4"
+QF_ABVFP="cvc4 z3 mathsat"
+QF_ABVFPLRA="cvc4 mathsat"
 QF_ALIA="cvc4 z3 yices"
 QF_ANIA="cvc4 mathsat z3"
 QF_AUFBV="cvc4 z3 yices"
 QF_AUFLIA="cvc4 z3 yices"
 QF_AUFNIA="cvc4 mathsat z3"
 QF_AX="cvc4 z3 yices"
-QF_BV="cvc4 z3 yices"
-QF_BVFP="cvc4 z3"
-QF_BVFPLRA="cvc4 z3"
-QF_DT="cvc4 z3"
-QF_FP="cvc4 z3"
-QF_FPLRA="cvc4 z3"
+QF_BV="cvc4 z3 mathsat"
+QF_BVFP="cvc4 z3 mathsat"
+QF_BVFPLRA="cvc4 z3 mathsat"
+QF_DT="cvc4 z3 alt-ergo"
+QF_FP="cvc4 z3 mathsat"
+QF_FPLRA="cvc4 z3 mathsat"
 QF_IDL="cvc4 z3 yices"
 QF_LIA="cvc4 z3 yices"
 QF_LIRA="cvc4 z3 yices"
@@ -102,25 +102,25 @@ QF_NIA="cvc4 mathsat z3"
 QF_NIRA="cvc4 mathsat z3"
 QF_NRA="cvc4 mathsat z3"
 QF_RDL="cvc4 z3 yices"
-QF_S="cvc4"
-QF_SLIA="cvc4"
+#QF_S="cvc4"
+#QF_SLIA="cvc4"
 QF_UF="cvc4 z3 yices"
 QF_UFBV="cvc4 z3 yices"
-QF_UFFP="cvc4"
+QF_UFFP="cvc4 mathsat bitwuzla"
 QF_UFIDL="cvc4 z3 yices"
 QF_UFLIA="cvc4 z3 yices"
 QF_UFLRA="cvc4 z3 yices"
 QF_UFNIA="cvc4 z3 mathsat"
 QF_UFNRA="cvc4 z3 mathsat"
 UF="cvc4 vampire z3"
-UFBV="cvc4 z3"
+UFBV="cvc4 z3 ultimateeliminator+mathsat"
 UFDT="cvc4 vampire z3"
 UFDTLIA="cvc4 vampire z3"
-UFDTLIRA="cvc4 vampire"
-UFDTNIA="cvc4 vampire"
-UFDTNIRA="cvc4 vampire"
-UFFPDTLIRA="cvc4"
-UFFPDTNIRA="cvc4"
+UFDTLIRA="cvc4 alt-ergo"
+UFDTNIA="cvc4 vampire alt-ergo"
+UFDTNIRA="cvc4 vampire alt-ergo"
+UFFPDTLIRA="cvc4 ultimateeliminator+mathsat"
+UFFPDTNIRA="cvc4 ultimateeliminator+mathsat"
 UFIDL="cvc4 vampire z3"
 UFLIA="cvc4 vampire z3"
 UFLRA="cvc4 vampire z3"