From 3a0677adc53f5a76dc21ed7cdcee7ba8f8b233a8 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?John=20L=C3=9C?= <65240623+JohnLyu2@users.noreply.github.com> Date: Mon, 27 May 2024 17:36:40 -0400 Subject: [PATCH 1/5] Z3-alpha draft PR --- submissions/Z3-alpha | 9 +++++++++ 1 file changed, 9 insertions(+) create mode 100644 submissions/Z3-alpha diff --git a/submissions/Z3-alpha b/submissions/Z3-alpha new file mode 100644 index 00000000..72037ddc --- /dev/null +++ b/submissions/Z3-alpha @@ -0,0 +1,9 @@ +{ + "name": "Z3-alpha", + "contributors": [ + "Zhengyang John Lu", "Stefan Siemer", "Paul Sarnighausen-Cahn", "Florin Manea", "Vijay Ganesh" + ], + "contacts": ["John Lu "], + "website": "https://github.com/JohnLyu2/z3alpha", + "solver_type": "derived" +} From 7980af16ba4733c470c5087527195b2d9d7c16de Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= Date: Fri, 31 May 2024 15:22:24 +0200 Subject: [PATCH 2/5] Add .json extension to Z3-alpha --- submissions/{Z3-alpha => Z3-alpha.json} | 0 1 file changed, 0 insertions(+), 0 deletions(-) rename submissions/{Z3-alpha => Z3-alpha.json} (100%) diff --git a/submissions/Z3-alpha b/submissions/Z3-alpha.json similarity index 100% rename from submissions/Z3-alpha rename to submissions/Z3-alpha.json From 57fe8d9e41c5a950ec0777696a33e8c256fc268d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?John=20L=C3=9C?= <65240623+JohnLyu2@users.noreply.github.com> Date: Fri, 31 May 2024 22:45:07 -0400 Subject: [PATCH 3/5] first-version submission --- submissions/Z3-alpha.json | 25 ++++++++++++++++++++++++- 1 file changed, 24 insertions(+), 1 deletion(-) diff --git a/submissions/Z3-alpha.json b/submissions/Z3-alpha.json index 72037ddc..7de29c22 100644 --- a/submissions/Z3-alpha.json +++ b/submissions/Z3-alpha.json @@ -4,6 +4,29 @@ "Zhengyang John Lu", "Stefan Siemer", "Paul Sarnighausen-Cahn", "Florin Manea", "Vijay Ganesh" ], "contacts": ["John Lu "], + "archive": { + "url": "https://drive.google.com/file/d/1uQqVQw_DvG7McBxqE_BzjMtrviY1L_bl/view?usp=sharing", + "h": { "sha256": "10ea5822dcbd01bed303c6c7c6b283c336019d49ae76a87124a2c8eacaf0aff3" } + }, "website": "https://github.com/JohnLyu2/z3alpha", - "solver_type": "derived" + "system_description": "https://drive.google.com/file/d/1aJOiNzKac_kwhZm8DoT-EFCa_2RHwVwj/view?usp=drive_link", + "solver_type": "derived", + "command": ["python3", "z3alpha.py"], + "seed": "1231", + "participations": [ + { + "tracks": ["SingleQuery"], + "divisions": [ + "QF_Bitvec", + "QF_LinearIntArith", + "QF_LinearRealArith", + "QF_NonLinearIntArith", + "QF_NonLinearRealArith" + ] + }, + { + "tracks": ["SingleQuery"], + "logics": ["QF_S", "QF_SLIA"] + } + ] } From be03601861b9735af54c8d3528b811dc72d9805e Mon Sep 17 00:00:00 2001 From: John Lu Date: Wed, 12 Jun 2024 20:17:30 -0400 Subject: [PATCH 4/5] second-time submission --- submissions/Z3-alpha.json | 16 ++++++++++------ 1 file changed, 10 insertions(+), 6 deletions(-) diff --git a/submissions/Z3-alpha.json b/submissions/Z3-alpha.json index 7de29c22..345a71c5 100644 --- a/submissions/Z3-alpha.json +++ b/submissions/Z3-alpha.json @@ -1,32 +1,36 @@ { "name": "Z3-alpha", "contributors": [ - "Zhengyang John Lu", "Stefan Siemer", "Paul Sarnighausen-Cahn", "Florin Manea", "Vijay Ganesh" + "Zhengyang John Lu", "Paul Sarnighausen-Cahn", "Stefan Siemer", "Florin Manea", "Vijay Ganesh" ], "contacts": ["John Lu "], "archive": { - "url": "https://drive.google.com/file/d/1uQqVQw_DvG7McBxqE_BzjMtrviY1L_bl/view?usp=sharing", - "h": { "sha256": "10ea5822dcbd01bed303c6c7c6b283c336019d49ae76a87124a2c8eacaf0aff3" } + "url": "https://drive.google.com/uc?export=download&id=16WDivwx35jRj-DnC_7anjcqMHH0WIifL", + "h": { "sha256": "6a184d56bb8ba643202742f9d0159057b6dae5db5741ebbfb6298bfd9a68719b" } }, "website": "https://github.com/JohnLyu2/z3alpha", "system_description": "https://drive.google.com/file/d/1aJOiNzKac_kwhZm8DoT-EFCa_2RHwVwj/view?usp=drive_link", "solver_type": "derived", - "command": ["python3", "z3alpha.py"], + "command": ["z3alpha.py"], "seed": "1231", "participations": [ { "tracks": ["SingleQuery"], "divisions": [ + "Equality", "QF_Bitvec", + "QF_Datatypes", + "QF_Equality", "QF_LinearIntArith", "QF_LinearRealArith", "QF_NonLinearIntArith", - "QF_NonLinearRealArith" + "QF_NonLinearRealArith", + "QF_Strings" ] }, { "tracks": ["SingleQuery"], - "logics": ["QF_S", "QF_SLIA"] + "logics": ["QF_AUFBV", "QF_UFBV"] } ] } From 6cfd2b559cae02d805f1388804da58fecbaaccd5 Mon Sep 17 00:00:00 2001 From: John Lu Date: Thu, 13 Jun 2024 17:27:58 -0400 Subject: [PATCH 5/5] third submission --- submissions/Z3-alpha.json | 9 ++++----- 1 file changed, 4 insertions(+), 5 deletions(-) diff --git a/submissions/Z3-alpha.json b/submissions/Z3-alpha.json index 345a71c5..85e6c680 100644 --- a/submissions/Z3-alpha.json +++ b/submissions/Z3-alpha.json @@ -5,19 +5,18 @@ ], "contacts": ["John Lu "], "archive": { - "url": "https://drive.google.com/uc?export=download&id=16WDivwx35jRj-DnC_7anjcqMHH0WIifL", - "h": { "sha256": "6a184d56bb8ba643202742f9d0159057b6dae5db5741ebbfb6298bfd9a68719b" } + "url": "https://zenodo.org/records/11643334/files/z3alpha.tar.gz?download=1" }, "website": "https://github.com/JohnLyu2/z3alpha", - "system_description": "https://drive.google.com/file/d/1aJOiNzKac_kwhZm8DoT-EFCa_2RHwVwj/view?usp=drive_link", + "system_description": "https://drive.google.com/uc?export=download&id=17IULX6QpcqKJ51BzeT6XttAtyRwJIFyY", "solver_type": "derived", - "command": ["z3alpha.py"], + "command": ["z3alpha_submission/z3alpha.py"], "seed": "1231", "participations": [ { "tracks": ["SingleQuery"], "divisions": [ - "Equality", + "Bitvec", "QF_Bitvec", "QF_Datatypes", "QF_Equality",