merge submissions

#189: UltimateEliminator submission 2025
#188: Z3-Siri Submission 2025
#187: OSTRICH version 2
#186: yicesQS submission to the 2025 SMT comp
#185: Bitwuzla 2025 submission.
#184: Yices2 Submission SMTCOMP 2025
#183: cvc5 for SMT-COMP 2025
#182: Create iProver
#181: Z3-Owl Submission 2025
#179: Z3-alpha SMT-COMP 2025
#178: Z3-Noodler-Mocha Submission for SMT-COMP 2025
#177: `bv_decide` submission 2025
#176: OpenSMT (min-ucore) submission 2025
#175: Z3-Noodler submission 2025
#172: SMTS submission 2025
#171: Bitwuzla-MachBV Submission for SMT-COMP 2025
#170: Z3-Parti-Z3++ Submission for SMT-COMP 2025
#169: STP-Parti-Bitwuzla Submission for SMT-COMP 2025
#168: SMTInterpol submission 2025
#167: OpenSMT submission 2025
#165: Amaya 2025
#164: SMT-RAT submission
#163: COLIBRI submission
#162: [Submission] colibri2
#156: upload z3-inc-z3++

Author: Martin Jonáš

archive/2024/participants/index.html

@@ -67,4 +67,9 @@
 David Chocholatý,
 Lukáš Holík,
 Ondřej Lengál</td><td><a href="https://drive.google.com/uc?export=download&amp;id=1XSj2PiVJLDx-JQyJRt76OEloC0dWFJqH">Archive</a></td><td><a href=https://github.com/VeriFIT/z3-noodler/blob/devel/doc/noodler/z3-noodler-system-description-2024.pdf>System description</a></td></tr><tr><td><a href=https://github.com/shaowei-cai-group/Z3-Parti-Z3pp-at-SMT-COMP-2024>Z3-Parti-Z3++</a></td><td></td><td></td><td></td><td></td><td>X</td><td>X</td><td class=authors>Mengyu Zhao,
-Shaowei Cai</td><td><a href=https://zenodo.org/records/11627838/files/Z3-Parti-Z3++.zip>Archive</a></td><td><a href=https://github.com/shaowei-cai-group/Z3-Parti-Z3pp-at-SMT-COMP-2024/blob/master/Z3_Parti_Z3pp_at_SMT_COMP_2024.pdf>System description</a></td></tr></tbody></table></section><footer></footer></div></body></html>
+    Shaowei Cai</td><td><a href=https://zenodo.org/records/11627838/files/Z3-Parti-Z3++.zip>Archive</a></td><td><a href=https://github.com/shaowei-cai-group/Z3-Parti-Z3pp-at-SMT-COMP-2024/blob/master/Z3_Parti_Z3pp_at_SMT_COMP_2024.pdf>System description</a></td></tr></tbody></table>
+
+The opening value of the NYSE Composite Index on 2024-06-17 was 17817.26, resulting in a competition seed of 17817 + 42417166 = <b>42434983</b>.
+</section><footer></footer>
+</div>
+</body></html>

archive/2024/results/index.html

@@ -1227,8 +1227,6 @@ class Participation(BaseModel, extra="forbid"):
     divisions: add all the logics of those divisions in each track
     logics: add all the specified logics in each selected track it exists
 
-    aws_repository should be used only in conjunction with Cloud and Parallel track
-
     archive and command should not be used with Cloud and Parallel track. They superseed the one given at the root.
     """
 
@@ -1237,18 +1235,10 @@ class Participation(BaseModel, extra="forbid"):
     divisions: list[Division] = []
     archive: Archive | None = None
     command: Command | None = None
-    aws_repository: str | None = None
     experimental: bool = False
 
     @model_validator(mode="after")
     def check_archive(self) -> Participation:
-        aws_track = {Track.Cloud, Track.Parallel}
-        if self.aws_repository is None and not set(self.tracks).isdisjoint(aws_track):
-            raise ValueError("aws_repository is required by Cloud and Parallel track")
-        if self.aws_repository is not None and not set(self.tracks).issubset(aws_track):
-            raise ValueError("aws_repository can be used only with Cloud and Parallel track")
-        if (self.archive is not None or self.command is not None) and not set(self.tracks).isdisjoint(aws_track):
-            raise ValueError("archive and command field can't be used with Cloud and Parallel track")
         return self
 
     def get(self, d: None | dict[Track, dict[Division, set[Logic]]] = None) -> dict[Track, dict[Division, set[Logic]]]:
@@ -1274,8 +1264,6 @@ def get_logics_by_track(self) -> dict[Track, set[Logic]]:
     def complete(self, archive: Archive | None, command: Command | None) -> ParticipationCompleted:
         archive = cast(Archive, archive if self.archive is None else self.archive)
         command = cast(Command, command if self.command is None else self.command)
-        if (self.aws_repository is not None) or set(self.tracks).issubset({Track.Cloud, Track.Parallel}):
-            raise ValueError("can't complete Cloud and Parallel track participations")
         return ParticipationCompleted(
             tracks=self.get(), archive=archive, command=command, experimental=self.experimental
         )
@@ -1339,14 +1327,10 @@ class Submission(BaseModel, extra="forbid"):
 
     @model_validator(mode="after")
     def check_archive(self) -> Submission:
-        if self.archive is None and not all(p.archive or p.aws_repository for p in self.participations.root):
-            raise ValueError(
-                "Field archive (or aws_repository) is needed in all participations if not present at the root"
-            )
-        if self.command is None and not all(p.command or p.aws_repository for p in self.participations.root):
-            raise ValueError(
-                "Field command (or aws_repository) is needed in all participations if not present at the root"
-            )
+        if self.archive is None and not all(p.archive for p in self.participations.root):
+            raise ValueError("Field archive is needed in all participations if not present at the root")
+        if self.command is None and not all(p.command for p in self.participations.root):
+            raise ValueError("Field command is needed in all participations if not present at the root")
 
         def check_archive(archive: None | Archive) -> None:
             if archive:
@@ -1364,7 +1348,7 @@ def uniq_id(self) -> str:
 
     def complete_participations(self) -> list[ParticipationCompleted]:
         """Push defaults from the submission into participations"""
-        return [p.complete(self.archive, self.command) for p in self.participations.root if p.aws_repository is None]
+        return [p.complete(self.archive, self.command) for p in self.participations.root]
 
 
 class Smt2File(BaseModel):

smtcomp/defs.py

@@ -1,5 +1,7 @@
+import math
 import functools, itertools
-from typing import Set, Dict, Optional, cast, List, DefaultDict
+from collections import defaultdict
+from typing import Set, Dict, Optional, cast, List, DefaultDict, Tuple
 from pathlib import Path, PurePath
 from smtcomp import defs
 from rich import progress
@@ -139,6 +141,38 @@ class PodiumSummaryResults(BaseModel):
     layout: Literal["results_summary"] = "results_summary"
 
 
+class PodiumStepOverallScore(BaseModel):
+    name: str
+    contribution: float_6dig  # nn_D * log10 N_D
+    division: str
+    tieBreakTimeScore: float_6dig
+
+
+class PodiumBestOverall(BaseModel):
+    resultdate: str
+    year: int
+    results: str
+    participants: str
+    track: track_name
+    recognition: Literal["best_overall"] = "best_overall"
+    winner_seq: str
+    winner_par: str
+    winner_sat: str
+    winner_unsat: str
+    winner_24s: str
+    winner_seq_score: float_6dig
+    winner_par_score: float_6dig
+    winner_sat_score: float_6dig
+    winner_unsat_score: float_6dig
+    winner_24s_score: float_6dig
+    sequential: list[PodiumStepOverallScore]
+    parallel: list[PodiumStepOverallScore]
+    sat: list[PodiumStepOverallScore]
+    unsat: list[PodiumStepOverallScore]
+    twentyfour: list[PodiumStepOverallScore]
+    layout: Literal["result_comp"] = "result_comp"
+
+
 class PodiumStepBiggestLead(BaseModel):
     name: str
     second: str
@@ -367,7 +401,7 @@ def get_kind(a: PodiumDivision, k: smtcomp.scoring.Kind) -> list[PodiumStep]:
 
 
 # Computes the new global ranking based on the distance between the winner of a
-# division and the second solver in a division as defined in secion 7.3.1 of
+# division and the second solver in a division as defined in section 7.3.1 of
 # the SMT-COMP'19 rules.
 #
 # data      : The podium as returned by process_csv.
@@ -456,6 +490,130 @@ def get_winner(l: List[PodiumStepBiggestLead] | None) -> str:
     )
 
 
+# Compute normalized correctness score
+#
+# normalized correctness score: nnD = (nD /ND)**2 if eD == 0
+#                                   = -2          otherwise
+def normalized_correctness_score(
+    data: dict[str, PodiumDivision], scores: pl.LazyFrame, track: defs.Track, k: smtcomp.scoring.Kind
+) -> list[PodiumStepOverallScore]:
+
+    podiumSteps: list[PodiumStepOverallScore] = []
+
+    for division, div_data in data.items():
+        solvers_in_div = get_kind(div_data, k)
+        if len(solvers_in_div) <= 1:
+            continue
+
+        N_D = get_N_D(scores, data, division, track)
+        for sol_in_div in solvers_in_div:
+            if sol_in_div.errorScore == 0:
+                nn_D = (sol_in_div.correctScore / N_D) ** 2
+            else:
+                nn_D = -2
+
+            podiumSteps.append(
+                PodiumStepOverallScore(
+                    name=sol_in_div.name,
+                    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,
+                )
+            )
+        podiumSteps = sorted(podiumSteps, key=lambda x: (x.contribution, x.tieBreakTimeScore), reverse=True)
+    return podiumSteps
+
+
+#  N_D  :=         total number of check sats in division D    if Incremental Track
+#                  total number of asserts in division D       if Unsat Core Track
+#                  total number of benchmarks                  otherwise
+def get_N_D(scores: pl.LazyFrame, data: dict[str, PodiumDivision], division: str, track: defs.Track) -> int:
+    if track == defs.Track.Incremental:
+        return int(
+            scores.unique(["division", "file"])
+            .group_by(["division"])
+            .agg([pl.col("check_sats").sum().alias("total_check_sats")])
+            .filter(pl.col("division") == int(defs.Division[division]))
+            .collect()["total_check_sats"][0]
+        )
+
+    elif track == defs.Track.UnsatCore:
+        return int(
+            scores.unique(["division", "file"])
+            .group_by(["division"])
+            .agg([pl.col("asserts").sum().alias("total_asserts")])
+            .filter(pl.col("division") == int(defs.Division[division]))
+            .collect()["total_asserts"][0]
+        )
+
+    return data[division].n_benchmarks
+
+
+# Computes the best overall ranking as specified in Section 7.3.1 of
+# SMT-COMP 2025 rules. I.e:
+#
+# normalized correctness score: nnD = (nD /ND)**2 if eD == 0
+#                                  = -2          otherwise
+# overall score               : sum_D nnD*log10 ND
+#
+# For the choices, see the footnote in the rules.
+#
+def best_overall_ranking(
+    config: defs.Config, scores: pl.LazyFrame, data: dict[str, PodiumDivision], track: defs.Track
+) -> PodiumBestOverall:
+    def get_winner(
+        l: Optional[List[PodiumStepOverallScore]],
+        scores: pl.LazyFrame,
+        data: dict[str, PodiumDivision],
+        track: defs.Track,
+    ) -> Tuple[str, float]:
+        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})
+            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"]))
+            return (winner, winner_data["score"])
+
+    sequential = normalized_correctness_score(data, scores, track, smtcomp.scoring.Kind.seq)
+    parallel = normalized_correctness_score(data, scores, track, smtcomp.scoring.Kind.par)
+    sat = normalized_correctness_score(data, scores, track, smtcomp.scoring.Kind.sat)
+    unsat = normalized_correctness_score(data, scores, track, smtcomp.scoring.Kind.unsat)
+    twentyfour = normalized_correctness_score(data, scores, track, smtcomp.scoring.Kind.twentyfour)
+
+    if track in (defs.Track.Cloud, defs.Track.Parallel):
+        winner_seq = ("-", 0.0)
+        sequential = []
+    else:
+        winner_seq = get_winner(sequential, scores, data, track)
+
+    return PodiumBestOverall(
+        resultdate="2024-07-08",
+        year=config.current_year,
+        track=track,
+        results=f"results_{config.current_year}",
+        participants=f"participants_{config.current_year}",
+        recognition="best_overall",
+        winner_seq=winner_seq[0],
+        winner_par=get_winner(parallel, scores, data, track)[0],
+        winner_sat=get_winner(sat, scores, data, track)[0],
+        winner_unsat=get_winner(unsat, scores, data, track)[0],
+        winner_24s=get_winner(twentyfour, scores, data, track)[0],
+        winner_seq_score=winner_seq[1],
+        winner_par_score=get_winner(parallel, scores, data, track)[1],
+        winner_sat_score=get_winner(sat, scores, data, track)[1],
+        winner_unsat_score=get_winner(unsat, scores, data, track)[1],
+        winner_24s_score=get_winner(twentyfour, scores, data, track)[1],
+        sequential=sequential,
+        parallel=parallel,
+        sat=sat,
+        unsat=unsat,
+        twentyfour=twentyfour,
+    )
+
+
 def largest_contribution_ranking(
     config: defs.Config,
     virtual_datas: Dict[str, PodiumDivision],
@@ -634,6 +792,9 @@ def export_results(config: defs.Config, selection: pl.LazyFrame, results: pl.Laz
                 all_divisions.append(data)
 
         if for_division:
+            data_best_overall = best_overall_ranking(config, scores, datas, track)
+            (dst / f"best-overall-{page_suffix}.md").write_text(data_best_overall.model_dump_json(indent=1))
+
             bigdata = biggest_lead_ranking(config, datas, track)
             (dst / f"biggest-lead-{page_suffix}.md").write_text(bigdata.model_dump_json(indent=1))
 

smtcomp/generate_website_page.py

@@ -176,3 +176,20 @@ def compute_results_read_podium_division(
         (config.web_results / f"{logic.name.lower()}-{page_suffix}.md").read_text()
     )
     return podium
+
+
+def compute_results_read_podium_best_overall(
+    config: defs.Config, track: defs.Track, check_sound_solvers: list[str] = []
+) -> smtcomp.generate_website_page.PodiumBestOverall:
+
+    results, selection = smtcomp.results.helper_get_results(config, [], track)
+    if check_sound_solvers:
+        scores = smtcomp.scoring.add_disagreements_info(results, track)
+        sound_solvers = scores.filter(sound_solver=True).select("solver").unique().collect()["solver"].sort().to_list()
+        assert sound_solvers == check_sound_solvers
+    smtcomp.generate_website_page.export_results(config, selection, results, track)
+    page_suffix = smtcomp.generate_website_page.page_track_suffix(track)
+    podium = smtcomp.generate_website_page.PodiumBestOverall.model_validate_json(
+        (config.web_results / f"best-overall-{page_suffix}.md").read_text()
+    )
+    return podium

smtcomp/test_generation.py

@@ -0,0 +1,22 @@
+{
+    "name": "Amaya",
+    "contributors": [
+        "Vojtěch Havlena", "Michal Hečko", "Lukáš Holík", "Ondřej Lengál"
+    ],
+    "contacts": ["Michal Hečko <[email protected]>", "Ondřej Lengál <[email protected]>"],
+    "archive": {
+        "url": "https://zenodo.org/records/15630432/files/amaya-smtcomp25-v2.tar.gz",
+        "h": { "sha256": "133058d14b7cb1ef45261e9d02ef3e6f76589dd3551c73870e318e2d3a75ad54" }
+    },
+    "website": "https://github.com/MichalHe/amaya",
+    "system_description": "https://raw.githubusercontent.com/VeriFIT/amaya-smt-comp/master/system-description-2025/main.pdf",
+    "command": ["amaya/run.sh"],
+    "solver_type": "Standalone",
+    "seed": "587087",
+    "participations": [
+        {
+            "tracks": ["SingleQuery"],
+            "logics": ["LIA", "NIA"]
+        }
+    ]
+}

submissions/Amaya.json

@@ -0,0 +1,17 @@
+{
+    "name": "Bitwuzla-0-7-0",
+    "archive": {
+        "url": "https://zenodo.org/records/15649785/files/Bitwuzla-0-7-0.zip"
+    },
+    "contributors": ["Aina Niemetz", "Mathias Preiner"],
+    "contacts": ["Mathias Preiner <[email protected]>"],
+    "website": "https://bitwuzla.github.io",
+    "system_description": "https://link.springer.com/content/pdf/10.1007/978-3-031-37703-7_1",
+    "command": [ "./bitwuzla" ],
+    "solver_type": "Standalone",
+    "seed": 42,
+    "participations": [
+        { "tracks": ["SingleQuery"], "logics": "QF_BV" }
+    ],
+    "competitive": false
+}

submissions/Bitwuzla-0-7-0.json

@@ -0,0 +1,32 @@
+{
+    "name": "Bitwuzla-MachBV",
+    "contributors": [
+        "Xiang Zhang",
+        "Shaohuang Chen",
+        "Mengyu Zhao",
+        "Shaowei Cai"
+    ],
+    "contacts": [
+        "Xiang Zhang <[email protected]>"
+    ],
+    "archive": {
+        "url": "https://zenodo.org/records/15642045/files/Bitwuzla-MachBV.zip"
+    },
+    "website": "https://github.com/Andeviking/Bitwuzla-MachBV-at-SMT-COMP-2025",
+    "system_description": "https://github.com/Andeviking/Bitwuzla-MachBV-at-SMT-COMP-2025/blob/main/Bitwuzla_MachBV_at_SMT_COMP_2025.pdf",
+    "command": [
+        "./MachBV"
+    ],
+    "solver_type": "derived",
+    "seed": "1126300213",
+    "participations": [
+        {
+            "tracks": [
+                "SingleQuery"
+            ],
+            "logics": [
+                "QF_BV"
+            ]
+        }
+    ]
+}

submissions/Bitwuzla-MachBV-at-SMT-COMP-2025.json

@@ -0,0 +1,22 @@
+{
+    "name": "COLIBRI",
+    "contributors": [
+        "Bruno Marre", "François Bobot", "Christophe Junke"
+    ],
+    "contacts": ["Christophe Junke <[email protected]>"],
+    "archive": {
+        "url": "https://git.frama-c.com/pub/colibri/-/releases/2025.06/downloads/bundle-v5",
+        "h": { "sha256": "f251f170c75a96af9ccde9859ac349e5c1cdd6fa6aeca779cb1ef4b9a8134871" }
+    },
+    "website": "http://colibri.frama-c.com/",
+    "system_description": "https://colibri.frama-c.com/assets/documents/colibri_2025.pdf",
+    "command": ["colibri-2025.06-v5/colibri", "--memlimit", "5000"],
+    "solver_type": "Standalone",
+    "participations": [
+        {
+            "tracks": ["SingleQuery"],
+            "logics": "QF_.*FP.*"
+        }
+    ],
+    "seed": 0
+}