From 8b9fe1c8c74d40a8eeac987ffecdef336b1c5305 Mon Sep 17 00:00:00 2001 From: Mathias Preiner Date: Tue, 15 Jul 2025 08:44:47 -0700 Subject: [PATCH 01/25] bitwuzla: Change options for parallel track. (#201) * bitwuzla: Change options for parallel track. Add additional configurations for lower CPU core counts. * Make additional configurations non-competitive. --- submissions/bitwuzla.json | 2 +- submissions/bitwuzla_parallel_16.json | 27 +++++++++++++++++++++++++++ submissions/bitwuzla_parallel_32.json | 27 +++++++++++++++++++++++++++ 3 files changed, 55 insertions(+), 1 deletion(-) create mode 100644 submissions/bitwuzla_parallel_16.json create mode 100644 submissions/bitwuzla_parallel_32.json diff --git a/submissions/bitwuzla.json b/submissions/bitwuzla.json index 43d6f6ed..8982e20d 100644 --- a/submissions/bitwuzla.json +++ b/submissions/bitwuzla.json @@ -39,7 +39,7 @@ { "tracks": ["Parallel"], "logics": "^((QF_)?(A)?(UF)?(BV|FP|FPLRA)+)$", - "command": ["bin/bitwuzla", "--sat-solver=gimsatul", "-j", "128"] + "command": ["bin/bitwuzla", "--sat-solver=gimsatul", "-j", "64"] } ] } diff --git a/submissions/bitwuzla_parallel_16.json b/submissions/bitwuzla_parallel_16.json new file mode 100644 index 00000000..02a0abdb --- /dev/null +++ b/submissions/bitwuzla_parallel_16.json @@ -0,0 +1,27 @@ +{ + "name": "Bitwuzla", + "contributors": ["Aina Niemetz", "Mathias Preiner"], + "contacts": ["Mathias Preiner "], + "final" : true, + + "archive": { + "url": "https://zenodo.org/records/15760031/files/bitwuzla-submission-smtcomp-2025.zip?download=1", + "h": {"sha256": "b97f018f4d92978c6b116c3f0b09f44f06ec15c885f6cc84a9dde3218cc1a583"} + }, + + "command": ["bin/bitwuzla"], + + "website": "https://bitwuzla.github.io", + "system_description": "https://bitwuzla.github.io/data/smtcomp2025/paper.pdf", + "solver_type": "Standalone", + "seed": "42", + "competitive": false, + "participations": [ + { + "tracks": ["Parallel"], + "logics": "^((QF_)?(A)?(UF)?(BV|FP|FPLRA)+)$", + "command": ["bin/bitwuzla", "--sat-solver=gimsatul", "-j", "16"] + } + ] +} + diff --git a/submissions/bitwuzla_parallel_32.json b/submissions/bitwuzla_parallel_32.json new file mode 100644 index 00000000..06113d44 --- /dev/null +++ b/submissions/bitwuzla_parallel_32.json @@ -0,0 +1,27 @@ +{ + "name": "Bitwuzla", + "contributors": ["Aina Niemetz", "Mathias Preiner"], + "contacts": ["Mathias Preiner "], + "final" : true, + + "archive": { + "url": "https://zenodo.org/records/15760031/files/bitwuzla-submission-smtcomp-2025.zip?download=1", + "h": {"sha256": "b97f018f4d92978c6b116c3f0b09f44f06ec15c885f6cc84a9dde3218cc1a583"} + }, + + "command": ["bin/bitwuzla"], + + "website": "https://bitwuzla.github.io", + "system_description": "https://bitwuzla.github.io/data/smtcomp2025/paper.pdf", + "solver_type": "Standalone", + "seed": "42", + "competitive": false, + "participations": [ + { + "tracks": ["Parallel"], + "logics": "^((QF_)?(A)?(UF)?(BV|FP|FPLRA)+)$", + "command": ["bin/bitwuzla", "--sat-solver=gimsatul", "-j", "32"] + } + ] +} + From 02a8c889f732216293a9174abae4d7c1f65bfa21 Mon Sep 17 00:00:00 2001 From: Mengyu Zhao Date: Tue, 15 Jul 2025 23:45:36 +0800 Subject: [PATCH 02/25] submission: add additional configurations for lower CPU core counts. (#202) --- submissions/STP-Parti-Bitwuzla-p16.json | 26 +++++++++++++++++++++++++ submissions/STP-Parti-Bitwuzla-p32.json | 26 +++++++++++++++++++++++++ submissions/STP-Parti-Bitwuzla-p8.json | 26 +++++++++++++++++++++++++ submissions/STP-Parti-Bitwuzla.json | 4 ++-- submissions/Z3-Parti-Z3pp-p16.json | 24 +++++++++++++++++++++++ submissions/Z3-Parti-Z3pp-p32.json | 24 +++++++++++++++++++++++ submissions/Z3-Parti-Z3pp-p8.json | 24 +++++++++++++++++++++++ submissions/Z3-Parti-Z3pp.json | 4 ++-- 8 files changed, 154 insertions(+), 4 deletions(-) create mode 100644 submissions/STP-Parti-Bitwuzla-p16.json create mode 100644 submissions/STP-Parti-Bitwuzla-p32.json create mode 100644 submissions/STP-Parti-Bitwuzla-p8.json create mode 100644 submissions/Z3-Parti-Z3pp-p16.json create mode 100644 submissions/Z3-Parti-Z3pp-p32.json create mode 100644 submissions/Z3-Parti-Z3pp-p8.json diff --git a/submissions/STP-Parti-Bitwuzla-p16.json b/submissions/STP-Parti-Bitwuzla-p16.json new file mode 100644 index 00000000..e343e55e --- /dev/null +++ b/submissions/STP-Parti-Bitwuzla-p16.json @@ -0,0 +1,26 @@ +{ + "name": "STP-Parti-Bitwuzla", + "contributors": [ + "Mengyu Zhao", + "Zhenghang Xu", + "Jinkun Lin", + "Shaowei Cai" + ], + "contacts": ["Mengyu Zhao "], + "archive": { + "url": "https://zenodo.org/records/15920866/files/STP-Parti-Bitwuzla-at-SMT-COMP-2025-build.zip" + }, + "website": "https://github.com/shaowei-cai-group/STP-Parti-Bitwuzla-at-SMT-COMP-2025", + "system_description": "https://github.com/shaowei-cai-group/STP-Parti-Bitwuzla-at-SMT-COMP-2025/blob/master/STP_Parti_Bitwuzla_at_SMT_COMP_2025.pdf", + "command": ["./STP-Parti-Bitwuzla-at-SMT-COMP-2025-build/solver/run_BVParti.py", "16"], + "solver_type": "wrapped", + "seed": "998244353", + "participations": [ + { + "tracks": ["Parallel"], + "logics": ["QF_BV"] + } + ], + "competitive": false, + "final": true +} diff --git a/submissions/STP-Parti-Bitwuzla-p32.json b/submissions/STP-Parti-Bitwuzla-p32.json new file mode 100644 index 00000000..e72bf73b --- /dev/null +++ b/submissions/STP-Parti-Bitwuzla-p32.json @@ -0,0 +1,26 @@ +{ + "name": "STP-Parti-Bitwuzla", + "contributors": [ + "Mengyu Zhao", + "Zhenghang Xu", + "Jinkun Lin", + "Shaowei Cai" + ], + "contacts": ["Mengyu Zhao "], + "archive": { + "url": "https://zenodo.org/records/15920866/files/STP-Parti-Bitwuzla-at-SMT-COMP-2025-build.zip" + }, + "website": "https://github.com/shaowei-cai-group/STP-Parti-Bitwuzla-at-SMT-COMP-2025", + "system_description": "https://github.com/shaowei-cai-group/STP-Parti-Bitwuzla-at-SMT-COMP-2025/blob/master/STP_Parti_Bitwuzla_at_SMT_COMP_2025.pdf", + "command": ["./STP-Parti-Bitwuzla-at-SMT-COMP-2025-build/solver/run_BVParti.py", "32"], + "solver_type": "wrapped", + "seed": "998244353", + "participations": [ + { + "tracks": ["Parallel"], + "logics": ["QF_BV"] + } + ], + "competitive": false, + "final": true +} diff --git a/submissions/STP-Parti-Bitwuzla-p8.json b/submissions/STP-Parti-Bitwuzla-p8.json new file mode 100644 index 00000000..f314ddfe --- /dev/null +++ b/submissions/STP-Parti-Bitwuzla-p8.json @@ -0,0 +1,26 @@ +{ + "name": "STP-Parti-Bitwuzla", + "contributors": [ + "Mengyu Zhao", + "Zhenghang Xu", + "Jinkun Lin", + "Shaowei Cai" + ], + "contacts": ["Mengyu Zhao "], + "archive": { + "url": "https://zenodo.org/records/15920866/files/STP-Parti-Bitwuzla-at-SMT-COMP-2025-build.zip" + }, + "website": "https://github.com/shaowei-cai-group/STP-Parti-Bitwuzla-at-SMT-COMP-2025", + "system_description": "https://github.com/shaowei-cai-group/STP-Parti-Bitwuzla-at-SMT-COMP-2025/blob/master/STP_Parti_Bitwuzla_at_SMT_COMP_2025.pdf", + "command": ["./STP-Parti-Bitwuzla-at-SMT-COMP-2025-build/solver/run_BVParti.py", "8"], + "solver_type": "wrapped", + "seed": "998244353", + "participations": [ + { + "tracks": ["Parallel"], + "logics": ["QF_BV"] + } + ], + "competitive": false, + "final": true +} diff --git a/submissions/STP-Parti-Bitwuzla.json b/submissions/STP-Parti-Bitwuzla.json index 99ce499f..5dedf932 100644 --- a/submissions/STP-Parti-Bitwuzla.json +++ b/submissions/STP-Parti-Bitwuzla.json @@ -8,11 +8,11 @@ ], "contacts": ["Mengyu Zhao "], "archive": { - "url": "https://zenodo.org/records/15640499/files/STP-Parti-Bitwuzla-at-SMT-COMP-2025-build.zip" + "url": "https://zenodo.org/records/15920866/files/STP-Parti-Bitwuzla-at-SMT-COMP-2025-build.zip" }, "website": "https://github.com/shaowei-cai-group/STP-Parti-Bitwuzla-at-SMT-COMP-2025", "system_description": "https://github.com/shaowei-cai-group/STP-Parti-Bitwuzla-at-SMT-COMP-2025/blob/master/STP_Parti_Bitwuzla_at_SMT_COMP_2025.pdf", - "command": ["./STP-Parti-Bitwuzla-at-SMT-COMP-2025-build/solver/run_BVParti.py"], + "command": ["./STP-Parti-Bitwuzla-at-SMT-COMP-2025-build/solver/run_BVParti.py", "64"], "solver_type": "wrapped", "seed": "998244353", "participations": [ diff --git a/submissions/Z3-Parti-Z3pp-p16.json b/submissions/Z3-Parti-Z3pp-p16.json new file mode 100644 index 00000000..306bbfb8 --- /dev/null +++ b/submissions/Z3-Parti-Z3pp-p16.json @@ -0,0 +1,24 @@ +{ + "name": "Z3-Parti-Z3pp", + "contributors": [ + "Mengyu Zhao", + "Shaowei Cai" + ], + "contacts": ["Mengyu Zhao "], + "archive": { + "url": "https://zenodo.org/records/15920863/files/Z3-Parti-Z3pp-at-SMT-COMP-2025-build.zip" + }, + "website": "https://github.com/shaowei-cai-group/Z3-Parti-Z3pp-at-SMT-COMP-2025", + "system_description": "https://github.com/shaowei-cai-group/Z3-Parti-Z3pp-at-SMT-COMP-2025/blob/master/Z3_Parti_Z3pp_at_SMT_COMP_2025.pdf", + "command": ["./Z3-Parti-Z3pp-at-SMT-COMP-2025-build/solver/run_AriParti.py", "16"], + "solver_type": "wrapped", + "seed": "998244353", + "participations": [ + { + "tracks": ["Parallel"], + "logics": ["QF_RDL", "QF_IDL", "QF_LRA", "QF_LIA", "QF_NRA", "QF_NIA"] + } + ], + "competitive": false, + "final": true +} diff --git a/submissions/Z3-Parti-Z3pp-p32.json b/submissions/Z3-Parti-Z3pp-p32.json new file mode 100644 index 00000000..2779c767 --- /dev/null +++ b/submissions/Z3-Parti-Z3pp-p32.json @@ -0,0 +1,24 @@ +{ + "name": "Z3-Parti-Z3pp", + "contributors": [ + "Mengyu Zhao", + "Shaowei Cai" + ], + "contacts": ["Mengyu Zhao "], + "archive": { + "url": "https://zenodo.org/records/15920863/files/Z3-Parti-Z3pp-at-SMT-COMP-2025-build.zip" + }, + "website": "https://github.com/shaowei-cai-group/Z3-Parti-Z3pp-at-SMT-COMP-2025", + "system_description": "https://github.com/shaowei-cai-group/Z3-Parti-Z3pp-at-SMT-COMP-2025/blob/master/Z3_Parti_Z3pp_at_SMT_COMP_2025.pdf", + "command": ["./Z3-Parti-Z3pp-at-SMT-COMP-2025-build/solver/run_AriParti.py", "32"], + "solver_type": "wrapped", + "seed": "998244353", + "participations": [ + { + "tracks": ["Parallel"], + "logics": ["QF_RDL", "QF_IDL", "QF_LRA", "QF_LIA", "QF_NRA", "QF_NIA"] + } + ], + "competitive": false, + "final": true +} diff --git a/submissions/Z3-Parti-Z3pp-p8.json b/submissions/Z3-Parti-Z3pp-p8.json new file mode 100644 index 00000000..b347c9f1 --- /dev/null +++ b/submissions/Z3-Parti-Z3pp-p8.json @@ -0,0 +1,24 @@ +{ + "name": "Z3-Parti-Z3pp", + "contributors": [ + "Mengyu Zhao", + "Shaowei Cai" + ], + "contacts": ["Mengyu Zhao "], + "archive": { + "url": "https://zenodo.org/records/15920863/files/Z3-Parti-Z3pp-at-SMT-COMP-2025-build.zip" + }, + "website": "https://github.com/shaowei-cai-group/Z3-Parti-Z3pp-at-SMT-COMP-2025", + "system_description": "https://github.com/shaowei-cai-group/Z3-Parti-Z3pp-at-SMT-COMP-2025/blob/master/Z3_Parti_Z3pp_at_SMT_COMP_2025.pdf", + "command": ["./Z3-Parti-Z3pp-at-SMT-COMP-2025-build/solver/run_AriParti.py", "8"], + "solver_type": "wrapped", + "seed": "998244353", + "participations": [ + { + "tracks": ["Parallel"], + "logics": ["QF_RDL", "QF_IDL", "QF_LRA", "QF_LIA", "QF_NRA", "QF_NIA"] + } + ], + "competitive": false, + "final": true +} diff --git a/submissions/Z3-Parti-Z3pp.json b/submissions/Z3-Parti-Z3pp.json index 78890447..6a7ba487 100644 --- a/submissions/Z3-Parti-Z3pp.json +++ b/submissions/Z3-Parti-Z3pp.json @@ -6,11 +6,11 @@ ], "contacts": ["Mengyu Zhao "], "archive": { - "url": "https://zenodo.org/records/15763079/files/Z3-Parti-Z3pp-at-SMT-COMP-2025-build.zip" + "url": "https://zenodo.org/records/15920863/files/Z3-Parti-Z3pp-at-SMT-COMP-2025-build.zip" }, "website": "https://github.com/shaowei-cai-group/Z3-Parti-Z3pp-at-SMT-COMP-2025", "system_description": "https://github.com/shaowei-cai-group/Z3-Parti-Z3pp-at-SMT-COMP-2025/blob/master/Z3_Parti_Z3pp_at_SMT_COMP_2025.pdf", - "command": ["./Z3-Parti-Z3pp-at-SMT-COMP-2025-build/solver/run_AriParti.py"], + "command": ["./Z3-Parti-Z3pp-at-SMT-COMP-2025-build/solver/run_AriParti.py", "64"], "solver_type": "wrapped", "seed": "998244353", "participations": [ From 68d603d32a6a3308f66220588167206f40e65908 Mon Sep 17 00:00:00 2001 From: Tomaqa Date: Sun, 20 Jul 2025 15:56:23 +0200 Subject: [PATCH 03/25] SMTS submission 2025 update (bug fix + 2 more versions) (#203) --- submissions/smts-32.json | 37 +++++++++++++++++++++++++++++++++++++ submissions/smts-64.json | 37 +++++++++++++++++++++++++++++++++++++ submissions/smts.json | 6 +++--- 3 files changed, 77 insertions(+), 3 deletions(-) create mode 100644 submissions/smts-32.json create mode 100644 submissions/smts-64.json diff --git a/submissions/smts-32.json b/submissions/smts-32.json new file mode 100644 index 00000000..08867c9e --- /dev/null +++ b/submissions/smts-32.json @@ -0,0 +1,37 @@ +{ + "name": "SMTS (32 cores)", + "contributors": [ + { "name": "Tomáš Kolárik", "website": "https://github.com/Tomaqa" } + , + { "name": "Antti E. J. Hyvärinen", "website": "https://github.com/aehyvari" } + , + { "name": "Seyedmasoud Asadzadeh", "website": "https://masoudasadzade.github.io" } + ], + "contacts": [ + "Tomáš Kolárik " + ], + "archive": { + "url": "https://zenodo.org/records/16024075/files/smts.tar.bz2" + , + "h": { "sha256": "2d8b45c2458493d45f632f9657a735d90957667caf7eb980b17b9b832b8bcc24" } + }, + "command": ["./SMTS/server/smts.py", "-l", "-p", "-o", "32", "-fp"], + "website": "https://github.com/usi-verification-and-security/SMTS", + "system_description": "https://github.com/usi-verification-and-security/opensmt-doc/blob/master/smt-comp/abstract-2025.pdf", + "solver_type": "Standalone", + "participations": [ + { + "tracks": ["Parallel"], + "logics": [ + "QF_UF", "QF_AX", + "QF_IDL", "QF_RDL", "QF_LIA", "QF_LRA", + "QF_UFIDL", "QF_UFLIA", "QF_UFLRA", + "QF_ALIA", + "QF_AUFLIA" + ] + } + ], + "seed": 89, + "competitive": false, + "final": true +} diff --git a/submissions/smts-64.json b/submissions/smts-64.json new file mode 100644 index 00000000..52223da8 --- /dev/null +++ b/submissions/smts-64.json @@ -0,0 +1,37 @@ +{ + "name": "SMTS (64 cores)", + "contributors": [ + { "name": "Tomáš Kolárik", "website": "https://github.com/Tomaqa" } + , + { "name": "Antti E. J. Hyvärinen", "website": "https://github.com/aehyvari" } + , + { "name": "Seyedmasoud Asadzadeh", "website": "https://masoudasadzade.github.io" } + ], + "contacts": [ + "Tomáš Kolárik " + ], + "archive": { + "url": "https://zenodo.org/records/16024075/files/smts.tar.bz2" + , + "h": { "sha256": "2d8b45c2458493d45f632f9657a735d90957667caf7eb980b17b9b832b8bcc24" } + }, + "command": ["./SMTS/server/smts.py", "-l", "-p", "-o", "64", "-fp"], + "website": "https://github.com/usi-verification-and-security/SMTS", + "system_description": "https://github.com/usi-verification-and-security/opensmt-doc/blob/master/smt-comp/abstract-2025.pdf", + "solver_type": "Standalone", + "participations": [ + { + "tracks": ["Parallel"], + "logics": [ + "QF_UF", "QF_AX", + "QF_IDL", "QF_RDL", "QF_LIA", "QF_LRA", + "QF_UFIDL", "QF_UFLIA", "QF_UFLRA", + "QF_ALIA", + "QF_AUFLIA" + ] + } + ], + "seed": 89, + "competitive": false, + "final": true +} diff --git a/submissions/smts.json b/submissions/smts.json index b3ccb33f..b973f5bc 100644 --- a/submissions/smts.json +++ b/submissions/smts.json @@ -11,11 +11,11 @@ "Tomáš Kolárik " ], "archive": { - "url": "https://zenodo.org/records/15756050/files/smts.tar.bz2" + "url": "https://zenodo.org/records/16024075/files/smts.tar.bz2" , - "h": { "sha256": "9de09b0fd757b904ef0c0e8bc515bdf1a9a615e3b140279bd41783c24638e2b8" } + "h": { "sha256": "2d8b45c2458493d45f632f9657a735d90957667caf7eb980b17b9b832b8bcc24" } }, - "command": ["./SMTS/server/smts.py", "-l", "-p", "-pt", "2", "-nt", "30", "-o", "128", "-fp"], + "command": ["./SMTS/server/smts.py", "-l", "-p", "-o", "128", "-fp"], "website": "https://github.com/usi-verification-and-security/SMTS", "system_description": "https://github.com/usi-verification-and-security/opensmt-doc/blob/master/smt-comp/abstract-2025.pdf", "solver_type": "Standalone", From f4fa30909530a2e1630ec5389c853931835bc7fc Mon Sep 17 00:00:00 2001 From: Dominik Winterer Date: Wed, 30 Jul 2025 11:32:17 +0200 Subject: [PATCH 04/25] present derived solvers' increment over base solver --- smtcomp/generate_website_page.py | 60 +++++++++++++------ .../smtcomp/layouts/_default/result.html | 12 +++- 2 files changed, 52 insertions(+), 20 deletions(-) diff --git a/smtcomp/generate_website_page.py b/smtcomp/generate_website_page.py index ce3a5b0c..ca241dd0 100644 --- a/smtcomp/generate_website_page.py +++ b/smtcomp/generate_website_page.py @@ -12,7 +12,6 @@ from smtcomp.utils import * import smtcomp.results - def to_track_name(track: defs.Track) -> str: match track: case defs.Track.SingleQuery: @@ -94,6 +93,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 @@ -241,24 +242,46 @@ def podium_steps(podium: List[dict[str, Any]] | None) -> List[PodiumStep]: if podium is None: return [] else: - return [ - PodiumStep( - name=s["solver"], - competing="yes", # TODO - errorScore=s["error_score"], - correctScore=s["correctly_solved_score"], - CPUScore=s["cpu_time_score"], - WallScore=s["wallclock_time_score"], - solved=s["solved"], - solved_sat=s["solved_sat"], - solved_unsat=s["solved_unsat"], - unsolved=s["unsolved"], - abstained=s["abstained"], - timeout=s["timeout"], - memout=s["memout"], + baseMap = { #TODO: remove hardcode for SMT-COMP 2025 + "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" + } + podiums = [] + for s in podium: + cscore = s["correctly_solved_score"] + delta = 0 + if baseMap.get(s["solver"], "") != "": + for sprime in podium: + if sprime["solver"] == baseMap.get(s["solver"], ""): + delta = cscore - sprime["correctly_solved_score"] + break + + podiums.append( + PodiumStep( + name=s["solver"], + baseSolver=baseMap.get(s["solver"], ""), + deltaBaseSolver=delta, + competing="yes", # TODO: Update this if needed + errorScore=s["error_score"], + correctScore=s["correctly_solved_score"], + CPUScore=s["cpu_time_score"], + WallScore=s["wallclock_time_score"], + solved=s["solved"], + solved_sat=s["solved_sat"], + solved_unsat=s["solved_unsat"], + unsolved=s["unsolved"], + abstained=s["abstained"], + timeout=s["timeout"], + memout=s["memout"], + ) ) - for s in podium - ] + return podiums + def make_podium(config: defs.Config, d: dict[str, Any], for_division: bool, track: defs.Track) -> PodiumDivision: @@ -768,7 +791,6 @@ def largest_contribution( def export_results(config: defs.Config, selection: pl.LazyFrame, results: pl.LazyFrame, track: defs.Track) -> None: - page_suffix = page_track_suffix(track) dst = config.web_results diff --git a/web/themes/smtcomp/layouts/_default/result.html b/web/themes/smtcomp/layouts/_default/result.html index 8e1e5a4f..a5caf468 100644 --- a/web/themes/smtcomp/layouts/_default/result.html +++ b/web/themes/smtcomp/layouts/_default/result.html @@ -97,7 +97,17 @@

{{ index $category_names $cat }} Performance

* {{ end }} - {{ $solver.correctScore }} + {{ $solver.correctScore }} + + {{ if not (eq $solver.baseSolver "") }} + {{ if not (lt $solver.deltaBaseSolver 0) }} + (+{{ $solver.deltaBaseSolver }}) + {{ else }} + (-{{ $solver.deltaBaseSolver }}) + {{ end }} + {{ end }} + + {{ $solver.CPUScore }} {{ $solver.WallScore }} From 9d64aeee0b5cfc79898242548924ce9642548e5b Mon Sep 17 00:00:00 2001 From: Dominik Winterer Date: Wed, 30 Jul 2025 13:39:31 +0200 Subject: [PATCH 05/25] cosmetics --- web/themes/smtcomp/layouts/_default/result.html | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/web/themes/smtcomp/layouts/_default/result.html b/web/themes/smtcomp/layouts/_default/result.html index a5caf468..a8b5b10a 100644 --- a/web/themes/smtcomp/layouts/_default/result.html +++ b/web/themes/smtcomp/layouts/_default/result.html @@ -98,7 +98,7 @@

{{ index $category_names $cat }} Performance

{{ end }} {{ $solver.correctScore }} - + {{ if not (eq $solver.baseSolver "") }} {{ if not (lt $solver.deltaBaseSolver 0) }} (+{{ $solver.deltaBaseSolver }}) @@ -106,7 +106,7 @@

{{ index $category_names $cat }} Performance

(-{{ $solver.deltaBaseSolver }}) {{ end }} {{ end }} - + {{ $solver.CPUScore }} {{ $solver.WallScore }} @@ -122,6 +122,9 @@

{{ index $category_names $cat }} Performance

{{ end }} + + (+/- n): for derived solvers: correct score increment over base solver + {{ end }} {{ end }} From 8f1c05422fe85172a5b567ef971684ff31d6c288 Mon Sep 17 00:00:00 2001 From: Dominik Winterer Date: Wed, 30 Jul 2025 16:18:39 +0200 Subject: [PATCH 06/25] interim --- smtcomp/defs.py | 16 ++++++- smtcomp/generate_website_page.py | 35 +++++++------- web/themes/smtcomp/assets/css/main.css | 2 +- .../smtcomp/layouts/_default/result.html | 48 ++++++++++--------- 4 files changed, 56 insertions(+), 45 deletions(-) diff --git a/smtcomp/defs.py b/smtcomp/defs.py index ebc3cc08..c6bb6974 100644 --- a/smtcomp/defs.py +++ b/smtcomp/defs.py @@ -15,6 +15,17 @@ U = TypeVar("U") +baseMapSMTLIB2025 = { + "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" +} + + class EnumAutoInt(Enum): """ Normal enum with strings, but each enum is associated to an int @@ -135,7 +146,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 +1328,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 @@ -1324,7 +1336,7 @@ class Submission(BaseModel, extra="forbid"): default=False, 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): diff --git a/smtcomp/generate_website_page.py b/smtcomp/generate_website_page.py index ca241dd0..30c0fd39 100644 --- a/smtcomp/generate_website_page.py +++ b/smtcomp/generate_website_page.py @@ -242,31 +242,23 @@ def podium_steps(podium: List[dict[str, Any]] | None) -> List[PodiumStep]: if podium is None: return [] else: - baseMap = { #TODO: remove hardcode for SMT-COMP 2025 - "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" - } podiums = [] + base_solvers = [] for s in podium: cscore = s["correctly_solved_score"] delta = 0 - if baseMap.get(s["solver"], "") != "": - for sprime in podium: - if sprime["solver"] == baseMap.get(s["solver"], ""): + derived_solver = defs.baseMapSMTLIB2025.get(s["solver"], "") + if derived_solver != "": + for sprime in podium: + if sprime["solver"] == defs.baseMapSMTLIB2025.get(s["solver"], ""): delta = cscore - sprime["correctly_solved_score"] break - podiums.append( - PodiumStep( + ps = PodiumStep( name=s["solver"], - baseSolver=baseMap.get(s["solver"], ""), + baseSolver=derived_solver, deltaBaseSolver=delta, - competing="yes", # TODO: Update this if needed + competing="no" if "-base" in s["solver"] else "yes", errorScore=s["error_score"], correctScore=s["correctly_solved_score"], CPUScore=s["cpu_time_score"], @@ -278,9 +270,14 @@ def podium_steps(podium: List[dict[str, Any]] | None) -> List[PodiumStep]: abstained=s["abstained"], timeout=s["timeout"], memout=s["memout"], - ) - ) - return podiums + ) + + if "-base" in s["solver"]: + base_solvers.append(ps) + else: + podiums.append(ps) + + return podiums + base_solvers diff --git a/web/themes/smtcomp/assets/css/main.css b/web/themes/smtcomp/assets/css/main.css index 6d9216c3..5df8e00e 100644 --- a/web/themes/smtcomp/assets/css/main.css +++ b/web/themes/smtcomp/assets/css/main.css @@ -593,7 +593,7 @@ td.left { } td.non-competing-grey { - color: #707070; + color:gray; a { color: #808080; } diff --git a/web/themes/smtcomp/layouts/_default/result.html b/web/themes/smtcomp/layouts/_default/result.html index a8b5b10a..635609fd 100644 --- a/web/themes/smtcomp/layouts/_default/result.html +++ b/web/themes/smtcomp/layouts/_default/result.html @@ -88,42 +88,44 @@

{{ index $category_names $cat }} Performance

{{ range $solver := . }} - - + + {{ $solver.name }} {{ if eq $solver.competing "no" }}n{{ end }} - {{ $solver.errorScore }} + {{ $solver.errorScore }} {{ if $solver.errorFootnote }} * {{ end }} - {{ $solver.correctScore }} - - {{ if not (eq $solver.baseSolver "") }} - {{ if not (lt $solver.deltaBaseSolver 0) }} - (+{{ $solver.deltaBaseSolver }}) - {{ else }} - (-{{ $solver.deltaBaseSolver }}) - {{ end }} + + {{ $solver.correctScore }} + {{ if not (eq $solver.baseSolver "") }} + {{ if not (lt $solver.deltaBaseSolver 0) }} +
(base +{{ $solver.deltaBaseSolver }}) + {{ else }} +
(base -{{ $solver.deltaBaseSolver }}) {{ end }} - + {{ end }} - {{ $solver.CPUScore }} - {{ $solver.WallScore }} + {{ $solver.CPUScore }} + {{ $solver.WallScore }} - {{ $solver.solved }} - {{ $solver.solved_sat }} - {{ $solver.solved_unsat }} - {{ $solver.unsolved }} - {{ $solver.abstained }} + {{ $solver.solved }} + {{ $solver.solved_sat }} + {{ $solver.solved_unsat }} + {{ $solver.unsolved }} + {{ $solver.abstained }} - {{ $solver.timeout }} - {{ $solver.memout }} + {{ $solver.timeout }} + {{ $solver.memout }} {{ end }} - - (+/- n): for derived solvers: correct score increment over base solver + + (base +/- n): for derived solvers: increment over base solver
+ + + n: non-competing solver {{ end }} {{ end }} From b338b904d4d7b479143fd52e2bd14a7be611f5f1 Mon Sep 17 00:00:00 2001 From: Dominik Winterer Date: Wed, 30 Jul 2025 16:22:43 +0200 Subject: [PATCH 07/25] minor --- smtcomp/generate_website_page.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/smtcomp/generate_website_page.py b/smtcomp/generate_website_page.py index 30c0fd39..6a41fb56 100644 --- a/smtcomp/generate_website_page.py +++ b/smtcomp/generate_website_page.py @@ -258,7 +258,7 @@ def podium_steps(podium: List[dict[str, Any]] | None) -> List[PodiumStep]: name=s["solver"], baseSolver=derived_solver, deltaBaseSolver=delta, - competing="no" if "-base" in s["solver"] else "yes", + competing="no" if "-base" in s["solver"] else "yes", #TODO: establish s["competing"] errorScore=s["error_score"], correctScore=s["correctly_solved_score"], CPUScore=s["cpu_time_score"], From 8b1ec77fe5f36a53b70746ac51edf74984057389 Mon Sep 17 00:00:00 2001 From: Dominik Winterer Date: Wed, 30 Jul 2025 16:37:15 +0200 Subject: [PATCH 08/25] fixing CI issues --- smtcomp/defs.py | 7 ++-- smtcomp/generate_website_page.py | 38 +++++++++---------- web/themes/smtcomp/assets/css/main.css | 2 +- .../smtcomp/layouts/_default/result.html | 4 +- 4 files changed, 26 insertions(+), 25 deletions(-) diff --git a/smtcomp/defs.py b/smtcomp/defs.py index c6bb6974..cb57c784 100644 --- a/smtcomp/defs.py +++ b/smtcomp/defs.py @@ -22,7 +22,7 @@ "Z3-Owl": "Z3-Owl-base", "Z3-Noodler": "Z3-Noodler", "z3siri": "z3siri-base", - "Z3-alpha": "Z3-alpha-base" + "Z3-alpha": "Z3-alpha-base", } @@ -146,7 +146,7 @@ def name_is_default_field(cls, data: Any) -> Any: class SolverType(EnumAutoInt): wrapped = "wrapped" - derived = "derived" # TODO: put a datatype information on base solver + derived = "derived" # TODO: put a datatype information on base solver standalone = "Standalone" portfolio = "Portfolio" @@ -1336,7 +1336,8 @@ class Submission(BaseModel, extra="forbid"): default=False, 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 + + # 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): diff --git a/smtcomp/generate_website_page.py b/smtcomp/generate_website_page.py index 6a41fb56..096d6bbd 100644 --- a/smtcomp/generate_website_page.py +++ b/smtcomp/generate_website_page.py @@ -12,6 +12,7 @@ from smtcomp.utils import * import smtcomp.results + def to_track_name(track: defs.Track) -> str: match track: case defs.Track.SingleQuery: @@ -255,30 +256,29 @@ def podium_steps(podium: List[dict[str, Any]] | None) -> List[PodiumStep]: break ps = PodiumStep( - name=s["solver"], - baseSolver=derived_solver, - deltaBaseSolver=delta, - competing="no" if "-base" in s["solver"] else "yes", #TODO: establish s["competing"] - errorScore=s["error_score"], - correctScore=s["correctly_solved_score"], - CPUScore=s["cpu_time_score"], - WallScore=s["wallclock_time_score"], - solved=s["solved"], - solved_sat=s["solved_sat"], - solved_unsat=s["solved_unsat"], - unsolved=s["unsolved"], - abstained=s["abstained"], - timeout=s["timeout"], - memout=s["memout"], - ) - + name=s["solver"], + baseSolver=derived_solver, + deltaBaseSolver=delta, + competing="no" if "-base" in s["solver"] else "yes", # TODO: establish s["competing"] + errorScore=s["error_score"], + correctScore=s["correctly_solved_score"], + CPUScore=s["cpu_time_score"], + WallScore=s["wallclock_time_score"], + solved=s["solved"], + solved_sat=s["solved_sat"], + solved_unsat=s["solved_unsat"], + unsolved=s["unsolved"], + abstained=s["abstained"], + timeout=s["timeout"], + memout=s["memout"], + ) + if "-base" in s["solver"]: base_solvers.append(ps) else: podiums.append(ps) - - return podiums + base_solvers + return podiums + base_solvers def make_podium(config: defs.Config, d: dict[str, Any], for_division: bool, track: defs.Track) -> PodiumDivision: diff --git a/web/themes/smtcomp/assets/css/main.css b/web/themes/smtcomp/assets/css/main.css index 5df8e00e..8203b2d2 100644 --- a/web/themes/smtcomp/assets/css/main.css +++ b/web/themes/smtcomp/assets/css/main.css @@ -593,7 +593,7 @@ td.left { } td.non-competing-grey { - color:gray; + color: gray; a { color: #808080; } diff --git a/web/themes/smtcomp/layouts/_default/result.html b/web/themes/smtcomp/layouts/_default/result.html index 635609fd..04216843 100644 --- a/web/themes/smtcomp/layouts/_default/result.html +++ b/web/themes/smtcomp/layouts/_default/result.html @@ -122,10 +122,10 @@

{{ index $category_names $cat }} Performance

{{ end }} - (base +/- n): for derived solvers: increment over base solver
+ (base +/- n): for derived solvers: increment over base solver
- n: non-competing solver + n: non-competing solver {{ end }} {{ end }} From 68cc10a581ff3f6114cc2f22fd46cc27955c3536 Mon Sep 17 00:00:00 2001 From: Dominik Winterer Date: Sat, 2 Aug 2025 18:52:24 +0200 Subject: [PATCH 09/25] establishing consistency among submissions with multiple cores --- submissions/STP-Parti-Bitwuzla-p16.json | 2 +- submissions/STP-Parti-Bitwuzla-p8.json | 2 +- submissions/Z3-Parti-Z3pp-p16.json | 2 +- submissions/Z3-Parti-Z3pp-p32.json | 2 +- submissions/Z3-Parti-Z3pp-p8.json | 2 +- submissions/bitwuzla_parallel_16.json | 2 +- submissions/bitwuzla_parallel_32.json | 2 +- 7 files changed, 7 insertions(+), 7 deletions(-) diff --git a/submissions/STP-Parti-Bitwuzla-p16.json b/submissions/STP-Parti-Bitwuzla-p16.json index eb5a13b4..79c8df9e 100644 --- a/submissions/STP-Parti-Bitwuzla-p16.json +++ b/submissions/STP-Parti-Bitwuzla-p16.json @@ -1,5 +1,5 @@ { - "name": "STP-Parti-Bitwuzla-32core", + "name": "STP-Parti-Bitwuzla-16core", "contributors": [ "Mengyu Zhao", "Zhenghang Xu", diff --git a/submissions/STP-Parti-Bitwuzla-p8.json b/submissions/STP-Parti-Bitwuzla-p8.json index a123e462..8e8f3436 100644 --- a/submissions/STP-Parti-Bitwuzla-p8.json +++ b/submissions/STP-Parti-Bitwuzla-p8.json @@ -1,5 +1,5 @@ { - "name": "STP-Parti-Bitwuzla-16core", + "name": "STP-Parti-Bitwuzla-8core", "contributors": [ "Mengyu Zhao", "Zhenghang Xu", diff --git a/submissions/Z3-Parti-Z3pp-p16.json b/submissions/Z3-Parti-Z3pp-p16.json index 03ea07d9..ed933335 100644 --- a/submissions/Z3-Parti-Z3pp-p16.json +++ b/submissions/Z3-Parti-Z3pp-p16.json @@ -1,5 +1,5 @@ { - "name": "Z3-Parti-Z3pp-32core", + "name": "Z3-Parti-Z3pp-16core", "contributors": [ "Mengyu Zhao", "Shaowei Cai" diff --git a/submissions/Z3-Parti-Z3pp-p32.json b/submissions/Z3-Parti-Z3pp-p32.json index 8cc45168..edc79836 100644 --- a/submissions/Z3-Parti-Z3pp-p32.json +++ b/submissions/Z3-Parti-Z3pp-p32.json @@ -1,5 +1,5 @@ { - "name": "Z3-Parti-Z3pp-64core", + "name": "Z3-Parti-Z3pp-32core", "contributors": [ "Mengyu Zhao", "Shaowei Cai" diff --git a/submissions/Z3-Parti-Z3pp-p8.json b/submissions/Z3-Parti-Z3pp-p8.json index 2e24e12c..451aedd8 100644 --- a/submissions/Z3-Parti-Z3pp-p8.json +++ b/submissions/Z3-Parti-Z3pp-p8.json @@ -1,5 +1,5 @@ { - "name": "Z3-Parti-Z3pp-16core", + "name": "Z3-Parti-Z3pp-8core", "contributors": [ "Mengyu Zhao", "Shaowei Cai" diff --git a/submissions/bitwuzla_parallel_16.json b/submissions/bitwuzla_parallel_16.json index 9e8bfd03..f2b6c74e 100644 --- a/submissions/bitwuzla_parallel_16.json +++ b/submissions/bitwuzla_parallel_16.json @@ -1,5 +1,5 @@ { - "name": "Bitwuzla-32core", + "name": "Bitwuzla-16core", "contributors": ["Aina Niemetz", "Mathias Preiner"], "contacts": ["Mathias Preiner "], "final" : true, diff --git a/submissions/bitwuzla_parallel_32.json b/submissions/bitwuzla_parallel_32.json index 7e50a7f5..20bb9a0a 100644 --- a/submissions/bitwuzla_parallel_32.json +++ b/submissions/bitwuzla_parallel_32.json @@ -1,5 +1,5 @@ { - "name": "Bitwuzla-64core", + "name": "Bitwuzla-32core", "contributors": ["Aina Niemetz", "Mathias Preiner"], "contacts": ["Mathias Preiner "], "final" : true, From 7468375cbf9ff2f4d6a5b5c3f076339fd7bba2ec Mon Sep 17 00:00:00 2001 From: Dominik Winterer Date: Mon, 4 Aug 2025 11:51:57 +0200 Subject: [PATCH 10/25] 2024 -> 2025 --- Makefile | 8 ++++---- smtcomp/generate_website_page.py | 8 ++++---- web/themes/smtcomp/layouts/_default/results_summary.html | 2 +- 3 files changed, 9 insertions(+), 9 deletions(-) diff --git a/Makefile b/Makefile index 34126eb9..0e6ba0cd 100644 --- a/Makefile +++ b/Makefile @@ -70,14 +70,14 @@ results-generation: @poetry run smtcomp export-results-pages data SingleQuery @echo "🚀 Generating results to web/content/results for ModelValidation" @poetry run smtcomp export-results-pages data ModelValidation - @echo "🚀 Generating results to web/content/results for UnsatCore" - @poetry run smtcomp export-results-pages data UnsatCore + #@echo "🚀 Generating results to web/content/results for UnsatCore" + #@poetry run smtcomp export-results-pages data UnsatCore @echo "🚀 Generating results to web/content/results for Incremental" @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 cache: @echo "🚀 Generating cache" diff --git a/smtcomp/generate_website_page.py b/smtcomp/generate_website_page.py index 096d6bbd..47ddbbb4 100644 --- a/smtcomp/generate_website_page.py +++ b/smtcomp/generate_website_page.py @@ -304,7 +304,7 @@ def get_winner(l: List[dict[str, str]] | None) -> str: steps_seq = podium_steps(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}", participants=f"participants_{config.current_year}", @@ -492,7 +492,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}", @@ -610,7 +610,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}", @@ -705,7 +705,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}", diff --git a/web/themes/smtcomp/layouts/_default/results_summary.html b/web/themes/smtcomp/layouts/_default/results_summary.html index 0718a9ff..09c75760 100644 --- a/web/themes/smtcomp/layouts/_default/results_summary.html +++ b/web/themes/smtcomp/layouts/_default/results_summary.html @@ -25,7 +25,7 @@ {{ $categories_pretty := .Site.Data.pretty_names.performance }} -

SMT-COMP 2024 Results - {{ $prettyTrack }}

+

SMT-COMP 2025 Results - {{ $prettyTrack }}

Summary of all competition results for the {{ $prettyTrack }}. From f4efacfca3766f0669926f079bf41c6c7c9d9c2e Mon Sep 17 00:00:00 2001 From: Dominik Winterer Date: Mon, 4 Aug 2025 11:54:42 +0200 Subject: [PATCH 11/25] 2024 -> 2025 --- web/themes/smtcomp/layouts/_default/results.html | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/web/themes/smtcomp/layouts/_default/results.html b/web/themes/smtcomp/layouts/_default/results.html index cfbd8812..33ac64b4 100644 --- a/web/themes/smtcomp/layouts/_default/results.html +++ b/web/themes/smtcomp/layouts/_default/results.html @@ -15,7 +15,7 @@ "UnsatCore" "unsat-core" }} -

SMT-COMP 2024 Results

+

SMT-COMP 2025 Results

{{ if isset $data "processed" }} The processed data are available in the GitHub repository. From 7ef410fe7933845d5995686300ba64e66a805f41 Mon Sep 17 00:00:00 2001 From: Dominik Winterer Date: Mon, 4 Aug 2025 12:13:46 +0200 Subject: [PATCH 12/25] target for cleaning up web results --- Makefile | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/Makefile b/Makefile index 0e6ba0cd..94eeb3c0 100644 --- a/Makefile +++ b/Makefile @@ -31,6 +31,10 @@ 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 + .PHONY: help help: @grep -E '^[a-zA-Z_-]+:.*?## .*$$' $(MAKEFILE_LIST) | awk 'BEGIN {FS = ":.*?## "}; {printf "\033[36m%-20s\033[0m %s\n", $$1, $$2}' @@ -70,8 +74,8 @@ results-generation: @poetry run smtcomp export-results-pages data SingleQuery @echo "🚀 Generating results to web/content/results for ModelValidation" @poetry run smtcomp export-results-pages data ModelValidation - #@echo "🚀 Generating results to web/content/results for UnsatCore" - #@poetry run smtcomp export-results-pages data UnsatCore + @echo "🚀 Generating results to web/content/results for UnsatCore" + @poetry run smtcomp export-results-pages data UnsatCore @echo "🚀 Generating results to web/content/results for Incremental" @poetry run smtcomp export-results-pages data Incremental # @echo "🚀 Generating results to web/content/results for Cloud" From 71e53652884844e9919222ce62371505b1b3004f Mon Sep 17 00:00:00 2001 From: Dominik Winterer Date: Mon, 4 Aug 2025 13:55:18 +0200 Subject: [PATCH 13/25] feat: show legends for base and non-competing only when at least one solver present --- .../smtcomp/layouts/_default/result.html | 19 +++++++++++++++++++ 1 file changed, 19 insertions(+) diff --git a/web/themes/smtcomp/layouts/_default/result.html b/web/themes/smtcomp/layouts/_default/result.html index 04216843..f23861e7 100644 --- a/web/themes/smtcomp/layouts/_default/result.html +++ b/web/themes/smtcomp/layouts/_default/result.html @@ -6,6 +6,9 @@ {{ $trueDivision := and (isset .Params "logics") (.Params.logics | len | ne 0) }} {{ $prettyTrack := index .Site.Data.pretty_names.track .Params.track }} + {{ $hasBaseSolvers := false }} + {{ $hasNoncompetingSolvers := false }} +

{{ .Params.division }} ({{ $prettyTrack }})

Competition results for the {{ .Params.division }} @@ -88,6 +91,12 @@

{{ index $category_names $cat }} Performance

{{ range $solver := . }} + +{{ if eq $solver.competing "no" }} + {{ $.Scratch.Set "hasNonCompetingSolvers" true }} +{{ end }} + + {{ $solver.name }} {{ if eq $solver.competing "no" }}n{{ end }} @@ -100,6 +109,7 @@

{{ index $category_names $cat }} Performance

{{ $solver.correctScore }} {{ if not (eq $solver.baseSolver "") }} + {{ $.Scratch.Set "hasBaseSolvers" true }} {{ if not (lt $solver.deltaBaseSolver 0) }}
(base +{{ $solver.deltaBaseSolver }}) {{ else }} @@ -121,12 +131,21 @@

{{ index $category_names $cat }} Performance

{{ end }} + +{{ if ($.Scratch.Get "hasBaseSolvers") }} (base +/- n): for derived solvers: increment over base solver
+{{ end }} + +{{ if ($.Scratch.Get "hasNonCompetingSolvers") }} n: non-competing solver +{{ end }} + + + {{ end }} {{ end }} From ac178bdadc11914310eb0fb4940fdefd9630f300 Mon Sep 17 00:00:00 2001 From: Dominik Winterer Date: Mon, 4 Aug 2025 18:18:05 +0200 Subject: [PATCH 14/25] feat: non-competitive divisions will be marked --- smtcomp/generate_website_page.py | 28 ++++++++++++++-- .../smtcomp/layouts/_default/result.html | 33 ++++++++++++------- .../layouts/_default/results_summary.html | 3 ++ 3 files changed, 51 insertions(+), 13 deletions(-) diff --git a/smtcomp/generate_website_page.py b/smtcomp/generate_website_page.py index 52a8f68c..2eb95b72 100644 --- a/smtcomp/generate_website_page.py +++ b/smtcomp/generate_website_page.py @@ -117,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 @@ -281,7 +282,9 @@ def podium_steps(podium: List[dict[str, Any]] | None) -> List[PodiumStep]: return podiums + base_solvers -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 or l[0]["correctly_solved_score"] == 0: @@ -289,7 +292,27 @@ def get_winner(l: List[dict[str, str]] | None) -> str: else: return l[0]["solver"] + def is_competitive(results: pl.LazyFrame, division: int) -> 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") == division) + .select("solver") + .unique() + .collect() + .get_column("solver") + .to_list() + ) + # Avoid solvers of the same solver family under the assumption + # of the following format: - (holds for SMT-COMP 2025) + # TODO: improve this criterion in the future + return len(set([sol.split("-")[0].lower() for sol in solvers])) >= 2 + + competitive_division = True if for_division: + competitive_division = is_competitive(results, d["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: @@ -307,6 +330,7 @@ def get_winner(l: List[dict[str, str]] | None) -> str: 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, @@ -403,7 +427,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]: diff --git a/web/themes/smtcomp/layouts/_default/result.html b/web/themes/smtcomp/layouts/_default/result.html index f23861e7..e2cbe4e1 100644 --- a/web/themes/smtcomp/layouts/_default/result.html +++ b/web/themes/smtcomp/layouts/_default/result.html @@ -9,20 +9,29 @@ {{ $hasBaseSolvers := false }} {{ $hasNoncompetingSolvers := false }} + +{{ if .Params.is_competitive }}

{{ .Params.division }} ({{ $prettyTrack }})

-

- Competition results for the {{ .Params.division }} - {{ if $trueDivision }} division {{ else }} logic {{ end }} - in the {{ $prettyTrack }}. -

+

+ Competition results for the {{ .Params.division }} + {{ if $trueDivision }} division {{ else }} logic {{ end }} + in the {{ $prettyTrack }}. +

Results were generated on {{ .Params.resultdate }}

+

+

+ Benchmarks: {{ .Params.n_benchmarks }}
+ Time Limit: {{ .Params.time_limit }} seconds
+ Memory Limit: {{ .Params.mem_limit }} GB +

+{{ else }} +

{{ .Params.division }} ({{ $prettyTrack }})
non-competitive

+

+ Benchmarks: {{ .Params.n_benchmarks }}
+

+{{ end }} + -

Results were generated on {{ .Params.resultdate }}

-

- Benchmarks: {{ .Params.n_benchmarks }}
- Time Limit: {{ .Params.time_limit }} seconds
- Memory Limit: {{ .Params.mem_limit }} GB -

{{ if $trueDivision }} Logics: