tididi-cnf
Copyright (c) The tididi-cnf authors.

This product is licensed under the Apache License, Version 2.0 (see LICENSE).

Cargo.lock identifies the dependencies and their source revisions. Licence
paths below are relative to each dependency's Cargo source directory; binary
release archives and the Python wheel carry the texts under notices/.

tididi — Tree Decision Diagram library
--------------------------------------
Apache License 2.0. Full text: LICENSE in the tididi crate (notices/tididi/LICENSE).

Managed by Cargo. It is pure Rust and carries no third-party
source.

Vitri — CNF preprocessing and vtree construction library
--------------------------------------------------------
Apache License 2.0. Full text: LICENSE in the vitri crate (notices/vitri/LICENSE).

Managed by Cargo. Vitri vendors and builds CaDiCaL and the
Arjun stack (Arjun, CryptoMiniSat, cadiback, SBVA), and links FlowCutter
through the goatd crate. Their copyright notices, exact provenance, local
modifications and complete licence texts are maintained with that library:

  vitri: docs/THIRD-PARTY.md (notices/vitri/THIRD-PARTY.md)

That file links goatd's own THIRD-PARTY.md for the FlowCutter backend
(notices/vitri/goatd-THIRD-PARTY.md). Both are the authoritative attribution
for the native dependency stack.

GMP — arbitrary-precision arithmetic library
--------------------------------------------
LGPLv3+, and GPLv2+. Vitri's native stack links it dynamically. The binary
loads the system's GMP. The Python wheel bundles GMP as shared libraries,
built unmodified from the upstream tarball that the release attaches with
GNU's signature; the licence texts are notices/vitri/GMP-COPYING.LESSERv3,
notices/vitri/GMP-COPYINGv3 and notices/vitri/GMP-COPYINGv2.

Rust crates
-----------
The other dependencies are Rust crates that Cargo fetches from crates.io, each
under its own licence; Cargo.lock names every one and its version. One of them,
tikv-jemalloc-sys, builds the jemalloc allocator into the binary. jemalloc is
BSD-2-Clause: a binary distribution must reproduce its copyright notice, which
is the file jemalloc/COPYING inside that crate (notices/jemalloc/COPYING).