diff --git a/Makefile b/Makefile index 6bcc769e..34126eb9 100644 --- a/Makefile +++ b/Makefile @@ -55,7 +55,7 @@ submission-doc: submission-generation participant-data: @echo "🚀 Generating participant data to $(PARTICIPANT_DATA_FILE)" - @if [ -e "submissions/*.json" ]; then poetry run smtcomp show-json submissions/*.json $(PARTICIPANT_DATA_FILE); fi + @poetry run smtcomp show-json submissions/*.json $(PARTICIPANT_DATA_FILE) track-data: @echo "🚀 Generating track data to $(TRACK_DATA_FILE)" diff --git a/smtcomp/defs.py b/smtcomp/defs.py index 38d86e96..ebc3cc08 100644 --- a/smtcomp/defs.py +++ b/smtcomp/defs.py @@ -1466,9 +1466,9 @@ class Config: """Prioritize triviality as much as possible for testing purpose. Look for simple problems instead of hard one""" - nyse_seed = 17817 + nyse_seed = 20_338_41 """The integer part of one hundred times the opening value of the New York Stock Exchange Composite Index on the first day the exchange is open on or after the date specified in nyse_date""" - nyse_date = date(year=2024, month=6, day=17) + nyse_date = date(year=2025, month=6, day=30) aws_timelimit_hard = 180 """ @@ -1594,6 +1594,9 @@ def seed(self) -> int: unknown_seed = 0 seed = 0 for s in self.submissions: + if not s.competitive: + continue + if s.seed is None: unknown_seed += 1 else: diff --git a/smtcomp/submission.py b/smtcomp/submission.py index 35393559..56f4c0b8 100644 --- a/smtcomp/submission.py +++ b/smtcomp/submission.py @@ -57,7 +57,9 @@ def raw_summary(s: Submission) -> dict[str, Any]: data["website"] = str(s.website) data["archive_url"] = str(s.archive.url if s.archive is not None else "") data["system_description"] = str(s.system_description) + data["competitive"] = s.competitive data["tracks"] = dict[str, dict[str, list[str]]]() + data["seed"] = s.seed tracks = s.participations.get() for track, divs in sorted(tracks.items()): diff --git a/submissions/Amaya.json b/submissions/Amaya.json index 7b306ca6..c3e787ce 100644 --- a/submissions/Amaya.json +++ b/submissions/Amaya.json @@ -18,5 +18,6 @@ "tracks": ["SingleQuery"], "logics": ["LIA", "NIA"] } - ] + ], + "final" : true } diff --git a/submissions/Bitwuzla-MachBV-at-SMT-COMP-2025-base.json b/submissions/Bitwuzla-MachBV-at-SMT-COMP-2025-base.json index 84252767..6667b11e 100644 --- a/submissions/Bitwuzla-MachBV-at-SMT-COMP-2025-base.json +++ b/submissions/Bitwuzla-MachBV-at-SMT-COMP-2025-base.json @@ -10,7 +10,6 @@ "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" } ], diff --git a/submissions/COLIBRI.json b/submissions/COLIBRI.json index efc15bf2..31364646 100644 --- a/submissions/COLIBRI.json +++ b/submissions/COLIBRI.json @@ -18,5 +18,6 @@ "logics": "QF_.*FP(?!DT).*" } ], - "seed": 0 + "seed": 0, + "final" : true } diff --git a/submissions/STP-Parti-Bitwuzla-at-SMT-COMP-2025.json b/submissions/STP-Parti-Bitwuzla.json similarity index 94% rename from submissions/STP-Parti-Bitwuzla-at-SMT-COMP-2025.json rename to submissions/STP-Parti-Bitwuzla.json index 8d90c1c6..99ce499f 100644 --- a/submissions/STP-Parti-Bitwuzla-at-SMT-COMP-2025.json +++ b/submissions/STP-Parti-Bitwuzla.json @@ -1,5 +1,5 @@ { - "name": "STP-Parti-Bitwuzla-at-SMT-COMP-2025", + "name": "STP-Parti-Bitwuzla", "contributors": [ "Mengyu Zhao", "Zhenghang Xu", diff --git a/submissions/Z3-Inc-Z3++-base.json b/submissions/Z3-Inc-Z3++-base.json index 0223b9df..6f9624f0 100644 --- a/submissions/Z3-Inc-Z3++-base.json +++ b/submissions/Z3-Inc-Z3++-base.json @@ -11,9 +11,9 @@ "system_description": "https://link.springer.com/chapter/10.1007/978-3-540-78800-3_24", "command": [ "./smtcomp_run_incremental" ], "solver_type": "Standalone", - "seed": 174228, "participations": [ { "tracks": ["Incremental"], "logics": "QF_NIA" } ], - "competitive": false + "competitive": false, + "final" : true } diff --git a/submissions/Z3-Inc-Z3++.json b/submissions/Z3-Inc-Z3++.json index 75bbfdb3..0f6637df 100644 --- a/submissions/Z3-Inc-Z3++.json +++ b/submissions/Z3-Inc-Z3++.json @@ -15,5 +15,6 @@ "seed": "19970530", "participations": [ { "tracks": ["Incremental"], "logics": "QF_NIA" } - ] + ], + "final" : true } diff --git a/submissions/Z3-Noodler-Mocha-base.json b/submissions/Z3-Noodler-Mocha-base.json index 16be9592..03cbc432 100644 --- a/submissions/Z3-Noodler-Mocha-base.json +++ b/submissions/Z3-Noodler-Mocha-base.json @@ -14,11 +14,10 @@ "contacts": ["Lukáš Holík "], "website": "https://github.com/VeriFIT/z3-noodler", "system_description": "https://github.com/VeriFIT/z3-noodler/blob/devel/doc/noodler/z3-noodler-system-description-2025.pdf", - "command": [ "./z3-noodler" ], + "command": [ "./z3-noodler/build/z3" ], "solver_type": "derived", - "seed": 48655, "participations": [ - { "tracks": ["SingleQuery"], "logics": "QF_Strings" } + { "tracks": ["SingleQuery"], "divisions": ["QF_Strings"] } ], "competitive": false, "final": true diff --git a/submissions/Z3-base.json b/submissions/Z3-Owl-base.json similarity index 90% rename from submissions/Z3-base.json rename to submissions/Z3-Owl-base.json index 5ac9c8e9..b3b2425d 100644 --- a/submissions/Z3-base.json +++ b/submissions/Z3-Owl-base.json @@ -1,5 +1,5 @@ { - "name": "Z3-4.15.2.0", + "name": "Z3-Owl-base", "contributors": [ "Nikolaj Bjørner et al." ], @@ -11,7 +11,6 @@ "system_description": "https://link.springer.com/content/pdf/10.1007/978-3-540-78800-3_24.pdf", "solver_type": "Standalone", "command": ["./z3"], - "seed": "421", "participations": [ { "tracks": ["SingleQuery"], @@ -24,5 +23,7 @@ "QF_BVFP" ] } - ] + ], + "final" : true, + "competitive": false } diff --git a/submissions/Z3-Owl.json b/submissions/Z3-Owl.json index 463d5330..a8ea9c93 100644 --- a/submissions/Z3-Owl.json +++ b/submissions/Z3-Owl.json @@ -24,5 +24,6 @@ "QF_BVFP" ] } - ] + ], + "final" : true } diff --git a/submissions/Z3-Parti-Z3pp-at-SMT-COMP-2025.json b/submissions/Z3-Parti-Z3pp.json similarity index 94% rename from submissions/Z3-Parti-Z3pp-at-SMT-COMP-2025.json rename to submissions/Z3-Parti-Z3pp.json index d3461c70..78890447 100644 --- a/submissions/Z3-Parti-Z3pp-at-SMT-COMP-2025.json +++ b/submissions/Z3-Parti-Z3pp.json @@ -1,5 +1,5 @@ { - "name": "Z3-Parti-Z3pp-at-SMT-COMP-2025", + "name": "Z3-Parti-Z3pp", "contributors": [ "Mengyu Zhao", "Shaowei Cai" diff --git a/submissions/bv_decide-nokernel.json b/submissions/bv_decide-nokernel.json index a90d06db..ed2791b5 100644 --- a/submissions/bv_decide-nokernel.json +++ b/submissions/bv_decide-nokernel.json @@ -43,5 +43,6 @@ "--maxRecDepth=1048576" ] } - ] + ], + "final" : true } diff --git a/submissions/bv_decide.json b/submissions/bv_decide.json index d3479ae9..4590e291 100644 --- a/submissions/bv_decide.json +++ b/submissions/bv_decide.json @@ -42,5 +42,6 @@ "--maxRecDepth=1048576" ] } - ] + ], + "final" : true } diff --git a/submissions/cvc5.json b/submissions/cvc5.json index bb3f1719..b63bf4b9 100644 --- a/submissions/cvc5.json +++ b/submissions/cvc5.json @@ -59,5 +59,6 @@ "command": [ "bin/smtcomp_run_incremental" ] } ], -"seed": 8465677983 + "seed": 8465677983, + "final" : true } diff --git a/submissions/iprover.json b/submissions/iprover.json index 508b12ff..5b97d4ce 100644 --- a/submissions/iprover.json +++ b/submissions/iprover.json @@ -51,5 +51,6 @@ ] } ], - "seed": 139 + "seed": 139, + "final" : true } diff --git a/submissions/ostrich.json b/submissions/ostrich.json index 553c1130..70ea487c 100644 --- a/submissions/ostrich.json +++ b/submissions/ostrich.json @@ -21,5 +21,6 @@ "seed": "718582", "participations": [ { "tracks": ["SingleQuery"], "divisions": ["QF_Strings"] } - ] + ], + "final" : true } diff --git a/submissions/smtinterpol.json b/submissions/smtinterpol.json index 04200e9b..a944d9af 100644 --- a/submissions/smtinterpol.json +++ b/submissions/smtinterpol.json @@ -40,5 +40,6 @@ "logics": "(QF_)?(AX?)?(UF)?(BV)?(DT)?([IR]DL|[NL][IR]*A)?", "command": ["smtinterpol"] } - ] + ], + "final" : true } diff --git a/submissions/z3-noodler-base.json b/submissions/z3-noodler-base.json index b12e83f1..b17c3646 100644 --- a/submissions/z3-noodler-base.json +++ b/submissions/z3-noodler-base.json @@ -11,7 +11,6 @@ "system_description": "https://link.springer.com/content/pdf/10.1007/978-3-540-78800-3_24.pdf", "solver_type": "Standalone", "command": ["./z3-noodler_smt-comp25/z3/z3"], - "seed": 4134, "participations": [ { "tracks": ["SingleQuery"], diff --git a/submissions/z3siri-base.json b/submissions/z3-siri-base.json similarity index 92% rename from submissions/z3siri-base.json rename to submissions/z3-siri-base.json index 82fc754f..3f9aafa7 100644 --- a/submissions/z3siri-base.json +++ b/submissions/z3-siri-base.json @@ -11,11 +11,12 @@ "system_description": "https://link.springer.com/content/pdf/10.1007/978-3-540-78800-3_24.pdf", "solver_type": "Standalone", "command": ["./z3"], - "seed": "33", "participations": [ { "tracks": ["SingleQuery"], "divisions": ["QF_NonLinearIntArith", "QF_NonLinearRealArith", "QF_Bitvec"] } - ] + ], + "final" : true, + "competitive": false } diff --git a/submissions/z3alpha-base.json b/submissions/z3alpha-base.json index aeaf8df7..d7a879a2 100644 --- a/submissions/z3alpha-base.json +++ b/submissions/z3alpha-base.json @@ -11,7 +11,6 @@ "system_description": "https://link.springer.com/content/pdf/10.1007/978-3-540-78800-3_24.pdf", "solver_type": "Standalone", "command": ["./z3"], - "seed": "33", "participations": [ { "tracks": ["SingleQuery"], @@ -26,5 +25,7 @@ "QF_Strings" ] } - ] + ], + "final" : true, + "competitive": false } diff --git a/submissions/z3alpha.json b/submissions/z3alpha.json index 97a19e9f..95a6ec37 100644 --- a/submissions/z3alpha.json +++ b/submissions/z3alpha.json @@ -29,5 +29,6 @@ "QF_Strings" ] } - ] -} \ No newline at end of file + ], + "final" : true +} diff --git a/web/content/news/2025-07-04-list-of-participants.md b/web/content/news/2025-07-04-list-of-participants.md new file mode 100644 index 00000000..d3084263 --- /dev/null +++ b/web/content/news/2025-07-04-list-of-participants.md @@ -0,0 +1,10 @@ +--- +layout: single +author: +title: List of participants is final +date: 2025-07-04T00:00:00+01:00 +--- + +The [list of participants](/2025/participants) of SMT-COMP 2025 is final. We are happy to have received so many solvers and we are looking forward to the results. + +New York Stock Exchange index on the date after the submission deadline (i.e, 2025-06-30) was 20338.41, resulting in a competition seed of 2033841 + 755033430 = **757067271**. diff --git a/web/content/participants/_index.md b/web/content/participants/_index.md new file mode 100644 index 00000000..7cf82c05 --- /dev/null +++ b/web/content/participants/_index.md @@ -0,0 +1,12 @@ ++++ +layout = 'single' +title = 'Participants' ++++ + +The following solvers have been submitted to SMT-COMP 2025 or were entered as non-competing solvers by the organizers for comparison. + +{{< participants >}} + +n Non-competing. + +The opening value of the NYSE Composite Index on 2025-06-30 was 20338.41, resulting in a competition seed of 2033841 + 755033430 = **757067271**. diff --git a/web/hugo.toml b/web/hugo.toml index 2fcc64a2..ad75f7eb 100644 --- a/web/hugo.toml +++ b/web/hugo.toml @@ -70,7 +70,7 @@ theme = 'smtcomp' pageRef = 'parallel_track' weight = 30 -# [[menu.year]] -# name = 'Participants' -# pageRef = 'participants' -# weight = 50 +[[menu.year]] + name = 'Participants' + pageRef = 'participants' + weight = 50 diff --git a/web/themes/smtcomp/assets/css/main.css b/web/themes/smtcomp/assets/css/main.css index 2dabbabb..6d9216c3 100644 --- a/web/themes/smtcomp/assets/css/main.css +++ b/web/themes/smtcomp/assets/css/main.css @@ -695,13 +695,19 @@ table.participants { col.authors, td.authors { - width: 35%; + width: 20%; + white-space: normal; +} + +col.seed, +td.seed { + width: 7em; white-space: normal; } col.track, td.track { - width: 6em; + width: 5.6em; white-space: normal; } @@ -710,3 +716,7 @@ td.archive { width: 6em; white-space: normal; } + +tr.noncompetitive a { + color: black; +} diff --git a/web/themes/smtcomp/layouts/partials/participant.html b/web/themes/smtcomp/layouts/partials/participant.html index 89d3da62..ae1c35f0 100644 --- a/web/themes/smtcomp/layouts/partials/participant.html +++ b/web/themes/smtcomp/layouts/partials/participant.html @@ -1,5 +1,7 @@ - - {{ .name }} + + {{ .name }} + {{ if not .competitive }}n{{ end }} + {{ with .tracks.SingleQuery }}X{{ end }} {{ with .tracks.Incremental }}X{{ end }} @@ -8,6 +10,7 @@ {{ with .tracks.Cloud }}X{{ end }} {{ with .tracks.Parallel }}X{{ end }} + {{ .seed | string }} {{ delimit .authors ",\n" }} Archive System description diff --git a/web/themes/smtcomp/layouts/shortcodes/participants.html b/web/themes/smtcomp/layouts/shortcodes/participants.html index 605a4947..a93fbf0e 100644 --- a/web/themes/smtcomp/layouts/shortcodes/participants.html +++ b/web/themes/smtcomp/layouts/shortcodes/participants.html @@ -9,6 +9,7 @@ + @@ -24,12 +25,13 @@ Cloud Track Parallel Track + Seed Contributors Archive System description - {{ range (sort $.Site.Data.participants "name" "asc") }} + {{ range (sort (sort $.Site.Data.participants "name" "asc") "competitive" "desc") }} {{ partial "participant.html" . }} {{ end }}