Metadata-Version: 2.4
Name: mlc-z3-static
Version: 5.3.1.post0
Summary: Prebuilt Z3 static libraries, headers, and CMake metadata
Keywords: z3,smt,static-library,cmake
Author: MLC AI
License-Expression: MIT
License-File: LICENSE
Classifier: Development Status :: 4 - Beta
Classifier: Intended Audience :: Developers
Classifier: Programming Language :: Python :: 3
Classifier: Programming Language :: Python :: 3 :: Only
Classifier: Programming Language :: C++
Classifier: Topic :: Software Development :: Build Tools
Project-URL: Repository, https://github.com/mlc-ai/package
Project-URL: Z3, https://github.com/Z3Prover/z3
Requires-Python: >=3.8
Provides-Extra: test
Requires-Dist: pytest; extra == "test"
Requires-Dist: cmake>=3.26; extra == "test"
Requires-Dist: ninja; extra == "test"
Description-Content-Type: text/markdown

# mlc-z3-static

`mlc-z3-static` is a Python package that carries native Z3 development
artifacts for build systems. It does not provide Z3 Python bindings. The pinned
Z3 release is recorded in [`version.py`](version.py); at runtime it is exposed
as `mlc_z3_static.Z3_VERSION`, `mlc_z3_static.Z3_TAG`, and
`mlc_z3_static.Z3_COMMIT`.

The wheel contains:

- Z3 C and C++ headers.
- A position-independent static `libz3` (`libz3.a` on Unix-like platforms,
  `.lib` on Windows).
- Relocatable CMake and pkg-config metadata under
  `mlc_z3_static/static/lib/cmake/z3` and `mlc_z3_static/static/lib/pkgconfig`.

The package is built with scikit-build-core: building a wheel runs
`scripts/prepare_z3.py`, which downloads the pinned Z3 source archive,
verifies its SHA-256 digest, and builds the static library. Prebuilt wheels
are published for common platforms; elsewhere pip builds from the sdist like
any other compiled package (see [Build From Source](#build-from-source)).

## Python Helpers

Build systems can locate the packaged artifacts from Python:

```python
import mlc_z3_static

print(mlc_z3_static.get_cmake_dir("static"))
print(mlc_z3_static.get_cmake_prefix_path())
print(mlc_z3_static.get_static_library_path())
```

Or from a build script through the configuration CLI:

```bash
python -m mlc_z3_static.config --cmake-dir
python -m mlc_z3_static.config --prefix
```

## Downstream CMake Usage

Install the wheel into the Python environment used by the downstream build:

```bash
python -m pip install mlc-z3-static
```

Point CMake at the packaged static Z3 and use Z3's exported target:

```bash
cmake -S . -B build \
  -DCMAKE_BUILD_TYPE=Release \
  -DZ3_DIR="$(python -m mlc_z3_static.config --cmake-dir)"
```

```cmake
cmake_minimum_required(VERSION 3.20)
project(my_z3_consumer LANGUAGES C CXX)

find_package(Z3 CONFIG REQUIRED)

add_executable(my_z3_consumer main.cpp)
target_link_libraries(my_z3_consumer PRIVATE z3::libz3)
target_compile_features(my_z3_consumer PRIVATE cxx_std_20)
```

Or resolve the directory from inside CMake:

```cmake
find_package(Python3 COMPONENTS Interpreter REQUIRED)
execute_process(
  COMMAND "${Python3_EXECUTABLE}" -m mlc_z3_static.config --cmake-dir
  OUTPUT_STRIP_TRAILING_WHITESPACE
  OUTPUT_VARIABLE Z3_DIR
)
find_package(Z3 CONFIG REQUIRED)
```

Z3 is implemented in C++, so even C-only consumers should enable CXX in the
CMake project and let CMake link through a C++ linker when using the static
archive. No shared Z3 library or DLL is bundled. See
`example_project/` for a complete uv-managed consumer.

## Build From Source

Building from the sdist (or this directory) needs a C++20 compiler with
`<format>` support (Z3 5.x requires it; e.g. GCC >= 13, Clang >= 17, Visual
Studio 2022), network access to download the pinned Z3 source archive, and
Python; CMake (>= 3.26) and Ninja are pulled in as build requirements. A static Z3 build
takes a while; set `CMAKE_BUILD_PARALLEL_LEVEL` to use more cores:

```bash
CMAKE_BUILD_PARALLEL_LEVEL=8 python -m pip install --no-binary mlc-z3-static mlc-z3-static
```

Build a wheel from a checkout:

```bash
python -m build --wheel
```

Use an existing Z3 checkout instead of downloading the pinned archive:

```bash
MLC_Z3_STATIC_SOURCE_DIR=/path/to/z3 python -m build --wheel
```

## Build Release Wheels

The publishing workflow builds `py3-none` wheels for manylinux_2_28
(`x86_64`, `aarch64`), macOS (`arm64`, `x86_64`), and Windows (`AMD64`,
`ARM64`). On Windows the inner Z3 build uses the same Visual Studio platform
(`-A x64` or `-A ARM64`) as the wheel being built. MSVC builds explicitly
enable `/Zc:inline` to omit unused inline COMDAT code and data from object
files while preserving the static linking interface.

From this directory:

```bash
scripts/wheel_manylinux_2_28.sh
```

```bash
scripts/wheel_macos.sh
```

```powershell
scripts\wheel_windows.ps1
```

The scripts use `uv` for host-side Python tooling, so Debian/Ubuntu system
Python restrictions such as PEP 668 and missing `ensurepip` do not affect the
host CIBW runner. They run `cibuildwheel==3.3.1`, which tests each wheel in a
clean virtual environment with the pytest suite (see [Tests](#tests)): it
links a small CMake consumer against `z3::libz3` against the static library, runs it,
and checks that the static flavor does not link a dynamic `libz3`. The
manylinux script retags Linux wheels as `manylinux_2_28`.

The manylinux script defaults to the host architecture. Set
`MLC_Z3_STATIC_ARCH=x86_64` or `MLC_Z3_STATIC_ARCH=aarch64` to choose explicitly.

On macOS, local CIBW builds require an official python.org CPython installation.
The script defaults to the newest installed python.org CPython only as the build
interpreter. The output wheel is still Python-agnostic and tagged
`py3-none-<platform>`. Override `CIBW_BUILD` to force a specific installed build
interpreter, for example `CIBW_BUILD=cp313-macosx_arm64`.

## Tests

The pytest suite under `tests/python/` exercises the installed package. The
tests check the version metadata, artifact paths, and the config CLI, and configure,
link, and run a small CMake consumer against the static library (this needs a C++ compiler). From this directory:

```bash
python -m pip install ".[test]"   # or: python -m pip install <wheel> pytest
pytest
```

Run pytest against an installed wheel; the tests import the installed
package, not `python/`. cibuildwheel runs the same suite on every built wheel.

## License

This package is distributed under the MIT License, the license of the Z3
artifacts it bundles. `LICENSE` is a verbatim copy of Z3's upstream
`LICENSE.txt`, so this directory and its sdist are self-contained. The wheel
also carries the license copied during packaging from the SHA-256-verified
upstream source archive as `mlc_z3_static/licenses/LICENSE-Z3.txt`; the build
fails if that file is missing.

## Bumping the version

[`version.py`](version.py) is the single version source. To move to a new Z3
release, edit only that file:

- `Z3_VERSION`: the upstream release (the Git tag is derived as
  `z3-<Z3_VERSION>`).
- `__version__`: the Python package version; it must equal `Z3_VERSION`, or
  `Z3_VERSION` plus a PEP 440 suffix such as `.post1`.
- `Z3_COMMIT`: the commit the release tag points to:

  ```bash
  gh api repos/Z3Prover/z3/commits/z3-<Z3_VERSION> --jq .sha
  ```

- `Z3_ARCHIVE_SHA256`: the SHA-256 of the archive `scripts/prepare_z3.py`
  downloads:

  ```bash
  curl -fsSL https://github.com/Z3Prover/z3/archive/<Z3_COMMIT>.tar.gz | sha256sum
  ```

Package metadata, the build scripts, the default build directory, and the
generated runtime module `mlc_z3_static/_version.py` all read these values.
The publishing workflow's `version_suffix` input runs
`scripts/stamp_version.py --suffix <suffix>`, which rewrites `__version__` in
the build checkout and rejects versions not based on `Z3_VERSION`.
