From 48587eaa4384b75f3aab4630fb3a3cdf8d483d89 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?John=20L=C3=9C?= <65240623+JohnLyu2@users.noreply.github.com> Date: Tue, 18 Jun 2024 03:05:38 -0400 Subject: [PATCH] Z3-alpha draft PR (#65) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit * Z3-alpha draft PR * Add .json extension to Z3-alpha * first-version submission * second-time submission * third submission --------- Co-authored-by: François Bobot --- submissions/Z3-alpha.json | 35 +++++++++++++++++++++++++++++++++++ 1 file changed, 35 insertions(+) create mode 100644 submissions/Z3-alpha.json diff --git a/submissions/Z3-alpha.json b/submissions/Z3-alpha.json new file mode 100644 index 00000000..85e6c680 --- /dev/null +++ b/submissions/Z3-alpha.json @@ -0,0 +1,35 @@ +{ + "name": "Z3-alpha", + "contributors": [ + "Zhengyang John Lu", "Paul Sarnighausen-Cahn", "Stefan Siemer", "Florin Manea", "Vijay Ganesh" + ], + "contacts": ["John Lu "], + "archive": { + "url": "https://zenodo.org/records/11643334/files/z3alpha.tar.gz?download=1" + }, + "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": "1231", + "participations": [ + { + "tracks": ["SingleQuery"], + "divisions": [ + "Bitvec", + "QF_Bitvec", + "QF_Datatypes", + "QF_Equality", + "QF_LinearIntArith", + "QF_LinearRealArith", + "QF_NonLinearIntArith", + "QF_NonLinearRealArith", + "QF_Strings" + ] + }, + { + "tracks": ["SingleQuery"], + "logics": ["QF_AUFBV", "QF_UFBV"] + } + ] +}