2025 webpage (#205)

* 2024 -> 2025

* target for cleaning up web results

* feat: show legends for base and non-competing only when at least one
solver present

* feat: non-competitive divisions will be marked

* skip non-competing solvers on podiums

* fix: -- -> -

* fix: missing case for determining competitive divisions

* fix: competitive solvers

* fix competitive divisions

* consistency submission vs. base solver

* refactor

* fix: ordering of solvers

Author: wintered

Makefile

@@ -31,6 +31,12 @@ build: clean-build ## Build wheel file using poetry
 clean-build: ## clean build artifacts
 	@rm -rf dist
 
+.PHONY: clean-web-results
+clean-web-results: ## clean web results
+	@rm -rf web/content/results
+	@rm -rf web/public/results
+
+
 .PHONY: help
 help:
 	@grep -E '^[a-zA-Z_-]+:.*?## .*$$' $(MAKEFILE_LIST) | awk 'BEGIN {FS = ":.*?## "}; {printf "\033[36m%-20s\033[0m %s\n", $$1, $$2}'

smtcomp/defs.py

@@ -135,7 +135,7 @@ def name_is_default_field(cls, data: Any) -> Any:
 
 class SolverType(EnumAutoInt):
     wrapped = "wrapped"
-    derived = "derived"
+    derived = "derived"  # TODO: put a datatype information on base solver
     standalone = "Standalone"
     portfolio = "Portfolio"
 
@@ -1317,6 +1317,7 @@ class Submission(BaseModel, extra="forbid"):
     website: HttpUrl
     system_description: HttpUrl
     solver_type: SolverType
+    # TODO add field base_solver?
     participations: Participations
     seed: int | None = None
     competitive: bool = True
@@ -1325,6 +1326,7 @@ class Submission(BaseModel, extra="forbid"):
         description="Must be set for the final version of the submission. An archive on zenodo is needed in this case.",
     )
 
+    # TODO: model validator to check the sanity of the new base_solver field
     @model_validator(mode="after")
     def check_archive(self) -> Submission:
         if self.archive is None and not all(p.archive for p in self.participations.root):
@@ -1510,11 +1512,26 @@ class Config:
     Benchmarks to remove before selection
     """
 
-    removed_results: Any = []
+    removed_results: list[Any] = []
+
     """
     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",
+        "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
@@ -1578,6 +1595,10 @@ def submissions(self) -> list[Submission]:
             Submission.model_validate_json(Path(file).read_text()) for file in self.data.glob("../submissions/*.json")
         ]
 
+    @functools.cached_property
+    def competitive_solvers(self) -> list[str]:
+        return [s.name for s in self.submissions if s.competitive]
+
     @functools.cached_property
     def web_results(self) -> Path:
         return self.data / ".." / "web" / "content" / "results"

smtcomp/generate_website_page.py

@@ -94,6 +94,8 @@ def page_track_suffix(track: defs.Track) -> str:
 
 class PodiumStep(BaseModel):
     name: str
+    baseSolver: str
+    deltaBaseSolver: int
     competing: str  # yes or no
     errorScore: int
     correctScore: int
@@ -115,6 +117,7 @@ class PodiumDivision(BaseModel):
     participants: str  # participants_2023
     disagreements: str  # disagreements_2023
     division: str  # Arith
+    is_competitive: bool  # true = least 2 subst. different solvers were submitted
     track: track_name
     n_benchmarks: int
     time_limit: int
@@ -237,14 +240,27 @@ class Podium(RootModel):
     root: PodiumDivision | PodiumCrossDivision | PodiumSummaryResults = Field(..., discriminator="layout")
 
 
-def podium_steps(podium: List[dict[str, Any]] | None) -> List[PodiumStep]:
+def podium_steps(config: defs.Config, podium: List[dict[str, Any]] | None) -> List[PodiumStep]:
     if podium is None:
         return []
     else:
-        return [
-            PodiumStep(
+        podiums = []
+        non_competitive = []
+        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
+
+            ps = PodiumStep(
                 name=s["solver"],
-                competing="yes",  # TODO
+                baseSolver=derived_solver,
+                deltaBaseSolver=delta,
+                competing="yes" if s["solver"] in config.competitive_solvers else "no",
                 errorScore=s["error_score"],
                 correctScore=s["correctly_solved_score"],
                 CPUScore=s["cpu_time_score"],
@@ -257,36 +273,70 @@ def podium_steps(podium: List[dict[str, Any]] | None) -> List[PodiumStep]:
                 timeout=s["timeout"],
                 memout=s["memout"],
             )
-            for s in podium
-        ]
 
+            if not s["solver"] in config.competitive_solvers:
+                non_competitive.append(ps)
+            else:
+                podiums.append(ps)
+
+        return podiums + non_competitive
 
-def make_podium(config: defs.Config, d: dict[str, Any], for_division: bool, track: defs.Track) -> PodiumDivision:
+
+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:
-        # TODO select only participating
+        if l is None or not l:
+            return "-"
+
+        l = [e for e in l if e["solver"] in config.competitive_solvers]
+
         if l is None or not l or l[0]["correctly_solved_score"] == 0:
             return "-"
         else:
             return l[0]["solver"]
 
+    def is_competitive_division(results: pl.LazyFrame, division: int, for_division: bool) -> bool:
+        """
+        A division in a track is competitive if at least two substantially different
+        solvers (i.e., solvers from two different teams) were submitted.
+        """
+
+        solvers = (
+            results.filter(pl.col("division" if for_division else "logic") == division)
+            .select("solver")
+            .unique()
+            .collect()
+            .get_column("solver")
+            .to_list()
+        )
+
+        # Avoid solvers of the same solver family under the assumption
+        # of the following format: <solver-family>-<suffix> (holds for SMT-COMP 2025)
+        # TODO: improve this criterion in the future
+        return len(set([sol.split("-")[0].lower() for sol in solvers])) >= 2
+
     if for_division:
+        competitive_division = is_competitive_division(results, d["division"], for_division)
         division = defs.Division.name_of_int(d["division"])
         logics = dict((defs.Logic.name_of_int(d2["logic"]), d2["n"]) for d2 in d["logics"])
     else:
         division = defs.Logic.name_of_int(d["logic"])
+        competitive_division = is_competitive_division(results, d["logic"], for_division)
         logics = dict()
 
     if (track == defs.Track.Cloud) | (track == defs.Track.Parallel):
         winner_seq = "-"
         steps_seq = []
     else:
         winner_seq = get_winner(d[smtcomp.scoring.Kind.seq.name])
-        steps_seq = podium_steps(d[smtcomp.scoring.Kind.seq.name])
+        steps_seq = podium_steps(config, d[smtcomp.scoring.Kind.seq.name])
 
     return PodiumDivision(
-        resultdate="2024-07-08",
+        resultdate="2025-08-11",
         year=config.current_year,
         divisions=f"divisions_{config.current_year}",
+        is_competitive=competitive_division,
         participants=f"participants_{config.current_year}",
         disagreements=f"disagreements_{config.current_year}",
         division=division,
@@ -301,10 +351,10 @@ def get_winner(l: List[dict[str, str]] | None) -> str:
         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(d[smtcomp.scoring.Kind.par.name]),
-        sat=podium_steps(d[smtcomp.scoring.Kind.sat.name]),
-        unsat=podium_steps(d[smtcomp.scoring.Kind.unsat.name]),
-        twentyfour=podium_steps(d[smtcomp.scoring.Kind.twentyfour.name]),
+        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]),
     )
 
 
@@ -382,7 +432,7 @@ def info_for_podium_step(kind: smtcomp.scoring.Kind, config: defs.Config, result
 
     df = r.collect()
 
-    return dict((name_of_int(d[group_by]), make_podium(config, d, for_division, track)) for d in df.to_dicts())
+    return dict((name_of_int(d[group_by]), make_podium(config, d, for_division, track, results)) for d in df.to_dicts())
 
 
 def get_kind(a: PodiumDivision, k: smtcomp.scoring.Kind) -> list[PodiumStep]:
@@ -471,7 +521,7 @@ def get_winner(l: List[PodiumStepBiggestLead] | None) -> str:
         winner_seq = get_winner(sequential)
 
     return PodiumBiggestLead(
-        resultdate="2024-07-08",
+        resultdate="2025-08-11",
         year=config.current_year,
         track=track,
         results=f"results_{config.current_year}",
@@ -589,7 +639,7 @@ def get_winner(
         winner_seq = get_winner(sequential, scores, data, track)
 
     return PodiumBestOverall(
-        resultdate="2024-07-08",
+        resultdate="2025-08-11",
         year=config.current_year,
         track=track,
         results=f"results_{config.current_year}",
@@ -630,7 +680,10 @@ def get_winner(l: List[PodiumStepLargestContribution] | None) -> str:
 
     def aux(k: smtcomp.scoring.Kind, div: str) -> List[PodiumStepLargestContribution]:
         v_steps = get_kind(virtual_datas[div], k)
-        vws_steps = get_kind(virtual_without_solver_datas[div], k)
+        if div in virtual_without_solver_datas:
+            vws_steps = get_kind(virtual_without_solver_datas[div], k)
+        else:
+            vws_steps = []
         if not v_steps:
             assert not vws_steps
             return []
@@ -684,7 +737,7 @@ def timeScore(vws_step: PodiumStep) -> float:
         steps_seq = ld[smtcomp.scoring.Kind.seq]
 
     return PodiumLargestContribution(
-        resultdate="2024-07-08",
+        resultdate="2025-08-11",
         year=config.current_year,
         track=track,
         results=f"results_{config.current_year}",
@@ -718,7 +771,7 @@ def largest_contribution(config: defs.Config, scores: pl.LazyFrame, track: defs.
 
     # Virtual solver
     virtual_scores = (
-        scores.group_by("division", "file")
+        scores.group_by("division", "logic", "file")
         .agg(
             pl.max("correctly_solved_score"),
             pl.min("walltime_s"),
@@ -727,7 +780,6 @@ def largest_contribution(config: defs.Config, scores: pl.LazyFrame, track: defs.
             pl.min("cpu_time_score"),
             sound_status=pl.col("sound_status").first(),
             answer=pl.col("answer").first(),
-            logic=-1,
         )
         .with_columns(solver=pl.lit("virtual"), error_score=0)
     )
@@ -739,7 +791,7 @@ def largest_contribution(config: defs.Config, scores: pl.LazyFrame, track: defs.
         intersect(scores.rename({"solver": "other_solver"}), solvers, on=["division"])
         .filter(pl.col("solver") != pl.col("other_solver"))
         .drop("other_solver")
-        .group_by("division", "solver", "file")
+        .group_by("division", "logic", "solver", "file")
         .agg(
             pl.max("correctly_solved_score"),
             pl.min("walltime_s"),
@@ -749,7 +801,6 @@ def largest_contribution(config: defs.Config, scores: pl.LazyFrame, track: defs.
             sound_status=pl.col("sound_status").first(),
             error_score=0,
             answer=pl.col("answer").first(),
-            logic=-1,
         )
     )
     virtual_without_solver_datas = sq_generate_datas(config, virtual_without_solver_scores, for_division, track)
@@ -765,7 +816,6 @@ def largest_contribution(config: defs.Config, scores: pl.LazyFrame, track: defs.
 
 
 def export_results(config: defs.Config, results: pl.LazyFrame, track: defs.Track) -> None:
-
     page_suffix = page_track_suffix(track)
 
     dst = config.web_results

web/content/solver_submission/template.json

@@ -0,0 +1,31 @@
+{
+    "name": "<solver name>",
+    "contributors": [
+        "First Smith",
+        { "name": "Second Baker", "website": "http://baker.com/" }
+    ],
+    "contacts": ["contact name <[email protected]>"],
+    "archive": {
+        "url": "http://example.com/solver.tar.gz",
+        "h": { "sha256": "012345" }
+    },
+    "website": "http://example.com/",
+    "system_description": "http://example.com/system.pdf",
+    "command": ["relative_cmd", "default_command_line"],
+    "solver_type": "Standalone",
+    "seed": "42",
+    "participations": [
+        { "tracks": ["SingleQuery"], "divisions": ["Equality"] },
+        {
+            "tracks": ["SingleQuery"],
+            "logics": "QF_.*LRA.*",
+            "command": ["relative_cmd", "other_option"]
+        },
+        {
+            "tracks": ["SingleQuery"],
+            "logics": ["LIA"],
+            "archive": { "url": "http://example.com/solver_lia.tar.gz" },
+            "command": ["relative_cmd", "--super-lia"]
+        }
+    ]
+}

web/content/solver_submission/template.json

@@ -593,7 +593,7 @@ td.left {
 }
 
 td.non-competing-grey {
-  color: #707070;
+  color: gray;
   a {
     color: #808080;
   }