From 95c258ec53ff22f798c9a363a035fee2aa6c7690 Mon Sep 17 00:00:00 2001 From: John Lu Date: Wed, 11 Jun 2025 17:12:43 +0900 Subject: [PATCH 1/8] create the submission JSON --- submissions/template/z3alpha.json | 33 +++++++++++++++++++++++++++++++ 1 file changed, 33 insertions(+) create mode 100644 submissions/template/z3alpha.json diff --git a/submissions/template/z3alpha.json b/submissions/template/z3alpha.json new file mode 100644 index 00000000..80cb9b0c --- /dev/null +++ b/submissions/template/z3alpha.json @@ -0,0 +1,33 @@ +{ + "name": "Z3-alpha", + "contributors": [ + "John Lu", + "Paul Sarnighausen-Cahn", + "Jiahao Chen", + "Florin Manea", + "Vijay Ganesh" + ], + "contacts": ["John Lu "], + "archive": { + "url": "http://example.com/solver.tar.gz", + "h": { "sha256": "012345" } + }, + "website": "https://github.com/JohnLyu2/z3alpha", + "system_description": "https://drive.google.com/uc?export=download&id=17IULX6QpcqKJ51BzeT6XttAtyRwJIFyY", + "solver_type": "derived", + "command": ["z3alpha_submission/z3alpha.py"], + "seed": "33", + "participations": [ + { + "tracks": ["SingleQuery"], + "divisions": [ + "Bitvec", + "QF_Bitvec", + "QF_LinearIntArith", + "QF_LinearRealArith", + "QF_NonLinearIntArith", + "QF_NonLinearRealArith" + ] + } + ] +} \ No newline at end of file From d9cf8d6c6a2a0134dbac9faf794780b040ff117b Mon Sep 17 00:00:00 2001 From: John Lu Date: Fri, 13 Jun 2025 18:05:10 +0900 Subject: [PATCH 2/8] 2025 first submission --- submissions/{template => }/z3alpha.json | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) rename submissions/{template => }/z3alpha.json (73%) diff --git a/submissions/template/z3alpha.json b/submissions/z3alpha.json similarity index 73% rename from submissions/template/z3alpha.json rename to submissions/z3alpha.json index 80cb9b0c..06d2d0cd 100644 --- a/submissions/template/z3alpha.json +++ b/submissions/z3alpha.json @@ -9,13 +9,13 @@ ], "contacts": ["John Lu "], "archive": { - "url": "http://example.com/solver.tar.gz", - "h": { "sha256": "012345" } + "url": "https://drive.google.com/uc?export=download&id=16B-DpR8xyyyGubQ5lS6-aaUlq0zASur2", + "h": { "sha256": "63b32b4f4d9a57672f1a9374a878875848f57a7820a22f5b99810e0c65157a78" } }, "website": "https://github.com/JohnLyu2/z3alpha", - "system_description": "https://drive.google.com/uc?export=download&id=17IULX6QpcqKJ51BzeT6XttAtyRwJIFyY", + "system_description": "https://drive.google.com/uc?export=download&id=193djU1kyWkdRXE-nmOKFZ8IyY6D2d8Kt", "solver_type": "derived", - "command": ["z3alpha_submission/z3alpha.py"], + "command": ["./z3alpha.py"], "seed": "33", "participations": [ { From b81b9045b56e9cb31ea7b4db28d766fa2035081d Mon Sep 17 00:00:00 2001 From: John Lu Date: Wed, 18 Jun 2025 16:35:40 +0900 Subject: [PATCH 3/8] add base solver JSON --- submissions/z3_base.json | 27 +++++++++++++++++++++++++++ 1 file changed, 27 insertions(+) create mode 100644 submissions/z3_base.json diff --git a/submissions/z3_base.json b/submissions/z3_base.json new file mode 100644 index 00000000..af276868 --- /dev/null +++ b/submissions/z3_base.json @@ -0,0 +1,27 @@ +{ + "name": "Z3-4.15.0", + "contributors": [ + "Nikolaj Bjørner et al." + ], + "contacts": ["Nikolaj Bjørner "], + "archive": { + "url": "https://zenodo.org/records/15687848/files/z3.zip?download=1" + }, + "website": "https://github.com/Z3Prover/z3", + "system_description": "https://link.springer.com/content/pdf/10.1007/978-3-540-78800-3_24.pdf", + "solver_type": "Standalone", + "command": ["./z3"], + "participations": [ + { + "tracks": ["SingleQuery"], + "divisions": [ + "Bitvec", + "QF_Bitvec", + "QF_LinearIntArith", + "QF_LinearRealArith", + "QF_NonLinearIntArith", + "QF_NonLinearRealArith" + ] + } + ] +} \ No newline at end of file From 68dd9b1ddd17c92285006fdacecc074ab8073188 Mon Sep 17 00:00:00 2001 From: John Lu Date: Wed, 18 Jun 2025 16:40:10 +0900 Subject: [PATCH 4/8] add seed in base JSON --- submissions/z3_base.json | 1 + 1 file changed, 1 insertion(+) diff --git a/submissions/z3_base.json b/submissions/z3_base.json index af276868..26770b0a 100644 --- a/submissions/z3_base.json +++ b/submissions/z3_base.json @@ -11,6 +11,7 @@ "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"], From c02cad08aded6b6c8b945f97c8723b9f021b898a Mon Sep 17 00:00:00 2001 From: John Lu Date: Thu, 26 Jun 2025 16:48:23 +0900 Subject: [PATCH 5/8] update submission JSON --- submissions/z3_base.json | 4 +++- submissions/z3alpha.json | 8 +++++--- 2 files changed, 8 insertions(+), 4 deletions(-) diff --git a/submissions/z3_base.json b/submissions/z3_base.json index 26770b0a..28a59e80 100644 --- a/submissions/z3_base.json +++ b/submissions/z3_base.json @@ -16,12 +16,14 @@ { "tracks": ["SingleQuery"], "divisions": [ + "Arith", "Bitvec", "QF_Bitvec", "QF_LinearIntArith", "QF_LinearRealArith", "QF_NonLinearIntArith", - "QF_NonLinearRealArith" + "QF_NonLinearRealArith", + "QF_Strings" ] } ] diff --git a/submissions/z3alpha.json b/submissions/z3alpha.json index 06d2d0cd..887256fa 100644 --- a/submissions/z3alpha.json +++ b/submissions/z3alpha.json @@ -9,8 +9,8 @@ ], "contacts": ["John Lu "], "archive": { - "url": "https://drive.google.com/uc?export=download&id=16B-DpR8xyyyGubQ5lS6-aaUlq0zASur2", - "h": { "sha256": "63b32b4f4d9a57672f1a9374a878875848f57a7820a22f5b99810e0c65157a78" } + "url": "https://drive.google.com/uc?export=download&id=1iSfJ8DpvWTMNCcpfDfsg2xbE083ciUsp", + "h": { "sha256": "abd39df9749066f4a145c595db5a95ace49158ad631df62e18138b6b53e35663" } }, "website": "https://github.com/JohnLyu2/z3alpha", "system_description": "https://drive.google.com/uc?export=download&id=193djU1kyWkdRXE-nmOKFZ8IyY6D2d8Kt", @@ -21,12 +21,14 @@ { "tracks": ["SingleQuery"], "divisions": [ + "Arith", "Bitvec", "QF_Bitvec", "QF_LinearIntArith", "QF_LinearRealArith", "QF_NonLinearIntArith", - "QF_NonLinearRealArith" + "QF_NonLinearRealArith", + "QF_Strings" ] } ] From e62db2756239ee2ac4891f9471f25c23e47f6f44 Mon Sep 17 00:00:00 2001 From: John Lu Date: Sat, 28 Jun 2025 21:20:24 +0900 Subject: [PATCH 6/8] update final description link --- submissions/z3alpha.json | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/submissions/z3alpha.json b/submissions/z3alpha.json index 887256fa..317068d9 100644 --- a/submissions/z3alpha.json +++ b/submissions/z3alpha.json @@ -13,7 +13,7 @@ "h": { "sha256": "abd39df9749066f4a145c595db5a95ace49158ad631df62e18138b6b53e35663" } }, "website": "https://github.com/JohnLyu2/z3alpha", - "system_description": "https://drive.google.com/uc?export=download&id=193djU1kyWkdRXE-nmOKFZ8IyY6D2d8Kt", + "system_description": "https://drive.google.com/uc?export=download&id=17n4WbrukfKz7CxdVBXtSQjU_EYmwo1ZR", "solver_type": "derived", "command": ["./z3alpha.py"], "seed": "33", From e45f8429935d4cdd381018210a257b7a4cc3ed41 Mon Sep 17 00:00:00 2001 From: John Lu Date: Sat, 28 Jun 2025 21:21:12 +0900 Subject: [PATCH 7/8] remove BV from participating division --- submissions/z3alpha.json | 1 - 1 file changed, 1 deletion(-) diff --git a/submissions/z3alpha.json b/submissions/z3alpha.json index 317068d9..6b7c46f5 100644 --- a/submissions/z3alpha.json +++ b/submissions/z3alpha.json @@ -22,7 +22,6 @@ "tracks": ["SingleQuery"], "divisions": [ "Arith", - "Bitvec", "QF_Bitvec", "QF_LinearIntArith", "QF_LinearRealArith", From edffded615597e978738e6edac3037869340170f Mon Sep 17 00:00:00 2001 From: John Lu Date: Sun, 29 Jun 2025 14:48:38 +0900 Subject: [PATCH 8/8] update to final solver zenodo link --- submissions/z3alpha.json | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/submissions/z3alpha.json b/submissions/z3alpha.json index 6b7c46f5..97a19e9f 100644 --- a/submissions/z3alpha.json +++ b/submissions/z3alpha.json @@ -9,8 +9,7 @@ ], "contacts": ["John Lu "], "archive": { - "url": "https://drive.google.com/uc?export=download&id=1iSfJ8DpvWTMNCcpfDfsg2xbE083ciUsp", - "h": { "sha256": "abd39df9749066f4a145c595db5a95ace49158ad631df62e18138b6b53e35663" } + "url": "https://zenodo.org/records/15765918/files/submission25.zip?download=1" }, "website": "https://github.com/JohnLyu2/z3alpha", "system_description": "https://drive.google.com/uc?export=download&id=17n4WbrukfKz7CxdVBXtSQjU_EYmwo1ZR",