Fixes to unsat core postprocessor (#5)

* Updated logics for this year on unsat core

* Bug fix: handle empty unsat core

There is no space after colon, so the old code didn't match

Co-authored-by: Jochen Hoenicke <[email protected]>

Author: aehyvari

unsat-core-track/process

@@ -56,24 +56,32 @@ set -u
 echo "ucpp-version=2019v0"
 
 # set validating solvers for each logic
+ABV="cvc4 z3"
 ABVFP="cvc4 z3"
+ABVFPLRA="cvc4"
 ALIA="cvc4 vampire z3"
-ANIA="cvc4 vampire z3"
-#AUFBVDTLIA="cvc4 z3"
+#ANIA="cvc4 vampire z3"
+AUFBVDTLIA="cvc4 z3"
 AUFDTLIA="cvc4 vampire z3"
+AUFDTLIRA="cvc4 vampire"
+AUFDTNIRA="cvc4 vampire"
+AUFFPDTLIRA="cvc4"
 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"
 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_ALIA="cvc4 z3 yices"
 QF_ANIA="cvc4 mathsat z3"
 QF_AUFBV="cvc4 z3 yices"
@@ -83,9 +91,9 @@ QF_AX="cvc4 z3 yices"
 QF_BV="cvc4 z3 yices"
 QF_BVFP="cvc4 z3"
 QF_BVFPLRA="cvc4 z3"
-#QF_DT="cvc4 z3"
+QF_DT="cvc4 z3"
 QF_FP="cvc4 z3"
-#QF_FPLRA="cvc4 z3"
+QF_FPLRA="cvc4 z3"
 QF_IDL="cvc4 z3 yices"
 QF_LIA="cvc4 z3 yices"
 QF_LIRA="cvc4 z3 yices"
@@ -94,19 +102,25 @@ QF_NIA="cvc4 mathsat z3"
 QF_NIRA="cvc4 mathsat z3"
 QF_NRA="cvc4 mathsat z3"
 QF_RDL="cvc4 z3 yices"
-#QF_S
-#QF_SLIA="cvc4 z3"
+QF_S="cvc4"
+QF_SLIA="cvc4"
 QF_UF="cvc4 z3 yices"
 QF_UFBV="cvc4 z3 yices"
+QF_UFFP="cvc4"
 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"
-#UFDT="cvc4 vampire z3"
-#UFDTLIA="cvc4 vampire z3"
+UFDT="cvc4 vampire z3"
+UFDTLIA="cvc4 vampire z3"
+UFDTLIRA="cvc4 vampire"
+UFDTNIA="cvc4 vampire"
+UFDTNIRA="cvc4 vampire"
+UFFPDTLIRA="cvc4"
+UFFPDTNIRA="cvc4"
 UFIDL="cvc4 vampire z3"
 UFLIA="cvc4 vampire z3"
 UFLRA="cvc4 vampire z3"
@@ -159,7 +173,7 @@ if [ "$CHECK_SAT_RESPONSE" == "unsat" ]; then
 		VALIDATION_SOLVERS=(${!LOGIC})
 		echo "parsable-unsat-core=true"
 		# size of unsat core was written as comment in the first line by the benchmark scrambler
-		SIZE_OF_UNSAT_CORE=$(head -n 1 ./unsat-core-validation-script.smt2 |sed -e 's/;; parsed //'|sed -e 's/ names:\ .*//')
+		SIZE_OF_UNSAT_CORE=$(head -n 1 ./unsat-core-validation-script.smt2 |sed -e 's/;; parsed \([0-9][0-9]*\) names:.*/\1/')
 		echo "size-unsat-core=$SIZE_OF_UNSAT_CORE"
 		REDUCTION=$((NUMBER_OF_ASSERT_COMMANDS - SIZE_OF_UNSAT_CORE))