2026 results (#297)

* feat: Add command for computing contribution of derived solvers.

* feat: Add results for all tracks except Parallel and Cloud.

* a few adjustments for 2026 result presentation

* fixing CI

* feat: New derived solver scoring for most of the tracks.

* chore: Fix typing.

* chore: Enable result generation.

* chore: Show results page.

* feat: Visually distinguish non-eligible solvers in the results.

* fix: Allow generated HTML pages.

* fix: Use only result files for cerfiticates (ignore e.g. charts)

* feat: Only consider competitive solvers for largest_contribution.

* feat: Derived score solving for Sequential and 24s scores.

* feat: Derived solver scoring for Overal Best score.

* chore: Lint.

* feat: Show PAR2 scores and base solver ratio on the website.

* chore: Update certificates for 2026.

* fix: Remove double Winners heading.

* chore: Update result dates.

* feat: Make the non-eligible solvers less visible.

* chore: Enable cache generation.

---------

Co-authored-by: Martin Jonáš <martin.jonas@mail.muni.cz>
Co-authored-by: Dominik Winterer <domwinterer@gmail.com>

Author: 3 people

Makefile

@@ -19,7 +19,7 @@ test: generation ## Test the code with pytest
 	@echo "🚀 Testing code: Running pytest"
 	@poetry run pytest
 
-generation: submission-generation participant-data track-data division-track-data # results-generation charts-generation ## Files generation for the website
+generation: submission-generation participant-data track-data division-track-data results-generation charts-generation ## Files generation for the website
 
 .PHONY: build
 build: clean-build ## Build wheel file using poetry
@@ -81,8 +81,8 @@ results-generation:
 	@poetry run smtcomp export-results-pages data Incremental
 	# @echo "🚀 Generating results to web/content/results for Cloud"
 	# @poetry run smtcomp export-results-pages data Cloud
-	@echo "🚀 Generating results to web/content/results for Parallel"
-	@poetry run smtcomp export-results-pages data Parallel
+	# @echo "🚀 Generating results to web/content/results for Parallel"
+	# @poetry run smtcomp export-results-pages data Parallel
 
 charts-generation:
 	@echo "🚀 Generating results to web/content/results for SingleQuery"
@@ -95,13 +95,13 @@ charts-generation:
 	@poetry run smtcomp generate-website-graphics data Incremental
 	# @echo "🚀 Generating results to web/content/results for Cloud"
 	# @poetry run smtcomp generate-website-graphics data Cloud
-	@echo "🚀 Generating results to web/content/results for Parallel"
-	@poetry run smtcomp generate-website-graphics data Parallel
+	# @echo "🚀 Generating results to web/content/results for Parallel"
+	# @poetry run smtcomp generate-website-graphics data Parallel
 
 
 cache:
-	# @echo "🚀 Generating cache"
-	# @poetry run smtcomp create-cache data
+	@echo "🚀 Generating cache"
+	@poetry run smtcomp create-cache data
 
 hugo-server:
 	(cd web; hugo server)

data/latex-certificates/gen_certificates_ornament.tex

@@ -73,7 +73,7 @@
     \vspace{1cm}
     \begin{tikzpicture}
       \node [align=center]
-              {\resizebox{10cm}{!}{\Huge\textsc{SMT-COMP 2025}}};
+              {\resizebox{10cm}{!}{\Huge\textsc{SMT-COMP 2026}}};
     \end{tikzpicture}
     \end{minipage}
     \vspace{1.55cm}
@@ -119,17 +119,15 @@
 %    \scalebox{.7}{
     {\tiny
     \begin{tabular}{ccccccc}
-        \includegraphics[scale=0.25,trim=1.5cm 2.75cm 0pt 0pt]{FB-signature.png} &&
-        \includegraphics[scale=0.06,trim=0pt 0.20cm 0pt 0pt]{DD-Signature.png} &&
-        \includegraphics[scale=0.4,trim=1.5pt 2.75cm 0pt 0pt]{MJ-Signature.png} &&
-        \includegraphics[scale=0.4,trim=0pt 23pt 0pt 0pt]{DW-Signature.png}\\
+       \includegraphics[scale=0.4,trim=1.5pt 2.75cm 0pt 0pt]{MJ-Signature.png} &&
+       \includegraphics[scale=0.1,trim=1.5pt 3.25cm 0pt 0pt]{TK-Signature.png} &&
+       \includegraphics[scale=0.4,trim=0pt 23pt 0pt 0pt]{DW-Signature.png}\\
     \cline{1-1}
     \cline{3-3}
     \cline{5-5}
-    \cline{7-7}
     \\ \
-    François Bobot & & David Déharbe  & & Martin Jon\'{a}\v{s} & & Dominik Winterer  \\
-    Organizer & & Organizer & & Chair & & Organizer \\
+    Martin Jon\'{a}\v{s} & & Tom\'{a}\v{s} Kol\'{a}rik & & Dominik Winterer  \\
+    Organizer & & Organizer & & Chair \\
     \end{tabular}
     }}
     \end{myframe}

data/results-inc-2026.json.gz

@@ -215,8 +215,8 @@ def generate_certificates(
     list_dir.sort()
     for result_basename in list_dir:
         file = website_results / result_basename
-        if not file.is_file():
-            break
+        if not file.is_file() or file.suffix != ".md":
+            continue
 
         result = page.Podium.model_validate_json(file.read_text()).root
 

data/results-mv-2026.json.gz

@@ -1520,20 +1520,6 @@ class Config:
     Benchmarks to remove after running the solvers. Can be used when the selection has already been done.
     """
 
-    """
-    Solver -> Base solver map for 2025
-    TODO: refactor this into Submission
-    """
-    baseSolverMap2025 = {
-        "Bitwuzla-MachBV": "Bitwuzla-MachBV-base",
-        "Z3-Inc-Z3++": "Z3-Inc-Z3++-base",
-        "Z3-Noodler-Mocha": "Z3-Noodler-Mocha-base",
-        "Z3-Owl": "Z3-Owl-base",
-        "Z3-Noodler": "Z3-Noodler-base",
-        "z3siri": "z3siri-base",
-        "Z3-alpha": "Z3-alpha-base",
-    }
-
     def __init__(self, data: Path | None) -> None:
         self.id = self.__class__.__next_id__
         self.__class__.__next_id__ += 1

data/results-sq-2026.json.gz

@@ -108,6 +108,9 @@ class PodiumStep(BaseModel):
     abstained: int
     timeout: int
     memout: int
+    par2score: float_6dig
+    par2scoreBase: float_6dig | None
+    eligibleForWinning: bool
 
 
 class PodiumDivision(BaseModel):
@@ -149,6 +152,7 @@ class PodiumStepOverallScore(BaseModel):
     contribution: float_6dig  # nn_D * log10 N_D
     division: str
     tieBreakTimeScore: float_6dig
+    eligibleForWinning: bool
 
 
 class PodiumBestOverall(BaseModel):
@@ -240,25 +244,37 @@ class Podium(RootModel):
     root: PodiumDivision | PodiumCrossDivision | PodiumSummaryResults = Field(..., discriminator="layout")
 
 
-def podium_steps(config: defs.Config, podium: List[dict[str, Any]] | None) -> List[PodiumStep]:
+def podium_steps(config: defs.Config, podium: List[dict[str, Any]] | None, scoring: str) -> List[PodiumStep]:
+    def par2(s: dict[str, Any]) -> Any:
+        if scoring == smtcomp.scoring.Kind.seq.name:
+            return s["cpu_time_score"] + 2 * config.cpuCores * config.timelimit_s * s["unsolved"]
+        elif scoring == smtcomp.scoring.Kind.twentyfour.name:
+            return s["wallclock_time_score"] + 2 * 24 * s["unsolved"]
+        else:
+            return s["wallclock_time_score"] + 2 * config.timelimit_s * s["unsolved"]
+
     if podium is None:
         return []
     else:
         podiums = []
-        non_competitive = []
+        base_solvers = []
         for s in podium:
-            cscore = s["correctly_solved_score"]
-            delta = 0
-            derived_solver = defs.Config.baseSolverMap2025.get(s["solver"], "")
-            if derived_solver != "":
-                for sprime in podium:
-                    if sprime["solver"] == defs.Config.baseSolverMap2025.get(s["solver"], ""):
-                        delta = cscore - sprime["correctly_solved_score"]
-                        break
+            base = None
+            for sprime in podium:
+                if sprime["solver"] == s["solver"] + "-base":
+                    base = sprime
+                    break
+
+            solver_par2 = par2(s)
+            base_par2 = None if base is None else par2(base)
+            eligible = s["solver"] in config.competitive_solvers and (
+                base_par2 is None or solver_par2 <= 0.9 * base_par2
+            )
+            delta = 0 if base is None else s["correctly_solved_score"] - base["correctly_solved_score"]
 
             ps = PodiumStep(
                 name=s["solver"],
-                baseSolver=derived_solver,
+                baseSolver=base["solver"] if base is not None else "",
                 deltaBaseSolver=delta,
                 competing="yes" if s["solver"] in config.competitive_solvers else "no",
                 errorScore=s["error_score"],
@@ -272,29 +288,32 @@ def podium_steps(config: defs.Config, podium: List[dict[str, Any]] | None) -> Li
                 abstained=s["abstained"],
                 timeout=s["timeout"],
                 memout=s["memout"],
+                par2score=solver_par2,
+                par2scoreBase=base_par2,
+                eligibleForWinning=eligible,
             )
 
-            if not s["solver"] in config.competitive_solvers:
-                non_competitive.append(ps)
+            if s["solver"].endswith("-base"):
+                base_solvers.append(ps)
             else:
                 podiums.append(ps)
 
-        return podiums + non_competitive
+        return podiums + base_solvers
 
 
 def make_podium(
     config: defs.Config, d: dict[str, Any], for_division: bool, track: defs.Track, results: pl.LazyFrame
 ) -> PodiumDivision:
-    def get_winner(l: List[dict[str, str]] | None) -> str:
+    def get_winner(l: List[PodiumStep] | None) -> str:
         if l is None or not l:
             return "-"
 
-        l = [e for e in l if e["solver"] in config.competitive_solvers]
+        l = [s for s in l if s.eligibleForWinning]
 
-        if l is None or not l or l[0]["correctly_solved_score"] == 0:
+        if l is None or not l or l[0].correctScore == 0:
             return "-"
         else:
-            return l[0]["solver"]
+            return l[0].name
 
     def is_competitive_division(results: pl.LazyFrame, division: int, for_division: bool) -> bool:
         """
@@ -312,7 +331,7 @@ def is_competitive_division(results: pl.LazyFrame, division: int, for_division:
         )
 
         # Avoid solvers of the same solver family under the assumption
-        # of the following format: <solver-family>-<suffix> (holds for SMT-COMP 2025)
+        # of the following format: <solver-family>-<suffix> (holds for SMT-COMP 2025/26)
         # TODO: improve this criterion in the future
         return len(set([sol.split("-")[0].lower() for sol in solvers])) >= 2
 
@@ -325,15 +344,25 @@ def is_competitive_division(results: pl.LazyFrame, division: int, for_division:
         competitive_division = is_competitive_division(results, d["logic"], for_division)
         logics = dict()
 
+    steps: dict[str, List[Any]] = {}
+
     if (track == defs.Track.Cloud) | (track == defs.Track.Parallel):
-        winner_seq = "-"
-        steps_seq = []
+        steps[smtcomp.scoring.Kind.seq.name] = []
     else:
-        winner_seq = get_winner(d[smtcomp.scoring.Kind.seq.name])
-        steps_seq = podium_steps(config, d[smtcomp.scoring.Kind.seq.name])
+        steps[smtcomp.scoring.Kind.seq.name] = podium_steps(
+            config, d[smtcomp.scoring.Kind.seq.name], smtcomp.scoring.Kind.seq.name
+        )
+
+    for score in (
+        smtcomp.scoring.Kind.par.name,
+        smtcomp.scoring.Kind.sat.name,
+        smtcomp.scoring.Kind.unsat.name,
+        smtcomp.scoring.Kind.twentyfour.name,
+    ):
+        steps[score] = podium_steps(config, d[score], score)
 
     return PodiumDivision(
-        resultdate="2025-08-11",
+        resultdate="2026-07-25",
         year=config.current_year,
         divisions=f"divisions_{config.current_year}",
         is_competitive=competitive_division,
@@ -345,16 +374,16 @@ def is_competitive_division(results: pl.LazyFrame, division: int, for_division:
         time_limit=config.timelimit_s,
         mem_limit=config.memlimit_M,
         logics=dict(sorted(logics.items())),
-        winner_seq=winner_seq,
-        winner_par=get_winner(d[smtcomp.scoring.Kind.par.name]),
-        winner_sat=get_winner(d[smtcomp.scoring.Kind.sat.name]),
-        winner_unsat=get_winner(d[smtcomp.scoring.Kind.unsat.name]),
-        winner_24s=get_winner(d[smtcomp.scoring.Kind.twentyfour.name]),
-        sequential=steps_seq,
-        parallel=podium_steps(config, d[smtcomp.scoring.Kind.par.name]),
-        sat=podium_steps(config, d[smtcomp.scoring.Kind.sat.name]),
-        unsat=podium_steps(config, d[smtcomp.scoring.Kind.unsat.name]),
-        twentyfour=podium_steps(config, d[smtcomp.scoring.Kind.twentyfour.name]),
+        winner_seq=get_winner(steps[smtcomp.scoring.Kind.seq.name]),
+        winner_par=get_winner(steps[smtcomp.scoring.Kind.par.name]),
+        winner_sat=get_winner(steps[smtcomp.scoring.Kind.sat.name]),
+        winner_unsat=get_winner(steps[smtcomp.scoring.Kind.unsat.name]),
+        winner_24s=get_winner(steps[smtcomp.scoring.Kind.twentyfour.name]),
+        sequential=steps[smtcomp.scoring.Kind.seq.name],
+        parallel=steps[smtcomp.scoring.Kind.par.name],
+        sat=steps[smtcomp.scoring.Kind.sat.name],
+        unsat=steps[smtcomp.scoring.Kind.unsat.name],
+        twentyfour=steps[smtcomp.scoring.Kind.twentyfour.name],
     )
 
 
@@ -521,7 +550,7 @@ def get_winner(l: List[PodiumStepBiggestLead] | None) -> str:
         winner_seq = get_winner(sequential)
 
     return PodiumBiggestLead(
-        resultdate="2025-08-11",
+        resultdate="2026-07-25",
         year=config.current_year,
         track=track,
         results=f"results_{config.current_year}",
@@ -567,6 +596,7 @@ def normalized_correctness_score(
                     contribution=nn_D * (math.log10(N_D) if N_D > 0 else 0),
                     tieBreakTimeScore=sol_in_div.CPUScore if k == smtcomp.scoring.Kind.seq else sol_in_div.WallScore,
                     division=division,
+                    eligibleForWinning=sol_in_div.eligibleForWinning,
                 )
             )
         podiumSteps = sorted(podiumSteps, key=lambda x: (x.contribution, x.tieBreakTimeScore), reverse=True)
@@ -619,11 +649,19 @@ def get_winner(
         if l is None or not l:
             return ("-", 0.0)
         else:
-            podium: DefaultDict[str, Dict[str, float]] = defaultdict(lambda: {"score": 0.0, "tie_break_time": 0.0})
+            podium: DefaultDict[str, Dict[str, Any]] = defaultdict(
+                lambda: {"score": 0.0, "tie_break_time": 0.0, "eligibleForWinning": False}
+            )
             for entry in l:
                 podium[entry.name]["score"] += entry.contribution
                 podium[entry.name]["tie_break_time"] += entry.tieBreakTimeScore
-            winner, winner_data = max(podium.items(), key=lambda item: (item[1]["score"], -item[1]["tie_break_time"]))
+                podium[entry.name]["eligibleForWinning"] = (
+                    podium[entry.name]["eligibleForWinning"] or entry.eligibleForWinning
+                )
+            winner, winner_data = max(
+                filter(lambda i: i[1]["eligibleForWinning"], podium.items()),
+                key=lambda item: (item[1]["score"], -item[1]["tie_break_time"]),
+            )
             return (winner, winner_data["score"])
 
     sequential = normalized_correctness_score(data, scores, track, smtcomp.scoring.Kind.seq)
@@ -639,7 +677,7 @@ def get_winner(
         winner_seq = get_winner(sequential, scores, data, track)
 
     return PodiumBestOverall(
-        resultdate="2025-08-11",
+        resultdate="2026-07-25",
         year=config.current_year,
         track=track,
         results=f"results_{config.current_year}",
@@ -737,7 +775,7 @@ def timeScore(vws_step: PodiumStep) -> float:
         steps_seq = ld[smtcomp.scoring.Kind.seq]
 
     return PodiumLargestContribution(
-        resultdate="2025-08-11",
+        resultdate="2026-07-25",
         year=config.current_year,
         track=track,
         results=f"results_{config.current_year}",
@@ -786,7 +824,7 @@ def largest_contribution(config: defs.Config, scores: pl.LazyFrame, track: defs.
     virtual_datas = sq_generate_datas(config, virtual_scores, for_division, track)
 
     # For each solver Compute virtual solver without the solver
-    solvers = scores.select("division", "solver").unique()
+    solvers = scores.select("division", "solver").unique().filter(pl.col("solver").is_in(config.competitive_solvers))
     virtual_without_solver_scores = (
         intersect(scores.rename({"solver": "other_solver"}), solvers, on=["division"])
         .filter(pl.col("solver") != pl.col("other_solver"))