Generate new input certificates

SMT-COMP · Aug 9, 2024 · 0b669c0 · 0b669c0
1 parent 56e6c36
commit 0b669c0
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git a/data/latex-certificates/input_for_certificates.tex b/data/latex-certificates/input_for_certificates.tex
@@ -6,7 +6,7 @@
 \newpage
 \MakeOnePage{COLIBRI}{}{}{\withtrack{QF\_ABVFPLRA}{\unsat}, \withtrack{QF\_FP}{\fast}, \withtrack{QF\_FPLRA}{\unsat,\fast}}{}{s}
 \newpage
-\MakeOnePage{cvc5}{\withtrack{Biggest Lead}{\seq,\paral,\sat,\unsat,\fast}, \withtrack{Largest Contribution}{\seq,\paral,\sat,\unsat,\fast}}{\withtrack{Arith}{\seq,\paral,\unsat,\inc}, \withtrack{Bitvec}{\seq,\paral,\unsat,\inc,\uc}, \withtrack{Equality}{\seq,\paral,\sat,\unsat,\fast,\inc}, \withtrack{Equality\_LinearArith}{\seq,\paral,\sat,\unsat,\fast,\inc}, \withtrack{Equality\_MachineArith}{\seq,\paral,\sat,\unsat,\fast}, \withtrack{Equality\_NonLinearArith}{\seq,\paral,\sat,\unsat,\fast,\inc}, \withtrack{FPArith}{\uc}, \withtrack{QF\_Datatypes}{\sat,\uc}, \withtrack{QF\_Equality\_LinearArith}{\uc\textsuperscript\paral}, \withtrack{QF\_Equality\_NonLinearArith}{\unsat,\inc,\uc\textsuperscript\seq,\mv}, \withtrack{QF\_FPArith}{\mv}, \withtrack{QF\_LinearIntArith}{\unsat}, \withtrack{QF\_LinearRealArith}{\unsat}, \withtrack{QF\_NonLinearRealArith}{\unsat}, \withtrack{QF\_Strings}{\uc}}{\withtrack{ANIA}{\uc}, \withtrack{AUFBV}{\uc\textsuperscript\paral}, \withtrack{AUFBVDTLIA}{\uc}, \withtrack{AUFBVDTNIRA}{\uc}, \withtrack{AUFDTLIRA}{\uc\textsuperscript\seq}, \withtrack{AUFFPDTNIRA}{\uc}, \withtrack{AUFLIRA}{\uc\textsuperscript\seq}, \withtrack{AUFNIA}{\uc\textsuperscript\paral}, \withtrack{BVFPLRA}{\unsat}, \withtrack{FP}{\fast}, \withtrack{LIA}{\sat,\fast}, \withtrack{NIA}{\sat}, \withtrack{QF\_AUFLIA}{\inc,\uc\textsuperscript\seq}, \withtrack{QF\_AX}{\mv}, \withtrack{QF\_FP}{\sat,\uc}, \withtrack{QF\_IDL}{\uc}, \withtrack{QF\_LIA}{\mv}, \withtrack{QF\_SNIA}{\seq,\paral,\sat,\fast}, \withtrack{QF\_UFBVDT}{\seq,\paral,\unsat,\fast,\uc,\mv}, \withtrack{QF\_UFDT}{\seq,\paral,\mv}, \withtrack{QF\_UFDTLIRA}{\seq,\paral,\sat,\unsat,\fast,\uc\textsuperscript\seq,\mv}, \withtrack{QF\_UFDTNIA}{\seq,\paral,\sat,\fast}, \withtrack{QF\_UFFPDTNIRA}{\seq,\paral,\sat,\unsat,\fast}, \withtrack{QF\_UFLRA}{\inc,\uc\textsuperscript\seq}, \withtrack{UFDT}{\uc\textsuperscript\seq}, \withtrack{UFDTLIA}{\uc\textsuperscript\seq}, \withtrack{UFDTNIA}{\uc\textsuperscript\seq}, \withtrack{UFFPDTNIRA}{\uc}, \withtrack{UFIDL}{\uc\textsuperscript\seq}, \withtrack{UFLRA}{\uc}, \withtrack{UFNIRA}{\uc\textsuperscript\seq}}{s}{s}
+\MakeOnePage{cvc5}{\withtrack{Biggest Lead}{\seq,\paral,\sat,\unsat,\fast}, \withtrack{Largest Contribution}{\seq,\paral,\sat,\unsat,\fast}}{\withtrack{Arith}{\seq,\paral,\unsat,\inc}, \withtrack{Bitvec}{\seq,\paral,\unsat,\inc,\uc}, \withtrack{Equality}{\seq,\paral,\sat,\unsat,\fast,\inc}, \withtrack{Equality\_LinearArith}{\seq,\paral,\sat,\unsat,\fast,\inc}, \withtrack{Equality\_MachineArith}{\seq,\paral,\sat,\unsat,\fast}, \withtrack{Equality\_NonLinearArith}{\seq,\paral,\sat,\unsat,\fast,\inc}, \withtrack{FPArith}{\uc}, \withtrack{QF\_Datatypes}{\sat,\uc}, \withtrack{QF\_Equality\_LinearArith}{\uc\textsuperscript\paral}, \withtrack{QF\_Equality\_NonLinearArith}{\unsat,\inc,\uc\textsuperscript\seq,\mv}, \withtrack{QF\_FPArith}{\mv}, \withtrack{QF\_LinearIntArith}{\unsat}, \withtrack{QF\_LinearRealArith}{\unsat}, \withtrack{QF\_NonLinearRealArith}{\unsat}, \withtrack{QF\_Strings}{\uc}}{\withtrack{ANIA}{\uc}, \withtrack{AUFBV}{\uc\textsuperscript\paral}, \withtrack{AUFBVDTLIA}{\uc}, \withtrack{AUFBVDTNIRA}{\uc}, \withtrack{AUFDTLIRA}{\uc\textsuperscript\seq}, \withtrack{AUFFPDTNIRA}{\uc}, \withtrack{AUFLIRA}{\uc\textsuperscript\seq}, \withtrack{AUFNIA}{\uc\textsuperscript\paral}, \withtrack{BVFPLRA}{\unsat}, \withtrack{FP}{\fast}, \withtrack{LIA}{\sat,\fast}, \withtrack{NIA}{\sat}, \withtrack{QF\_AUFLIA}{\inc,\uc\textsuperscript\seq}, \withtrack{QF\_AX}{\mv}, \withtrack{QF\_BVFP}{\inc}, \withtrack{QF\_FP}{\sat,\uc}, \withtrack{QF\_IDL}{\uc}, \withtrack{QF\_LIA}{\mv}, \withtrack{QF\_SNIA}{\seq,\paral,\sat,\fast}, \withtrack{QF\_UFBVDT}{\seq,\paral,\unsat,\fast,\uc,\mv}, \withtrack{QF\_UFDT}{\seq,\paral,\mv}, \withtrack{QF\_UFDTLIRA}{\seq,\paral,\sat,\unsat,\fast,\uc\textsuperscript\seq,\mv}, \withtrack{QF\_UFDTNIA}{\seq,\paral,\sat,\fast}, \withtrack{QF\_UFFPDTNIRA}{\seq,\paral,\sat,\unsat,\fast}, \withtrack{QF\_UFLRA}{\inc,\uc\textsuperscript\seq}, \withtrack{UFDT}{\uc\textsuperscript\seq}, \withtrack{UFDTLIA}{\uc\textsuperscript\seq}, \withtrack{UFDTNIA}{\uc\textsuperscript\seq}, \withtrack{UFFPDTNIRA}{\uc}, \withtrack{UFIDL}{\uc\textsuperscript\seq}, \withtrack{UFLRA}{\uc}, \withtrack{UFNIRA}{\uc\textsuperscript\seq}}{s}{s}
 \newpage
 \MakeOnePage{iProver v3.9}{}{}{\withtrack{ALIA}{\paral,\unsat}, \withtrack{UF}{\fast}, \withtrack{UFNIRA}{\seq,\unsat}}{}{s}
 \newpage

diff --git a/smtcomp/certificates.py b/smtcomp/certificates.py
@@ -218,7 +218,7 @@ def generate_certificates(
         result = page.Podium.model_validate_json(file.read_text()).root
 
         match result:
-            case page.Summary():
+            case page.PodiumSummaryResults():
                 print("Useless: ", file)
                 continue
             case page.PodiumCrossDivision():