diff --git a/.github/workflows/build-python-sat.yml b/.github/workflows/build-python-sat.yml new file mode 100644 index 00000000000..9cfa32858d1 --- /dev/null +++ b/.github/workflows/build-python-sat.yml @@ -0,0 +1,146 @@ +# SPDX-FileCopyrightText: 2026 The RISE Project +# SPDX-License-Identifier: MIT +--- +# Based on the `build_wheels` job of +# https://github.com/pysathq/pysat/blob/master/.github/workflows/build.yml +# and the test job of +# https://github.com/pysathq/pysat/blob/master/.github/workflows/test.yml +name: Build python-sat wheels (riscv64) + +on: + workflow_dispatch: + inputs: + version: + description: 'Version glob to (re)build; empty builds every version of docs/packages/python-sat.yaml not released yet' + required: false + default: '' + pull_request: + branches: [main] + paths: + - '.github/workflows/build-python-sat.yml' + - 'docs/packages/python-sat.yaml' + - 'patches/python-sat/**' + push: + branches: [main] + paths: + - '.github/workflows/build-python-sat.yml' + - 'docs/packages/python-sat.yaml' + - 'patches/python-sat/**' + +concurrency: + group: ${{ github.workflow }}-${{ github.head_ref || github.run_id }} + cancel-in-progress: true + +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 + +jobs: + setup: + uses: $/.github/workflows/_setup.yml + with: + package: python-sat + version: ${{ inputs.version }} + + build_wheels: + needs: [setup] + if: needs.setup.outputs.versions != '[]' + name: Build python-sat ${{ matrix.version }} ${{ matrix.python }}-${{ matrix.libc }}_riscv64 + runs-on: ubuntu-24.04-riscv + timeout-minutes: 150 + strategy: + fail-fast: false + matrix: + version: ${{ fromJSON(needs.setup.outputs.versions) }} + python: ["cp312", "cp313", "cp314", "cp314t"] + libc: [manylinux, musllinux] + + env: + PYTHON_SAT_VERSION: ${{ matrix.version }} + + steps: + - name: Checkout pysat ${{ env.PYTHON_SAT_REF }} + uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 + with: + repository: pysathq/pysat + ref: ${{ env.PYTHON_SAT_REF }} + persist-credentials: false + + - name: Checkout python-wheels + uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 + with: + path: python-wheels + persist-credentials: false + + - name: Patch pysat source + run: git apply python-wheels/patches/python-sat/${{ env.PYTHON_SAT_VERSION }}/*.patch + + - name: Build wheels + uses: pypa/cibuildwheel@1828c10ab37f080699c7b81cea34097c684a7074 # v4.2.0 + env: + CIBW_ARCHS: riscv64 + CIBW_BUILD: ${{ matrix.python }}-${{ matrix.libc }}_riscv64 + CIBW_MANYLINUX_RISCV64_IMAGE: ${{ env.MANYLINUX_RISCV64_IMAGE }} + CIBW_MUSLLINUX_RISCV64_IMAGE: ${{ env.MUSLLINUX_RISCV64_IMAGE }} + CIBW_ENVIRONMENT: PIP_EXTRA_INDEX_URL=https://pypi.riseproject.dev/simple/ + # pypblib (a test-only requirement of tests/test_encode_pb_conditional.py + # and tests/test_integer.py) has no riscv64 wheel and builds from its + # 0.0.4 sdist (last release, 2019), which has two musl-only C++ breaks: + # - PBParser.h uses the BSD `uint` typedef without including + # : glibc's libstdc++ headers pull that in transitively, + # musl's do not ("'uint' was not declared in this scope"). Force-include + # it (musl defines `uint` there under _GNU_SOURCE, which g++ always sets); + # CPPFLAGS reaches both the C and C++ compile lines of build_ext. + # - every PyTypeObject initialiser in Modules/pblib/*.cpp passes NULL in the + # old tp_print slot, which is tp_vectorcall_offset (a Py_ssize_t) since + # CPython 3.8. On glibc NULL is GCC's `__null`, which converts to 0 with a + # warning; musl's headers define NULL as `nullptr` in C++11, which cannot + # initialise an integer ("cannot convert 'std::nullptr_t' to 'Py_ssize_t'"). + # 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. + CIBW_BEFORE_TEST: >- + if [ -f /etc/alpine-release ]; 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 + CIBW_TEST_REQUIRES: pytest + CIBW_TEST_SOURCES: tests + CIBW_TEST_COMMAND: >- + python -c "import importlib.metadata as m, pysolvers; + l = [p.name for p in m.files('python-sat') if '.dist-info/licenses/' in str(p)]; + assert len(l) == 20 and not hasattr(pysolvers, 'lingeling_new'), l" + && python -m pytest tests + + - uses: actions/upload-artifact@043fb46d1a93c77aae656e7c1c64a875d1fc6a0a # v7.0.1 + with: + name: python-sat-${{ env.PYTHON_SAT_VERSION }}-${{ matrix.python }}-${{ matrix.libc }}_riscv64 + path: wheelhouse/*.whl + if-no-files-found: error + + publish: + name: Publish python-sat ${{ matrix.version }} + needs: [setup, build_wheels] + if: needs.setup.outputs.versions != '[]' + strategy: + fail-fast: false + matrix: + version: ${{ fromJSON(needs.setup.outputs.versions) }} + permissions: + contents: write + pull-requests: write + uses: $/.github/workflows/_publish-wheel.yml + secrets: + app-private-key: ${{ secrets.RISEPROJECT_APP_PRIVATE_KEY }} + with: + artifact-pattern: python-sat-${{ matrix.version }}-*riscv64 diff --git a/docs/packages/python-sat.yaml b/docs/packages/python-sat.yaml new file mode 100644 index 00000000000..e5631ba055d --- /dev/null +++ b/docs/packages/python-sat.yaml @@ -0,0 +1,10 @@ +package-name: python-sat +source-code: https://github.com/pysathq/pysat +license: MIT +versions: +- version: 1.9.dev15 + patched: true + warning: >- + The riscv64 wheel does not include the Lingeling solver: its licence grants use for + evaluation and research only and no right to redistribute it. pysat.solvers.Lingeling + and Solver(name='lingeling') are unavailable; the other eighteen solvers are included. diff --git a/patches/python-sat/1.9.dev15/0001-build-without-the-Lingeling-solver.patch b/patches/python-sat/1.9.dev15/0001-build-without-the-Lingeling-solver.patch new file mode 100644 index 00000000000..80bdcb80e8a --- /dev/null +++ b/patches/python-sat/1.9.dev15/0001-build-without-the-Lingeling-solver.patch @@ -0,0 +1,82 @@ +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 eighteen. + +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 e487226..e7b2338 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', + '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 a71a900..9560e7a 100644 +--- a/tests/test_accum_stats.py ++++ b/tests/test_accum_stats.py +@@ -8,7 +8,6 @@ solvers = ['cadical103', + 'gluecard41', + 'glucose30', + 'glucose42', +- 'lingeling', + 'maplechrono', + 'maplecm', + 'maplesat', +diff --git a/tests/test_cnf.py b/tests/test_cnf.py +index c8a53aa..cacacc9 100644 +--- a/tests/test_cnf.py ++++ b/tests/test_cnf.py +@@ -12,7 +12,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 1a4004b..40f4597 100644 +--- a/tests/test_unique_model.py ++++ b/tests/test_unique_model.py +@@ -9,7 +9,6 @@ solvers = ['cadical103', + 'glucose30', + 'glucose41', + 'glucose42', +- 'lingeling', + 'maplechrono', + 'maplecm', + 'maplesat', +-- +2.43.0 + diff --git a/patches/python-sat/1.9.dev15/0002-ship-the-licences-of-the-bundled-SAT-solvers.patch b/patches/python-sat/1.9.dev15/0002-ship-the-licences-of-the-bundled-SAT-solvers.patch new file mode 100644 index 00000000000..6bf65ac6a6a --- /dev/null +++ b/patches/python-sat/1.9.dev15/0002-ship-the-licences-of-the-bundled-SAT-solvers.patch @@ -0,0 +1,722 @@ +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 +