From 481c852ee7e24ab2f323a3cb64e9eba763631abc Mon Sep 17 00:00:00 2001 From: linxi99 Date: Tue, 15 Jul 2025 13:32:23 +0000 Subject: [PATCH] submission: add additional configurations for lower CPU core counts. --- 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": [