From f851c30ce708e0723df2f1d1b34dd96a3e4fe7ae Mon Sep 17 00:00:00 2001 From: "riseproject-dev[bot]" <330740410+riseproject-dev[bot]@users.noreply.github.com> Date: Thu, 22 Oct 2026 12:11:05 +0000 Subject: [PATCH 1/5] python-sat: Add version 1.9.dev17 Signed-off-by: riseproject-dev[bot] <330740410+riseproject-dev[bot]@users.noreply.github.com> --- docs/packages/python-sat.yaml | 1 + 1 file changed, 1 insertion(+) diff --git a/docs/packages/python-sat.yaml b/docs/packages/python-sat.yaml index e74275c35eb1..3424f73c8b71 100644 --- a/docs/packages/python-sat.yaml +++ b/docs/packages/python-sat.yaml @@ -26,3 +26,4 @@ versions: sha256: 4e98da83841abe57e67d39820a0088b2cb8849b688497049bb695445c6e03d57 - filename: python_sat-1.9.dev15-cp314-cp314t-musllinux_1_2_riscv64.whl sha256: 97ddffdf92f0de0da940ca2e5a51064839eb08bc65e26e8246f40729c1dac9ff +- version: 1.9.dev17 From e66b2ea1f7b1ae0d027a8affa10478d0cd6858d6 Mon Sep 17 00:00:00 2001 From: Ludovic Henry Date: Fri, 23 Oct 2026 12:30:23 +0800 Subject: [PATCH 2/5] python-sat: rebase the build-without-Lingeling patch onto 1.9.dev17 --- ...1-build-without-the-Lingeling-solver.patch | 81 +++++++++++++++++++ 1 file changed, 81 insertions(+) create mode 100644 patches/python-sat/1.9.dev17/0001-build-without-the-Lingeling-solver.patch diff --git a/patches/python-sat/1.9.dev17/0001-build-without-the-Lingeling-solver.patch b/patches/python-sat/1.9.dev17/0001-build-without-the-Lingeling-solver.patch new file mode 100644 index 000000000000..73d366822d02 --- /dev/null +++ b/patches/python-sat/1.9.dev17/0001-build-without-the-Lingeling-solver.patch @@ -0,0 +1,81 @@ +From c2359bfbabe0826799295fb3df2bca120a8c4179 Mon Sep 17 00:00:00 2001 +From: Ludovic Henry +Date: Sun, 27 Sep 2026 22:08:42 +0000 +Subject: [PATCH 1/2] build without the Lingeling solver + +Upstream-Status: Inappropriate [licensing: the bundled Lingeling bbc-9230380-160707 licence grants use for evaluation and research only, forbids commercial use and reserves all other rights, so it gives no permission to redistribute it in a binary wheel] + +setup.py statically links every solver listed in to_install into the +pysolvers extension. The Lingeling tarball in solvers/lingeling.tar.gz +(lingeling-bbc-9230380-160707/COPYING) is not under the MIT terms that +cover PySAT and the other bundled solvers: it permits use "for +evaluation and research purposes", prohibits use "in a commercial +context" and ends with "All other usage is reserved". A third party +rebuilding and publishing wheels has no grant to redistribute it. + +Drop 'lingeling' from to_install. pysolvers.cc guards all Lingeling +code behind WITH_LINGELING, so the extension builds and links without +it; pysat.solvers.Lingeling (and Solver(name='lingeling')) then fails +with an AttributeError on pysolvers.lingeling_new. Remove 'lingeling' +from the solver lists of the three tests that loop over every solver +so that they keep exercising the remaining nineteen. + +Signed-off-by: Ludovic Henry +--- + setup.py | 2 +- + tests/test_accum_stats.py | 1 - + tests/test_cnf.py | 1 - + tests/test_unique_model.py | 1 - + 4 files changed, 1 insertion(+), 4 deletions(-) + +diff --git a/setup.py b/setup.py +index 65da94a..837c620 100644 +--- a/setup.py ++++ b/setup.py +@@ -70,7 +70,7 @@ Details can be found at `https://pysathq.github.io `_ + #============================================================================== + to_install = ['cadical103', 'cadical153', 'cadical195', 'cadical300', + 'ergo', 'gluecard30', 'gluecard41', 'glucose30', 'glucose41', +- 'glucose421', 'kissat404', 'lingeling', 'maplechrono', ++ 'glucose421', 'kissat404', 'maplechrono', + 'maplecm', 'maplesat', 'mergesat3', 'minicard', 'minisat22', + 'minisatgh', 'minisatep'] + +diff --git a/tests/test_accum_stats.py b/tests/test_accum_stats.py +index db93994..24f560f 100644 +--- a/tests/test_accum_stats.py ++++ b/tests/test_accum_stats.py +@@ -10,7 +10,6 @@ solvers = ['cadical103', + 'gluecard41', + 'glucose30', + 'glucose42', +- 'lingeling', + 'maplechrono', + 'maplecm', + 'maplesat', +diff --git a/tests/test_cnf.py b/tests/test_cnf.py +index 00a2205..1511ce1 100644 +--- a/tests/test_cnf.py ++++ b/tests/test_cnf.py +@@ -14,7 +14,6 @@ solvers = ['cadical103', + 'glucose30', + 'glucose41', + 'glucose42', +- 'lingeling', + 'maplechrono', + 'maplecm', + 'maplesat', +diff --git a/tests/test_unique_model.py b/tests/test_unique_model.py +index 35d86b6..9fd127d 100644 +--- a/tests/test_unique_model.py ++++ b/tests/test_unique_model.py +@@ -11,7 +11,6 @@ solvers = ['cadical103', + 'glucose30', + 'glucose41', + 'glucose42', +- 'lingeling', + 'maplechrono', + 'maplecm', + 'maplesat', +-- +2.43.0 From a16a494e7e254d161a86eb7e5ce7c256f075cdfd Mon Sep 17 00:00:00 2001 From: Ludovic Henry Date: Fri, 23 Oct 2026 12:31:49 +0800 Subject: [PATCH 3/5] python-sat: carry the solver licences patch to 1.9.dev17 --- ...-licences-of-the-bundled-SAT-solvers.patch | 721 ++++++++++++++++++ 1 file changed, 721 insertions(+) create mode 100644 patches/python-sat/1.9.dev17/0002-ship-the-licences-of-the-bundled-SAT-solvers.patch diff --git a/patches/python-sat/1.9.dev17/0002-ship-the-licences-of-the-bundled-SAT-solvers.patch b/patches/python-sat/1.9.dev17/0002-ship-the-licences-of-the-bundled-SAT-solvers.patch new file mode 100644 index 000000000000..82a93a72a577 --- /dev/null +++ b/patches/python-sat/1.9.dev17/0002-ship-the-licences-of-the-bundled-SAT-solvers.patch @@ -0,0 +1,721 @@ +From dc6a8edff84cd7800a50f047bfffb2d51592686d Mon Sep 17 00:00:00 2001 +From: Ludovic Henry +Date: Sun, 27 Sep 2026 22:09:15 +0000 +Subject: [PATCH 2/2] ship the licences of the bundled SAT solvers in the wheel + +Upstream-Status: To upstream [not yet submitted; the same gap exists in every python-sat wheel on PyPI, so this needs a maintainer discussion rather than a drive-by PR] + +The pysolvers extension statically links every solver in to_install, +built from the archives in solvers/ (kissat404 and minisatep are +downloaded at build time). Each of them carries its own copyright +notice and requires it to be included with copies of the software, but +setup.py and setup.cfg name only PySAT's own LICENSE.txt, and +solvers/prepare.py deletes the solvers' licence files when it unpacks +them, so the wheel ships PySAT's MIT licence alone (confirmed against +the published 1.9.dev15 PyPI wheel). + +Add each solver's licence, as found in the exact archive setup.py +builds, under solvers/licenses/, and list that directory in +license_files so that the files land in the wheel's +dist-info/licenses/. Glucose 3.0 ships no licence file, so its notice +is the header of core/Solver.cc (identical in every file); MergeSat 3.0 +ships a second notice for its Glucose-derived code (licence.txt), kept +as LICENSE.mergesat3.glucose. Gluecard 3.0/4.1 are built from the +Glucose 3.0/4.1 archives and reuse their notices. + +Signed-off-by: Ludovic Henry +--- + setup.cfg | 4 +- + setup.py | 2 +- + solvers/licenses/LICENSE.cadical103 | 21 ++++++++++ + solvers/licenses/LICENSE.cadical153 | 24 +++++++++++ + solvers/licenses/LICENSE.cadical195 | 27 +++++++++++++ + solvers/licenses/LICENSE.cadical300 | 28 +++++++++++++ + solvers/licenses/LICENSE.glucose30 | 26 ++++++++++++ + solvers/licenses/LICENSE.glucose41 | 47 ++++++++++++++++++++++ + solvers/licenses/LICENSE.glucose421 | 21 ++++++++++ + solvers/licenses/LICENSE.gluecard30 | 26 ++++++++++++ + solvers/licenses/LICENSE.gluecard41 | 47 ++++++++++++++++++++++ + solvers/licenses/LICENSE.kissat404 | 22 ++++++++++ + solvers/licenses/LICENSE.maplechrono | 30 ++++++++++++++ + solvers/licenses/LICENSE.maplecm | 22 ++++++++++ + solvers/licenses/LICENSE.maplesat | 23 +++++++++++ + solvers/licenses/LICENSE.mergesat3 | 30 ++++++++++++++ + solvers/licenses/LICENSE.mergesat3.glucose | 30 ++++++++++++++ + solvers/licenses/LICENSE.minicard | 25 ++++++++++++ + solvers/licenses/LICENSE.minisat22 | 21 ++++++++++ + solvers/licenses/LICENSE.minisatep | 21 ++++++++++ + solvers/licenses/LICENSE.minisatgh | 21 ++++++++++ + 21 files changed, 516 insertions(+), 2 deletions(-) + create mode 100644 solvers/licenses/LICENSE.cadical103 + create mode 100644 solvers/licenses/LICENSE.cadical153 + create mode 100644 solvers/licenses/LICENSE.cadical195 + create mode 100644 solvers/licenses/LICENSE.cadical300 + create mode 100644 solvers/licenses/LICENSE.glucose30 + create mode 100644 solvers/licenses/LICENSE.glucose41 + create mode 100644 solvers/licenses/LICENSE.glucose421 + create mode 100644 solvers/licenses/LICENSE.gluecard30 + create mode 100644 solvers/licenses/LICENSE.gluecard41 + create mode 100644 solvers/licenses/LICENSE.kissat404 + create mode 100644 solvers/licenses/LICENSE.maplechrono + create mode 100644 solvers/licenses/LICENSE.maplecm + create mode 100644 solvers/licenses/LICENSE.maplesat + create mode 100644 solvers/licenses/LICENSE.mergesat3 + create mode 100644 solvers/licenses/LICENSE.mergesat3.glucose + create mode 100644 solvers/licenses/LICENSE.minicard + create mode 100644 solvers/licenses/LICENSE.minisat22 + create mode 100644 solvers/licenses/LICENSE.minisatep + create mode 100644 solvers/licenses/LICENSE.minisatgh + +diff --git a/setup.cfg b/setup.cfg +index c921d9d..b1970db 100644 +--- a/setup.cfg ++++ b/setup.cfg +@@ -1,3 +1,5 @@ + [metadata] + description_file = README.rst +-license_files = LICENSE.txt ++license_files = ++ LICENSE.txt ++ solvers/licenses/LICENSE.* +diff --git a/setup.py b/setup.py +index e7b2338..572cf45 100644 +--- a/setup.py ++++ b/setup.py +@@ -192,7 +192,7 @@ setup(name='python-sat', + long_description=LONG_DESCRIPTION, + long_description_content_type='text/x-rst; charset=UTF-8', + license='MIT', +- license_files=('LICENSE.txt',), ++ license_files=('LICENSE.txt', 'solvers/licenses/LICENSE.*'), + author='Alexey Ignatiev, Joao Marques-Silva, Antonio Morgado', + author_email='alexey.ignatiev@monash.edu, joao.marques-silva@univ-toulouse.fr, ajrmorgado@gmail.com', + url='https://github.com/pysathq/pysat', +diff --git a/solvers/licenses/LICENSE.cadical103 b/solvers/licenses/LICENSE.cadical103 +new file mode 100644 +index 0000000..23d808a +--- /dev/null ++++ b/solvers/licenses/LICENSE.cadical103 +@@ -0,0 +1,21 @@ ++MIT License ++ ++Copyright (c) 2016-2019 Armin Biere, Johannes Kepler University Linz, Austria ++ ++Permission is hereby granted, free of charge, to any person obtaining a copy ++of this software and associated documentation files (the "Software"), to deal ++in the Software without restriction, including without limitation the rights ++to use, copy, modify, merge, publish, distribute, sublicense, and/or sell ++copies of the Software, and to permit persons to whom the Software is ++furnished to do so, subject to the following conditions: ++ ++The above copyright notice and this permission notice shall be included in all ++copies or substantial portions of the Software. ++ ++THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR ++IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, ++FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE ++AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER ++LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, ++OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE ++SOFTWARE. +diff --git a/solvers/licenses/LICENSE.cadical153 b/solvers/licenses/LICENSE.cadical153 +new file mode 100644 +index 0000000..e52376b +--- /dev/null ++++ b/solvers/licenses/LICENSE.cadical153 +@@ -0,0 +1,24 @@ ++MIT License ++ ++Copyright (c) 2016-2021 Armin Biere, Johannes Kepler University Linz, Austria ++Copyright (c) 2021-2021 Armin Biere, Albert-Ludwigs-University Freiburg, Germany ++Copyright (c) 2020-2021 Mathias Fleury, Johannes Kepler University Linz, Austria ++Copyright (c) 2020-2021 Nils Froleyks, Johannes Kepler University Linz, Austria ++ ++Permission is hereby granted, free of charge, to any person obtaining a copy ++of this software and associated documentation files (the "Software"), to deal ++in the Software without restriction, including without limitation the rights ++to use, copy, modify, merge, publish, distribute, sublicense, and/or sell ++copies of the Software, and to permit persons to whom the Software is ++furnished to do so, subject to the following conditions: ++ ++The above copyright notice and this permission notice shall be included in all ++copies or substantial portions of the Software. ++ ++THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR ++IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, ++FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE ++AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER ++LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, ++OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE ++SOFTWARE. +diff --git a/solvers/licenses/LICENSE.cadical195 b/solvers/licenses/LICENSE.cadical195 +new file mode 100644 +index 0000000..13fd3c3 +--- /dev/null ++++ b/solvers/licenses/LICENSE.cadical195 +@@ -0,0 +1,27 @@ ++MIT License ++ ++Copyright (c) 2016-2021 Armin Biere, Johannes Kepler University Linz, Austria ++Copyright (c) 2020-2021 Mathias Fleury, Johannes Kepler University Linz, Austria ++Copyright (c) 2020-2021 Nils Froleyks, Johannes Kepler University Linz, Austria ++Copyright (c) 2022-2023 Katalin Fazekas, Vienna University of Technology, Austria ++Copyright (c) 2021-2023 Armin Biere, University of Freiburg, Germany ++Copyright (c) 2021-2023 Mathias Fleury, University of Freiburg, Germany ++Copyright (c) 2023 Florian Pollitt, University of Freiburg, Germany ++ ++Permission is hereby granted, free of charge, to any person obtaining a copy ++of this software and associated documentation files (the "Software"), to deal ++in the Software without restriction, including without limitation the rights ++to use, copy, modify, merge, publish, distribute, sublicense, and/or sell ++copies of the Software, and to permit persons to whom the Software is ++furnished to do so, subject to the following conditions: ++ ++The above copyright notice and this permission notice shall be included in all ++copies or substantial portions of the Software. ++ ++THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR ++IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, ++FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE ++AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER ++LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, ++OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE ++SOFTWARE. +diff --git a/solvers/licenses/LICENSE.cadical300 b/solvers/licenses/LICENSE.cadical300 +new file mode 100644 +index 0000000..fd52947 +--- /dev/null ++++ b/solvers/licenses/LICENSE.cadical300 +@@ -0,0 +1,28 @@ ++MIT License ++ ++Copyright (c) 2016-2021 Armin Biere, Johannes Kepler University Linz, Austria ++Copyright (c) 2020-2021 Mathias Fleury, Johannes Kepler University Linz, Austria ++Copyright (c) 2020-2021 Nils Froleyks, Johannes Kepler University Linz, Austria ++Copyright (c) 2022-2025 Katalin Fazekas, Vienna University of Technology, Austria ++Copyright (c) 2021-2025 Armin Biere, University of Freiburg, Germany ++Copyright (c) 2021-2025 Mathias Fleury, University of Freiburg, Germany ++Copyright (c) 2023-2025 Florian Pollitt, University of Freiburg, Germany ++Copyright (c) 2024-2024 Tobias Faller, University of Freiburg, Germany ++ ++Permission is hereby granted, free of charge, to any person obtaining a copy ++of this software and associated documentation files (the "Software"), to deal ++in the Software without restriction, including without limitation the rights ++to use, copy, modify, merge, publish, distribute, sublicense, and/or sell ++copies of the Software, and to permit persons to whom the Software is ++furnished to do so, subject to the following conditions: ++ ++The above copyright notice and this permission notice shall be included in all ++copies or substantial portions of the Software. ++ ++THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR ++IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, ++FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE ++AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER ++LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, ++OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE ++SOFTWARE. +diff --git a/solvers/licenses/LICENSE.glucose30 b/solvers/licenses/LICENSE.glucose30 +new file mode 100644 +index 0000000..46da7b2 +--- /dev/null ++++ b/solvers/licenses/LICENSE.glucose30 +@@ -0,0 +1,26 @@ ++ Glucose -- Copyright (c) 2013, Gilles Audemard, Laurent Simon ++ CRIL - Univ. Artois, France ++ LRI - Univ. Paris Sud, France ++ ++Glucose sources are based on MiniSat (see below MiniSat copyrights). Permissions and copyrights of ++Glucose are exactly the same as Minisat on which it is based on. (see below). ++ ++--------------- ++ ++Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson ++Copyright (c) 2007-2010, Niklas Sorensson ++ ++Permission is hereby granted, free of charge, to any person obtaining a copy of this software and ++associated documentation files (the "Software"), to deal in the Software without restriction, ++including without limitation the rights to use, copy, modify, merge, publish, distribute, ++sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is ++furnished to do so, subject to the following conditions: ++ ++The above copyright notice and this permission notice shall be included in all copies or ++substantial portions of the Software. ++ ++THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT ++NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND ++NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, ++DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT ++OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. +diff --git a/solvers/licenses/LICENSE.glucose41 b/solvers/licenses/LICENSE.glucose41 +new file mode 100644 +index 0000000..5100350 +--- /dev/null ++++ b/solvers/licenses/LICENSE.glucose41 +@@ -0,0 +1,47 @@ ++ Glucose -- Copyright (c) 2009-2017, Gilles Audemard, Laurent Simon ++ CRIL - Univ. Artois, France ++ LRI - Univ. Paris Sud, France (2009-2013) ++ Labri - Univ. Bordeaux, France ++ ++ Syrup (Glucose Parallel) -- Copyright (c) 2013-2014, Gilles Audemard, Laurent Simon ++ CRIL - Univ. Artois, France ++ Labri - Univ. Bordeaux, France ++ ++Glucose sources are based on MiniSat (see below MiniSat copyrights). Permissions and copyrights of ++Glucose (sources until 2013, Glucose 3.0, single core) are exactly the same as Minisat on which it ++is based on. (see below). ++ ++Glucose-Syrup sources are based on another copyright. Permissions and copyrights for the parallel ++version of Glucose-Syrup (the "Software") are granted, free of charge, to deal with the Software ++without restriction, including the rights to use, copy, modify, merge, publish, distribute, ++sublicence, and/or sell copies of the Software, and to permit persons to whom the Software is ++furnished to do so, subject to the following conditions: ++ ++- The above and below copyrights notices and this permission notice shall be included in all ++copies or substantial portions of the Software; ++- The parallel version of Glucose (all files modified since Glucose 3.0 releases, 2013) cannot ++be used in any competitive event (sat competitions/evaluations) without the express permission of ++the authors (Gilles Audemard / Laurent Simon). This is also the case for any competitive event ++using Glucose Parallel as an embedded SAT engine (single core or not). ++ ++ ++--------------- Original Minisat Copyrights ++ ++Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson ++Copyright (c) 2007-2010, Niklas Sorensson ++ ++Permission is hereby granted, free of charge, to any person obtaining a copy of this software and ++associated documentation files (the "Software"), to deal in the Software without restriction, ++including without limitation the rights to use, copy, modify, merge, publish, distribute, ++sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is ++furnished to do so, subject to the following conditions: ++ ++The above copyright notice and this permission notice shall be included in all copies or ++substantial portions of the Software. ++ ++THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT ++NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND ++NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, ++DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT ++OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. ++ +diff --git a/solvers/licenses/LICENSE.glucose421 b/solvers/licenses/LICENSE.glucose421 +new file mode 100644 +index 0000000..b89c77f +--- /dev/null ++++ b/solvers/licenses/LICENSE.glucose421 +@@ -0,0 +1,21 @@ ++MIT License ++ ++Copyright (c) 2023 Gilles Audemard ++ ++Permission is hereby granted, free of charge, to any person obtaining a copy ++of this software and associated documentation files (the "Software"), to deal ++in the Software without restriction, including without limitation the rights ++to use, copy, modify, merge, publish, distribute, sublicense, and/or sell ++copies of the Software, and to permit persons to whom the Software is ++furnished to do so, subject to the following conditions: ++ ++The above copyright notice and this permission notice shall be included in all ++copies or substantial portions of the Software. ++ ++THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR ++IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, ++FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE ++AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER ++LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, ++OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE ++SOFTWARE. +diff --git a/solvers/licenses/LICENSE.gluecard30 b/solvers/licenses/LICENSE.gluecard30 +new file mode 100644 +index 0000000..46da7b2 +--- /dev/null ++++ b/solvers/licenses/LICENSE.gluecard30 +@@ -0,0 +1,26 @@ ++ Glucose -- Copyright (c) 2013, Gilles Audemard, Laurent Simon ++ CRIL - Univ. Artois, France ++ LRI - Univ. Paris Sud, France ++ ++Glucose sources are based on MiniSat (see below MiniSat copyrights). Permissions and copyrights of ++Glucose are exactly the same as Minisat on which it is based on. (see below). ++ ++--------------- ++ ++Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson ++Copyright (c) 2007-2010, Niklas Sorensson ++ ++Permission is hereby granted, free of charge, to any person obtaining a copy of this software and ++associated documentation files (the "Software"), to deal in the Software without restriction, ++including without limitation the rights to use, copy, modify, merge, publish, distribute, ++sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is ++furnished to do so, subject to the following conditions: ++ ++The above copyright notice and this permission notice shall be included in all copies or ++substantial portions of the Software. ++ ++THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT ++NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND ++NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, ++DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT ++OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. +diff --git a/solvers/licenses/LICENSE.gluecard41 b/solvers/licenses/LICENSE.gluecard41 +new file mode 100644 +index 0000000..5100350 +--- /dev/null ++++ b/solvers/licenses/LICENSE.gluecard41 +@@ -0,0 +1,47 @@ ++ Glucose -- Copyright (c) 2009-2017, Gilles Audemard, Laurent Simon ++ CRIL - Univ. Artois, France ++ LRI - Univ. Paris Sud, France (2009-2013) ++ Labri - Univ. Bordeaux, France ++ ++ Syrup (Glucose Parallel) -- Copyright (c) 2013-2014, Gilles Audemard, Laurent Simon ++ CRIL - Univ. Artois, France ++ Labri - Univ. Bordeaux, France ++ ++Glucose sources are based on MiniSat (see below MiniSat copyrights). Permissions and copyrights of ++Glucose (sources until 2013, Glucose 3.0, single core) are exactly the same as Minisat on which it ++is based on. (see below). ++ ++Glucose-Syrup sources are based on another copyright. Permissions and copyrights for the parallel ++version of Glucose-Syrup (the "Software") are granted, free of charge, to deal with the Software ++without restriction, including the rights to use, copy, modify, merge, publish, distribute, ++sublicence, and/or sell copies of the Software, and to permit persons to whom the Software is ++furnished to do so, subject to the following conditions: ++ ++- The above and below copyrights notices and this permission notice shall be included in all ++copies or substantial portions of the Software; ++- The parallel version of Glucose (all files modified since Glucose 3.0 releases, 2013) cannot ++be used in any competitive event (sat competitions/evaluations) without the express permission of ++the authors (Gilles Audemard / Laurent Simon). This is also the case for any competitive event ++using Glucose Parallel as an embedded SAT engine (single core or not). ++ ++ ++--------------- Original Minisat Copyrights ++ ++Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson ++Copyright (c) 2007-2010, Niklas Sorensson ++ ++Permission is hereby granted, free of charge, to any person obtaining a copy of this software and ++associated documentation files (the "Software"), to deal in the Software without restriction, ++including without limitation the rights to use, copy, modify, merge, publish, distribute, ++sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is ++furnished to do so, subject to the following conditions: ++ ++The above copyright notice and this permission notice shall be included in all copies or ++substantial portions of the Software. ++ ++THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT ++NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND ++NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, ++DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT ++OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. ++ +diff --git a/solvers/licenses/LICENSE.kissat404 b/solvers/licenses/LICENSE.kissat404 +new file mode 100644 +index 0000000..6626569 +--- /dev/null ++++ b/solvers/licenses/LICENSE.kissat404 +@@ -0,0 +1,22 @@ ++Copyright (c) 2021-2025 Armin Biere, University of Freiburg, Germany ++Copyright (c) 2025-2025 Mathias Fleury, University of Freiburg, Germany ++Copyright (c) 2025-2025 Florian Pollitt, University of Freiburg, Germany ++Copyright (c) 2019-2021 Armin Biere, Johannes Kepler University Linz, Austria ++ ++Permission is hereby granted, free of charge, to any person obtaining a copy ++of this software and associated documentation files (the "Software"), to deal ++in the Software without restriction, including without limitation the rights ++to use, copy, modify, merge, publish, distribute, sublicense, and/or sell ++copies of the Software, and to permit persons to whom the Software is ++furnished to do so, subject to the following conditions: ++ ++The above copyright notice and this permission notice shall be included in all ++copies or substantial portions of the Software. ++ ++THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR ++IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, ++FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE ++AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER ++LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, ++OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE ++SOFTWARE. +diff --git a/solvers/licenses/LICENSE.maplechrono b/solvers/licenses/LICENSE.maplechrono +new file mode 100644 +index 0000000..659cd30 +--- /dev/null ++++ b/solvers/licenses/LICENSE.maplechrono +@@ -0,0 +1,30 @@ ++Maple_LCM_Dist_Chrono -- Copyright (c) 2018, Vadim Ryvchin, Alexander Nadel ++ ++GlucoseNbSAT -- Copyright (c) 2016,Chu Min LI,Mao Luo and Fan Xiao ++ Huazhong University of science and technology, China ++ MIS, Univ. Picardie Jules Verne, France ++ ++MapleSAT -- Copyright (c) 2016, Jia Hui Liang, Vijay Ganesh ++ ++MiniSat -- Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson ++ Copyright (c) 2007-2010 Niklas Sorensson ++ ++Permission is hereby granted, free of charge, to any person obtaining a ++copy of this software and associated documentation files (the ++"Software"), to deal in the Software without restriction, including ++without limitation the rights to use, copy, modify, merge, publish, ++distribute, sublicense, and/or sell copies of the Software, and to ++permit persons to whom the Software is furnished to do so, subject to ++the following conditions: ++ ++The above copyright notice and this permission notice shall be included ++in all copies or substantial portions of the Software. ++ ++THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS ++OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF ++MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND ++NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE ++LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION ++OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION ++WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. ++ +diff --git a/solvers/licenses/LICENSE.maplecm b/solvers/licenses/LICENSE.maplecm +new file mode 100644 +index 0000000..80c9cd9 +--- /dev/null ++++ b/solvers/licenses/LICENSE.maplecm +@@ -0,0 +1,22 @@ ++Maple_CM -- Copyright (c) 2018,Chu Min LI,Mao Luo and Fan Xiao ++ Huazhong University of science and technology, China ++ MIS, Univ. Picardie Jules Verne, France ++ ++Permission is hereby granted, free of charge, to any person obtaining a ++copy of this software and associated documentation files (the ++"Software"), to deal in the Software without restriction, including ++without limitation the rights to use, copy, modify, merge, publish, ++distribute, sublicense, and/or sell copies of the Software, and to ++permit persons to whom the Software is furnished to do so, subject to ++the following conditions: ++ ++The above copyright notice and this permission notice shall be included ++in all copies or substantial portions of the Software. ++ ++THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS ++OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF ++MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND ++NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE ++LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION ++OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION ++WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. +diff --git a/solvers/licenses/LICENSE.maplesat b/solvers/licenses/LICENSE.maplesat +new file mode 100644 +index 0000000..9ecdbc9 +--- /dev/null ++++ b/solvers/licenses/LICENSE.maplesat +@@ -0,0 +1,23 @@ ++MiniSat -- Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson ++ Copyright (c) 2007-2010 Niklas Sorensson ++ ++Chanseok Oh's MiniSat Patch Series -- Copyright (c) 2015, Chanseok Oh ++ ++Permission is hereby granted, free of charge, to any person obtaining a ++copy of this software and associated documentation files (the ++"Software"), to deal in the Software without restriction, including ++without limitation the rights to use, copy, modify, merge, publish, ++distribute, sublicense, and/or sell copies of the Software, and to ++permit persons to whom the Software is furnished to do so, subject to ++the following conditions: ++ ++The above copyright notice and this permission notice shall be included ++in all copies or substantial portions of the Software. ++ ++THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS ++OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF ++MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND ++NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE ++LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION ++OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION ++WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. +diff --git a/solvers/licenses/LICENSE.mergesat3 b/solvers/licenses/LICENSE.mergesat3 +new file mode 100644 +index 0000000..e0ed582 +--- /dev/null ++++ b/solvers/licenses/LICENSE.mergesat3 +@@ -0,0 +1,30 @@ ++Copyright (c) 2016-2020 Norbert Manthey ++Copyright (c) 2019-2020 Armin Biere, Johannes Kepler University Linz, Austria ++Maple_LCM_Dist_Chrono -- Copyright (c) 2018, Vadim Ryvchin, Alexander Nadel ++MapleSAT -- Copyright (c) 2016, Jia Hui Liang, Vijay Ganesh ++GlucoseNbSAT -- Copyright (c) 2016, Chu Min LI, Mao Luo and Fan Xiao ++ Huazhong University of science and technology, China ++ MIS, Univ. Picardie Jules Verne, France ++MiniSat -- Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson ++ Copyright (c) 2007-2010 Niklas Sorensson ++ ++ ++ ++Permission is hereby granted, free of charge, to any person obtaining a ++copy of this software and associated documentation files (the ++"Software"), to deal in the Software without restriction, including ++without limitation the rights to use, copy, modify, merge, publish, ++distribute, sublicense, and/or sell copies of the Software, and to ++permit persons to whom the Software is furnished to do so, subject to ++the following conditions: ++ ++The above copyright notice and this permission notice shall be included ++in all copies or substantial portions of the Software. ++ ++THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS ++OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF ++MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND ++NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE ++LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION ++OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION ++WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. +diff --git a/solvers/licenses/LICENSE.mergesat3.glucose b/solvers/licenses/LICENSE.mergesat3.glucose +new file mode 100644 +index 0000000..6d52141 +--- /dev/null ++++ b/solvers/licenses/LICENSE.mergesat3.glucose +@@ -0,0 +1,30 @@ ++Glucose -- Copyright (c) 2009, Gilles Audemard, Laurent Simon ++ CRIL - Univ. Artois, France ++ LRI - Univ. Paris Sud, France ++ ++Glucose sources are based on MiniSat (see below MiniSat copyrights). Permissions and copyrights of ++Glucose are exactly the same as Minisat on which it is based on. (see below). ++ ++-------- ++ ++MiniSat -- Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson ++ Copyright (c) 2007-2010 Niklas Sorensson ++ ++Permission is hereby granted, free of charge, to any person obtaining a ++copy of this software and associated documentation files (the ++"Software"), to deal in the Software without restriction, including ++without limitation the rights to use, copy, modify, merge, publish, ++distribute, sublicense, and/or sell copies of the Software, and to ++permit persons to whom the Software is furnished to do so, subject to ++the following conditions: ++ ++The above copyright notice and this permission notice shall be included ++in all copies or substantial portions of the Software. ++ ++THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS ++OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF ++MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND ++NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE ++LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION ++OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION ++WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. +diff --git a/solvers/licenses/LICENSE.minicard b/solvers/licenses/LICENSE.minicard +new file mode 100644 +index 0000000..04604ab +--- /dev/null ++++ b/solvers/licenses/LICENSE.minicard +@@ -0,0 +1,25 @@ ++MiniCARD - Copyright (c) 2012-2015 Mark Liffiton, Jordyn Maglalang ++ ++ based on ++ ++MiniSat -- Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson ++ Copyright (c) 2007-2010 Niklas Sorensson ++ ++Permission is hereby granted, free of charge, to any person obtaining a ++copy of this software and associated documentation files (the ++"Software"), to deal in the Software without restriction, including ++without limitation the rights to use, copy, modify, merge, publish, ++distribute, sublicense, and/or sell copies of the Software, and to ++permit persons to whom the Software is furnished to do so, subject to ++the following conditions: ++ ++The above copyright notice and this permission notice shall be included ++in all copies or substantial portions of the Software. ++ ++THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS ++OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF ++MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND ++NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE ++LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION ++OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION ++WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. +diff --git a/solvers/licenses/LICENSE.minisat22 b/solvers/licenses/LICENSE.minisat22 +new file mode 100644 +index 0000000..22816ff +--- /dev/null ++++ b/solvers/licenses/LICENSE.minisat22 +@@ -0,0 +1,21 @@ ++MiniSat -- Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson ++ Copyright (c) 2007-2010 Niklas Sorensson ++ ++Permission is hereby granted, free of charge, to any person obtaining a ++copy of this software and associated documentation files (the ++"Software"), to deal in the Software without restriction, including ++without limitation the rights to use, copy, modify, merge, publish, ++distribute, sublicense, and/or sell copies of the Software, and to ++permit persons to whom the Software is furnished to do so, subject to ++the following conditions: ++ ++The above copyright notice and this permission notice shall be included ++in all copies or substantial portions of the Software. ++ ++THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS ++OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF ++MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND ++NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE ++LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION ++OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION ++WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. +diff --git a/solvers/licenses/LICENSE.minisatep b/solvers/licenses/LICENSE.minisatep +new file mode 100644 +index 0000000..22816ff +--- /dev/null ++++ b/solvers/licenses/LICENSE.minisatep +@@ -0,0 +1,21 @@ ++MiniSat -- Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson ++ Copyright (c) 2007-2010 Niklas Sorensson ++ ++Permission is hereby granted, free of charge, to any person obtaining a ++copy of this software and associated documentation files (the ++"Software"), to deal in the Software without restriction, including ++without limitation the rights to use, copy, modify, merge, publish, ++distribute, sublicense, and/or sell copies of the Software, and to ++permit persons to whom the Software is furnished to do so, subject to ++the following conditions: ++ ++The above copyright notice and this permission notice shall be included ++in all copies or substantial portions of the Software. ++ ++THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS ++OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF ++MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND ++NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE ++LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION ++OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION ++WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. +diff --git a/solvers/licenses/LICENSE.minisatgh b/solvers/licenses/LICENSE.minisatgh +new file mode 100644 +index 0000000..22816ff +--- /dev/null ++++ b/solvers/licenses/LICENSE.minisatgh +@@ -0,0 +1,21 @@ ++MiniSat -- Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson ++ Copyright (c) 2007-2010 Niklas Sorensson ++ ++Permission is hereby granted, free of charge, to any person obtaining a ++copy of this software and associated documentation files (the ++"Software"), to deal in the Software without restriction, including ++without limitation the rights to use, copy, modify, merge, publish, ++distribute, sublicense, and/or sell copies of the Software, and to ++permit persons to whom the Software is furnished to do so, subject to ++the following conditions: ++ ++The above copyright notice and this permission notice shall be included ++in all copies or substantial portions of the Software. ++ ++THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS ++OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF ++MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND ++NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE ++LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION ++WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. +-- +2.43.0 + From 006c9fa23b89c4db6cca91d7e23348b6fcf9c9bc Mon Sep 17 00:00:00 2001 From: Ludovic Henry Date: Fri, 23 Oct 2026 12:33:25 +0800 Subject: [PATCH 4/5] python-sat: fix a joined line in the 1.9.dev17 solver licences patch --- .../0002-ship-the-licences-of-the-bundled-SAT-solvers.patch | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/patches/python-sat/1.9.dev17/0002-ship-the-licences-of-the-bundled-SAT-solvers.patch b/patches/python-sat/1.9.dev17/0002-ship-the-licences-of-the-bundled-SAT-solvers.patch index 82a93a72a577..6bf65ac6a6a4 100644 --- a/patches/python-sat/1.9.dev17/0002-ship-the-licences-of-the-bundled-SAT-solvers.patch +++ b/patches/python-sat/1.9.dev17/0002-ship-the-licences-of-the-bundled-SAT-solvers.patch @@ -714,7 +714,8 @@ index 0000000..22816ff +OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF +MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND +NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE -+LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION ++LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION ++OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION +WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. -- 2.43.0 From a97ea131a007751e043aa62dc3859e7078858bfd Mon Sep 17 00:00:00 2001 From: Ludovic Henry Date: Fri, 23 Oct 2026 12:34:15 +0800 Subject: [PATCH 5/5] python-sat: pick the upstream commit per version and skip the pindakaas requirement --- .github/workflows/build-python-sat.yml | 29 +++++++++++++++++++------- 1 file changed, 21 insertions(+), 8 deletions(-) diff --git a/.github/workflows/build-python-sat.yml b/.github/workflows/build-python-sat.yml index 9cfa32858d10..d4b1b9141338 100644 --- a/.github/workflows/build-python-sat.yml +++ b/.github/workflows/build-python-sat.yml @@ -35,10 +35,6 @@ permissions: contents: read # to fetch code (actions/checkout) env: - # Upstream pushes no git tag for its releases; this commit sets - # VERSION = (1, 9, 'dev', 15) and its tree is byte-identical to the released - # sdist. Move it together with the version in docs/packages/python-sat.yaml. - PYTHON_SAT_REF: 152884a6d1889f56a61049aaa773be23f0a8d8c1 MANYLINUX_RISCV64_IMAGE: quay.io/pypa/manylinux_2_39_riscv64 MUSLLINUX_RISCV64_IMAGE: quay.io/pypa/musllinux_1_2_riscv64 @@ -66,11 +62,24 @@ jobs: PYTHON_SAT_VERSION: ${{ matrix.version }} steps: - - name: Checkout pysat ${{ env.PYTHON_SAT_REF }} + # Upstream pushes no git tag for its releases; each commit below sets + # VERSION = (1, 9, 'dev', N) and its tree is the released sdist's. Add the + # commit of every new version here, together with docs/packages/python-sat.yaml. + - name: Resolve upstream commit for ${{ env.PYTHON_SAT_VERSION }} + id: upstream_ref + run: | + case "$PYTHON_SAT_VERSION" in + 1.9.dev15) ref=152884a6d1889f56a61049aaa773be23f0a8d8c1 ;; + 1.9.dev17) ref=5c6d801fb1fae958f6504af5692fa26b807c8e76 ;; + *) echo "No upstream commit recorded for python-sat $PYTHON_SAT_VERSION" >&2; exit 1 ;; + esac + echo "ref=${ref}" >> "$GITHUB_OUTPUT" + + - name: Checkout pysat ${{ steps.upstream_ref.outputs.ref }} uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 with: repository: pysathq/pysat - ref: ${{ env.PYTHON_SAT_REF }} + ref: ${{ steps.upstream_ref.outputs.ref }} persist-credentials: false - name: Checkout python-wheels @@ -106,14 +115,18 @@ jobs: # Rewrite that one slot to 0 in the unpacked sdist before installing it. # The python-sat wheel itself builds unchanged on musllinux; only this # test dependency needs the workaround. Alpine is detected in-container. + # From 1.9.dev17 requirements.txt lists pindakaas (a Rust extension with no + # riscv64 wheel) instead of pypblib; the tests that need it importorskip it, + # so it is left out rather than source-built. CIBW_BEFORE_TEST: >- - if [ -f /etc/alpine-release ]; then + if [ -f /etc/alpine-release ] && grep -q '^pypblib' {project}/requirements.txt; then pip download --no-deps --no-binary :all: pypblib==0.0.4 -d /tmp/pypblib && tar -xzf /tmp/pypblib/pypblib-0.0.4.tar.gz -C /tmp/pypblib && sed -i 's|NULL\(, */\* tp_print \*/\)|0\1|' /tmp/pypblib/pypblib-0.0.4/Modules/pblib/*.cpp && CPPFLAGS="-include sys/types.h" pip install /tmp/pypblib/pypblib-0.0.4; fi && - pip install -r {project}/requirements.txt + grep -v '^pindakaas' {project}/requirements.txt > /tmp/requirements.txt && + pip install -r /tmp/requirements.txt CIBW_TEST_REQUIRES: pytest CIBW_TEST_SOURCES: tests CIBW_TEST_COMMAND: >-