diff --git a/.github/workflows/cpp.yml b/.github/workflows/cpp.yml index 2f9fe58..f13f0ef 100644 --- a/.github/workflows/cpp.yml +++ b/.github/workflows/cpp.yml @@ -10,6 +10,7 @@ on: - CMakeLists.txt - crates/** - "!crates/oxidd-cli/**" + - "!crates/oxidd-ffi-python/**" - Cargo.* concurrency: diff --git a/.github/workflows/python.yml b/.github/workflows/python.yml index 0cd042c..33197f4 100644 --- a/.github/workflows/python.yml +++ b/.github/workflows/python.yml @@ -1,6 +1,8 @@ name: Python -# spell-checker:ignore awalsh,CIBW,jakebailey,pkgs,pydata,pyproject +# spell-checker:ignore armv,autodoc,awalsh,CIBW,gnueabihf,jakebailey,musleabihf +# spell-checker:ignore pkgs,pydata,pyproject,pythonx86,pythonarm64 +# spell-checker:ignore sdist,stubtest,xwin on: push: @@ -10,6 +12,7 @@ on: - pyproject.toml - crates/** - "!crates/oxidd-cli/**" + - "!crates/oxidd-ffi/**" - Cargo.* concurrency: @@ -20,33 +23,83 @@ env: CARGO_TERM_COLOR: always jobs: - lint-test-doc: - name: Lint, Test & Doc + linux: + name: Lint, Test, Doc & Build Wheels for Linux runs-on: ubuntu-24.04 steps: - uses: actions/checkout@v4 - - uses: awalsh128/cache-apt-pkgs-action@latest - with: - packages: cbindgen - version: 1.0 - uses: actions/setup-python@v5 with: - python-version: 3.x - - name: Install tools & dependencies - run: python -m pip install --upgrade pip ruff sphinx pydata-sphinx-theme cibuildwheel pytest + python-version: | + pypy3.9 + pypy3.10 + 3.x - name: Build - run: python -m pip install . + run: python -m pip install maturin[zig] mypy ruff -e '.[docs,test]' - name: Ruff check run: ruff check --output-format=github - name: Ruff format check run: ruff format --check + - name: mypy + run: mypy + - name: stubtest + run: python -m mypy.stubtest oxidd._oxidd - uses: jakebailey/pyright-action@v2 - name: Test run: pytest - name: Sphinx - run: sphinx-build bindings/python/doc target/python/doc + run: | + mkdir -p target/python/autodoc/oxidd + cp bindings/python/oxidd/*.py target/python/autodoc/oxidd + cp bindings/python/oxidd/_oxidd.pyi target/python/autodoc/oxidd/_oxidd.py + PYTHONPATH=target/python/autodoc sphinx-build bindings/python/doc target/python/doc + - name: Add Rust targets to build wheels + run: | + rustup target add \ + x86_64-unknown-linux-gnu x86_64-unknown-linux-musl \ + i686-unknown-linux-gnu i686-unknown-linux-musl \ + aarch64-unknown-linux-gnu aarch64-unknown-linux-musl \ + armv7-unknown-linux-gnueabihf armv7-unknown-linux-musleabihf + - name: Build wheels + run: | + manylinux=manylinux2014 + musllinux=musllinux_1_2 + + maturin sdist --out dist + + for target in x86_64-unknown-linux-gnu i686-unknown-linux-gnu aarch64-unknown-linux-gnu armv7-unknown-linux-gnueabihf; do + maturin build --release --out dist --compatibility $manylinux --zig --target $target + done + + for target in x86_64-unknown-linux-musl i686-unknown-linux-musl aarch64-unknown-linux-musl armv7-unknown-linux-musleabihf; do + maturin build --release --out dist --compatibility $musllinux --zig --target $target + done + + for pypy in pypy3.9 pypy3.10; do + for target in x86_64-unknown-linux-gnu i686-unknown-linux-gnu aarch64-unknown-linux-gnu; do + maturin build --release --out dist --interpreter $pypy --compatibility $manylinux --zig --target $target + done + for target in x86_64-unknown-linux-musl i686-unknown-linux-musl aarch64-unknown-linux-musl; do + maturin build --release --out dist --interpreter $pypy --compatibility $musllinux --zig --target $target + done + done + - name: Test wheels + run: | + run_tests() { + $1 -m venv .venv-$1 + .venv-$1/bin/pip install "${2}[test]" + .venv-$1/bin/pytest + } + run_tests python3 dist/oxidd-*-cp*-manylinux*_x86_64*.whl + run_tests pypy3.9 dist/oxidd-*-pp39-*-manylinux*_x86_64*.whl + run_tests pypy3.10 dist/oxidd-*-pp310-*-manylinux*_x86_64*.whl + - name: Upload wheels + uses: actions/upload-artifact@v4 + with: + name: python-wheels-linux + path: dist - name: Deploy Docs if: ${{ github.repository == 'OxiDD/oxidd' && github.ref == 'refs/heads/main' }} working-directory: target/python/doc @@ -61,31 +114,7 @@ jobs: KEY: ${{ secrets.WEBSITE_SSH_KEY }} KNOWN_HOSTS: ${{ secrets.WEBSITE_SSH_KNOWN_HOSTS }} - buildwheel-linux: - name: Build wheels for Linux - - runs-on: ubuntu-24.04 - - steps: - - uses: actions/checkout@v4 - - uses: docker/setup-qemu-action@v3 - - uses: awalsh128/cache-apt-pkgs-action@latest - with: - packages: cbindgen - version: 1.0 - - uses: actions/setup-python@v5 - with: - python-version: 3.x - - name: Install cibuildwheel - run: python3 -m pip install cibuildwheel - - name: Build (linux-buildwheel.py) - run: python3 bindings/python/build/linux-buildwheel.py --install-targets --archs all - - uses: actions/upload-artifact@v4 - with: - name: python-wheels-linux - path: wheelhouse/*.whl - - buildwheel-mac: + mac: name: Build wheels for macOS runs-on: ${{ matrix.os.image }} @@ -93,38 +122,91 @@ jobs: matrix: os: - { arch: x86_64, image: macos-13 } - - { arch: arm64, image: macos-14 } + - { arch: arm64, image: macos-14 } steps: - - uses: actions/checkout@v4 - - name: Install cbindgen - run: brew install cbindgen - - name: Build wheels - uses: pypa/cibuildwheel@v2.21.3 - env: - CIBW_ARCHS_MACOS: native - - - uses: actions/upload-artifact@v4 - with: - name: python-wheels-mac-${{ matrix.os.arch }} - path: ./wheelhouse/*.whl - - buildwheel-win: + - uses: actions/checkout@v4 + - uses: actions/setup-python@v5 + with: + python-version: | + pypy3.9 + pypy3.10 + 3.x + - name: Install Python build dependencies + run: python -m pip install maturin ruff + - name: Build CPython wheel + run: maturin build --release --out dist + - name: Build PyPy 3.9 wheel + run: maturin build --release --out dist --interpreter pypy3.9 + - name: Build PyPy 3.10 wheel + run: maturin build --release --out dist --interpreter pypy3.10 + - name: Test wheels + run: | + run_tests() { + $1 -m venv .venv-$1 + .venv-$1/bin/pip install "${2}[test]" + .venv-$1/bin/pytest + } + run_tests python3 dist/oxidd-*-cp*-*.whl + run_tests pypy3.9 dist/oxidd-*-pp39-*.whl + run_tests pypy3.10 dist/oxidd-*-pp310-*.whl + - uses: actions/upload-artifact@v4 + with: + name: python-wheels-mac-${{ matrix.os.arch }} + path: dist + + win: name: Build wheels for Windows runs-on: windows-2022 steps: - - uses: actions/checkout@v4 - - name: Install Rust targets - run: rustup target add aarch64-pc-windows-msvc - - name: Build wheels - uses: pypa/cibuildwheel@v2.21.3 - env: - CIBW_ARCHS_WINDOWS: all - CIBW_TEST_SKIP: "*-win_arm64" - - - uses: actions/upload-artifact@v4 - with: - name: python-wheels-win - path: ./wheelhouse/*.whl + - uses: actions/checkout@v4 + - name: Install Rust targets + run: rustup target add x86_64-pc-windows-msvc i686-pc-windows-msvc aarch64-pc-windows-msvc + - name: Install Maturin + uses: baptiste0928/cargo-install@v3 + with: + crate: maturin + args: --no-default-features # this is the important part: we don't want xwin + - uses: actions/setup-python@v5 + with: + python-version: | + pypy3.9 + pypy3.10 + 3.x + - name: Install Python (i686) + run: nuget install pythonx86 -OutputDirectory .python + - name: Install Python (aarch64) + run: nuget install pythonarm64 -OutputDirectory .python + - name: Install Python build dependencies + run: python -m pip install ruff + - name: Build CPython wheel (x86_64) + run: maturin build --release --out dist + - name: Build PyPy 3.9 wheel (x86_64) + run: maturin build --release --out dist --interpreter "$(where.exe pypy3.9)" + - name: Build PyPy 3.10 wheel (x86_64) + run: maturin build --release --out dist --interpreter "$(where.exe pypy3.10)" + - name: Build CPython wheel (i686) + run: maturin build --release --out dist --interpreter "$(get-item .python\pythonx86*\tools\python.exe)" --target i686-pc-windows-msvc + - name: Build CPython wheel (aarch64) + run: | + $env:PYO3_CROSS_LIB_DIR = "$(get-item .python\pythonarm64*\tools\libs)" + maturin build --release --out dist --target aarch64-pc-windows-msvc + - name: Test + run: | + python -m venv .venv-cp + pypy3.9 -m venv .venv-pp39 + pypy3.10 -m venv .venv-pp310 + foreach ($py in 'cp', 'pp39', 'pp310') { + & ".venv-$py\Scripts\pip.exe" install "$(get-item dist\oxidd-*-$py*-*amd64.whl)[test]" + & ".venv-$py\Scripts\pytest.exe" + } + + python -m venv .venv-cp-i686 + .venv-cp-i686\Scripts\pip.exe install "$(get-item dist\oxidd-*-$py*-*win32.whl)[test]" + .venv-cp-i686\Scripts\pytest.exe + - uses: actions/upload-artifact@v4 + with: + name: python-wheels-win-${{ matrix.target.arch }} + path: dist diff --git a/.gitignore b/.gitignore index d4294e6..43a9503 100644 --- a/.gitignore +++ b/.gitignore @@ -38,6 +38,8 @@ # clangd index (".clangd" is a config file now, thus trailing slash) .clangd/ .cache +# clangd compile flags +compile_flags.txt # Coverage reports .coverage # Python cache diff --git a/.project-words.txt b/.project-words.txt index d8c9a77..2ac00b5 100644 --- a/.project-words.txt +++ b/.project-words.txt @@ -25,6 +25,8 @@ cfgs CFLAGS cibuildwheel clangd +classattr +classmethod clippy codegen cofactor @@ -54,6 +56,7 @@ fieldless filesystems forall fullname +getattr Graphviz hashable hasher @@ -84,6 +87,7 @@ liboxidd linenos madvise manylinux +Maturin mdbook memchr minterm @@ -92,6 +96,7 @@ mmap MSVC MTBDD musllinux +mypy NAND nanorand nanos @@ -106,14 +111,21 @@ postprocess precompute ptrdiff pycache +pyclass pycodestyle +pydocstyle PYFFI Pyflakes +pyfunction +pylint +pymethods +pymodule pypa pyproject pypy pyright pytest +PYTHONPATH pyupgrade RAII realloc @@ -140,12 +152,14 @@ spinlock spinlocks sptr staticlib +staticmethod stdarg stdbool stdint stdlib struct structs +subclassable subdir subdirs subgroup diff --git a/Cargo.lock b/Cargo.lock index a069bd3..9cfc24d 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -57,6 +57,12 @@ dependencies = [ "windows-sys 0.52.0", ] +[[package]] +name = "anyhow" +version = "1.0.93" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "4c95c10ba0b00a02636238b814946408b1322d5ac4760326e6fb8ec956d85775" + [[package]] name = "arcslab" version = "0.1.0" @@ -367,6 +373,12 @@ dependencies = [ "hashbrown", ] +[[package]] +name = "indoc" +version = "2.0.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "b248f5224d1d606005e02c97f5aa4e88eeb230488bcc03bc9ca4d7991399f2b5" + [[package]] name = "is_sorted" version = "0.1.1" @@ -426,6 +438,15 @@ version = "2.7.4" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "78ca9ab1a0babb1e7d5695e3530886289c18cf2f87ec19a575a0abdce112e3a3" +[[package]] +name = "memoffset" +version = "0.9.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "488016bfae457b036d996092f6cb448677611ce4449e970ceaf42695203f218a" +dependencies = [ + "autocfg", +] + [[package]] name = "minimal-lexical" version = "0.2.1" @@ -587,6 +608,21 @@ dependencies = [ "rustc-hash", ] +[[package]] +name = "oxidd-ffi-python" +version = "0.8.1" +dependencies = [ + "anyhow", + "oxidd", + "oxidd-core", + "oxidd-dump", + "proc-macro2", + "pyo3", + "quote", + "rustc-hash", + "syn", +] + [[package]] name = "oxidd-manager-index" version = "0.8.1" @@ -712,6 +748,12 @@ dependencies = [ "windows-targets", ] +[[package]] +name = "portable-atomic" +version = "1.9.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "cc9c68a3f6da06753e9335d63e27f6b9754dd1920d941135b7ea8224f141adb2" + [[package]] name = "proc-macro-error" version = "1.0.4" @@ -737,13 +779,76 @@ dependencies = [ [[package]] name = "proc-macro2" -version = "1.0.87" +version = "1.0.89" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b3e4daa0dcf6feba26f985457cdf104d4b4256fc5a09547140f3631bb076b19a" +checksum = "f139b0662de085916d1fb67d2b4169d1addddda1919e696f3252b740b629986e" dependencies = [ "unicode-ident", ] +[[package]] +name = "pyo3" +version = "0.22.6" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "f402062616ab18202ae8319da13fa4279883a2b8a9d9f83f20dbade813ce1884" +dependencies = [ + "cfg-if", + "indoc", + "libc", + "memoffset", + "once_cell", + "portable-atomic", + "pyo3-build-config", + "pyo3-ffi", + "pyo3-macros", + "unindent", +] + +[[package]] +name = "pyo3-build-config" +version = "0.22.6" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "b14b5775b5ff446dd1056212d778012cbe8a0fbffd368029fd9e25b514479c38" +dependencies = [ + "once_cell", + "target-lexicon", +] + +[[package]] +name = "pyo3-ffi" +version = "0.22.6" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "9ab5bcf04a2cdcbb50c7d6105de943f543f9ed92af55818fd17b660390fc8636" +dependencies = [ + "libc", + "pyo3-build-config", +] + +[[package]] +name = "pyo3-macros" +version = "0.22.6" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "0fd24d897903a9e6d80b968368a34e1525aeb719d568dba8b3d4bfa5dc67d453" +dependencies = [ + "proc-macro2", + "pyo3-macros-backend", + "quote", + "syn", +] + +[[package]] +name = "pyo3-macros-backend" +version = "0.22.6" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "36c011a03ba1e50152b4b394b479826cad97e7a21eb52df179cd91ac411cbfbe" +dependencies = [ + "heck", + "proc-macro2", + "pyo3-build-config", + "quote", + "syn", +] + [[package]] name = "quote" version = "1.0.37" @@ -889,9 +994,9 @@ checksum = "7da8b5736845d9f2fcb837ea5d9e2628564b3b043a70948a3f0b778838c5fb4f" [[package]] name = "syn" -version = "2.0.79" +version = "2.0.87" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "89132cd0bf050864e1d38dc3bbc07a0eb8e7530af26344d3d2bbbef83499f590" +checksum = "25aa4ce346d03a6dcd68dd8b4010bcb74e54e62c90c573f394c46eae99aba32d" dependencies = [ "proc-macro2", "quote", @@ -919,6 +1024,12 @@ version = "1.0.1" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "55937e1799185b12863d447f42597ed69d9928686b8d88a1df17376a097d8369" +[[package]] +name = "target-lexicon" +version = "0.12.16" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "61c41af27dd6d1e27b1b16b489db798443478cef1f06a660c96db617ba5de3b1" + [[package]] name = "termcolor" version = "1.4.1" @@ -998,6 +1109,12 @@ version = "0.1.14" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "7dd6e30e90baa6f72411720665d41d89b9a3d039dc45b8faea1ddd07f617f6af" +[[package]] +name = "unindent" +version = "0.2.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "c7de7d73e1754487cb58364ee906a499937a0dfabd86bcb980fa99ec8c8fa2ce" + [[package]] name = "utf8parse" version = "0.2.2" diff --git a/bindings/python/build/__init__.py b/bindings/python/build/__init__.py deleted file mode 100644 index e69de29..0000000 diff --git a/bindings/python/build/ffi.py b/bindings/python/build/ffi.py deleted file mode 100644 index a6e233b..0000000 --- a/bindings/python/build/ffi.py +++ /dev/null @@ -1,227 +0,0 @@ -"""This script is run form setup.py (in the project root)""" - -from __future__ import annotations - -import io -import os -import platform -import sys -from enum import Enum -from pathlib import Path - -# Make relative imports work -sys.path.append(str(Path(__file__).parent.parent)) -__package__ = "build" - -from cffi import FFI - -from .util import fatal, linux_targets, repo_dir, run, which - -# spell-checker:ignore AUDITWHEEL,cdef,cdefs,liboxidd - - -if os.name != "posix" and os.name != "nt": - fatal("Error: only Unix and Windows systems are currently supported") - -target_dir = repo_dir / "target" -include_dir = target_dir / "include" -oxidd_h = include_dir / "oxidd.h" -profile = "release" -target = os.environ.get("CARGO_BUILD_TARGET") -lib_dir = target_dir / target / profile if target else target_dir / profile - -include_dir.mkdir(parents=True, exist_ok=True) - -container_build = os.environ.get("OXIDD_PYFFI_CONTAINER_BUILD", "") == "1" - - -class LinkMode(Enum): - """Modes to build OxiDD, set via the environment variable OXIDD_PYFFI_LINK_MODE""" - - STATIC = 0 - """ - Statically link against `liboxidd_ffi.a` or `oxidd_ffi.lib` in the - `target/` directory. - - This is the mode we will be using for shipping via PyPI since we do not need - to mess around with the RPath (which does not exist on Windows anyway). It - is also the default mode on Windows. - """ - - SHARED_SYSTEM = 1 - """ - Dynamically link against a system-installed `liboxidd.so`, `liboxidd.dylib`, - or `oxidd.dll`, respectively. - - This mode is useful for packaging in, e.g., Linux distributions. With this - mode, we do not need to ship the main OxiDD library in both packages, - `liboxidd` and `python3-oxidd`. We can furthermore decouple updates of the - two packages. - """ - - SHARED_DEV = 2 - """ - Dynamically link against `liboxidd_ffi.so`, `liboxidd_ffi.dylib`, or - `oxidd_ffi.dll` in the `target/` directory. - - This mode is the default for developing on Unix systems. When tuning - heuristics for instance, a simple `cargo build --release` suffices, no - `pip install --editable .` is required before re-running the Python script. - On Windows, setting this mode up requires extra work, since there is no - RPath like on Unix systems. - """ - - @staticmethod - def from_env() -> LinkMode: - """Read from the OXIDD_PYFFI_LINK_MODE environment variable""" - if container_build: - return LinkMode.STATIC - - key = "OXIDD_PYFFI_LINK_MODE" - s = os.environ.get(key, None) - if s is None: - # Since Windows does not have an RPath, static linking yields the - # better developer experience. - return LinkMode.SHARED_DEV if os.name != "nt" else LinkMode.STATIC - s = s.lower() - if s == "static": - return LinkMode.STATIC - if s == "shared-system": - return LinkMode.SHARED_SYSTEM - if s == "shared-dev": - return LinkMode.SHARED_DEV - fatal( - f"Error: unknown build mode '{s}', supported values for {key} are " - "`static`, `shared-system`, and `shared-dev`.", - ) - - def crate_type(self) -> str: - """Associated Rust crate type""" - if self == LinkMode.STATIC: - return "staticlib" - return "cdylib" - - -build_mode = LinkMode.from_env() - -if container_build: - lib_dir = target_dir / linux_targets[os.environ["AUDITWHEEL_PLAT"]] / profile -else: - cbindgen_bin = which("cbindgen") - - if build_mode != LinkMode.SHARED_SYSTEM: - cargo_bin = which("cargo") - - # Fix win32 build on win64 - if ( - platform.system() == "Windows" - and platform.machine() == "AMD64" - and sys.maxsize <= 0x1_0000_0000 - and not target - ): - target = "i686-pc-windows-msvc" - lib_dir = target_dir / target / profile - os.environ["CARGO_BUILD_TARGET"] = target - - print(f"building crates/oxidd-ffi ({target if target else 'native'}) ...") - # Use --crate-type=... to avoid missing linker errors when cross-compiling - run( - cargo_bin, - "rustc", - f"--profile={profile}", - "--package=oxidd-ffi", - f"--crate-type={build_mode.crate_type()}", - ) - - print("running cbindgen ...") - run( - cbindgen_bin, - f"--config={repo_dir / 'crates' / 'oxidd-ffi' / 'cbindgen.toml'}", - f"--output={oxidd_h}", - str(repo_dir / "crates" / "oxidd-ffi"), - ) - - -def read_cdefs(header: Path) -> str: - """Remove C macros and include directives from the include header since CFFI - cannot deal with them. - """ - - res = io.StringIO() - # encoding="utf-8" seems to be important on Windows - with header.open("r", encoding="utf-8") as f: - lines = iter(f) - while True: - line = next(lines, None) - if line is None: - break - if all(c == "\n" or c == "\r" for c in line): - continue - if line[0] == "#": - if line.startswith("#if") and not line.startswith( - "#ifndef __cplusplus" - ): - while True: - line = next(lines, None) - if line is None: - fatal( - f"Error parsing {header}: reached end of file while" - "searching for #endif", - ) - if line.startswith("#endif"): - break - continue - res.write(line) - return res.getvalue() - - -cdefs = read_cdefs(oxidd_h) - -flags: dict[str, list[str]] = { - "libraries": [] # for `+=` (MSVC) -} - -if build_mode == LinkMode.STATIC: - flags["include_dirs"] = [str(include_dir)] - - if os.name == "posix": - flags["extra_link_args"] = [str(lib_dir / "liboxidd_ffi.a")] - elif os.name == "nt": - # TODO: This should be derived from - # `cargo rustc -q -- --print=native-static-libs`, but without the - # `windows.lib` and without duplicates? - # spell-checker:ignore advapi,ntdll,userenv - flags["libraries"] += [ - "kernel32", - "advapi32", - "bcrypt", - "ntdll", - "userenv", - "ws2_32", - "msvcrt", - ] - flags["extra_link_args"] = [str(lib_dir / "oxidd_ffi.lib")] -elif build_mode == LinkMode.SHARED_SYSTEM: - if os.name == "posix": - flags["libraries"] = ["oxidd"] - elif os.name == "nt": - flags["libraries"] = ["oxidd.dll"] -elif build_mode == LinkMode.SHARED_DEV: - flags["include_dirs"] = [str(include_dir)] - flags["library_dirs"] = [str(lib_dir)] - if os.name == "posix": - flags["libraries"] = ["oxidd_ffi"] - flags["runtime_library_dirs"] = flags["library_dirs"] - elif os.name == "nt": - flags["libraries"] = ["oxidd_ffi.dll"] - # There is no RPath on Windows :( - -flags["extra_compile_args"] = ["-O2" if os.name != "nt" else "/O2"] - - -ffi = FFI() -ffi.set_source("_oxidd", "#include \n", ".c", **flags) -ffi.cdef(cdefs) - -if __name__ == "__main__": - ffi.compile(verbose=True) diff --git a/bindings/python/build/linux-buildwheel.py b/bindings/python/build/linux-buildwheel.py deleted file mode 100755 index 0c7ba71..0000000 --- a/bindings/python/build/linux-buildwheel.py +++ /dev/null @@ -1,150 +0,0 @@ -#!/usr/bin/env python3 - -from __future__ import annotations - -import argparse -import os -import sys -from pathlib import Path - -# Make relative imports work -sys.path.append(str(Path(__file__).parent.parent)) -__package__ = "build" - -import cibuildwheel.__main__ -import cibuildwheel.options - -from .util import linux_targets, repo_dir, run, which - -target_dir = repo_dir / "target" -include_dir = target_dir / "include" -oxidd_h = include_dir / "oxidd.h" -profile = "release" -lib_dir = target_dir / profile -wheelhouse_dir = repo_dir / "wheelhouse" - -include_dir.mkdir(parents=True, exist_ok=True) - - -def install_targets(triples: list[str], toolchain: str | None) -> None: - """Install Rust targets using `rustup target add`""" - rustup = which("rustup") - toolchain_args = [] - if toolchain: - toolchain_args = [f"--toolchain={toolchain}"] - run(rustup, "target", "add", *toolchain_args, *triples) - - -def build(archs: str, triples: list[str], toolchain: str | None) -> None: - """Build wheels - - - `archs` is passed to cibuildwheel - - `triples` are the Rust target triples to build - - `toolchain` is the Rust toolchain to use - - Must be run from the repository root directory. - """ - cargo = which("cargo") - cbindgen = which("cbindgen") - - toolchain_args = [] - if toolchain: - toolchain_args = [f"+{toolchain}"] - - for target in triples: - print(f"building crates/oxidd-ffi for {target} ...") - run( - cargo, - *toolchain_args, - "rustc", - f"--profile={profile}", - f"--target={target}", - "--package=oxidd-ffi", - "--crate-type=staticlib", - ) - - print("running cbindgen ...") - run( - cbindgen, - f"--config={repo_dir / 'crates' / 'oxidd-ffi' / 'cbindgen.toml'}", - f"--output={oxidd_h}", - str(repo_dir / "crates" / "oxidd-ffi"), - ) - - args = cibuildwheel.options.CommandLineArguments.defaults() - args.platform = "linux" - args.archs = archs - args.output_dir = wheelhouse_dir - - cibuildwheel.__main__.build_in_directory(args) - - -def get_triples(*archs: str) -> list[str]: - """Get the list of Rust triples""" - arch_set = set(archs) - # We don't handle auto* and native specifically but over-approximate - all_triples = ["auto", "auto64", "auto32", "native", "all"] - for k in all_triples: - if k in arch_set: - triples = list(linux_targets.values()) - break - else: - triples = [] - for triple in linux_targets.values(): - arch = triple.split("-")[0] - if arch == "ppc64le": - arch = "powerpc64le" - if arch in arch_set: - triples.append(triple) - return triples - - -def main() -> None: - parser = argparse.ArgumentParser( - description=( - "Build Python wheels for Linux using Rust cross compilation on the " - "host and cibuildwheel with OCI containers afterwards" - ), - ) - parser.add_argument( - "--install-targets", - action="store_true", - help="Run `rustup target add` for the respective targets", - ) - parser.add_argument( - "--archs", - default="auto", - help=( - "Comma-separated list of CPU architectures to build for. When set " - "to 'auto', builds the architectures natively supported on this " - "machine. Set this option to build an architecture via emulation, " - "for example, using binfmt_misc and QEMU. Default: auto. Choices: " - "auto, auto64, auto32, native, all, x86_64, i686, aarch64, " - "ppc64le, s390x" - ), - ) - parser.add_argument( - "--toolchain", - help=( - "Which Rust toolchain to use (stable, nightly, 1.77.2, ...). If " - "omitted, the default Rust toolchain will be picked." - ), - ) - - args = parser.parse_args() - archs = str(args.archs) - toolchain = None - if args.toolchain: - toolchain = str(args.toolchain) - - os.chdir(repo_dir) - - triples = get_triples(*(a.strip() for a in archs.split(","))) - if args.install_targets: - print("installing targets ...") - install_targets(triples, toolchain) - build(archs, triples, toolchain) - - -if __name__ == "__main__": - main() diff --git a/bindings/python/build/util.py b/bindings/python/build/util.py deleted file mode 100644 index 082027e..0000000 --- a/bindings/python/build/util.py +++ /dev/null @@ -1,60 +0,0 @@ -from __future__ import annotations - -import shlex -import shutil -import subprocess -import sys -from pathlib import Path -from typing import NoReturn - -# This is `bindings/python/build/util.py`, so we need four times `.parent` -repo_dir = Path(__file__).parent.parent.parent.parent.absolute() - - -def fatal(msg: str) -> NoReturn: - """Print an error message and exit""" - print(msg, file=sys.stderr) - exit(1) - - -def which(bin: str) -> str: - """shutil.which() but exit with a human-readable message if not found""" - res = shutil.which(bin) - if res is None: - fatal(f"Error: could not find {bin}") - return res - - -def run(*args: str) -> None: - """Run the given command and exit with a human-readable error message in - case of a non-zero exit code""" - res = subprocess.run(args, cwd=repo_dir, check=False) - if res.returncode != 0: - fatal(f"Error: {shlex.join(args)} failed") - - -#: Python platform tag -> Rust target triple -# spell-checker:ignore armv,gnueabi,musleabihf -linux_targets = { - # manylinux - # --------- - "manylinux2014_x86_64": "x86_64-unknown-linux-gnu", - "manylinux2014_i686": "i686-unknown-linux-gnu", - "manylinux2014_aarch64": "aarch64-unknown-linux-gnu", - "manylinux2014_ppc64le": "powerpc64le-unknown-linux-gnu", - "manylinux2014_s390x": "s390x-unknown-linux-gnu", - # not supported by cibuildwheel: - # "manylinux2014_armv7l": "armv7-unknown-linux-gnueabi", - # "manylinux2014_ppc64": "powerpc64-unknown-linux-gnu", - # - # musllinux - # --------- - # Note: Rust's targets require musl 1.2 - "musllinux_1_2_x86_64": "x86_64-unknown-linux-musl", - "musllinux_1_2_i686": "i686-unknown-linux-musl", - "musllinux_1_2_aarch64": "aarch64-unknown-linux-musl", - "musllinux_1_2_armv7l": "armv7-unknown-linux-musleabihf", - # Currently tier 3 targets, so we cannot install them using rustup - # "musllinux_1_2_ppc64le": "powerpc64le-unknown-linux-gnu", - # "musllinux_1_2_s390x": "s390x-unknown-linux-gnu", -} diff --git a/bindings/python/doc/conf.py b/bindings/python/doc/conf.py index d981093..e5995d2 100644 --- a/bindings/python/doc/conf.py +++ b/bindings/python/doc/conf.py @@ -1,11 +1,11 @@ -# Configuration file for the Sphinx documentation builder. -# -# For the full list of built-in configuration values, see the documentation: -# https://www.sphinx-doc.org/en/master/usage/configuration.html +"""Configuration file for the Sphinx documentation builder.""" # spell-checker:ignore intersphinx,sphinxcontrib,katex,pydata # spell-checker:ignore prerender,sourcelink,subclasshook,bysource +# For the full list of built-in configuration values, see the documentation: +# https://www.sphinx-doc.org/en/master/usage/configuration.html + # -- Project information ----------------------------------------------------- # https://www.sphinx-doc.org/en/master/usage/configuration.html#project-information @@ -25,13 +25,14 @@ "sphinx.ext.autodoc", "sphinx.ext.autosummary", "sphinx.ext.intersphinx", + "sphinx.ext.napoleon", ] autodoc_class_signature = "separated" autodoc_default_options = { "members": True, "member-order": "bysource", - "inherited-members": True, + "inherited-members": False, "show-inheritance": True, "special-members": True, "exclude-members": ( diff --git a/bindings/python/oxidd/.gitignore b/bindings/python/oxidd/.gitignore new file mode 100644 index 0000000..662931a --- /dev/null +++ b/bindings/python/oxidd/.gitignore @@ -0,0 +1 @@ +/_oxidd.pyi diff --git a/bindings/python/oxidd/__init__.py b/bindings/python/oxidd/__init__.py index 3b90d0a..7dfbe86 100644 --- a/bindings/python/oxidd/__init__.py +++ b/bindings/python/oxidd/__init__.py @@ -1,7 +1,7 @@ """OxiDD A concurrent decision diagram library. -""" +""" # noqa: D400 from __future__ import annotations diff --git a/bindings/python/oxidd/bcdd.py b/bindings/python/oxidd/bcdd.py index 350c702..aaf0e72 100644 --- a/bindings/python/oxidd/bcdd.py +++ b/bindings/python/oxidd/bcdd.py @@ -1,407 +1,5 @@ -"""Binary decision diagrams with complement edges (BCDDs)""" +"""Binary decision diagrams with complement edges (BCDDs).""" -from __future__ import annotations +__all__ = ["BCDDFunction", "BCDDManager", "BCDDSubstitution"] -__all__ = ["BCDDManager", "BCDDFunction"] - -import collections.abc - -from _oxidd import ffi as _ffi -from _oxidd import lib as _lib -from typing_extensions import Never, Self, override - -from . import protocols, util - - -class BCDDManager(protocols.BooleanFunctionManager["BCDDFunction"]): - """Manager for binary decision diagrams with complement edges""" - - _mgr: ... #: Wrapped FFI object (``oxidd_bcdd_manager_t``) - - def __init__(self, inner_node_capacity: int, apply_cache_size: int, threads: int): - """Create a new manager - - :param inner_node_capacity: Maximum count of inner nodes - :param apply_cache_capacity: Maximum count of apply cache entries - :param threads: Worker thread count for the internal thread pool - """ - self._mgr = _lib.oxidd_bcdd_manager_new( - inner_node_capacity, apply_cache_size, threads - ) - - @classmethod - def _from_raw(cls, raw) -> Self: - """Create a manager from a raw FFI object (``oxidd_bcdd_manager_t``)""" - manager = cls.__new__(cls) - manager._mgr = raw - return manager - - def __del__(self): - _lib.oxidd_bcdd_manager_unref(self._mgr) - - @override - def __eq__(self, other: object) -> bool: - """Check for referential equality""" - return isinstance(other, BCDDManager) and self._mgr._p == other._mgr._p - - @override - def __hash__(self) -> int: - return hash(self._mgr._p) - - @override - def new_var(self) -> BCDDFunction: - return BCDDFunction._from_raw(_lib.oxidd_bcdd_new_var(self._mgr)) - - @override - def true(self) -> BCDDFunction: - return BCDDFunction._from_raw(_lib.oxidd_bcdd_true(self._mgr)) - - @override - def false(self) -> BCDDFunction: - return BCDDFunction._from_raw(_lib.oxidd_bcdd_false(self._mgr)) - - @override - def num_inner_nodes(self) -> int: - return _lib.oxidd_bcdd_num_inner_nodes(self._mgr) - - @override - def dump_all_dot_file( - self, - path: str, - functions: collections.abc.Iterable[tuple[BCDDFunction, str]] = [], - variables: collections.abc.Iterable[tuple[BCDDFunction, str]] = [], - ) -> bool: - fs = [] - f_names = [] - for f, name in functions: - fs.append(f._func) - f_names.append(_ffi.new("char[]", name.encode())) - - vars = [] - var_names = [] - for f, name in variables: - vars.append(f._func) - var_names.append(_ffi.new("char[]", name.encode())) - - return bool( - _lib.oxidd_bcdd_manager_dump_all_dot_file( - self._mgr, - path.encode(), - fs, - f_names, - len(fs), - vars, - var_names, - len(vars), - ) - ) - - -class BCDDSubstitution: - """Substitution mapping variables to replacement functions""" - - _subst: ... #: Wrapped FFI object (``oxidd_bcdd_substitution_t *``) - - def __init__( - self, pairs: collections.abc.Iterable[tuple[BCDDFunction, BCDDFunction]] - ): - """Create a new substitution object for BCDDs - - See :meth:`abc.FunctionSubst.make_substitution` fore more details. - """ - self._subst = _lib.oxidd_bcdd_substitution_new( - len(pairs) if isinstance(pairs, collections.abc.Sized) else 0 - ) - for v, r in pairs: - _lib.oxidd_bcdd_substitution_add_pair(self._subst, v._func, r._func) - - def __del__(self): - _lib.oxidd_bcdd_substitution_free(self._subst) - - -class BCDDFunction( - protocols.BooleanFunctionQuant, - protocols.FunctionSubst[BCDDSubstitution], - protocols.HasLevel, -): - """Boolean function represented as a binary decision diagram with complement - edges (BCDD) - - All operations constructing BCDDs may throw a :exc:`MemoryError` in case - they run out of memory. - """ - - _func: ... #: Wrapped FFI object (``oxidd_bcdd_t``) - - def __init__(self, _: Never): - """Private constructor - - Functions cannot be instantiated directly and must be created from the - :class:`BCDDManager` or by combining existing functions instead. - """ - raise RuntimeError( - "Functions cannot be instantiated directly and must be created " - "from the BCDDManager and by combining existing functions instead." - ) - - @classmethod - def _from_raw(cls, raw) -> Self: - """Create a BCDD function from a raw FFI object (``oxidd_bcdd_t``)""" - if raw._p == _ffi.NULL: - raise MemoryError("OxiDD BCDD operation ran out of memory") - function = cls.__new__(cls) - function._func = raw - return function - - def __del__(self): - _lib.oxidd_bcdd_unref(self._func) - - @override - def __eq__(self, other: object) -> bool: - """Check if ``other`` references the same node in the same manager and - has the same edge tag - - Since BCDDs are a strong canonical form, ``self`` and ``other`` are - semantically equal (i.e., represent the same Boolean functions) if and - only if this method returns ``True``. - """ - return ( - isinstance(other, BCDDFunction) - and self._func._p == other._func._p - and self._func._i == other._func._i - ) - - @override - def __lt__(self, other: Self) -> bool: - return (self._func._p, self._func._i) < (other._func._p, other._func._i) - - @override - def __gt__(self, other: Self) -> bool: - return (self._func._p, self._func._i) > (other._func._p, other._func._i) - - @override - def __le__(self, other: Self) -> bool: - return (self._func._p, self._func._i) <= (other._func._p, other._func._i) - - @override - def __ge__(self, other: Self) -> bool: - return (self._func._p, self._func._i) >= (other._func._p, other._func._i) - - @override - def __hash__(self) -> int: - return hash((self._func._p, self._func._i)) - - @property - @override - def manager(self) -> BCDDManager: - return BCDDManager._from_raw(_lib.oxidd_bcdd_containing_manager(self._func)) - - @override - def cofactors(self) -> tuple[Self, Self] | None: - raw_pair = _lib.oxidd_bcdd_cofactors(self._func) - if raw_pair.first._p == _ffi.NULL: - return None - assert raw_pair.second._p != _ffi.NULL - return ( - self.__class__._from_raw(raw_pair.first), - self.__class__._from_raw(raw_pair.second), - ) - - @override - def cofactor_true(self) -> Self | None: - raw = _lib.oxidd_bcdd_cofactor_true(self._func) - return self.__class__._from_raw(raw) if raw._p != _ffi.NULL else None - - @override - def cofactor_false(self) -> Self | None: - raw = _lib.oxidd_bcdd_cofactor_false(self._func) - return self.__class__._from_raw(raw) if raw._p != _ffi.NULL else None - - @override - def level(self) -> int | None: - val = _lib.oxidd_bcdd_level(self._func) - return val if val != util._LEVEL_NO_MAX else None - - @override - def __invert__(self) -> Self: - return self.__class__._from_raw(_lib.oxidd_bcdd_not(self._func)) - - @override - def __and__(self, rhs: Self) -> Self: - assert ( - self._func._p == rhs._func._p - ), "`self` and `rhs` must belong to the same manager" - return self.__class__._from_raw(_lib.oxidd_bcdd_and(self._func, rhs._func)) - - @override - def __or__(self, rhs: Self) -> Self: - assert ( - self._func._p == rhs._func._p - ), "`self` and `rhs` must belong to the same manager" - return self.__class__._from_raw(_lib.oxidd_bcdd_or(self._func, rhs._func)) - - @override - def __xor__(self, rhs: Self) -> Self: - assert ( - self._func._p == rhs._func._p - ), "`self` and `rhs` must belong to the same manager" - return self.__class__._from_raw(_lib.oxidd_bcdd_xor(self._func, rhs._func)) - - @override - def nand(self, rhs: Self) -> Self: - assert ( - self._func._p == rhs._func._p - ), "`self` and `rhs` must belong to the same manager" - return self.__class__._from_raw(_lib.oxidd_bcdd_nand(self._func, rhs._func)) - - @override - def nor(self, rhs: Self) -> Self: - assert ( - self._func._p == rhs._func._p - ), "`self` and `rhs` must belong to the same manager" - return self.__class__._from_raw(_lib.oxidd_bcdd_nor(self._func, rhs._func)) - - @override - def equiv(self, rhs: Self) -> Self: - assert ( - self._func._p == rhs._func._p - ), "`self` and `rhs` must belong to the same manager" - return self.__class__._from_raw(_lib.oxidd_bcdd_equiv(self._func, rhs._func)) - - @override - def imp(self, rhs: Self) -> Self: - assert ( - self._func._p == rhs._func._p - ), "`self` and `rhs` must belong to the same manager" - return self.__class__._from_raw(_lib.oxidd_bcdd_imp(self._func, rhs._func)) - - @override - def imp_strict(self, rhs: Self) -> Self: - assert ( - self._func._p == rhs._func._p - ), "`self` and `rhs` must belong to the same manager" - return self.__class__._from_raw( - _lib.oxidd_bcdd_imp_strict(self._func, rhs._func) - ) - - @override - def ite(self, t: Self, e: Self) -> Self: - assert ( - self._func._p == t._func._p == e._func._p - ), "`self` and `t` and `e` must belong to the same manager" - return self.__class__._from_raw( - _lib.oxidd_bcdd_ite(self._func, t._func, e._func) - ) - - @override - @classmethod - def make_substitution( - cls, pairs: collections.abc.Iterable[tuple[Self, Self]] - ) -> BCDDSubstitution: - return BCDDSubstitution(pairs) - - @override - def substitute(self, substitution: BCDDSubstitution) -> Self: - return self.__class__._from_raw( - _lib.oxidd_bcdd_substitute(self._func, substitution._subst) - ) - - @override - def forall(self, vars: Self) -> Self: - assert ( - self._func._p == vars._func._p - ), "`self` and `vars` must belong to the same manager" - return self.__class__._from_raw(_lib.oxidd_bcdd_forall(self._func, vars._func)) - - @override - def exist(self, vars: Self) -> Self: - assert ( - self._func._p == vars._func._p - ), "`self` and `vars` must belong to the same manager" - return self.__class__._from_raw(_lib.oxidd_bcdd_exist(self._func, vars._func)) - - @override - def unique(self, vars: Self) -> Self: - assert ( - self._func._p == vars._func._p - ), "`self` and `vars` must belong to the same manager" - return self.__class__._from_raw(_lib.oxidd_bcdd_unique(self._func, vars._func)) - - @override - def apply_forall(self, op: util.BooleanOperator, rhs: Self, vars: Self): - if not isinstance(op, util.BooleanOperator): - # If op were an arbitrary integer that is not part of the enum, - # this would lead to undefined behavior - raise ValueError("`op` must be a BooleanOperator") - assert ( - self._func._p == rhs._func._p == vars._func._p - ), "`self`, `rhs`, and `vars` must belong to the same manager" - return self.__class__._from_raw( - _lib.oxidd_bcdd_apply_forall(op, self._func, rhs._func, vars._func) - ) - - @override - def apply_exist(self, op: util.BooleanOperator, rhs: Self, vars: Self): - if not isinstance(op, util.BooleanOperator): - raise ValueError("`op` must be a BooleanOperator") - assert ( - self._func._p == rhs._func._p == vars._func._p - ), "`self`, `rhs`, and `vars` must belong to the same manager" - return self.__class__._from_raw( - _lib.oxidd_bcdd_apply_exist(op, self._func, rhs._func, vars._func) - ) - - @override - def apply_unique(self, op: util.BooleanOperator, rhs: Self, vars: Self): - if not isinstance(op, util.BooleanOperator): - raise ValueError("`op` must be a BooleanOperator") - assert ( - self._func._p == rhs._func._p == vars._func._p - ), "`self`, `rhs`, and `vars` must belong to the same manager" - return self.__class__._from_raw( - _lib.oxidd_bcdd_apply_unique(op, self._func, rhs._func, vars._func) - ) - - @override - def node_count(self) -> int: - return int(_lib.oxidd_bcdd_node_count(self._func)) - - @override - def satisfiable(self) -> bool: - return bool(_lib.oxidd_bcdd_satisfiable(self._func)) - - @override - def valid(self) -> bool: - return bool(_lib.oxidd_bcdd_valid(self._func)) - - @override - def sat_count_float(self, vars: int) -> float: - return float(_lib.oxidd_bcdd_sat_count_double(self._func, vars)) - - @override - def pick_cube(self) -> util.Assignment | None: - raw = _lib.oxidd_bcdd_pick_cube(self._func) - return util.Assignment._from_raw(raw) if raw.len > 0 else None - - @override - def pick_cube_dd(self) -> Self: - return self.__class__._from_raw(_lib.oxidd_bcdd_pick_cube_dd(self._func)) - - @override - def pick_cube_dd_set(self, literal_set: Self) -> Self: - assert ( - self._func._p == literal_set._func._p - ), "`self` and `literal_set` must belong to the same manager" - return self.__class__._from_raw( - _lib.oxidd_bcdd_pick_cube_dd_set(self._func, literal_set._func) - ) - - @override - def eval(self, args: collections.abc.Collection[tuple[Self, bool]]) -> bool: - n = len(args) - c_args = util._alloc("oxidd_bcdd_bool_pair_t[]", n) - for c_arg, (f, v) in zip(c_args, args): - c_arg.func = f._func - c_arg.val = v - - return bool(_lib.oxidd_bcdd_eval(self._func, c_args, n)) +from ._oxidd import BCDDFunction, BCDDManager, BCDDSubstitution diff --git a/bindings/python/oxidd/bdd.py b/bindings/python/oxidd/bdd.py index 01429a3..cd3f788 100644 --- a/bindings/python/oxidd/bdd.py +++ b/bindings/python/oxidd/bdd.py @@ -1,405 +1,5 @@ -"""Binary decision diagrams (BDDs, without complement edges)""" +"""Binary decision diagrams (BDDs, without complement edges).""" -from __future__ import annotations +__all__ = ["BDDFunction", "BDDManager", "BDDSubstitution"] -__all__ = ["BDDManager", "BDDFunction"] - -import collections.abc - -from _oxidd import ffi as _ffi -from _oxidd import lib as _lib -from typing_extensions import Never, Self, override - -from . import protocols, util - - -class BDDManager(protocols.BooleanFunctionManager["BDDFunction"]): - """Manager for binary decision diagrams (without complement edges)""" - - _mgr: ... #: Wrapped FFI object (``oxidd_bdd_manager_t``) - - def __init__(self, inner_node_capacity: int, apply_cache_size: int, threads: int): - """Create a new manager - - :param inner_node_capacity: Maximum count of inner nodes - :param apply_cache_capacity: Maximum count of apply cache entries - :param threads: Worker thread count for the internal thread pool - """ - self._mgr = _lib.oxidd_bdd_manager_new( - inner_node_capacity, apply_cache_size, threads - ) - - @classmethod - def _from_raw(cls, raw) -> Self: - """Create a manager from a raw FFI object (``oxidd_bdd_manager_t``)""" - manager = cls.__new__(cls) - manager._mgr = raw - return manager - - def __del__(self): - _lib.oxidd_bdd_manager_unref(self._mgr) - - @override - def __eq__(self, other: object) -> bool: - """Check for referential equality""" - return isinstance(other, BDDManager) and self._mgr._p == other._mgr._p - - @override - def __hash__(self) -> int: - return hash(self._mgr._p) - - @override - def new_var(self) -> BDDFunction: - return BDDFunction._from_raw(_lib.oxidd_bdd_new_var(self._mgr)) - - @override - def true(self) -> BDDFunction: - return BDDFunction._from_raw(_lib.oxidd_bdd_true(self._mgr)) - - @override - def false(self) -> BDDFunction: - return BDDFunction._from_raw(_lib.oxidd_bdd_false(self._mgr)) - - @override - def num_inner_nodes(self) -> int: - return _lib.oxidd_bdd_num_inner_nodes(self._mgr) - - @override - def dump_all_dot_file( - self, - path: str, - functions: collections.abc.Iterable[tuple[BDDFunction, str]] = [], - variables: collections.abc.Iterable[tuple[BDDFunction, str]] = [], - ) -> bool: - fs = [] - f_names = [] - for f, name in functions: - fs.append(f._func) - f_names.append(_ffi.new("char[]", name.encode())) - - vars = [] - var_names = [] - for f, name in variables: - vars.append(f._func) - var_names.append(_ffi.new("char[]", name.encode())) - - return bool( - _lib.oxidd_bdd_manager_dump_all_dot_file( - self._mgr, - path.encode(), - fs, - f_names, - len(fs), - vars, - var_names, - len(vars), - ) - ) - - -class BDDSubstitution: - """Substitution mapping variables to replacement functions""" - - _subst: ... #: Wrapped FFI object (``oxidd_bdd_substitution_t *``) - - def __init__( - self, pairs: collections.abc.Iterable[tuple[BDDFunction, BDDFunction]] - ): - """Create a new substitution object for BDDs - - See :meth:`abc.FunctionSubst.make_substitution` fore more details. - """ - self._subst = _lib.oxidd_bdd_substitution_new( - len(pairs) if isinstance(pairs, collections.abc.Sized) else 0 - ) - for v, r in pairs: - _lib.oxidd_bdd_substitution_add_pair(self._subst, v._func, r._func) - - def __del__(self): - _lib.oxidd_bdd_substitution_free(self._subst) - - -class BDDFunction( - protocols.BooleanFunctionQuant, - protocols.FunctionSubst[BDDSubstitution], - protocols.HasLevel, -): - """Boolean function represented as a simple binary decision diagram (BDD) - - All operations constructing BDDs may throw a :exc:`MemoryError` in case they - run out of memory. - """ - - _func: ... #: Wrapped FFI object (``oxidd_bdd_t``) - - def __init__(self, _: Never): - """Private constructor - - Functions cannot be instantiated directly and must be created from the - :class:`BDDManager` or by combining existing functions instead. - """ - raise RuntimeError( - "Functions cannot be instantiated directly and must be created " - "from the BDDManager and by combining existing functions instead." - ) - - @classmethod - def _from_raw(cls, raw) -> Self: - """Create a BDD function from a raw FFI object (``oxidd_bdd_t``)""" - if raw._p == _ffi.NULL: - raise MemoryError("OxiDD BDD operation ran out of memory") - function = cls.__new__(cls) - function._func = raw - return function - - def __del__(self): - _lib.oxidd_bdd_unref(self._func) - - @override - def __eq__(self, other: object) -> bool: - """Check if ``other`` references the same node in the same manager - - Since BDDs are a strong canonical form, ``self`` and ``other`` are - semantically equal (i.e., represent the same Boolean functions) if and - only if this method returns ``True``. - """ - return ( - isinstance(other, BDDFunction) - and self._func._p == other._func._p - and self._func._i == other._func._i - ) - - @override - def __lt__(self, other: Self) -> bool: - return (self._func._p, self._func._i) < (other._func._p, other._func._i) - - @override - def __gt__(self, other: Self) -> bool: - return (self._func._p, self._func._i) > (other._func._p, other._func._i) - - @override - def __le__(self, other: Self) -> bool: - return (self._func._p, self._func._i) <= (other._func._p, other._func._i) - - @override - def __ge__(self, other: Self) -> bool: - return (self._func._p, self._func._i) >= (other._func._p, other._func._i) - - @override - def __hash__(self) -> int: - return hash((self._func._p, self._func._i)) - - @property - @override - def manager(self) -> BDDManager: - return BDDManager._from_raw(_lib.oxidd_bdd_containing_manager(self._func)) - - @override - def cofactors(self) -> tuple[Self, Self] | None: - raw_pair = _lib.oxidd_bdd_cofactors(self._func) - if raw_pair.first._p == _ffi.NULL: - return None - assert raw_pair.second._p != _ffi.NULL - return ( - self.__class__._from_raw(raw_pair.first), - self.__class__._from_raw(raw_pair.second), - ) - - @override - def cofactor_true(self) -> Self | None: - raw = _lib.oxidd_bdd_cofactor_true(self._func) - return self.__class__._from_raw(raw) if raw._p != _ffi.NULL else None - - @override - def cofactor_false(self) -> Self | None: - raw = _lib.oxidd_bdd_cofactor_false(self._func) - return self.__class__._from_raw(raw) if raw._p != _ffi.NULL else None - - @override - def level(self) -> int | None: - val = _lib.oxidd_bdd_level(self._func) - return val if val != util._LEVEL_NO_MAX else None - - @override - def __invert__(self) -> Self: - return self.__class__._from_raw(_lib.oxidd_bdd_not(self._func)) - - @override - def __and__(self, rhs: Self) -> Self: - assert ( - self._func._p == rhs._func._p - ), "`self` and `rhs` must belong to the same manager" - return self.__class__._from_raw(_lib.oxidd_bdd_and(self._func, rhs._func)) - - @override - def __or__(self, rhs: Self) -> Self: - assert ( - self._func._p == rhs._func._p - ), "`self` and `rhs` must belong to the same manager" - return self.__class__._from_raw(_lib.oxidd_bdd_or(self._func, rhs._func)) - - @override - def __xor__(self, rhs: Self) -> Self: - assert ( - self._func._p == rhs._func._p - ), "`self` and `rhs` must belong to the same manager" - return self.__class__._from_raw(_lib.oxidd_bdd_xor(self._func, rhs._func)) - - @override - def nand(self, rhs: Self) -> Self: - assert ( - self._func._p == rhs._func._p - ), "`self` and `rhs` must belong to the same manager" - return self.__class__._from_raw(_lib.oxidd_bdd_nand(self._func, rhs._func)) - - @override - def nor(self, rhs: Self) -> Self: - assert ( - self._func._p == rhs._func._p - ), "`self` and `rhs` must belong to the same manager" - return self.__class__._from_raw(_lib.oxidd_bdd_nor(self._func, rhs._func)) - - @override - def equiv(self, rhs: Self) -> Self: - assert ( - self._func._p == rhs._func._p - ), "`self` and `rhs` must belong to the same manager" - return self.__class__._from_raw(_lib.oxidd_bdd_equiv(self._func, rhs._func)) - - @override - def imp(self, rhs: Self) -> Self: - assert ( - self._func._p == rhs._func._p - ), "`self` and `rhs` must belong to the same manager" - return self.__class__._from_raw(_lib.oxidd_bdd_imp(self._func, rhs._func)) - - @override - def imp_strict(self, rhs: Self) -> Self: - assert ( - self._func._p == rhs._func._p - ), "`self` and `rhs` must belong to the same manager" - return self.__class__._from_raw( - _lib.oxidd_bdd_imp_strict(self._func, rhs._func) - ) - - @override - def ite(self, t: Self, e: Self) -> Self: - assert ( - self._func._p == t._func._p == e._func._p - ), "`self` and `t` and `e` must belong to the same manager" - return self.__class__._from_raw( - _lib.oxidd_bdd_ite(self._func, t._func, e._func) - ) - - @override - @classmethod - def make_substitution( - cls, pairs: collections.abc.Iterable[tuple[Self, Self]] - ) -> BDDSubstitution: - return BDDSubstitution(pairs) - - @override - def substitute(self, substitution: BDDSubstitution) -> Self: - return self.__class__._from_raw( - _lib.oxidd_bdd_substitute(self._func, substitution._subst) - ) - - @override - def forall(self, vars: Self) -> Self: - assert ( - self._func._p == vars._func._p - ), "`self` and `vars` must belong to the same manager" - return self.__class__._from_raw(_lib.oxidd_bdd_forall(self._func, vars._func)) - - @override - def exist(self, vars: Self) -> Self: - assert ( - self._func._p == vars._func._p - ), "`self` and `vars` must belong to the same manager" - return self.__class__._from_raw(_lib.oxidd_bdd_exist(self._func, vars._func)) - - @override - def unique(self, vars: Self) -> Self: - assert ( - self._func._p == vars._func._p - ), "`self` and `vars` must belong to the same manager" - return self.__class__._from_raw(_lib.oxidd_bdd_unique(self._func, vars._func)) - - @override - def apply_forall(self, op: util.BooleanOperator, rhs: Self, vars: Self): - if not isinstance(op, util.BooleanOperator): - # If op were an arbitrary integer that is not part of the enum, - # this would lead to undefined behavior - raise ValueError("`op` must be a BooleanOperator") - assert ( - self._func._p == rhs._func._p == vars._func._p - ), "`self`, `rhs`, and `vars` must belong to the same manager" - return self.__class__._from_raw( - _lib.oxidd_bdd_apply_forall(op, self._func, rhs._func, vars._func) - ) - - @override - def apply_exist(self, op: util.BooleanOperator, rhs: Self, vars: Self): - if not isinstance(op, util.BooleanOperator): - raise ValueError("`op` must be a BooleanOperator") - assert ( - self._func._p == rhs._func._p == vars._func._p - ), "`self`, `rhs`, and `vars` must belong to the same manager" - return self.__class__._from_raw( - _lib.oxidd_bdd_apply_exist(op, self._func, rhs._func, vars._func) - ) - - @override - def apply_unique(self, op: util.BooleanOperator, rhs: Self, vars: Self): - if not isinstance(op, util.BooleanOperator): - raise ValueError("`op` must be a BooleanOperator") - assert ( - self._func._p == rhs._func._p == vars._func._p - ), "`self`, `rhs`, and `vars` must belong to the same manager" - return self.__class__._from_raw( - _lib.oxidd_bdd_apply_unique(op, self._func, rhs._func, vars._func) - ) - - @override - def node_count(self) -> int: - return int(_lib.oxidd_bdd_node_count(self._func)) - - @override - def satisfiable(self) -> bool: - return bool(_lib.oxidd_bdd_satisfiable(self._func)) - - @override - def valid(self) -> bool: - return bool(_lib.oxidd_bdd_valid(self._func)) - - @override - def sat_count_float(self, vars: int) -> float: - return float(_lib.oxidd_bdd_sat_count_double(self._func, vars)) - - @override - def pick_cube(self) -> util.Assignment | None: - raw = _lib.oxidd_bdd_pick_cube(self._func) - return util.Assignment._from_raw(raw) if raw.len > 0 else None - - @override - def pick_cube_dd(self) -> Self: - return self.__class__._from_raw(_lib.oxidd_bdd_pick_cube_dd(self._func)) - - @override - def pick_cube_dd_set(self, literal_set: Self) -> Self: - assert ( - self._func._p == literal_set._func._p - ), "`self` and `literal_set` must belong to the same manager" - return self.__class__._from_raw( - _lib.oxidd_bdd_pick_cube_dd_set(self._func, literal_set._func) - ) - - @override - def eval(self, args: collections.abc.Collection[tuple[Self, bool]]) -> bool: - n = len(args) - c_args = util._alloc("oxidd_bdd_bool_pair_t[]", n) - for c_arg, (f, v) in zip(c_args, args): - c_arg.func = f._func - c_arg.val = v - - return bool(_lib.oxidd_bdd_eval(self._func, c_args, n)) +from ._oxidd import BDDFunction, BDDManager, BDDSubstitution diff --git a/bindings/python/oxidd/protocols.py b/bindings/python/oxidd/protocols.py index 8732398..7f4badf 100644 --- a/bindings/python/oxidd/protocols.py +++ b/bindings/python/oxidd/protocols.py @@ -1,7 +1,4 @@ -""" -The protocols classes declared in this module allow abstracting away the -concrete decision diagram kind in a type-safe fashion. -""" +"""Protocols that allow abstracting away the concrete DD kind in a type-safe fashion.""" from __future__ import annotations @@ -15,17 +12,18 @@ "HasLevel", ] -import collections.abc from abc import abstractmethod +from collections.abc import Iterable +from os import PathLike from typing import Generic, Protocol, TypeVar from typing_extensions import Self -from .util import Assignment, BooleanOperator +from .util import BooleanOperator class Function(Protocol): - """Function represented as decision diagram + """Function represented as decision diagram. A function is the combination of a reference to a :class:`Manager` and a (possibly tagged) edge pointing to a node. Obtaining the manager reference @@ -34,23 +32,24 @@ class Function(Protocol): @property @abstractmethod - def manager(self) -> Manager[Self]: - """The associated manager""" + def manager(self, /) -> Manager[Self]: + """The associated manager.""" raise NotImplementedError @abstractmethod - def node_count(self) -> int: - """Get the number of descendant nodes + def node_count(self, /) -> int: + """Get the number of descendant nodes. - The returned number includes the root node itself and terminal nodes. + Locking behavior: acquires the manager's lock for shared access. - Acquires the manager's lock for shared access. + Returns: + The count of descendant nodes including the node referenced by + ``self`` and terminal nodes. """ raise NotImplementedError - def __lt__(self, other: Self) -> bool: - """Check if ``self`` is less than ``other`` according to an arbitrary - total order + def __lt__(self, other: Self, /) -> bool: + """Check if ``self < other`` according to an arbitrary total order. The following restrictions apply: Assuming two functions ``f``, ``g`` with ``f < g``, then if either ``f`` or ``g`` is deleted and recreated @@ -61,16 +60,16 @@ def __lt__(self, other: Self) -> bool: """ raise NotImplementedError - def __gt__(self, other: Self) -> bool: - """Same as ``other < self``""" + def __gt__(self, other: Self, /) -> bool: + """Same as ``other < self``.""" raise NotImplementedError - def __le__(self, other: Self) -> bool: - """Same as ``not self > other``""" + def __le__(self, other: Self, /) -> bool: + """Same as ``not self > other``.""" raise NotImplementedError - def __ge__(self, other: Self) -> bool: - """Same as ``not self < other``""" + def __ge__(self, other: Self, /) -> bool: + """Same as ``not self < other``.""" raise NotImplementedError @@ -78,63 +77,71 @@ def __ge__(self, other: Self) -> bool: class FunctionSubst(Function, Generic[S], Protocol): - """Substitution extension for :class:`Function`""" + """Substitution extension for :class:`Function`.""" @classmethod @abstractmethod - def make_substitution(cls, pairs: collections.abc.Iterable[tuple[Self, Self]]) -> S: - """Create a new substitution object from a collection of pairs - ``(var, replacement)`` + def make_substitution(cls, pairs: Iterable[tuple[Self, Self]], /) -> S: + """Create a new substitution object from pairs ``(var, replacement)``. The intent behind substitution objects is to optimize the case where the same substitution is applied multiple times. We would like to re-use apply cache entries across these operations, and therefore, we need a - compact identifier for the substitution (provided by the returned - substitution object). + compact identifier for the substitution. This identifier is provided by + the returned substitution object. + + Args: + pairs: ``(variable, replacement)`` pairs, where all variables are + distinct. Furthermore, variables must be handles for the + respective decision diagram levels, i.e., the Boolean function + representing the variable for B(C)DDs, and a singleton set for + ZBDDs. The order of the pairs is irrelevant. - All variables of must be distinct. Furthermore, variables must be - handles for the respective decision diagram levels, e.g., the respective - Boolean function for B(C)DDs, and a singleton set for ZBDDs. The order - of the pairs is irrelevant. + Returns: + The substitution to be used with :meth:`substitute` """ raise NotImplementedError @abstractmethod - def substitute(self, substitution: S) -> Self: - """Substitute variables in ``self`` according to ``substitution``, which - can be created using :meth:`make_substitution` + def substitute(self, substitution: S, /) -> Self: + """Substitute variables in ``self`` according to ``substitution``. The substitution is performed in a parallel fashion, e.g.: ``(¬x ∧ ¬y)[x ↦ ¬x ∧ ¬y, y ↦ ⊥] = ¬(¬x ∧ ¬y) ∧ ¬⊥ = x ∨ y`` - Acquires the manager's lock for shared access. + Locking behavior: acquires the manager's lock for shared access. - ``self`` and all functions in ``substitution`` must belong to the same - manager. + Args: + substitution: A substitution object created using + :meth:`make_substitution`. All contained DD functions must + belong to the same manager as ``self``. """ raise NotImplementedError class HasLevel(Function, Protocol): - """Function whose decision diagram node is associated with a level""" + """Function whose decision diagram node is associated with a level.""" @abstractmethod - def level(self) -> int | None: - """Get the level of the underlying node (``None`` for terminals) + def level(self, /) -> int | None: + """Get the level of the underlying node. Locking behavior: acquires the manager's lock for shared access. - Runtime complexity: O(1) + Time complexity: O(1) + + Returns: + The level number or ``None`` for terminals """ raise NotImplementedError class BooleanFunction(Function, Protocol): - """Boolean function represented as decision diagram""" + """Boolean function represented as decision diagram.""" @abstractmethod - def cofactors(self) -> tuple[Self, Self] | None: - r"""Get the cofactors ``(f_true, f_false)`` of ``self`` + def cofactors(self, /) -> tuple[Self, Self] | None: + r"""Get the cofactors ``(f_true, f_false)`` of ``self``. Let f(x₀, …, xₙ) be represented by ``self``, where x₀ is (currently) the top-most variable. Then f\ :sub:`true`\ (x₁, …, xₙ) = f(⊤, x₁, …, xₙ) @@ -148,306 +155,433 @@ def cofactors(self) -> tuple[Self, Self] | None: Structurally, the cofactors are simply the children in case of BDDs and ZBDDs. (For BCDDs, the edge tags are adjusted accordingly.) On these - representations, runtime is thus in O(1). - - Returns ``None`` iff ``self`` references a terminal node. If you only - need ``f_true`` or ``f_false``, :meth:`cofactor_true` or - :meth:`cofactor_false` are slightly more efficient. + representations, the running time is thus in O(1). Locking behavior: acquires the manager's lock for shared access. + + Returns: + The cofactors ``(f_true, f_false)``, or ``None`` if ``self`` + references a terminal node + + See Also: + :meth:`cofactor_true`, :meth:`cofactor_false` if you only need one + of the cofactors """ raise NotImplementedError @abstractmethod - def cofactor_true(self) -> Self | None: - """Get the cofactor ``f_true`` of ``self`` - - This method is slightly more efficient than :meth:`Self::cofactors` in - case ``f_false`` is not needed. + def cofactor_true(self, /) -> Self | None: + """Get the cofactor ``f_true`` of ``self``. - For a more detailed description, see :meth:`cofactors`. + Locking behavior: acquires the manager's lock for shared access. - Returns ``None`` iff ``self`` references a terminal node. + Returns: + The cofactor ``f_true``, or ``None`` if ``self`` references a + terminal node - Locking behavior: acquires the manager's lock for shared access. + See Also: + :meth:`cofactors`, also for a more detailed description """ raise NotImplementedError @abstractmethod - def cofactor_false(self) -> Self | None: - """Get the cofactor ``f_true`` of ``self`` + def cofactor_false(self, /) -> Self | None: + """Get the cofactor ``f_false`` of ``self``. - This method is slightly more efficient than :meth:`Self::cofactors` in - case ``f_true`` is not needed. - - For a more detailed description, see :meth:`cofactors`. + Locking behavior: acquires the manager's lock for shared access. - Returns ``None`` iff ``self`` references a terminal node. + Returns: + The cofactor ``f_false``, or ``None`` if ``self`` references a + terminal node - Locking behavior: acquires the manager's lock for shared access. + See Also: + :meth:`cofactors`, also for a more detailed description """ raise NotImplementedError @abstractmethod - def __invert__(self) -> Self: - """Compute the negation ``¬self`` + def __invert__(self, /) -> Self: + """Compute the negation ``¬self``. + + Locking behavior: acquires the manager's lock for shared access. - Acquires the manager's lock for shared access. + Raises: + DDMemoryError: If the operation runs out of memory """ raise NotImplementedError @abstractmethod - def __and__(self, rhs: Self) -> Self: - """Compute the conjunction ``self ∧ rhs`` + def __and__(self, rhs: Self, /) -> Self: + """Compute the conjunction ``self ∧ rhs``. - ``self`` and ``rhs`` must belong to the same manager. + Locking behavior: acquires the manager's lock for shared access. + + Args: + rhs: Right-hand side operand. Must belong to the same manager as + ``self``. - Acquires the manager's lock for shared access. + Raises: + DDMemoryError: If the operation runs out of memory """ raise NotImplementedError @abstractmethod - def __or__(self, rhs: Self) -> Self: - """Compute the disjunction ``self ∨ rhs`` + def __or__(self, rhs: Self, /) -> Self: + """Compute the disjunction ``self ∨ rhs``. + + Locking behavior: acquires the manager's lock for shared access. - ``self`` and ``rhs`` must belong to the same manager. + Args: + rhs: Right-hand side operand. Must belong to the same manager as + ``self``. - Acquires the manager's lock for shared access. + Raises: + DDMemoryError: If the operation runs out of memory """ raise NotImplementedError @abstractmethod - def __xor__(self, rhs: Self) -> Self: - """Compute the exclusive disjunction ``self ⊕ rhs`` + def __xor__(self, rhs: Self, /) -> Self: + """Compute the exclusive disjunction ``self ⊕ rhs``. - ``self`` and ``rhs`` must belong to the same manager. + Locking behavior: acquires the manager's lock for shared access. + + Args: + rhs: Right-hand side operand. Must belong to the same manager as + ``self``. - Acquires the manager's lock for shared access. + Raises: + DDMemoryError: If the operation runs out of memory """ raise NotImplementedError @abstractmethod - def nand(self, rhs: Self) -> Self: - """Compute the negated conjunction ``self ⊼ rhs`` + def nand(self, rhs: Self, /) -> Self: + """Compute the negated conjunction ``self ⊼ rhs``. - ``self`` and ``rhs`` must belong to the same manager. + Locking behavior: acquires the manager's lock for shared access. - Acquires the manager's lock for shared access. + Args: + rhs: Right-hand side operand. Must belong to the same manager as + ``self``. + + Raises: + DDMemoryError: If the operation runs out of memory """ raise NotImplementedError @abstractmethod - def nor(self, rhs: Self) -> Self: - """Compute the negated disjunction ``self ⊽ rhs`` + def nor(self, rhs: Self, /) -> Self: + """Compute the negated disjunction ``self ⊽ rhs``. - ``self`` and ``rhs`` must belong to the same manager. + Locking behavior: acquires the manager's lock for shared access. - Acquires the manager's lock for shared access. + Args: + rhs: Right-hand side operand. Must belong to the same manager as + ``self``. + + Raises: + DDMemoryError: If the operation runs out of memory """ raise NotImplementedError @abstractmethod - def equiv(self, rhs: Self) -> Self: - """Compute the equivalence ``self ↔ rhs`` + def equiv(self, rhs: Self, /) -> Self: + """Compute the equivalence ``self ↔ rhs``. + + Locking behavior: acquires the manager's lock for shared access. - ``self`` and ``rhs`` must belong to the same manager. + Args: + rhs: Right-hand side operand. Must belong to the same manager as + ``self``. - Acquires the manager's lock for shared access. + Raises: + DDMemoryError: If the operation runs out of memory """ raise NotImplementedError @abstractmethod - def imp(self, rhs: Self) -> Self: - """Compute the implication ``self → rhs`` (or ``f ≤ g``) + def imp(self, rhs: Self, /) -> Self: + """Compute the implication ``self → rhs`` (or ``f ≤ g``). + + Locking behavior: acquires the manager's lock for shared access. - ``self`` and ``rhs`` must belong to the same manager. + Args: + rhs: Right-hand side operand. Must belong to the same manager as + ``self``. - Acquires the manager's lock for shared access. + Raises: + DDMemoryError: If the operation runs out of memory """ raise NotImplementedError @abstractmethod - def imp_strict(self, rhs: Self) -> Self: - """Compute the strict implication ``self < rhs`` + def imp_strict(self, rhs: Self, /) -> Self: + """Compute the strict implication ``self < rhs``. + + Locking behavior: acquires the manager's lock for shared access. - ``self`` and ``rhs`` must belong to the same manager. + Args: + rhs: Right-hand side operand. Must belong to the same manager as + ``self``. - Acquires the manager's lock for shared access. + Raises: + DDMemoryError: If the operation runs out of memory """ raise NotImplementedError @abstractmethod - def ite(self, t: Self, e: Self) -> Self: - """Compute the BDD for the conditional ``t if self else e`` + def ite(self, /, t: Self, e: Self) -> Self: + """Compute the decision diagram for the conditional ``t if self else e``. + + Locking behavior: acquires the manager's lock for shared access. - ``self``, ``t``, and ``e`` must belong to the same manager. + Args: + t: Then-case; must belong to the same manager as ``self`` + e: Else-case; must belong to the same manager as ``self`` - Acquires the manager's lock for shared access. + Raises: + DDMemoryError: If the operation runs out of memory """ raise NotImplementedError @abstractmethod - def satisfiable(self) -> bool: - """Check for satisfiability (i.e., at least one satisfying assignment) + def satisfiable(self, /) -> bool: + """Check for satisfiability. - Acquires the manager's lock for shared access. + Locking behavior: acquires the manager's lock for shared access. + + Returns: + Whether the Boolean function has at least one satisfying assignment """ raise NotImplementedError @abstractmethod - def valid(self) -> bool: - """Check for validity (i.e., that all assignments are satisfying) + def valid(self, /) -> bool: + """Check for validity. + + Locking behavior: acquires the manager's lock for shared access. - Acquires the manager's lock for shared access. + Returns: + Whether all assignments satisfy the Boolean function """ raise NotImplementedError @abstractmethod - def sat_count_float(self, vars: int) -> float: - """Count the number of satisfying assignments + def sat_count_float(self, /, vars: int) -> float: + """Count the number of satisfying assignments. - This method assumes that the function's domain of has `vars` many - variables. + Locking behavior: acquires the manager's lock for shared access. - Acquires the manager's lock for shared access. + Args: + vars: Assume that the function's domain has this many variables. """ raise NotImplementedError @abstractmethod - def pick_cube(self) -> Assignment | None: - """Pick a satisfying assignment + def pick_cube(self, /) -> list[bool | None] | None: + """Pick a satisfying assignment. - Returns ``None`` iff ``self`` is unsatisfiable. + Locking behavior: acquires the manager's lock for shared access. - Acquires the manager's lock for shared access. + Returns: + The satisfying assignment where the i-th value means that the i-th + variable is false, true, or don't care, respectively, or ``None`` if + ``self`` is unsatisfiable """ raise NotImplementedError @abstractmethod - def pick_cube_dd(self) -> Self: - """Pick a satisfying assignment, represented as decision diagram + def pick_cube_dd(self, /) -> Self: + """Pick a satisfying assignment, represented as decision diagram. - Returns ``⊥`` iff ``self`` is unsatisfiable. + Locking behavior: acquires the manager's lock for shared access. - Acquires the manager's lock for shared access. + Returns: + The satisfying assignment as decision diagram, or ``⊥`` if ``self`` + is unsatisfiable + + Raises: + DDMemoryError: If the operation runs out of memory """ raise NotImplementedError @abstractmethod - def pick_cube_dd_set(self, literal_set: Self) -> Self: - """Pick a satisfying assignment, represented as BDD, using the - literals in ``literal_set`` if there is a choice + def pick_cube_dd_set(self, /, literal_set: Self) -> Self: + """Pick a satisfying assignment as DD, with choices as of ``literal_set``. + + ``literal_set`` is a conjunction of literals. Whenever there is a choice + for a variable, it will be set to true if the variable has a positive + occurrence in ``literal_set``, and set to false if it occurs negated in + ``literal_set``. If the variable does not occur in ``literal_set``, then + it will be left as don't care if possible, otherwise an arbitrary (not + necessarily random) choice will be performed. - ``literal_set`` is represented as a conjunction of literals. Whenever - there is a choice for a variable, it will be set to true if the variable - has a positive occurrence in ``literal_set``, and set to false if it - occurs negated in ``literal_set``. If the variable does not occur in - ``literal_set``, then it will be left as don't care if possible, - otherwise an arbitrary (not necessarily random) choice will be - performed. + Locking behavior: acquires the manager's lock for shared access. + + Args: + literal_set: Conjunction of literals to determine the choice for + variables + + Returns: + The satisfying assignment as decision diagram, or ``⊥`` if ``self`` + is unsatisfiable - Acquires the manager's lock for shared access. + Raises: + DDMemoryError: If the operation runs out of memory """ raise NotImplementedError @abstractmethod - def eval(self, args: collections.abc.Collection[tuple[Self, bool]]) -> bool: - """Evaluate this Boolean function with arguments ``args`` + def eval(self, /, args: Iterable[tuple[Self, bool]]) -> bool: + """Evaluate this Boolean function with arguments ``args``. + + Locking behavior: acquires the manager's lock for shared access. - ``args`` determines the valuation for all variables. Missing values are - assumed to be false. However, note that the arguments may also determine - the domain, e.g., in case of ZBDDs. If values are specified multiple - times, the last one counts. Panics if any function in `args` refers to a - terminal node. + Args: + args: ``(variable, value)`` pairs where variables must be handles + for the respective decision diagram levels, i.e., the Boolean + function representing the variable for B(C)DDs, and a singleton + set for ZBDDs. + Missing variables are assumed to be false. However, note that + the arguments may also determine the domain, e.g., in case of + ZBDDs. If variables are given multiple times, the last value + counts. Besides that, the order is irrelevant. + All variable handles must belong to the same manager as ``self`` + and must reference inner nodes. - Acquires the manager's lock for shared access. + Returns: + The result of applying the function ``self`` to ``args`` """ raise NotImplementedError class BooleanFunctionQuant(BooleanFunction, Protocol): - """Quantification extension for :class:`BooleanFunction`""" + """Quantification extension for :class:`BooleanFunction`.""" @abstractmethod - def forall(self, vars: Self) -> Self: - """Compute the universal quantification over ``vars`` + def forall(self, /, vars: Self) -> Self: + """Compute the universal quantification over ``vars``. - ``vars`` is a set of variables, which in turn is just the conjunction of - the variables. This operation removes all occurrences of the variables - by universal quantification. Universal quantification ∀x. f(…, x, …) - of a boolean function f(…, x, …) over a single variable x is + This operation removes all occurrences of variables in ``vars`` by + universal quantification. Universal quantification ∀x. f(…, x, …) of a + Boolean function f(…, x, …) over a single variable x is f(…, 0, …) ∧ f(…, 1, …). - ``self`` and ``vars`` must belong to the same manager. + Locking behavior: acquires the manager's lock for shared access. + + Args: + vars: Set of variables represented as conjunction thereof. Must + belong to the same manager as ``self``. - Acquires the manager's lock for shared access. + Raises: + DDMemoryError: If the operation runs out of memory """ raise NotImplementedError @abstractmethod - def exist(self, vars: Self) -> Self: - """Compute the existential quantification over ``vars`` + def exist(self, /, vars: Self) -> Self: + """Compute the existential quantification over ``vars``. - ``vars`` is a set of variables, which in turn is just the conjunction of - the variables. This operation removes all occurrences of the variables - by existential quantification. Existential quantification ∃x. f(…, x, …) - of a boolean function f(…, x, …) over a single variable x is + This operation removes all occurrences of variables in ``vars`` by + existential quantification. Existential quantification ∃x. f(…, x, …) of + a Boolean function f(…, x, …) over a single variable x is f(…, 0, …) ∨ f(…, 1, …). - ``self`` and ``vars`` must belong to the same manager. + Locking behavior: acquires the manager's lock for shared access. - Acquires the manager's lock for shared access. + Args: + vars: Set of variables represented as conjunction thereof. Must + belong to the same manager as ``self``. + + Raises: + DDMemoryError: If the operation runs out of memory """ raise NotImplementedError @abstractmethod - def unique(self, vars: Self) -> Self: - """Compute the unique quantification over ``vars`` - - ``vars`` is a set of variables, which in turn is just the conjunction of - the variables. This operation removes all occurrences of the variables - by unique quantification. Unique quantification ∃!x. f(…, x, …) of a - boolean function f(…, x, …) over a single variable x is - f(…, 0, …) ⊕ f(…, 1, …). + def unique(self, /, vars: Self) -> Self: + """Compute the unique quantification over ``vars``. - Unique quantification is also known as the + This operation removes all occurrences of variables in ``vars`` by + unique quantification. Unique quantification ∃!x. f(…, x, …) of a + Boolean function f(…, x, …) over a single variable x is + f(…, 0, …) ⊕ f(…, 1, …). Unique quantification is also known as the `Boolean difference `_ or `Boolean derivative `_. - ``self`` and ``vars`` must belong to the same manager. + Locking behavior: acquires the manager's lock for shared access. + + Args: + vars: Set of variables represented as conjunction thereof. Must + belong to the same manager as ``self``. - Acquires the manager's lock for shared access. + Raises: + DDMemoryError: If the operation runs out of memory """ # noqa: E501 raise NotImplementedError @abstractmethod - def apply_forall(self, op: BooleanOperator, rhs: Self, vars: Self) -> Self: - """Combined application of ``op`` and :meth:`forall()`: - ``∀ vars. self  rhs`` + def apply_forall(self, /, op: BooleanOperator, rhs: Self, vars: Self) -> Self: + """Combined application of ``op`` and :meth:`forall()`. + + Locking behavior: acquires the manager's lock for shared access. - ``self``, ``rhs``, and ``vars`` must belong to the same manager. + Args: + op: Binary Boolean operator to apply to ``self`` and ``rhs`` + rhs: Right-hand side of the operator. Must belong to the same + manager as ``self``. + vars: Set of variables to quantify over. Represented as conjunction + of variables. Must belong to the same manager as ``self``. - Acquires the manager's lock for shared access.""" + Returns: + ``∀ vars. self  rhs`` + + Raises: + DDMemoryError: If the operation runs out of memory + """ raise NotImplementedError @abstractmethod - def apply_exist(self, op: BooleanOperator, rhs: Self, vars: Self) -> Self: - """Combined application of ``op`` and :meth:`exist()`: - ``∃ vars. self  rhs`` + def apply_exist(self, /, op: BooleanOperator, rhs: Self, vars: Self) -> Self: + """Combined application of ``op`` and :meth:`exist()`. + + Locking behavior: acquires the manager's lock for shared access. + + Args: + op: Binary Boolean operator to apply to ``self`` and ``rhs`` + rhs: Right-hand side of the operator. Must belong to the same + manager as ``self``. + vars: Set of variables to quantify over. Represented as conjunction + of variables. Must belong to the same manager as ``self``. - ``self``, ``rhs``, and ``vars`` must belong to the same manager. + Returns: + ``∃ vars. self  rhs`` - Acquires the manager's lock for shared access.""" + Raises: + DDMemoryError: If the operation runs out of memory + """ raise NotImplementedError @abstractmethod - def apply_unique(self, op: BooleanOperator, rhs: Self, vars: Self) -> Self: - """Combined application of ``op`` and :meth:`unique()`: - ``∃! vars. self  rhs`` + def apply_unique(self, /, op: BooleanOperator, rhs: Self, vars: Self) -> Self: + """Combined application of ``op`` and :meth:`unique()`. + + Locking behavior: acquires the manager's lock for shared access. + + Args: + op: Binary Boolean operator to apply to ``self`` and ``rhs`` + rhs: Right-hand side of the operator. Must belong to the same + manager as ``self``. + vars: Set of variables to quantify over. Represented as conjunction + of variables. Must belong to the same manager as ``self``. - ``self``, ``rhs``, and ``vars`` must belong to the same manager. + Returns: + ``∃! vars. self  rhs`` - Acquires the manager's lock for shared access.""" + Raises: + DDMemoryError: If the operation runs out of memory + """ raise NotImplementedError @@ -455,7 +589,7 @@ def apply_unique(self, op: BooleanOperator, rhs: Self, vars: Self) -> Self: class Manager(Generic[F], Protocol): - """Manager storing nodes and ensuring their uniqueness + """Manager storing nodes and ensuring their uniqueness. A manager is the data structure responsible for storing nodes and ensuring their uniqueness. It also defines the variable order. @@ -466,33 +600,36 @@ class Manager(Generic[F], Protocol): """ @abstractmethod - def num_inner_nodes(self) -> int: - """Get the number of inner nodes + def num_inner_nodes(self, /) -> int: + """Get the number of inner nodes. - Acquires the manager's lock for shared access. + Locking behavior: acquires the manager's lock for shared access. """ raise NotImplementedError @abstractmethod def dump_all_dot_file( self, - path: str, - functions: collections.abc.Iterable[tuple[F, str]] = [], - variables: collections.abc.Iterable[tuple[F, str]] = [], - ) -> bool: - """ - Dump the entire decision diagram in this manager as Graphviz DOT code to - a file at ``path`` - - If a file at ``path`` exists, it will be truncated, otherwise a new one - will be created. - - This method optionally allows to name BDD functions and variables. The - output may also include nodes that are not reachable from ``functions``. + /, + path: str | PathLike[str], + functions: Iterable[tuple[F, str]] = [], + variables: Iterable[tuple[F, str]] = [], + ) -> None: + """Dump the entire decision diagram in this manager as Graphviz DOT code. - Returns ``true`` on success. + The output may also include nodes that are not reachable from + ``functions``. Locking behavior: acquires the manager's lock for shared access. + + Args: + path: Path of the output file. If a file at ``path`` exists, it will + be truncated, otherwise a new one will be created. + functions: Optional names for DD functions + variables: Optional names for variables. The variables must be + handles for the respective decision diagram levels, i.e., the + Boolean function representing the variable for B(C)DDs, and a + singleton set for ZBDDs. """ raise NotImplementedError @@ -501,29 +638,31 @@ def dump_all_dot_file( class BooleanFunctionManager(Manager[BF], Protocol): - """Manager whose nodes represent Boolean functions""" + """Manager whose nodes represent Boolean functions.""" @abstractmethod - def new_var(self) -> BF: - """Get a fresh variable, i.e., a function that is true if and only if - the variable is true. This adds a new level to a decision diagram. + def new_var(self, /) -> BF: + """Get a fresh variable, adding a new level to a decision diagram. Acquires the manager's lock for exclusive access. + + Returns: + A Boolean function that is true if and only if the variable is true """ raise NotImplementedError @abstractmethod - def true(self) -> BF: - """Get the constant true Boolean function ``⊤`` + def true(self, /) -> BF: + """Get the constant true Boolean function ``⊤``. - Acquires the manager's lock for shared access. + Locking behavior: acquires the manager's lock for shared access. """ raise NotImplementedError @abstractmethod - def false(self) -> BF: - """Get the constant false Boolean function ``⊥`` + def false(self, /) -> BF: + """Get the constant false Boolean function ``⊥``. - Acquires the manager's lock for shared access. + Locking behavior: acquires the manager's lock for shared access. """ raise NotImplementedError diff --git a/bindings/python/oxidd/tests/test_boolean_function.py b/bindings/python/oxidd/tests/test_boolean_function.py index db5d874..746bdcc 100644 --- a/bindings/python/oxidd/tests/test_boolean_function.py +++ b/bindings/python/oxidd/tests/test_boolean_function.py @@ -1,3 +1,5 @@ +"""Test all Boolean functions over a fixed number of variables.""" + from __future__ import annotations from collections.abc import Sequence @@ -14,6 +16,8 @@ # spell-checker:ignore nvars,BFQS +__all__: list[str] = [] + class BooleanFunctionQuantSubst(BooleanFunctionQuant, FunctionSubst[Any], Protocol): pass @@ -24,7 +28,7 @@ class BooleanFunctionQuantSubst(BooleanFunctionQuant, FunctionSubst[Any], Protoc def bit_count(x: int) -> int: - """Count the number of one bits + """Count the number of one bits. To be replaced by int.bit_count() once we require Python 3.10 """ @@ -36,8 +40,10 @@ def bit_count(x: int) -> int: class AllBooleanFunctions(Generic[BF]): - """Python translation of ``TestAllBooleanFunctions`` from - ``crates/oxidd/tests/boolean_function.rs``""" + """Python translation of ``TestAllBooleanFunctions``. + + See ``crates/oxidd/tests/boolean_function.rs`` + """ _mgr: BooleanFunctionManager[BF] _vars: Sequence[BF] @@ -52,10 +58,13 @@ def __init__( vars: Sequence[BF], var_handles: Sequence[BF], ): - """Initialize the test, generating DDs for all Boolean functions for the - given variable set. ``vars`` are the Boolean functions representing the - variables identified by ``var_handles``. For BDDs, the two coincide, but - not for ZBDDs.""" + """Initialize the test. + + Generate DDs for all Boolean functions for the given variable set. + + ``vars`` are the Boolean functions representing the variables identified + by ``var_handles``. For B(C)DDs, the two coincide, but not for ZBDDs. + """ assert len(vars) == len(var_handles) self._mgr = manager @@ -121,8 +130,7 @@ def make_cube(self, positive: int, negative: int) -> BF: return cube def basic(self) -> None: - """Test basic operations on all Boolean function""" - + """Test basic operations on all Boolean function.""" nvars = len(self._vars) num_assignments = 1 << nvars num_functions = 1 << num_assignments @@ -296,12 +304,11 @@ def _subst_rec(self, replacements: list[int | None], current_var: int) -> None: assert actual == expected def subst(self) -> None: - """Test all possible substitutions""" + """Test all possible substitutions.""" self._subst_rec([None] * len(self._vars), 0) def quant(self) -> None: - """Test quantification operations on all Boolean function""" - + """Test quantification operations on all Boolean function.""" nvars = len(self._vars) num_assignments = 1 << nvars num_functions = 1 << num_assignments @@ -416,7 +423,10 @@ def test_zbdd_all_boolean_functions_2vars_t1() -> None: def pick_cube(mgr: oxidd.bdd.BDDManager | oxidd.bcdd.BCDDManager) -> None: - """Only works for B(C)DDs""" + """Tests related to ``pick_cube``. + + Only works for B(C)DDs. + """ tt = mgr.true() assert tt.level() is None diff --git a/bindings/python/oxidd/util.py b/bindings/python/oxidd/util.py index e85ce10..b2bb785 100644 --- a/bindings/python/oxidd/util.py +++ b/bindings/python/oxidd/util.py @@ -1,107 +1,5 @@ -"""Primitives and utilities""" +"""Primitives and utilities.""" -from __future__ import annotations +__all__ = ["BooleanOperator", "DDMemoryError"] -__all__ = ["BooleanOperator", "Assignment"] - -import enum -from collections.abc import Iterator, Sequence -from typing import Optional - -from _oxidd import ffi as _ffi -from _oxidd import lib as _lib -from typing_extensions import Never, Self, overload, override - -#: CFFI allocator that does not zero the newly allocated region -_alloc = _ffi.new_allocator(should_clear_after_alloc=False) - -#: Maximum numeric value of the Rust ``LevelNo`` type (used for terminals) -_LEVEL_NO_MAX = (1 << 32) - 1 - - -class BooleanOperator(enum.IntEnum): - """Binary operators on Boolean functions""" - - AND = _lib.OXIDD_BOOLEAN_OPERATOR_AND - """Conjunction ``lhs ∧ rhs``""" - OR = _lib.OXIDD_BOOLEAN_OPERATOR_OR - """Disjunction ``lhs ∨ rhs``""" - XOR = _lib.OXIDD_BOOLEAN_OPERATOR_XOR - """Exclusive disjunction ``lhs ⊕ rhs``""" - EQUIV = _lib.OXIDD_BOOLEAN_OPERATOR_EQUIV - """Equivalence ``lhs ↔ rhs``""" - NAND = _lib.OXIDD_BOOLEAN_OPERATOR_NAND - """Negated conjunction ``lhs ⊼ rhs``""" - NOR = _lib.OXIDD_BOOLEAN_OPERATOR_NOR - """Negated disjunction ``lhs ⊽ rhs``""" - IMP = _lib.OXIDD_BOOLEAN_OPERATOR_IMP - """Implication ``lhs → rhs``""" - IMP_STRICT = _lib.OXIDD_BOOLEAN_OPERATOR_IMP_STRICT - """Strict implication ``lhs < rhs``""" - - -class Assignment(Sequence[Optional[bool]]): - """Boolean Assignment returned by an FFI function""" - - _data: ... #: Wrapped oxidd_assignment_t - - def __init__(self, _: Never): - """Private constructor - - Assignments cannot be instantiated directly, they are only returned by - FFI functions. - """ - raise RuntimeError( - "Assignments cannot be instantiated directly, they are only " - "returned by FFI functions." - ) - - @classmethod - def _from_raw(cls, raw) -> Self: - """Create an assignment from a raw FFI object (``oxidd_assignment_t``)""" - assignment = cls.__new__(cls) - assignment._data = raw - return assignment - - def __del__(self): - _lib.oxidd_assignment_free(self._data) - - @override - def __len__(self) -> int: - return int(self._data.len) - - def _get_unchecked(self, index: int) -> bool | None: - """Get the element at ``index`` without bounds checking - - SAFETY: ``index`` must be in bounds (``0 <= index < len(self)``) - """ - v = int(self._data.data[index]) - return bool(v) if v >= 0 else None - - @override - @overload - def __getitem__(self, index: int) -> bool | None: ... - - @override - @overload - def __getitem__(self, index: slice) -> list[bool | None]: ... - - @override - def __getitem__(self, index: int | slice) -> bool | None | list[bool | None]: - n = len(self) - if isinstance(index, slice): - start, stop, step = index.indices(n) - return [self._get_unchecked(i) for i in range(start, stop, step)] - - i = index if index >= 0 else n + index - if i < 0 or i >= n: - raise IndexError("Assignment index out of range") - return self._get_unchecked(i) - - @override - def __iter__(self) -> Iterator[bool | None]: - return (self._get_unchecked(i) for i in range(len(self))) - - @override - def __reversed__(self) -> Iterator[bool | None]: - return (self._get_unchecked(i) for i in range(len(self) - 1, -1, -1)) +from ._oxidd import BooleanOperator, DDMemoryError diff --git a/bindings/python/oxidd/zbdd.py b/bindings/python/oxidd/zbdd.py index 7ef211d..5d38643 100644 --- a/bindings/python/oxidd/zbdd.py +++ b/bindings/python/oxidd/zbdd.py @@ -1,378 +1,5 @@ -"""Zero-suppressed binary decision diagrams (ZBDDs)""" +"""Zero-suppressed binary decision diagrams (ZBDDs).""" -from __future__ import annotations +__all__ = ["ZBDDFunction", "ZBDDManager"] -__all__ = ["ZBDDManager", "ZBDDFunction"] - -import collections.abc - -from _oxidd import ffi as _ffi -from _oxidd import lib as _lib -from typing_extensions import Never, Self, override - -from . import protocols, util - - -class ZBDDManager(protocols.BooleanFunctionManager["ZBDDFunction"]): - """Manager for zero-suppressed binary decision diagrams""" - - _mgr: ... #: Wrapped FFI object (``oxidd_zbdd_manager_t``) - - def __init__(self, inner_node_capacity: int, apply_cache_size: int, threads: int): - """Create a new manager - - :param inner_node_capacity: Maximum count of inner nodes - :param apply_cache_capacity: Maximum count of apply cache entries - :param threads: Worker thread count for the internal thread pool - """ - self._mgr = _lib.oxidd_zbdd_manager_new( - inner_node_capacity, apply_cache_size, threads - ) - - @classmethod - def _from_raw(cls, raw) -> Self: - """Create a manager from a raw FFI object (``oxidd_zbdd_manager_t``)""" - manager = cls.__new__(cls) - manager._mgr = raw - return manager - - def __del__(self): - _lib.oxidd_zbdd_manager_unref(self._mgr) - - @override - def __eq__(self, other: object) -> bool: - """Check for referential equality""" - return isinstance(other, ZBDDManager) and self._mgr._p == other._mgr._p - - @override - def __hash__(self) -> int: - return hash(self._mgr._p) - - def new_singleton(self) -> ZBDDFunction: - """Get a fresh variable in the form of a singleton set - - This adds a new level to a decision diagram. - - Acquires the manager's lock for exclusive access. - """ - return ZBDDFunction._from_raw(_lib.oxidd_zbdd_new_singleton(self._mgr)) - - @override - def new_var(self) -> ZBDDFunction: - return ZBDDFunction._from_raw(_lib.oxidd_zbdd_new_var(self._mgr)) - - def empty(self) -> ZBDDFunction: - """Get the ZBDD set ∅ - - Acquires the manager's lock for shared access. - """ - return ZBDDFunction._from_raw(_lib.oxidd_zbdd_empty(self._mgr)) - - def base(self) -> ZBDDFunction: - """Get the ZBDD set {∅} - - Acquires the manager's lock for shared access. - """ - return ZBDDFunction._from_raw(_lib.oxidd_zbdd_base(self._mgr)) - - @override - def true(self) -> ZBDDFunction: - return ZBDDFunction._from_raw(_lib.oxidd_zbdd_true(self._mgr)) - - @override - def false(self) -> ZBDDFunction: - return ZBDDFunction._from_raw(_lib.oxidd_zbdd_false(self._mgr)) - - @override - def num_inner_nodes(self) -> int: - return _lib.oxidd_zbdd_num_inner_nodes(self._mgr) - - @override - def dump_all_dot_file( - self, - path: str, - functions: collections.abc.Iterable[tuple[ZBDDFunction, str]] = [], - variables: collections.abc.Iterable[tuple[ZBDDFunction, str]] = [], - ) -> bool: - fs = [] - f_names = [] - for f, name in functions: - fs.append(f._func) - f_names.append(_ffi.new("char[]", name.encode())) - - vars = [] - var_names = [] - for f, name in variables: - vars.append(f._func) - var_names.append(_ffi.new("char[]", name.encode())) - - return bool( - _lib.oxidd_zbdd_manager_dump_all_dot_file( - self._mgr, - path.encode(), - fs, - f_names, - len(fs), - vars, - var_names, - len(vars), - ) - ) - - -class ZBDDFunction(protocols.BooleanFunction, protocols.HasLevel): - """Boolean function 𝔹ⁿ → 𝔹 (or set of Boolean vectors 𝔹ⁿ) represented as - zero-suppressed binary decision diagram - - All operations constructing ZBDDs may throw a :exc:`MemoryError` in case they - run out of memory. - """ - - _func: ... #: Wrapped FFI object (``oxidd_zbdd_t``) - - def __init__(self, _: Never): - """Private constructor - - Functions cannot be instantiated directly and must be created from the - :class:`ZBDDManager` or by combining existing functions instead. - """ - raise RuntimeError( - "Functions cannot be instantiated directly and must be created " - "from the ZBDDManager and by combining existing functions instead." - ) - - @classmethod - def _from_raw(cls, raw) -> Self: - """Create a ZBDD function from a raw FFI object (``oxidd_zbdd_t``)""" - if raw._p == _ffi.NULL: - raise MemoryError("OxiDD ZBDD operation ran out of memory") - function = cls.__new__(cls) - function._func = raw - return function - - def __del__(self): - _lib.oxidd_zbdd_unref(self._func) - - @override - def __eq__(self, other: object) -> bool: - """Check if ``other`` references the same node in the same manager - - Since ZBDDs are a strong canonical form, ``self`` and ``other`` are - semantically equal (i.e., represent the same Boolean functions) if and - only if this method returns ``True``. - """ - return ( - isinstance(other, ZBDDFunction) - and self._func._p == other._func._p - and self._func._i == other._func._i - ) - - @override - def __lt__(self, other: Self) -> bool: - return (self._func._p, self._func._i) < (other._func._p, other._func._i) - - @override - def __gt__(self, other: Self) -> bool: - return (self._func._p, self._func._i) > (other._func._p, other._func._i) - - @override - def __le__(self, other: Self) -> bool: - return (self._func._p, self._func._i) <= (other._func._p, other._func._i) - - @override - def __ge__(self, other: Self) -> bool: - return (self._func._p, self._func._i) >= (other._func._p, other._func._i) - - @override - def __hash__(self) -> int: - return hash((self._func._p, self._func._i)) - - @property - @override - def manager(self) -> ZBDDManager: - return ZBDDManager._from_raw(_lib.oxidd_zbdd_containing_manager(self._func)) - - @override - def cofactors(self) -> tuple[Self, Self] | None: - raw_pair = _lib.oxidd_zbdd_cofactors(self._func) - if raw_pair.first._p == _ffi.NULL: - return None - assert raw_pair.second._p != _ffi.NULL - return ( - self.__class__._from_raw(raw_pair.first), - self.__class__._from_raw(raw_pair.second), - ) - - @override - def cofactor_true(self) -> Self | None: - raw = _lib.oxidd_zbdd_cofactor_true(self._func) - return self.__class__._from_raw(raw) if raw._p != _ffi.NULL else None - - @override - def cofactor_false(self) -> Self | None: - raw = _lib.oxidd_zbdd_cofactor_false(self._func) - return self.__class__._from_raw(raw) if raw._p != _ffi.NULL else None - - @override - def level(self) -> int | None: - val = _lib.oxidd_zbdd_level(self._func) - return val if val != util._LEVEL_NO_MAX else None - - def var_boolean_function(self) -> Self: - """Get the ZBDD Boolean function v for the singleton set {v} - - Acquires the manager's lock for shared access. - """ - return self.__class__._from_raw( - _lib.oxidd_zbdd_var_boolean_function(self._func) - ) - - @override - def __invert__(self) -> Self: - return self.__class__._from_raw(_lib.oxidd_zbdd_not(self._func)) - - @override - def __and__(self, rhs: Self) -> Self: - assert ( - self._func._p == rhs._func._p - ), "`self` and `rhs` must belong to the same manager" - return self.__class__._from_raw(_lib.oxidd_zbdd_and(self._func, rhs._func)) - - @override - def __or__(self, rhs: Self) -> Self: - assert ( - self._func._p == rhs._func._p - ), "`self` and `rhs` must belong to the same manager" - return self.__class__._from_raw(_lib.oxidd_zbdd_or(self._func, rhs._func)) - - @override - def __xor__(self, rhs: Self) -> Self: - assert ( - self._func._p == rhs._func._p - ), "`self` and `rhs` must belong to the same manager" - return self.__class__._from_raw(_lib.oxidd_zbdd_xor(self._func, rhs._func)) - - def __sub__(self, rhs: Self) -> Self: - """Compute the ZBDD for the set difference ``self ∖ rhs`` - - This is equivalent to the strict implication ``rhs < lhs`` on Boolean - functions. - - ``self`` and ``rhs`` must belong to the same manager. - - Acquires the manager's lock for shared access. - """ - assert ( - self._func._p == rhs._func._p - ), "`self` and `rhs` must belong to the same manager" - return self.__class__._from_raw(_lib.oxidd_zbdd_diff(self._func, rhs._func)) - - @override - def nand(self, rhs: Self) -> Self: - assert ( - self._func._p == rhs._func._p - ), "`self` and `rhs` must belong to the same manager" - return self.__class__._from_raw(_lib.oxidd_zbdd_nand(self._func, rhs._func)) - - @override - def nor(self, rhs: Self) -> Self: - assert ( - self._func._p == rhs._func._p - ), "`self` and `rhs` must belong to the same manager" - return self.__class__._from_raw(_lib.oxidd_zbdd_nor(self._func, rhs._func)) - - @override - def equiv(self, rhs: Self) -> Self: - assert ( - self._func._p == rhs._func._p - ), "`self` and `rhs` must belong to the same manager" - return self.__class__._from_raw(_lib.oxidd_zbdd_equiv(self._func, rhs._func)) - - @override - def imp(self, rhs: Self) -> Self: - assert ( - self._func._p == rhs._func._p - ), "`self` and `rhs` must belong to the same manager" - return self.__class__._from_raw(_lib.oxidd_zbdd_imp(self._func, rhs._func)) - - @override - def imp_strict(self, rhs: Self) -> Self: - assert ( - self._func._p == rhs._func._p - ), "`self` and `rhs` must belong to the same manager" - return self.__class__._from_raw( - _lib.oxidd_zbdd_imp_strict(self._func, rhs._func) - ) - - @override - def ite(self, t: Self, e: Self) -> Self: - assert ( - self._func._p == t._func._p == e._func._p - ), "`self` and `t` and `e` must belong to the same manager" - return self.__class__._from_raw( - _lib.oxidd_zbdd_ite(self._func, t._func, e._func) - ) - - def make_node(self, hi: Self, lo: Self) -> Self: - """Create a new ZBDD node at the level of `this` with the given `hi` and - `lo` edges - - `var` must be a singleton set. - - Acquires the manager's lock for shared access. - """ - assert ( - self._func._p == hi._func._p == lo._func._p - ), "`self` and `hi` and `lo` must belong to the same manager" - # `oxidd_zbdd_make_node()` takes ownership of `hi` and `lo`, but we - # cannot give up ownership in Python, so we need to increment their - # reference counts. - _lib.oxidd_zbdd_ref(hi._func) - _lib.oxidd_zbdd_ref(lo._func) - return self.__class__._from_raw( - _lib.oxidd_zbdd_make_node(self._func, hi._func, lo._func) - ) - - @override - def node_count(self) -> int: - return int(_lib.oxidd_zbdd_node_count(self._func)) - - @override - def satisfiable(self) -> bool: - return bool(_lib.oxidd_zbdd_satisfiable(self._func)) - - @override - def valid(self) -> bool: - return bool(_lib.oxidd_zbdd_valid(self._func)) - - @override - def sat_count_float(self, vars: int) -> float: - return float(_lib.oxidd_zbdd_sat_count_double(self._func, vars)) - - @override - def pick_cube(self) -> util.Assignment | None: - raw = _lib.oxidd_zbdd_pick_cube(self._func) - return util.Assignment._from_raw(raw) if raw.len > 0 else None - - @override - def pick_cube_dd(self) -> Self: - return self.__class__._from_raw(_lib.oxidd_zbdd_pick_cube_dd(self._func)) - - @override - def pick_cube_dd_set(self, literal_set: Self) -> Self: - assert ( - self._func._p == literal_set._func._p - ), "`self` and `literal_set` must belong to the same manager" - return self.__class__._from_raw( - _lib.oxidd_zbdd_pick_cube_dd_set(self._func, literal_set._func) - ) - - @override - def eval(self, args: collections.abc.Collection[tuple[Self, bool]]) -> bool: - n = len(args) - c_args = util._alloc("oxidd_zbdd_bool_pair_t[]", n) - for c_arg, (f, v) in zip(c_args, args): - c_arg.func = f._func - c_arg.val = v - - return bool(_lib.oxidd_zbdd_eval(self._func, c_args, n)) +from ._oxidd import ZBDDFunction, ZBDDManager diff --git a/crates/oxidd-core/src/function.rs b/crates/oxidd-core/src/function.rs index e98e094..359cd03 100644 --- a/crates/oxidd-core/src/function.rs +++ b/crates/oxidd-core/src/function.rs @@ -782,13 +782,19 @@ pub trait BooleanFunction: Function { /// Evaluate this Boolean function /// - /// `args` determines the valuation for all variables. Missing values are - /// assumed to be false. However, note that the arguments may also determine - /// the domain, e.g., in case of ZBDDs. If values are specified multiple - /// times, the last one counts. Panics if any function in `args` refers to a - /// terminal node. + /// `args` consists of pairs `(variable, value)` and determines the + /// valuation for all variables. Missing values are assumed to be false. + /// However, note that the arguments may also determine the domain, + /// e.g., in case of ZBDDs. If values are specified multiple times, the + /// last one counts. + /// + /// Note that all variables in `args` must be handles for the respective + /// decision diagram levels, i.e., the Boolean function representing the + /// variable in case of B(C)DDs, and a singleton set for ZBDDs. /// /// Locking behavior: acquires the manager's lock for shared access. + /// + /// Panics if any function in `args` refers to a terminal node. fn eval<'a>(&'a self, args: impl IntoIterator) -> bool { self.with_manager_shared(|manager, edge| { Self::eval_edge( @@ -905,7 +911,7 @@ pub trait BooleanFunctionQuant: BooleanFunction { /// `vars` is a set of variables, which in turn is just the conjunction of /// the variables. This operation removes all occurrences of the variables /// by universal quantification. Universal quantification `∀x. f(…, x, …)` - /// of a boolean function `f(…, x, …)` over a single variable `x` is + /// of a Boolean function `f(…, x, …)` over a single variable `x` is /// `f(…, 0, …) ∧ f(…, 1, …)`. /// /// Locking behavior: acquires the manager's lock for shared access. @@ -923,7 +929,7 @@ pub trait BooleanFunctionQuant: BooleanFunction { /// `vars` is a set of variables, which in turn is just the conjunction of /// the variables. This operation removes all occurrences of the variables /// by existential quantification. Existential quantification - /// `∃x. f(…, x, …)` of a boolean function `f(…, x, …)` over a single + /// `∃x. f(…, x, …)` of a Boolean function `f(…, x, …)` over a single /// variable `x` is `f(…, 0, …) ∨ f(…, 1, …)`. /// /// Locking behavior: acquires the manager's lock for shared access. @@ -941,7 +947,7 @@ pub trait BooleanFunctionQuant: BooleanFunction { /// `vars` is a set of variables, which in turn is just the conjunction of /// the variables. This operation removes all occurrences of the variables /// by unique quantification. Unique quantification `∃!x. f(…, x, …)` of a - /// boolean function `f(…, x, …)` over a single variable `x` is + /// Boolean function `f(…, x, …)` over a single variable `x` is /// `f(…, 0, …) ⊕ f(…, 1, …)`. /// /// Unique quantification is also known as the diff --git a/crates/oxidd-ffi-python/Cargo.toml b/crates/oxidd-ffi-python/Cargo.toml new file mode 100644 index 0000000..3ff559b --- /dev/null +++ b/crates/oxidd-ffi-python/Cargo.toml @@ -0,0 +1,62 @@ +[package] +name = "oxidd-ffi-python" +version = "0.8.1" +edition = "2021" +description = "Python interface for OxiDD" +readme = "../../bindings/python/README.md" + +authors.workspace = true +license.workspace = true +homepage.workspace = true +repository.workspace = true + +publish = false + + +[lib] +crate-type = ["cdylib"] +name = "_oxidd" +doc = false + +[dependencies] +oxidd-core = { workspace = true } +oxidd-dump = { workspace = true, features = ["dddmp", "dot"] } +oxidd = { workspace = true, features = ["bdd", "bcdd", "zbdd"] } + +pyo3 = { version = "0.22.6", features = ["extension-module", "abi3-py39"] } + +# fast hash function +# +# Note that there is a performance regression with 2.0, see +# https://github.com/rust-lang/rustc-hash/issues/45 +rustc-hash = "1.1" + +[build-dependencies] +proc-macro2 = "1.0.89" +syn = { version = "2.0.87", features = ["full", "parsing", "printing"], default-features = false } +quote = "1.0.37" +anyhow = "1.0" + +[features] +default = ["manager-index", "multi-threading", "apply-cache-direct-mapped"] + +## Use multi-threaded implementations of the apply algorithm +multi-threading = ["oxidd/multi-threading"] + +## Use the index-based manager implementation +## +## This implementation is generally faster than the pointer-based +## implementation, but is more restricted: There is no possibility to reserve +## space for more nodes after the initial allocation and the total number of +## nodes is limited to 2³² nodes for BDDs/ZBDDs, or 2³¹ nodes for BCDDs. +manager-index = ["oxidd/manager-index"] + +## Use the pointer-based manager implementation (suitable for BDDs/ZBDDs with +## more than 2³² nodes, or BCDDs with more than 2³¹ nodes) +## +## If both `manager-index` and `manager-pointer` are specified, the +## pointer-based implementation will be used. +manager-pointer = ["oxidd/manager-pointer"] + +## Enable the direct mapped apply cache +apply-cache-direct-mapped = ["oxidd/apply-cache-direct-mapped"] diff --git a/crates/oxidd-ffi-python/build.rs b/crates/oxidd-ffi-python/build.rs new file mode 100644 index 0000000..cbb9e35 --- /dev/null +++ b/crates/oxidd-ffi-python/build.rs @@ -0,0 +1,89 @@ +use std::fs; +use std::io::{self, Write as _}; + +use anyhow::Result; + +mod stub_gen; + +fn main() -> Result<()> { + let out_path = "../../bindings/python/oxidd/_oxidd.pyi"; + + let mut output = io::BufWriter::new(fs::File::create(out_path)?); + output.write_all( + "\ +from __future__ import annotations + +import enum +from collections.abc import Iterable +from os import PathLike +from typing import final + +from typing_extensions import Never, Self +" + .as_bytes(), + )?; + + let mut env = stub_gen::TypeEnv::new(); + { + let types = [ + "None", + "bool", + "int", + "float", + "str", + "tuple", + "list", + "Never", + "Self", + "PathLike", + "Iterable", + "BooleanOperator", + ]; + for ty in types { + env.register_python_type(ty.to_string())?; + } + + let handle = env.register_python_type("MemoryError".into())?; + env.register_rust_type("PyMemoryError", handle)?; + } + + let mut writer = stub_gen::StubGen::new(env); + writer.process_files(["src/bdd.rs", "src/bcdd.rs", "src/zbdd.rs", "src/util.rs"])?; + writer.write(&mut output)?; + output.write_all( + " +class BooleanOperator(enum.Enum): + \"\"\"Binary operators on Boolean functions.\"\"\" + + AND = ... + \"\"\"Conjunction ``lhs ∧ rhs``\"\"\" + OR = ... + \"\"\"Disjunction ``lhs ∨ rhs``\"\"\" + XOR = ... + \"\"\"Exclusive disjunction ``lhs ⊕ rhs``\"\"\" + EQUIV = ... + \"\"\"Equivalence ``lhs ↔ rhs``\"\"\" + NAND = ... + \"\"\"Negated conjunction ``lhs ⊼ rhs``\"\"\" + NOR = ... + \"\"\"Negated disjunction ``lhs ⊽ rhs``\"\"\" + IMP = ... + \"\"\"Implication ``lhs → rhs`` (or `lhs ≤ rhs)`\"\"\" + IMP_STRICT = ... + \"\"\"Strict implication ``lhs < rhs``\"\"\" +" + .as_bytes(), + )?; + drop(output); + + // Format the resulting .pyi file using Ruff (if Ruff is installed) + if let Ok(mut process) = std::process::Command::new("ruff") + .arg("format") + .arg(out_path) + .spawn() + { + process.wait().ok(); + } + + Ok(()) +} diff --git a/crates/oxidd-ffi-python/src/bcdd.rs b/crates/oxidd-ffi-python/src/bcdd.rs new file mode 100644 index 0000000..928326e --- /dev/null +++ b/crates/oxidd-ffi-python/src/bcdd.rs @@ -0,0 +1,801 @@ +//! Binary decision diagrams with complement edges (BCDDs) + +use std::hash::BuildHasherDefault; +use std::path::PathBuf; + +use pyo3::prelude::*; +use pyo3::types::{PyList, PyTuple, PyType}; +use rustc_hash::FxHasher; + +use oxidd::util::{num::F64, AllocResult, OptBool}; +use oxidd::{ + BooleanFunction, BooleanFunctionQuant, Function, FunctionSubst, LevelNo, Manager, ManagerRef, + Subst, +}; + +use crate::util::DDMemoryError; + +/// Manager for binary decision diagrams with complement edges. +/// +/// Implements: :class:`~oxidd.protocols.BooleanFunctionManager`\ +/// [:class:`BCDDFunction`] +#[pyclass(frozen, eq, hash, module = "oxidd.bcdd")] +#[derive(PartialEq, Eq, Hash)] +pub struct BCDDManager(oxidd::bcdd::BCDDManagerRef); + +#[pymethods] +impl BCDDManager { + /// Create a new manager. + /// + /// Args: + /// inner_node_capacity (int): Maximum count of inner nodes + /// apply_cache_capacity (int): Maximum count of apply cache entries + /// threads (int): Worker thread count for the internal thread pool + /// + /// Returns: + /// BCDDManager: The new manager + #[new] + fn new(inner_node_capacity: usize, apply_cache_capacity: usize, threads: u32) -> Self { + Self(oxidd::bcdd::new_manager( + inner_node_capacity, + apply_cache_capacity, + threads, + )) + } + + /// Get a fresh variable, adding a new level to a decision diagram. + /// + /// Acquires the manager's lock for exclusive access. + /// + /// Returns: + /// BCDDFunction: A Boolean function that is true if and only if the + /// variable is true + /// + /// Raises: + /// DDMemoryError: If the operation runs out of memory + fn new_var(&self) -> PyResult { + self.0 + .with_manager_exclusive(|manager| oxidd::bcdd::BCDDFunction::new_var(manager)) + .try_into() + } + + /// Get the constant true Boolean function ``⊤``. + /// + /// Locking behavior: acquires the manager's lock for shared access. + /// + /// Returns: + /// BCDDFunction: The constant true Boolean function ``⊤`` + fn r#true(&self) -> BCDDFunction { + self.0 + .with_manager_shared(|manager| BCDDFunction(oxidd::bcdd::BCDDFunction::t(manager))) + } + + /// Get the constant false Boolean function ``⊥``. + /// + /// Locking behavior: acquires the manager's lock for shared access. + /// + /// Returns: + /// BCDDFunction: The constant false Boolean function ``⊥`` + fn r#false(&self) -> BCDDFunction { + self.0 + .with_manager_shared(|manager| BCDDFunction(oxidd::bcdd::BCDDFunction::f(manager))) + } + + /// Get the number of inner nodes. + /// + /// Locking behavior: acquires the manager's lock for shared access. + /// + /// Returns: + /// int: The number of inner nodes stored in this manager + fn num_inner_nodes(&self) -> usize { + self.0 + .with_manager_shared(|manager| manager.num_inner_nodes()) + } + + /// Dump the entire decision diagram in this manager as Graphviz DOT code. + /// + /// The output may also include nodes that are not reachable from + /// ``functions``. + /// + /// Locking behavior: acquires the manager's lock for shared access. + /// + /// Args: + /// path (str | PathLike[str]): Path of the output file. If a file at + /// ``path`` exists, it will be truncated, otherwise a new one will + /// be created. + /// functions (Iterable[tuple[BCDDFunction, str]]): Optional names for + /// BCDD functions + /// variables (Iterable[tuple[BCDDFunction, str]]): Optional names for + /// variables + /// + /// Returns: + /// None + #[pyo3( + signature = (/, path, functions=None, variables=None), + text_signature = "($self, /, path, functions=[], variables=[])" + )] + fn dump_all_dot_file<'py>( + &self, + path: PathBuf, + functions: Option<&Bound<'py, PyAny>>, + variables: Option<&Bound<'py, PyAny>>, + ) -> PyResult<()> { + let collect = + crate::util::collect_func_str_pairs::; + let functions = collect(functions)?; + let variables = collect(variables)?; + + let file = std::fs::File::create(path)?; + + self.0.with_manager_shared(|manager| { + oxidd_dump::dot::dump_all( + file, + manager, + variables.iter().map(|(v, s)| (v, s.to_string_lossy())), + functions.iter().map(|(f, s)| (f, s.to_string_lossy())), + ) + })?; + + Ok(()) + } +} + +/// Substitution mapping variables to replacement functions. +/// +/// Implements: :class:`~oxidd.protocols.FunctionSubst` +#[pyclass(frozen, module = "oxidd.bcdd")] +pub struct BCDDSubstitution(Subst>); + +#[pymethods] +impl BCDDSubstitution { + /// Create a new substitution object for BCDDs. + /// + /// See :meth:`BCDDFunction.make_substitution` fore more details. + /// + /// Args: + /// pairs (Iterable[tuple[BCDDFunction, BCDDFunction]]): + /// ``(variable, replacement)`` pairs, where all variables are + /// distinct. The order of the pairs is irrelevant. + /// + /// Returns: + /// BCDDSubstitution: The new substitution + #[new] + fn new(pairs: &Bound) -> PyResult { + let len = pairs.len().unwrap_or(0); + let mut vars = Vec::with_capacity(len); + let mut replacements = Vec::with_capacity(len); + for pair in pairs.iter()? { + let pair: Bound = pair?.downcast_into()?; + let v = pair.get_borrowed_item(0)?; + let r = pair.get_borrowed_item(1)?; + vars.push(v.downcast::()?.get().0.clone()); + replacements.push(r.downcast::()?.get().0.clone()); + } + + Ok(Self(Subst::new(vars, replacements))) + } +} + +/// Boolean function as binary decision diagram with complement edges (BCDD). +/// +/// Implements: +/// :class:`~oxidd.protocols.BooleanFunctionQuant`, +/// :class:`~oxidd.protocols.FunctionSubst`\ [:class:`BCDDSubstitution`], +/// :class:`~oxidd.protocols.HasLevel` +/// +/// All operations constructing BCDDs may throw a +/// :exc:`~oxidd.util.DDMemoryError` in case they run out of memory. +/// +/// Note that comparisons like ``f <= g`` are based on an arbitrary total order +/// and not related to logical implications. See the +/// :meth:`Function ` protocol for more +/// details. +#[pyclass(frozen, eq, ord, hash, module = "oxidd.bcdd")] +#[derive(PartialEq, Eq, PartialOrd, Ord, Hash)] +pub struct BCDDFunction(oxidd::bcdd::BCDDFunction); + +impl TryFrom> for BCDDFunction { + type Error = PyErr; + + fn try_from(value: AllocResult) -> Result { + match value { + Ok(f) => Ok(Self(f)), + Err(_) => Err(DDMemoryError::new_err( + "OxiDD BCDD operation ran out of memory", + )), + } + } +} + +impl AsRef for BCDDFunction { + fn as_ref(&self) -> &oxidd::bcdd::BCDDFunction { + &self.0 + } +} + +#[pymethods] +impl BCDDFunction { + /// BCDDManager: The associated manager. + #[getter] + fn manager(&self) -> BCDDManager { + BCDDManager(self.0.manager_ref()) + } + + /// Get the cofactors ``(f_true, f_false)`` of ``self``. + /// + /// Let f(x₀, …, xₙ) be represented by ``self``, where x₀ is (currently) the + /// top-most variable. Then f\ :sub:`true`\ (x₁, …, xₙ) = f(⊤, x₁, …, xₙ) + /// and f\ :sub:`false`\ (x₁, …, xₙ) = f(⊥, x₁, …, xₙ). + /// + /// Structurally, the cofactors are simply the children in case with edge + /// tags adjusted accordingly. + /// + /// Locking behavior: acquires the manager's lock for shared access. + /// + /// Time complexity: O(1) + /// + /// Returns: + /// tuple[Self, Self] | None: The cofactors ``(f_true, f_false)``, or + /// ``None`` if ``self`` references a terminal node. + /// + /// See Also: + /// :meth:`cofactor_true`, :meth:`cofactor_false` if you only need one + /// of the cofactors. + fn cofactors(&self, py: Python) -> PyObject { + match self.0.cofactors() { + Some((ct, cf)) => { + let ct = Self(ct).into_py(py); + let cf = Self(cf).into_py(py); + PyTuple::new_bound(py, [ct, cf]).into_py(py) + } + None => ().into_py(py), + } + } + + /// Get the cofactor ``f_true`` of ``self``. + /// + /// Locking behavior: acquires the manager's lock for shared access. + /// + /// Time complexity: O(1) + /// + /// Returns: + /// Self | None: The cofactor ``f_true``, or ``None`` if ``self`` + /// references a terminal node. + /// + /// See Also: + /// :meth:`cofactors`, also for a more detailed description + fn cofactor_true(&self) -> Option { + Some(Self(self.0.cofactor_true()?)) + } + /// Get the cofactor ``f_false`` of ``self``. + /// + /// Locking behavior: acquires the manager's lock for shared access. + /// + /// Time complexity: O(1) + /// + /// Returns: + /// Self | None: The cofactor ``f_false``, or ``None`` if ``self`` + /// references a terminal node. + /// + /// See Also: + /// :meth:`cofactors`, also for a more detailed description + fn cofactor_false(&self) -> Option { + Some(Self(self.0.cofactor_false()?)) + } + + /// Get the level of the underlying node. + /// + /// Locking behavior: acquires the manager's lock for shared access. + /// + /// Time complexity: O(1) + /// + /// Returns: + /// int | None: The level, or ``None`` if the node is a terminal + fn level(&self) -> Option { + match self + .0 + .with_manager_shared(|manager, edge| manager.get_node(edge).level()) + { + LevelNo::MAX => None, + l => Some(l), + } + } + + /// Compute the negation ``¬self``. + /// + /// Locking behavior: acquires the manager's lock for shared access. + /// + /// Time complexity: O(1) + /// + /// Returns: + /// Self: ``¬self`` + /// + /// Raises: + /// DDMemoryError: If the operation runs out of memory + fn __invert__(&self) -> PyResult { + self.0.not().try_into() + } + /// Compute the conjunction ``self ∧ rhs``. + /// + /// Locking behavior: acquires the manager's lock for shared access. + /// + /// Args: + /// rhs (Self): Right-hand side operand. Must belong to the same manager + /// as ``self`` + /// + /// Returns: + /// Self: ``self ∧ rhs`` + /// + /// Raises: + /// DDMemoryError: If the operation runs out of memory + fn __and__(&self, py: Python, rhs: &Self) -> PyResult { + py.allow_threads(move || self.0.and(&rhs.0)).try_into() + } + /// Compute the disjunction ``self ∨ rhs``. + /// + /// Locking behavior: acquires the manager's lock for shared access. + /// + /// Args: + /// rhs (Self): Right-hand side operand. Must belong to the same manager + /// as ``self`` + /// + /// Returns: + /// Self: ``self ∨ rhs`` + /// + /// Raises: + /// DDMemoryError: If the operation runs out of memory + fn __or__(&self, py: Python, rhs: &Self) -> PyResult { + py.allow_threads(move || self.0.or(&rhs.0)).try_into() + } + /// Compute the exclusive disjunction ``self ⊕ rhs``. + /// + /// Locking behavior: acquires the manager's lock for shared access. + /// + /// Args: + /// rhs (Self): Right-hand side operand. Must belong to the same manager + /// as ``self`` + /// + /// Returns: + /// Self: ``self ⊕ rhs`` + /// + /// Raises: + /// DDMemoryError: If the operation runs out of memory + fn __xor__(&self, py: Python, rhs: &Self) -> PyResult { + py.allow_threads(move || self.0.xor(&rhs.0)).try_into() + } + /// Compute the negated conjunction ``self ⊼ rhs``. + /// + /// Locking behavior: acquires the manager's lock for shared access. + /// + /// Args: + /// rhs (Self): Right-hand side operand. Must belong to the same manager + /// as ``self`` + /// + /// Returns: + /// Self: ``self ⊼ rhs`` + /// + /// Raises: + /// DDMemoryError: If the operation runs out of memory + #[pyo3(signature = (rhs, /))] + fn nand(&self, py: Python, rhs: &Self) -> PyResult { + py.allow_threads(move || self.0.nand(&rhs.0)).try_into() + } + /// Compute the negated disjunction ``self ⊽ rhs``. + /// + /// Locking behavior: acquires the manager's lock for shared access. + /// + /// Args: + /// rhs (Self): Right-hand side operand. Must belong to the same manager + /// as ``self`` + /// + /// Returns: + /// Self: ``self ⊽ rhs`` + /// + /// Raises: + /// DDMemoryError: If the operation runs out of memory + #[pyo3(signature = (rhs, /))] + fn nor(&self, py: Python, rhs: &Self) -> PyResult { + py.allow_threads(move || self.0.nor(&rhs.0)).try_into() + } + /// Compute the equivalence ``self ↔ rhs``. + /// + /// Locking behavior: acquires the manager's lock for shared access. + /// + /// Args: + /// rhs (Self): Right-hand side operand. Must belong to the same manager + /// as ``self`` + /// + /// Returns: + /// Self: ``self ↔ rhs`` + /// + /// Raises: + /// DDMemoryError: If the operation runs out of memory + #[pyo3(signature = (rhs, /))] + fn equiv(&self, py: Python, rhs: &Self) -> PyResult { + py.allow_threads(move || self.0.equiv(&rhs.0)).try_into() + } + /// Compute the implication ``self → rhs`` (or ``f ≤ g``). + /// + /// Locking behavior: acquires the manager's lock for shared access. + /// + /// Args: + /// rhs (Self): Right-hand side operand. Must belong to the same manager + /// as ``self`` + /// + /// Returns: + /// Self: ``self → rhs`` + /// + /// Raises: + /// DDMemoryError: If the operation runs out of memory + #[pyo3(signature = (rhs, /))] + fn imp(&self, py: Python, rhs: &Self) -> PyResult { + py.allow_threads(move || self.0.imp(&rhs.0)).try_into() + } + /// Compute the strict implication ``self < rhs``. + /// + /// Locking behavior: acquires the manager's lock for shared access. + /// + /// Args: + /// rhs (Self): Right-hand side operand. Must belong to the same manager + /// as ``self`` + /// + /// Returns: + /// Self: ``self < rhs`` + /// + /// Raises: + /// DDMemoryError: If the operation runs out of memory + #[pyo3(signature = (rhs, /))] + fn imp_strict(&self, py: Python, rhs: &Self) -> PyResult { + py.allow_threads(move || self.0.imp_strict(&rhs.0)) + .try_into() + } + + /// Compute the BCDD for the conditional ``t if self else e``. + /// + /// Locking behavior: acquires the manager's lock for shared access. + /// + /// Args: + /// t (Self): Then-case; must belong to the same manager as ``self`` + /// e (Self): Else-case; must belong to the same manager as ``self`` + /// + /// Returns: + /// Self: The Boolean function ``f(v: 𝔹ⁿ) = t(v) if self(v) else e(v)`` + /// + /// Raises: + /// DDMemoryError: If the operation runs out of memory + fn ite(&self, py: Python, t: &Self, e: &Self) -> PyResult { + py.allow_threads(move || self.0.ite(&t.0, &e.0)).try_into() + } + + /// Create a new substitution object from pairs ``(var, replacement)``. + /// + /// The intent behind substitution objects is to optimize the case where the + /// same substitution is applied multiple times. We would like to re-use + /// apply cache entries across these operations, and therefore, we need a + /// compact identifier for the substitution. This identifier is provided by + /// the returned substitution object. + /// + /// Args: + /// pairs (Iterable[tuple[Self, Self]]): ``(variable, replacement)`` + /// pairs, where all variables are distinct. The order of the pairs + /// is irrelevant. + /// + /// Returns: + /// Self: The substitution to be used with :meth:`substitute` + #[classmethod] + #[pyo3(signature = (pairs, /))] + fn make_substitution(_cls: &Bound, pairs: &Bound) -> PyResult { + BCDDSubstitution::new(pairs) + } + + /// Substitute variables in ``self`` according to ``substitution``. + /// + /// The substitution is performed in a parallel fashion, e.g.: + /// ``(¬x ∧ ¬y)[x ↦ ¬x ∧ ¬y, y ↦ ⊥] = ¬(¬x ∧ ¬y) ∧ ¬⊥ = x ∨ y`` + /// + /// Locking behavior: acquires the manager's lock for shared access. + /// + /// Args: + /// substitution (BCDDSubstitution): A substitution object created using + /// :meth:`make_substitution`. All contained DD functions must + /// belong to the same manager as ``self``. + /// + /// Returns: + /// Self: ``self`` with variables substituted + #[pyo3(signature = (substitution, /))] + fn substitute(&self, py: Python, substitution: &BCDDSubstitution) -> PyResult { + py.allow_threads(move || self.0.substitute(&substitution.0)) + .try_into() + } + + /// Compute the universal quantification over ``vars``. + /// + /// This operation removes all occurrences of variables in ``vars`` by + /// universal quantification. Universal quantification ∀x. f(…, x, …) of a + /// Boolean function f(…, x, …) over a single variable x is + /// f(…, 0, …) ∧ f(…, 1, …). + /// + /// Locking behavior: acquires the manager's lock for shared access. + /// + /// Args: + /// vars (Self): Set of variables represented as conjunction thereof. + /// Must belong to the same manager as ``self``. + /// + /// Returns: + /// Self: ∀ vars: self + /// + /// Raises: + /// DDMemoryError: If the operation runs out of memory + fn forall(&self, py: Python, vars: &Self) -> PyResult { + py.allow_threads(move || self.0.forall(&vars.0)).try_into() + } + /// Compute the existential quantification over ``vars``. + /// + /// This operation removes all occurrences of variables in ``vars`` by + /// existential quantification. Existential quantification ∃x. f(…, x, …) of + /// a Boolean function f(…, x, …) over a single variable x is + /// f(…, 0, …) ∨ f(…, 1, …). + /// + /// Locking behavior: acquires the manager's lock for shared access. + /// + /// Args: + /// vars (Self): Set of variables represented as conjunction thereof. + /// Must belong to the same manager as ``self``. + /// + /// Returns: + /// Self: ∃ vars: self + /// + /// Raises: + /// DDMemoryError: If the operation runs out of memory + fn exist(&self, py: Python, vars: &Self) -> PyResult { + py.allow_threads(move || self.0.exist(&vars.0)).try_into() + } + /// Compute the unique quantification over ``vars``. + /// + /// This operation removes all occurrences of variables in ``vars`` by + /// unique quantification. Unique quantification ∃!x. f(…, x, …) of a + /// Boolean function f(…, x, …) over a single variable x is + /// f(…, 0, …) ⊕ f(…, 1, …). Unique quantification is also known as the + /// `Boolean difference `_ or + /// `Boolean derivative `_. + /// + /// Locking behavior: acquires the manager's lock for shared access. + /// + /// Args: + /// vars (Self): Set of variables represented as conjunction thereof. + /// Must belong to the same manager as ``self``. + /// + /// Returns: + /// Self: ∃! vars: self + /// + /// Raises: + /// DDMemoryError: If the operation runs out of memory + fn unique(&self, py: Python, vars: &Self) -> PyResult { + py.allow_threads(move || self.0.unique(&vars.0)).try_into() + } + + /// Combined application of ``op`` and :meth:`forall()`. + /// + /// Locking behavior: acquires the manager's lock for shared access. + /// + /// Args: + /// op (BooleanOperator): Binary Boolean operator to apply to ``self`` + /// and ``rhs`` + /// rhs (Self): Right-hand side of the operator. Must belong to the same + /// manager as ``self``. + /// vars (Self): Set of variables to quantify over. Represented as + /// conjunction of variables. Must belong to the same manager as + /// ``self``. + /// + /// Returns: + /// Self: ``∀ vars. self  rhs`` + /// + /// Raises: + /// DDMemoryError: If the operation runs out of memory + fn apply_forall( + &self, + py: Python, + op: &Bound, + rhs: &Self, + vars: &Self, + ) -> PyResult { + let op = crate::util::boolean_operator(op)?; + py.allow_threads(move || self.0.apply_forall(op, &rhs.0, &vars.0)) + .try_into() + } + /// Combined application of ``op`` and :meth:`exist()`. + /// + /// Locking behavior: acquires the manager's lock for shared access. + /// + /// Args: + /// op (BooleanOperator): Binary Boolean operator to apply to ``self`` + /// and ``rhs`` + /// rhs (Self): Right-hand side of the operator. Must belong to the same + /// manager as ``self``. + /// vars (Self): Set of variables to quantify over. Represented as + /// conjunction of variables. Must belong to the same manager as + /// ``self``. + /// + /// Returns: + /// Self: ``∃ vars. self  rhs`` + /// + /// Raises: + /// DDMemoryError: If the operation runs out of memory + fn apply_exist( + &self, + py: Python, + op: &Bound, + rhs: &Self, + vars: &Self, + ) -> PyResult { + let op = crate::util::boolean_operator(op)?; + py.allow_threads(move || self.0.apply_exist(op, &rhs.0, &vars.0)) + .try_into() + } + /// Combined application of ``op`` and :meth:`unique()`. + /// + /// Locking behavior: acquires the manager's lock for shared access. + /// + /// Args: + /// op (BooleanOperator): Binary Boolean operator to apply to ``self`` + /// and ``rhs`` + /// rhs (Self): Right-hand side of the operator. Must belong to the same + /// manager as ``self``. + /// vars (Self): Set of variables to quantify over. Represented as + /// conjunction of variables. Must belong to the same manager as + /// ``self``. + /// + /// Returns: + /// Self: ``∃! vars. self  rhs`` + /// + /// Raises: + /// DDMemoryError: If the operation runs out of memory + fn apply_unique( + &self, + py: Python, + op: &Bound, + rhs: &Self, + vars: &Self, + ) -> PyResult { + let op = crate::util::boolean_operator(op)?; + py.allow_threads(move || self.0.apply_unique(op, &rhs.0, &vars.0)) + .try_into() + } + + /// Get the number of descendant nodes. + /// + /// Locking behavior: acquires the manager's lock for shared access. + /// + /// Returns: + /// int: The count of descendant nodes including the node referenced by + /// ``self`` and terminal nodes. + fn node_count(&self, py: Python) -> usize { + py.allow_threads(move || self.0.node_count()) + } + + /// Check for satisfiability. + /// + /// Locking behavior: acquires the manager's lock for shared access. + /// + /// Time complexity: O(1) + /// + /// Returns: + /// bool: Whether the Boolean function has at least one satisfying + /// assignment + fn satisfiable(&self) -> bool { + self.0.satisfiable() + } + /// Check for validity. + /// + /// Locking behavior: acquires the manager's lock for shared access. + /// + /// Returns: + /// bool: Whether all assignments satisfy the Boolean function + fn valid(&self) -> bool { + self.0.valid() + } + + /// Count the number of satisfying assignments. + /// + /// Locking behavior: acquires the manager's lock for shared access. + /// + /// Args: + /// vars (int): Assume that the function's domain has this many + /// variables. + /// + /// Returns: + /// float: (An approximation of) the number of satisfying assignments + fn sat_count_float(&self, py: Python, vars: LevelNo) -> f64 { + py.allow_threads(move || { + self.0 + .sat_count::>(vars, &mut Default::default()) + .0 + }) + } + + /// Pick a satisfying assignment. + /// + /// Locking behavior: acquires the manager's lock for shared access. + /// + /// Returns: + /// list[bool | None] | None: The satisfying assignment where the i-th + /// value means that the i-th variable is false, true, or "don't care," + /// respectively, or ``None`` if ``self`` is unsatisfiable + fn pick_cube(&self, py: Python) -> PyObject { + match py.allow_threads(move || self.0.pick_cube([], move |_, _, _| false)) { + Some(r) => PyList::new_bound( + py, + r.into_iter().map(|v| match v { + OptBool::None => ().into_py(py), + _ => (v != OptBool::False).into_py(py), + }), + ) + .into_py(py), + None => ().into_py(py), + } + } + /// Pick a satisfying assignment, represented as decision diagram. + /// + /// Locking behavior: acquires the manager's lock for shared access. + /// + /// Returns: + /// Self: The satisfying assignment as decision diagram, or ``⊥`` if + /// ``self`` is unsatisfiable + fn pick_cube_dd(&self, py: Python) -> PyResult { + py.allow_threads(move || self.0.pick_cube_dd(move |_, _, _| false)) + .try_into() + } + /// Pick a satisfying assignment as DD, with choices as of ``literal_set``. + /// + /// ``literal_set`` is a conjunction of literals. Whenever there is a choice + /// for a variable, it will be set to true if the variable has a positive + /// occurrence in ``literal_set``, and set to false if it occurs negated in + /// ``literal_set``. If the variable does not occur in ``literal_set``, then + /// it will be left as don't care if possible, otherwise an arbitrary (not + /// necessarily random) choice will be performed. + /// + /// Locking behavior: acquires the manager's lock for shared access. + /// + /// Args: + /// literal_set (Self): Conjunction of literals to determine the choice + /// for variables + /// + /// Returns: + /// Self: The satisfying assignment as decision diagram, or ``⊥`` if + /// ``self`` is unsatisfiable + /// + /// Raises: + /// DDMemoryError: If the operation runs out of memory + fn pick_cube_dd_set(&self, py: Python, literal_set: &Self) -> PyResult { + py.allow_threads(move || self.0.pick_cube_dd_set(&literal_set.0)) + .try_into() + } + + /// Evaluate this Boolean function with arguments ``args``. + /// + /// Locking behavior: acquires the manager's lock for shared access. + /// + /// Args: + /// args (Iterable[tuple[Self, bool]]): ``(variable, value)`` pairs. + /// Missing variables are assumed to be false. However, note that + /// the arguments may also determine the domain, e.g., in case of + /// ZBDDs. If variables are given multiple times, the last value + /// counts. Besides that, the order is irrelevant. + /// All variable handles must belong to the same manager as ``self`` + /// and must reference inner nodes. + /// + /// Returns: + /// bool: The result of applying the function ``self`` to ``args`` + fn eval(&self, args: &Bound) -> PyResult { + let mut fs = Vec::with_capacity(args.len().unwrap_or(0)); + for pair in args.iter()? { + let pair: Bound = pair?.downcast_into()?; + let f = pair.get_borrowed_item(0)?; + let f = f.downcast::()?.get().0.clone(); + let b = pair.get_borrowed_item(1)?.is_truthy()?; + fs.push((f, b)); + } + + Ok(self.0.eval(fs.iter().map(|(f, b)| (f, *b)))) + } +} diff --git a/crates/oxidd-ffi-python/src/bdd.rs b/crates/oxidd-ffi-python/src/bdd.rs new file mode 100644 index 0000000..7cb0590 --- /dev/null +++ b/crates/oxidd-ffi-python/src/bdd.rs @@ -0,0 +1,799 @@ +//! Binary decision diagrams (BDDs, without complement edges) + +use std::hash::BuildHasherDefault; +use std::path::PathBuf; + +use pyo3::prelude::*; +use pyo3::types::{PyList, PyTuple, PyType}; +use rustc_hash::FxHasher; + +use oxidd::util::{num::F64, AllocResult, OptBool}; +use oxidd::{ + BooleanFunction, BooleanFunctionQuant, Function, FunctionSubst, LevelNo, Manager, ManagerRef, + Subst, +}; + +use crate::util::DDMemoryError; + +/// Manager for binary decision diagrams (without complement edges). +/// +/// Implements: :class:`~oxidd.protocols.BooleanFunctionManager`\ +/// [:class:`BDDFunction`] +#[pyclass(frozen, eq, hash, module = "oxidd.bdd")] +#[derive(PartialEq, Eq, Hash)] +pub struct BDDManager(oxidd::bdd::BDDManagerRef); + +#[pymethods] +impl BDDManager { + /// Create a new manager. + /// + /// Args: + /// inner_node_capacity (int): Maximum count of inner nodes + /// apply_cache_capacity (int): Maximum count of apply cache entries + /// threads (int): Worker thread count for the internal thread pool + /// + /// Returns: + /// BDDManager: The new manager + #[new] + fn new(inner_node_capacity: usize, apply_cache_capacity: usize, threads: u32) -> Self { + Self(oxidd::bdd::new_manager( + inner_node_capacity, + apply_cache_capacity, + threads, + )) + } + + /// Get a fresh variable, adding a new level to a decision diagram. + /// + /// Acquires the manager's lock for exclusive access. + /// + /// Returns: + /// BDDFunction: A Boolean function that is true if and only if the + /// variable is true + /// Raises: + /// DDMemoryError: If the operation runs out of memory + fn new_var(&self) -> PyResult { + self.0 + .with_manager_exclusive(|manager| oxidd::bdd::BDDFunction::new_var(manager)) + .try_into() + } + + /// Get the constant true Boolean function ``⊤``. + /// + /// Locking behavior: acquires the manager's lock for shared access. + /// + /// Returns: + /// BDDFunction: The constant true Boolean function ``⊤`` + fn r#true(&self) -> BDDFunction { + self.0 + .with_manager_shared(|manager| BDDFunction(oxidd::bdd::BDDFunction::t(manager))) + } + + /// Get the constant false Boolean function ``⊥``. + /// + /// Locking behavior: acquires the manager's lock for shared access. + /// + /// Returns: + /// BDDFunction: The constant false Boolean function ``⊥`` + fn r#false(&self) -> BDDFunction { + self.0 + .with_manager_shared(|manager| BDDFunction(oxidd::bdd::BDDFunction::f(manager))) + } + + /// Get the number of inner nodes. + /// + /// Locking behavior: acquires the manager's lock for shared access. + /// + /// Returns: + /// int: The number of inner nodes stored in this manager + fn num_inner_nodes(&self) -> usize { + self.0 + .with_manager_shared(|manager| manager.num_inner_nodes()) + } + + /// Dump the entire decision diagram in this manager as Graphviz DOT code. + /// + /// The output may also include nodes that are not reachable from + /// ``functions``. + /// + /// Locking behavior: acquires the manager's lock for shared access. + /// + /// Args: + /// path (str | PathLike[str]): Path of the output file. If a file at + /// ``path`` exists, it will be truncated, otherwise a new one will + /// be created. + /// functions (Iterable[tuple[BDDFunction, str]]): Optional names for + /// BDD functions + /// variables (Iterable[tuple[BDDFunction, str]]): Optional names for + /// variables + /// + /// Returns: + /// None + #[pyo3( + signature = (/, path, functions=None, variables=None), + text_signature = "($self, /, path, functions=[], variables=[])" + )] + fn dump_all_dot_file<'py>( + &self, + path: PathBuf, + functions: Option<&Bound<'py, PyAny>>, + variables: Option<&Bound<'py, PyAny>>, + ) -> PyResult<()> { + let collect = crate::util::collect_func_str_pairs::; + let functions = collect(functions)?; + let variables = collect(variables)?; + + let file = std::fs::File::create(path)?; + + self.0.with_manager_shared(|manager| { + oxidd_dump::dot::dump_all( + file, + manager, + variables.iter().map(|(v, s)| (v, s.to_string_lossy())), + functions.iter().map(|(f, s)| (f, s.to_string_lossy())), + ) + })?; + + Ok(()) + } +} + +/// Substitution mapping variables to replacement functions. +/// +/// Implements: :class:`~oxidd.protocols.FunctionSubst` +#[pyclass(frozen, module = "oxidd.bdd")] +pub struct BDDSubstitution(Subst>); + +#[pymethods] +impl BDDSubstitution { + /// Create a new substitution object for BDDs. + /// + /// See :meth:`BDDFunction.make_substitution` fore more details. + /// + /// Args: + /// pairs (Iterable[tuple[BDDFunction, BDDFunction]]): + /// ``(variable, replacement)`` pairs, where all variables are + /// distinct. The order of the pairs is irrelevant. + /// + /// Returns: + /// BDDSubstitution: The new substitution + #[new] + fn new(pairs: &Bound) -> PyResult { + let len = pairs.len().unwrap_or(0); + let mut vars = Vec::with_capacity(len); + let mut replacements = Vec::with_capacity(len); + for pair in pairs.iter()? { + let pair: Bound = pair?.downcast_into()?; + let v = pair.get_borrowed_item(0)?; + let r = pair.get_borrowed_item(1)?; + vars.push(v.downcast::()?.get().0.clone()); + replacements.push(r.downcast::()?.get().0.clone()); + } + + Ok(Self(Subst::new(vars, replacements))) + } +} + +/// Boolean function represented as a simple binary decision diagram (BDD). +/// +/// Implements: +/// :class:`~oxidd.protocols.BooleanFunctionQuant`, +/// :class:`~oxidd.protocols.FunctionSubst`\ [:class:`BDDSubstitution`], +/// :class:`~oxidd.protocols.HasLevel` +/// +/// All operations constructing BDDs may throw a +/// :exc:`~oxidd.util.DDMemoryError` in case they run out of memory. +/// +/// Note that comparisons like ``f <= g`` are based on an arbitrary total order +/// and not related to logical implications. See the +/// :meth:`Function ` protocol for more +/// details. +#[pyclass(frozen, eq, ord, hash, module = "oxidd.bdd")] +#[derive(PartialEq, Eq, PartialOrd, Ord, Hash)] +pub struct BDDFunction(oxidd::bdd::BDDFunction); + +impl TryFrom> for BDDFunction { + type Error = PyErr; + + fn try_from(value: AllocResult) -> Result { + match value { + Ok(f) => Ok(Self(f)), + Err(_) => Err(DDMemoryError::new_err( + "OxiDD BDD operation ran out of memory", + )), + } + } +} + +impl AsRef for BDDFunction { + fn as_ref(&self) -> &oxidd::bdd::BDDFunction { + &self.0 + } +} + +#[pymethods] +impl BDDFunction { + /// BDDManager: The associated manager. + #[getter] + fn manager(&self) -> BDDManager { + BDDManager(self.0.manager_ref()) + } + + /// Get the cofactors ``(f_true, f_false)`` of ``self``. + /// + /// Let f(x₀, …, xₙ) be represented by ``self``, where x₀ is (currently) the + /// top-most variable. Then f\ :sub:`true`\ (x₁, …, xₙ) = f(⊤, x₁, …, xₙ) + /// and f\ :sub:`false`\ (x₁, …, xₙ) = f(⊥, x₁, …, xₙ). + /// + /// Structurally, the cofactors are simply the children in case with edge + /// tags adjusted accordingly. + /// + /// Locking behavior: acquires the manager's lock for shared access. + /// + /// Time complexity: O(1) + /// + /// Returns: + /// tuple[Self, Self] | None: The cofactors ``(f_true, f_false)``, or + /// ``None`` if ``self`` references a terminal node. + /// + /// See Also: + /// :meth:`cofactor_true`, :meth:`cofactor_false` if you only need one + /// of the cofactors. + fn cofactors(&self, py: Python) -> PyObject { + match self.0.cofactors() { + Some((ct, cf)) => { + let ct = Self(ct).into_py(py); + let cf = Self(cf).into_py(py); + PyTuple::new_bound(py, [ct, cf]).into_py(py) + } + None => ().into_py(py), + } + } + + /// Get the cofactor ``f_true`` of ``self``. + /// + /// Locking behavior: acquires the manager's lock for shared access. + /// + /// Time complexity: O(1) + /// + /// Returns: + /// Self | None: The cofactor ``f_true``, or ``None`` if ``self`` + /// references a terminal node. + /// + /// See Also: + /// :meth:`cofactors`, also for a more detailed description + fn cofactor_true(&self) -> Option { + Some(Self(self.0.cofactor_true()?)) + } + /// Get the cofactor ``f_false`` of ``self``. + /// + /// Locking behavior: acquires the manager's lock for shared access. + /// + /// Time complexity: O(1) + /// + /// Returns: + /// Self | None: The cofactor ``f_false``, or ``None`` if ``self`` + /// references a terminal node. + /// + /// See Also: + /// :meth:`cofactors`, also for a more detailed description + fn cofactor_false(&self) -> Option { + Some(Self(self.0.cofactor_false()?)) + } + + /// Get the level of the underlying node. + /// + /// Locking behavior: acquires the manager's lock for shared access. + /// + /// Time complexity: O(1) + /// + /// Returns: + /// int | None: The level, or ``None`` if the node is a terminal + fn level(&self) -> Option { + match self + .0 + .with_manager_shared(|manager, edge| manager.get_node(edge).level()) + { + LevelNo::MAX => None, + l => Some(l), + } + } + + /// Compute the negation ``¬self``. + /// + /// Locking behavior: acquires the manager's lock for shared access. + /// + /// Time complexity: O(1) + /// + /// Returns: + /// Self: ``¬self`` + /// + /// Raises: + /// DDMemoryError: If the operation runs out of memory + fn __invert__(&self, py: Python) -> PyResult { + py.allow_threads(move || self.0.not()).try_into() + } + /// Compute the conjunction ``self ∧ rhs``. + /// + /// Locking behavior: acquires the manager's lock for shared access. + /// + /// Args: + /// rhs (Self): Right-hand side operand. Must belong to the same manager + /// as ``self`` + /// + /// Returns: + /// Self: ``self ∧ rhs`` + /// + /// Raises: + /// DDMemoryError: If the operation runs out of memory + fn __and__(&self, py: Python, rhs: &Self) -> PyResult { + py.allow_threads(move || self.0.and(&rhs.0)).try_into() + } + /// Compute the disjunction ``self ∨ rhs``. + /// + /// Locking behavior: acquires the manager's lock for shared access. + /// + /// Args: + /// rhs (Self): Right-hand side operand. Must belong to the same manager + /// as ``self`` + /// + /// Returns: + /// Self: ``self ∨ rhs`` + /// + /// Raises: + /// DDMemoryError: If the operation runs out of memory + fn __or__(&self, py: Python, rhs: &Self) -> PyResult { + py.allow_threads(move || self.0.or(&rhs.0)).try_into() + } + /// Compute the exclusive disjunction ``self ⊕ rhs``. + /// + /// Locking behavior: acquires the manager's lock for shared access. + /// + /// Args: + /// rhs (Self): Right-hand side operand. Must belong to the same manager + /// as ``self`` + /// + /// Returns: + /// Self: ``self ⊕ rhs`` + /// + /// Raises: + /// DDMemoryError: If the operation runs out of memory + fn __xor__(&self, py: Python, rhs: &Self) -> PyResult { + py.allow_threads(move || self.0.xor(&rhs.0)).try_into() + } + /// Compute the negated conjunction ``self ⊼ rhs``. + /// + /// Locking behavior: acquires the manager's lock for shared access. + /// + /// Args: + /// rhs (Self): Right-hand side operand. Must belong to the same manager + /// as ``self`` + /// + /// Returns: + /// Self: ``self ⊼ rhs`` + /// + /// Raises: + /// DDMemoryError: If the operation runs out of memory + #[pyo3(signature = (rhs, /))] + fn nand(&self, py: Python, rhs: &Self) -> PyResult { + py.allow_threads(move || self.0.nand(&rhs.0)).try_into() + } + /// Compute the negated disjunction ``self ⊽ rhs``. + /// + /// Locking behavior: acquires the manager's lock for shared access. + /// + /// Args: + /// rhs (Self): Right-hand side operand. Must belong to the same manager + /// as ``self`` + /// + /// Returns: + /// Self: ``self ⊽ rhs`` + /// + /// Raises: + /// DDMemoryError: If the operation runs out of memory + #[pyo3(signature = (rhs, /))] + fn nor(&self, py: Python, rhs: &Self) -> PyResult { + py.allow_threads(move || self.0.nor(&rhs.0)).try_into() + } + /// Compute the equivalence ``self ↔ rhs``. + /// + /// Locking behavior: acquires the manager's lock for shared access. + /// + /// Args: + /// rhs (Self): Right-hand side operand. Must belong to the same manager + /// as ``self`` + /// + /// Returns: + /// Self: ``self ↔ rhs`` + /// + /// Raises: + /// DDMemoryError: If the operation runs out of memory + #[pyo3(signature = (rhs, /))] + fn equiv(&self, py: Python, rhs: &Self) -> PyResult { + py.allow_threads(move || self.0.equiv(&rhs.0)).try_into() + } + /// Compute the implication ``self → rhs`` (or ``f ≤ g``). + /// + /// Locking behavior: acquires the manager's lock for shared access. + /// + /// Args: + /// rhs (Self): Right-hand side operand. Must belong to the same manager + /// as ``self`` + /// + /// Returns: + /// Self: ``self → rhs`` + /// + /// Raises: + /// DDMemoryError: If the operation runs out of memory + #[pyo3(signature = (rhs, /))] + fn imp(&self, py: Python, rhs: &Self) -> PyResult { + py.allow_threads(move || self.0.imp(&rhs.0)).try_into() + } + /// Compute the strict implication ``self < rhs``. + /// + /// Locking behavior: acquires the manager's lock for shared access. + /// + /// Args: + /// rhs (Self): Right-hand side operand. Must belong to the same manager + /// as ``self`` + /// + /// Returns: + /// Self: ``self < rhs`` + /// + /// Raises: + /// DDMemoryError: If the operation runs out of memory + #[pyo3(signature = (rhs, /))] + fn imp_strict(&self, py: Python, rhs: &Self) -> PyResult { + py.allow_threads(move || self.0.imp_strict(&rhs.0)) + .try_into() + } + + /// Compute the BDD for the conditional ``t if self else e``. + /// + /// Locking behavior: acquires the manager's lock for shared access. + /// + /// Args: + /// t (Self): Then-case; must belong to the same manager as ``self`` + /// e (Self): Else-case; must belong to the same manager as ``self`` + /// + /// Returns: + /// Self: The Boolean function ``f(v: 𝔹ⁿ) = t(v) if self(v) else e(v)`` + /// + /// Raises: + /// DDMemoryError: If the operation runs out of memory + fn ite(&self, py: Python, t: &Self, e: &Self) -> PyResult { + py.allow_threads(move || self.0.ite(&t.0, &e.0)).try_into() + } + + /// Create a new substitution object from pairs ``(var, replacement)``. + /// + /// The intent behind substitution objects is to optimize the case where the + /// same substitution is applied multiple times. We would like to re-use + /// apply cache entries across these operations, and therefore, we need a + /// compact identifier for the substitution. This identifier is provided by + /// the returned substitution object. + /// + /// Args: + /// pairs (Iterable[tuple[Self, Self]]): ``(variable, replacement)`` + /// pairs, where all variables are distinct. The order of the pairs + /// is irrelevant. + /// + /// Returns: + /// Self: The substitution to be used with :meth:`substitute` + #[classmethod] + #[pyo3(signature = (pairs, /))] + fn make_substitution(_cls: &Bound, pairs: &Bound) -> PyResult { + BDDSubstitution::new(pairs) + } + + /// Substitute variables in ``self`` according to ``substitution``. + /// + /// The substitution is performed in a parallel fashion, e.g.: + /// ``(¬x ∧ ¬y)[x ↦ ¬x ∧ ¬y, y ↦ ⊥] = ¬(¬x ∧ ¬y) ∧ ¬⊥ = x ∨ y`` + /// + /// Locking behavior: acquires the manager's lock for shared access. + /// + /// Args: + /// substitution (BDDSubstitution): A substitution object created using + /// :meth:`make_substitution`. All contained DD functions must + /// belong to the same manager as ``self``. + /// + /// Returns: + /// Self: ``self`` with variables substituted + #[pyo3(signature = (substitution, /))] + fn substitute(&self, py: Python, substitution: &BDDSubstitution) -> PyResult { + py.allow_threads(move || self.0.substitute(&substitution.0)) + .try_into() + } + + /// Compute the universal quantification over ``vars``. + /// + /// This operation removes all occurrences of variables in ``vars`` by + /// universal quantification. Universal quantification ∀x. f(…, x, …) of a + /// Boolean function f(…, x, …) over a single variable x is + /// f(…, 0, …) ∧ f(…, 1, …). + /// + /// Locking behavior: acquires the manager's lock for shared access. + /// + /// Args: + /// vars (Self): Set of variables represented as conjunction thereof. + /// Must belong to the same manager as ``self``. + /// + /// Returns: + /// Self: ∀ vars: self + /// + /// Raises: + /// DDMemoryError: If the operation runs out of memory + fn forall(&self, py: Python, vars: &Self) -> PyResult { + py.allow_threads(move || self.0.forall(&vars.0)).try_into() + } + /// Compute the existential quantification over ``vars``. + /// + /// This operation removes all occurrences of variables in ``vars`` by + /// existential quantification. Existential quantification ∃x. f(…, x, …) of + /// a Boolean function f(…, x, …) over a single variable x is + /// f(…, 0, …) ∨ f(…, 1, …). + /// + /// Locking behavior: acquires the manager's lock for shared access. + /// + /// Args: + /// vars (Self): Set of variables represented as conjunction thereof. + /// Must belong to the same manager as ``self``. + /// + /// Returns: + /// Self: ∃ vars: self + /// + /// Raises: + /// DDMemoryError: If the operation runs out of memory + fn exist(&self, py: Python, vars: &Self) -> PyResult { + py.allow_threads(move || self.0.exist(&vars.0)).try_into() + } + /// Compute the unique quantification over ``vars``. + /// + /// This operation removes all occurrences of variables in ``vars`` by + /// unique quantification. Unique quantification ∃!x. f(…, x, …) of a + /// Boolean function f(…, x, …) over a single variable x is + /// f(…, 0, …) ⊕ f(…, 1, …). Unique quantification is also known as the + /// `Boolean difference `_ or + /// `Boolean derivative `_. + /// + /// Locking behavior: acquires the manager's lock for shared access. + /// + /// Args: + /// vars (Self): Set of variables represented as conjunction thereof. + /// Must belong to the same manager as ``self``. + /// + /// Returns: + /// Self: ∃! vars: self + /// + /// Raises: + /// DDMemoryError: If the operation runs out of memory + fn unique(&self, py: Python, vars: &Self) -> PyResult { + py.allow_threads(move || self.0.unique(&vars.0)).try_into() + } + + /// Combined application of ``op`` and :meth:`forall()`. + /// + /// Locking behavior: acquires the manager's lock for shared access. + /// + /// Args: + /// op (BooleanOperator): Binary Boolean operator to apply to ``self`` + /// and ``rhs`` + /// rhs (Self): Right-hand side of the operator. Must belong to the same + /// manager as ``self``. + /// vars (Self): Set of variables to quantify over. Represented as + /// conjunction of variables. Must belong to the same manager as + /// ``self``. + /// + /// Returns: + /// Self: ``∀ vars. self  rhs`` + /// + /// Raises: + /// DDMemoryError: If the operation runs out of memory + fn apply_forall( + &self, + py: Python, + op: &Bound, + rhs: &Self, + vars: &Self, + ) -> PyResult { + let op = crate::util::boolean_operator(op)?; + py.allow_threads(move || self.0.apply_forall(op, &rhs.0, &vars.0)) + .try_into() + } + /// Combined application of ``op`` and :meth:`exist()`. + /// + /// Locking behavior: acquires the manager's lock for shared access. + /// + /// Args: + /// op (BooleanOperator): Binary Boolean operator to apply to ``self`` + /// and ``rhs`` + /// rhs (Self): Right-hand side of the operator. Must belong to the same + /// manager as ``self``. + /// vars (Self): Set of variables to quantify over. Represented as + /// conjunction of variables. Must belong to the same manager as + /// ``self``. + /// + /// Returns: + /// Self: ``∃ vars. self  rhs`` + /// + /// Raises: + /// DDMemoryError: If the operation runs out of memory + fn apply_exist( + &self, + py: Python, + op: &Bound, + rhs: &Self, + vars: &Self, + ) -> PyResult { + let op = crate::util::boolean_operator(op)?; + py.allow_threads(move || self.0.apply_exist(op, &rhs.0, &vars.0)) + .try_into() + } + /// Combined application of ``op`` and :meth:`unique()`. + /// + /// Locking behavior: acquires the manager's lock for shared access. + /// + /// Args: + /// op (BooleanOperator): Binary Boolean operator to apply to ``self`` + /// and ``rhs`` + /// rhs (Self): Right-hand side of the operator. Must belong to the same + /// manager as ``self``. + /// vars (Self): Set of variables to quantify over. Represented as + /// conjunction of variables. Must belong to the same manager as + /// ``self``. + /// + /// Returns: + /// Self: ``∃! vars. self  rhs`` + /// + /// Raises: + /// DDMemoryError: If the operation runs out of memory + fn apply_unique( + &self, + py: Python, + op: &Bound, + rhs: &Self, + vars: &Self, + ) -> PyResult { + let op = crate::util::boolean_operator(op)?; + py.allow_threads(move || self.0.apply_unique(op, &rhs.0, &vars.0)) + .try_into() + } + + /// Get the number of descendant nodes. + /// + /// Locking behavior: acquires the manager's lock for shared access. + /// + /// Returns: + /// int: The count of descendant nodes including the node referenced by + /// ``self`` and terminal nodes. + fn node_count(&self, py: Python) -> usize { + py.allow_threads(move || self.0.node_count()) + } + + /// Check for satisfiability. + /// + /// Locking behavior: acquires the manager's lock for shared access. + /// + /// Time complexity: O(1) + /// + /// Returns: + /// bool: Whether the Boolean function has at least one satisfying + /// assignment + fn satisfiable(&self) -> bool { + self.0.satisfiable() + } + /// Check for validity. + /// + /// Locking behavior: acquires the manager's lock for shared access. + /// + /// Returns: + /// bool: Whether all assignments satisfy the Boolean function + fn valid(&self) -> bool { + self.0.valid() + } + + /// Count the number of satisfying assignments. + /// + /// Locking behavior: acquires the manager's lock for shared access. + /// + /// Args: + /// vars (int): Assume that the function's domain has this many + /// variables. + /// + /// Returns: + /// float: (An approximation of) the number of satisfying assignments + fn sat_count_float(&self, py: Python, vars: LevelNo) -> f64 { + py.allow_threads(move || { + self.0 + .sat_count::>(vars, &mut Default::default()) + .0 + }) + } + + /// Pick a satisfying assignment. + /// + /// Locking behavior: acquires the manager's lock for shared access. + /// + /// Returns: + /// list[bool | None] | None: The satisfying assignment where the i-th + /// value means that the i-th variable is false, true, or "don't care," + /// respectively, or ``None`` if ``self`` is unsatisfiable + fn pick_cube(&self, py: Python) -> PyObject { + match py.allow_threads(move || self.0.pick_cube([], move |_, _, _| false)) { + Some(r) => PyList::new_bound( + py, + r.into_iter().map(|v| match v { + OptBool::None => ().into_py(py), + _ => (v != OptBool::False).into_py(py), + }), + ) + .into_py(py), + None => ().into_py(py), + } + } + /// Pick a satisfying assignment, represented as decision diagram. + /// + /// Locking behavior: acquires the manager's lock for shared access. + /// + /// Returns: + /// Self: The satisfying assignment as decision diagram, or ``⊥`` if + /// ``self`` is unsatisfiable + fn pick_cube_dd(&self, py: Python) -> PyResult { + py.allow_threads(move || self.0.pick_cube_dd(move |_, _, _| false)) + .try_into() + } + /// Pick a satisfying assignment as DD, with choices as of ``literal_set``. + /// + /// ``literal_set`` is a conjunction of literals. Whenever there is a choice + /// for a variable, it will be set to true if the variable has a positive + /// occurrence in ``literal_set``, and set to false if it occurs negated in + /// ``literal_set``. If the variable does not occur in ``literal_set``, then + /// it will be left as don't care if possible, otherwise an arbitrary (not + /// necessarily random) choice will be performed. + /// + /// Locking behavior: acquires the manager's lock for shared access. + /// + /// Args: + /// literal_set (Self): Conjunction of literals to determine the choice + /// for variables + /// + /// Returns: + /// Self: The satisfying assignment as decision diagram, or ``⊥`` if + /// ``self`` is unsatisfiable + /// + /// Raises: + /// DDMemoryError: If the operation runs out of memory + fn pick_cube_dd_set(&self, py: Python, literal_set: &Self) -> PyResult { + py.allow_threads(move || self.0.pick_cube_dd_set(&literal_set.0)) + .try_into() + } + + /// Evaluate this Boolean function with arguments ``args``. + /// + /// Locking behavior: acquires the manager's lock for shared access. + /// + /// Args: + /// args (Iterable[tuple[Self, bool]]): ``(variable, value)`` pairs. + /// Missing variables are assumed to be false. However, note that + /// the arguments may also determine the domain, e.g., in case of + /// ZBDDs. If variables are given multiple times, the last value + /// counts. Besides that, the order is irrelevant. + /// All variable handles must belong to the same manager as ``self`` + /// and must reference inner nodes. + /// + /// Returns: + /// bool: The result of applying the function ``self`` to ``args`` + fn eval(&self, args: &Bound) -> PyResult { + let mut fs = Vec::with_capacity(args.len().unwrap_or(0)); + for pair in args.iter()? { + let pair: Bound = pair?.downcast_into()?; + let f = pair.get_borrowed_item(0)?; + let f = f.downcast::()?.get().0.clone(); + let b = pair.get_borrowed_item(1)?.is_truthy()?; + fs.push((f, b)); + } + + Ok(self.0.eval(fs.iter().map(|(f, b)| (f, *b)))) + } +} diff --git a/crates/oxidd-ffi-python/src/lib.rs b/crates/oxidd-ffi-python/src/lib.rs new file mode 100644 index 0000000..6366ec5 --- /dev/null +++ b/crates/oxidd-ffi-python/src/lib.rs @@ -0,0 +1,64 @@ +//! All items of this crate are not intended to be used from other Rust crates +//! but only from Python. Consult the Python API documentation for details on +//! the provided classes. +use pyo3::prelude::*; + +// Docstrings in this crate follow Google Python Style Guide (see +// https://google.github.io/styleguide/pyguide.html and +// https://www.sphinx-doc.org/en/master/usage/extensions/napoleon.html) + +mod bcdd; +mod bdd; +mod zbdd; + +mod util; + +#[pymodule] +mod _oxidd { + use oxidd::BooleanOperator; + use pyo3::prelude::*; + + // bdd + #[pymodule_export] + use crate::bdd::BDDFunction; + #[pymodule_export] + use crate::bdd::BDDManager; + #[pymodule_export] + use crate::bdd::BDDSubstitution; + + // bcdd + #[pymodule_export] + use crate::bcdd::BCDDFunction; + #[pymodule_export] + use crate::bcdd::BCDDManager; + #[pymodule_export] + use crate::bcdd::BCDDSubstitution; + + // zbdd + #[pymodule_export] + use crate::zbdd::ZBDDFunction; + #[pymodule_export] + use crate::zbdd::ZBDDManager; + + // util + #[pymodule_export] + use crate::util::DDMemoryError; + + #[pymodule_init] + fn init(m: &Bound) -> PyResult<()> { + let py = m.py(); + let enum_name = "BooleanOperator"; + let variants = [ + ("AND", BooleanOperator::And as u8), + ("OR", BooleanOperator::Or as u8), + ("XOR", BooleanOperator::Xor as u8), + ("EQUIV", BooleanOperator::Equiv as u8), + ("NAND", BooleanOperator::Nand as u8), + ("NOR", BooleanOperator::Nor as u8), + ("IMP", BooleanOperator::Imp as u8), + ("IMP_STRICT", BooleanOperator::ImpStrict as u8), + ]; + let enum_cls = PyModule::import_bound(py, "enum")?.getattr("Enum")?; + m.add(enum_name, enum_cls.call((enum_name, variants), None)?) + } +} diff --git a/crates/oxidd-ffi-python/src/util.rs b/crates/oxidd-ffi-python/src/util.rs new file mode 100644 index 0000000..5f5b3a2 --- /dev/null +++ b/crates/oxidd-ffi-python/src/util.rs @@ -0,0 +1,59 @@ +//! Primitives and utilities + +use oxidd_core::Countable; +use pyo3::exceptions::PyTypeError; +use pyo3::prelude::*; +use pyo3::pyclass::boolean_struct::True; +use pyo3::types::{PyString, PyTuple}; +use pyo3::PyClass; + +use oxidd::BooleanOperator; + +// pyi: class DDMemoryError(MemoryError): +//d Exception that is raised in case a DD operation runs out of memory +pyo3::create_exception!( + oxidd.util, + DDMemoryError, + pyo3::exceptions::PyMemoryError, + "Exception that is raised in case a DD operation runs out of memory." +); + +pub(crate) fn collect_func_str_pairs<'py, F, PYF>( + pairs: Option<&Bound<'py, PyAny>>, +) -> PyResult)>> +where + F: Clone, + PYF: Sync + PyClass + AsRef, +{ + let mut ps = Vec::new(); + if let Some(pairs) = pairs { + if let Ok(len) = pairs.len() { + ps.reserve(len); + } + for pair in pairs.iter()? { + let pair: Bound = pair?.downcast_into()?; + let f = pair.get_borrowed_item(0)?; + let f = f.downcast::()?.get().as_ref().clone(); + let s: Bound = pair.get_item(1)?.downcast_into()?; + ps.push((f, s)); + } + } + Ok(ps) +} + +pub(crate) fn boolean_operator(obj: &Bound) -> PyResult { + if let Ok(val) = obj.getattr("value") { + if let Ok(val) = val.extract() { + if val <= BooleanOperator::MAX_VALUE { + return Ok(BooleanOperator::from_usize(val)); + } + } + } + Err(match obj.get_type().fully_qualified_name() { + Ok(name) => PyTypeError::new_err(format!( + "Expected an instance of oxidd.util.BooleanOperator, got {}", + name.to_string_lossy() + )), + Err(_) => PyTypeError::new_err("Expected an instance of oxidd.util.BooleanOperator"), + }) +} diff --git a/crates/oxidd-ffi-python/src/zbdd.rs b/crates/oxidd-ffi-python/src/zbdd.rs new file mode 100644 index 0000000..93b8964 --- /dev/null +++ b/crates/oxidd-ffi-python/src/zbdd.rs @@ -0,0 +1,688 @@ +//! Zero-suppressed binary decision diagrams (ZBDDs) + +use std::hash::BuildHasherDefault; +use std::path::PathBuf; + +use pyo3::prelude::*; +use pyo3::types::{PyList, PyTuple}; +use rustc_hash::FxHasher; + +use oxidd::util::{num::F64, AllocResult, OptBool}; +use oxidd::{BooleanFunction, BooleanVecSet, Function, LevelNo, Manager, ManagerRef}; + +use crate::util::DDMemoryError; + +/// Manager for zero-suppressed binary decision diagrams. +/// +/// Implements: :class:`~oxidd.protocols.BooleanFunctionManager`\ +/// [:class`ZBDDFunction`] +#[pyclass(frozen, eq, hash, module = "oxidd.zbdd")] +#[derive(PartialEq, Eq, Hash)] +pub struct ZBDDManager(oxidd::zbdd::ZBDDManagerRef); + +#[pymethods] +impl ZBDDManager { + /// Create a new manager. + /// + /// Args: + /// inner_node_capacity (int): Maximum count of inner nodes + /// apply_cache_capacity (int): Maximum count of apply cache entries + /// threads (int): Worker thread count for the internal thread pool + /// + /// Returns: + /// ZBDDManager: The new manager + #[new] + fn new(inner_node_capacity: usize, apply_cache_capacity: usize, threads: u32) -> Self { + Self(oxidd::zbdd::new_manager( + inner_node_capacity, + apply_cache_capacity, + threads, + )) + } + + /// Get a fresh variable in the form of a singleton set. + /// + /// This adds a new level to a decision diagram. Note that if you interpret + /// Boolean functions with respect to all variables, then the semantics + /// change from f to f'(x₁, …, xₙ, xₙ₊₁) = f(x₁, …, xₙ) ∧ ¬xₙ₊₁. This is + /// different compared to B(C)DDs where we have + /// f'(x₁, …, xₙ, xₙ₊₁) = f(x₁, …, xₙ). + /// + /// Locking behavior: acquires the manager's lock for exclusive access. + /// + /// Returns: + /// ZBDDFunction: The singleton set + /// + /// Raises: + /// DDMemoryError: If the operation runs out of memory + fn new_singleton(&self) -> PyResult { + self.0 + .with_manager_exclusive(|manager| oxidd::zbdd::ZBDDFunction::new_singleton(manager)) + .try_into() + } + + /// Get a fresh variable, adding a new level to a decision diagram. + /// + /// Note that if you interpret Boolean functions with respect to all + /// variables, then adding a level changes the semantics change from + /// f to f'(x₁, …, xₙ, xₙ₊₁) = f(x₁, …, xₙ) ∧ ¬xₙ₊₁. This is different + /// compared to B(C)DDs where we have f'(x₁, …, xₙ, xₙ₊₁) = f(x₁, …, xₙ). + /// + /// Locking behavior: acquires the manager's lock for exclusive access. + /// + /// Returns: + /// ZBDDFunction: A Boolean function that is true if and only if the + /// variable is true + /// + /// Raises: + /// DDMemoryError: If the operation runs out of memory + fn new_var(&self) -> PyResult { + self.0 + .with_manager_exclusive(|manager| oxidd::zbdd::ZBDDFunction::new_var(manager)) + .try_into() + } + + /// Get the ZBDD set ∅. + /// + /// Locking behavior: acquires the manager's lock for shared access. + /// + /// Returns: + /// ZBDDFunction: The set `∅` (or equivalently `⊥`) + fn empty(&self) -> ZBDDFunction { + self.0 + .with_manager_shared(|manager| ZBDDFunction(oxidd::zbdd::ZBDDFunction::empty(manager))) + } + + /// Get the ZBDD set {∅}. + /// + /// Locking behavior: acquires the manager's lock for shared access. + /// + /// Returns: + /// ZBDDFunction: The set `{∅}` + fn base(&self) -> ZBDDFunction { + self.0 + .with_manager_shared(|manager| ZBDDFunction(oxidd::zbdd::ZBDDFunction::base(manager))) + } + + /// Get the constant true Boolean function ``⊤``. + /// + /// Locking behavior: acquires the manager's lock for shared access. + /// + /// Returns: + /// ZBDDFunction: The constant true Boolean function ``⊤`` + fn r#true(&self) -> ZBDDFunction { + self.0 + .with_manager_shared(|manager| ZBDDFunction(oxidd::zbdd::ZBDDFunction::t(manager))) + } + + /// Get the constant false Boolean function ``⊥``. + /// + /// Locking behavior: acquires the manager's lock for shared access. + /// + /// Returns: + /// ZBDDFunction: The constant false Boolean function ``⊥`` + fn r#false(&self) -> ZBDDFunction { + self.empty() + } + + /// Get the number of inner nodes. + /// + /// Locking behavior: acquires the manager's lock for shared access. + /// + /// Returns: + /// int: The number of inner nodes stored in this manager + fn num_inner_nodes(&self) -> usize { + self.0 + .with_manager_shared(|manager| manager.num_inner_nodes()) + } + + /// Dump the entire decision diagram in this manager as Graphviz DOT code. + /// + /// The output may also include nodes that are not reachable from + /// ``functions``. + /// + /// Locking behavior: acquires the manager's lock for shared access. + /// + /// Args: + /// path (str | PathLike[str]): Path of the output file. If a file at + /// ``path`` exists, it will be truncated, otherwise a new one will + /// be created. + /// functions (Iterable[tuple[ZBDDFunction, str]]): Optional names for + /// ZBDD functions + /// variables (Iterable[tuple[ZBDDFunction, str]]): Optional names for + /// variables. The variables must be handles for the respective + /// decision diagram levels, i.e., singleton sets. + /// + /// Returns: + /// None + #[pyo3( + signature = (/, path, functions=None, variables=None), + text_signature = "($self, /, path, functions=[], variables=[])" + )] + fn dump_all_dot_file<'py>( + &self, + path: PathBuf, + functions: Option<&Bound<'py, PyAny>>, + variables: Option<&Bound<'py, PyAny>>, + ) -> PyResult<()> { + let collect = + crate::util::collect_func_str_pairs::; + let functions = collect(functions)?; + let variables = collect(variables)?; + + let file = std::fs::File::create(path)?; + + self.0.with_manager_shared(|manager| { + oxidd_dump::dot::dump_all( + file, + manager, + variables.iter().map(|(v, s)| (v, s.to_string_lossy())), + functions.iter().map(|(f, s)| (f, s.to_string_lossy())), + ) + })?; + + Ok(()) + } +} + +/// Boolean function as zero-suppressed binary decision diagram (ZBDD). +/// +/// Implements: +/// :class:`~oxidd.protocols.BooleanFunction`, +/// :class:`~oxidd.protocols.HasLevel` +/// +/// All operations constructing ZBDDs may throw a +/// :exc:`~oxidd.util.DDMemoryError` in case they run out of memory. +/// +/// Note that comparisons like ``f <= g`` are based on an arbitrary total order +/// and not related to logical implications. See the +/// :meth:`Function ` protocol for more +/// details. +#[pyclass(frozen, eq, ord, hash, module = "oxidd.zbdd")] +#[derive(PartialEq, Eq, PartialOrd, Ord, Hash)] +pub struct ZBDDFunction(oxidd::zbdd::ZBDDFunction); + +impl TryFrom> for ZBDDFunction { + type Error = PyErr; + + fn try_from(value: AllocResult) -> Result { + match value { + Ok(f) => Ok(Self(f)), + Err(_) => Err(DDMemoryError::new_err( + "OxiDD ZBDD operation ran out of memory", + )), + } + } +} + +impl AsRef for ZBDDFunction { + fn as_ref(&self) -> &oxidd::zbdd::ZBDDFunction { + &self.0 + } +} + +#[pymethods] +impl ZBDDFunction { + /// ZBDDManager: The associated manager. + #[getter] + fn manager(&self) -> ZBDDManager { + ZBDDManager(self.0.manager_ref()) + } + + /// Get the cofactors ``(f_true, f_false)`` of ``self``. + /// + /// Let f(x₀, …, xₙ) be represented by ``self``, where x₀ is (currently) the + /// top-most variable. Then f\ :sub:`true`\ (x₁, …, xₙ) = f(⊤, x₁, …, xₙ) + /// and f\ :sub:`false`\ (x₁, …, xₙ) = f(⊥, x₁, …, xₙ). + /// + /// Note that the domain of f is 𝔹\ :sup:`n+1` while the domain of + /// f\ :sub:`true` and f\ :sub:`false` is 𝔹\ :sup:`n`. This is irrelevant in + /// case of BDDs and BCDDs, but not for ZBDDs: For instance, g(x₀) = x₀ and + /// g'(x₀, x₁) = x₀ have the same representation as BDDs or BCDDs, but + /// different representations as ZBDDs. + /// + /// Structurally, the cofactors are simply the children in case with edge + /// tags adjusted accordingly. + /// + /// Locking behavior: acquires the manager's lock for shared access. + /// + /// Time complexity: O(1) + /// + /// Returns: + /// tuple[Self, Self] | None: The cofactors ``(f_true, f_false)``, or + /// ``None`` if ``self`` references a terminal node. + /// + /// See Also: + /// :meth:`cofactor_true`, :meth:`cofactor_false` if you only need one + /// of the cofactors. + fn cofactors(&self, py: Python) -> PyObject { + match self.0.cofactors() { + Some((ct, cf)) => { + let ct = ZBDDFunction(ct).into_py(py); + let cf = ZBDDFunction(cf).into_py(py); + PyTuple::new_bound(py, [ct, cf]).into_py(py) + } + None => ().into_py(py), + } + } + + /// Get the cofactor ``f_true`` of ``self``. + /// + /// Locking behavior: acquires the manager's lock for shared access. + /// + /// Time complexity: O(1) + /// + /// Returns: + /// Self | None: The cofactor ``f_true``, or ``None`` if ``self`` + /// references a terminal node. + /// + /// See Also: + /// :meth:`cofactors`, also for a more detailed description + fn cofactor_true(&self) -> Option { + Some(Self(self.0.cofactor_true()?)) + } + /// Get the cofactor ``f_false`` of ``self``. + /// + /// Locking behavior: acquires the manager's lock for shared access. + /// + /// Time complexity: O(1) + /// + /// Returns: + /// Self | None: The cofactor ``f_false``, or ``None`` if ``self`` + /// references a terminal node. + /// + /// See Also: + /// :meth:`cofactors`, also for a more detailed description + fn cofactor_false(&self) -> Option { + Some(Self(self.0.cofactor_false()?)) + } + + /// Get the level of the underlying node. + /// + /// Locking behavior: acquires the manager's lock for shared access. + /// + /// Time complexity: O(1) + /// + /// Returns: + /// int | None: The level, or ``None`` if the node is a terminal + fn level(&self) -> Option { + match self + .0 + .with_manager_shared(|manager, edge| manager.get_node(edge).level()) + { + LevelNo::MAX => None, + l => Some(l), + } + } + + /// Get the Boolean function v for the singleton set {v}. + /// + /// Locking behavior: acquires the manager's lock for shared access. + /// + /// Returns: + /// Self: The Boolean function `v` as ZBDD + /// + /// Raises: + /// DDMemoryError: If the operation runs out of memory + fn var_boolean_function(&self, py: Python) -> PyResult { + py.allow_threads(move || { + self.0.with_manager_shared(move |manager, singleton| { + let res = oxidd::zbdd::var_boolean_function(manager, singleton)?; + Ok(oxidd::zbdd::ZBDDFunction::from_edge(manager, res)) + }) + }) + .try_into() + } + + /// Compute the negation ``¬self``. + /// + /// Locking behavior: acquires the manager's lock for shared access. + /// + /// Time complexity: O(1) + /// + /// Returns: + /// Self: ``¬self`` + /// + /// Raises: + /// DDMemoryError: If the operation runs out of memory + fn __invert__(&self, py: Python) -> PyResult { + py.allow_threads(move || self.0.not()).try_into() + } + /// Compute the conjunction ``self ∧ rhs``. + /// + /// Locking behavior: acquires the manager's lock for shared access. + /// + /// Args: + /// rhs (Self): Right-hand side operand. Must belong to the same manager + /// as ``self`` + /// + /// Returns: + /// Self: ``self ∧ rhs`` + /// + /// Raises: + /// DDMemoryError: If the operation runs out of memory + fn __and__(&self, py: Python, rhs: &Self) -> PyResult { + py.allow_threads(move || self.0.and(&rhs.0)).try_into() + } + /// Compute the disjunction ``self ∨ rhs``. + /// + /// Locking behavior: acquires the manager's lock for shared access. + /// + /// Args: + /// rhs (Self): Right-hand side operand. Must belong to the same manager + /// as ``self`` + /// + /// Returns: + /// Self: ``self ∨ rhs`` + /// + /// Raises: + /// DDMemoryError: If the operation runs out of memory + fn __or__(&self, py: Python, rhs: &Self) -> PyResult { + py.allow_threads(move || self.0.or(&rhs.0)).try_into() + } + /// Compute the exclusive disjunction ``self ⊕ rhs``. + /// + /// Locking behavior: acquires the manager's lock for shared access. + /// + /// Args: + /// rhs (Self): Right-hand side operand. Must belong to the same manager + /// as ``self`` + /// + /// Returns: + /// Self: ``self ⊕ rhs`` + /// + /// Raises: + /// DDMemoryError: If the operation runs out of memory + fn __xor__(&self, py: Python, rhs: &Self) -> PyResult { + py.allow_threads(move || self.0.xor(&rhs.0)).try_into() + } + /// Compute the set difference ``self ∖ rhs``. + /// + /// Locking behavior: acquires the manager's lock for exclusive access. + /// + /// Args: + /// rhs (Self): Right-hand side operand. Must belong to the same manager + /// as ``self`` + /// + /// Returns: + /// Self: ``self ∖ rhs``, or equivalently ``rhs.strict_imp(self)`` + /// + /// Raises: + /// DDMemoryError: If the operation runs out of memory + fn __sub__(&self, py: Python, rhs: &Self) -> PyResult { + rhs.imp_strict(py, self) + } + /// Compute the negated conjunction ``self ⊼ rhs``. + /// + /// Locking behavior: acquires the manager's lock for shared access. + /// + /// Args: + /// rhs (Self): Right-hand side operand. Must belong to the same manager + /// as ``self`` + /// + /// Returns: + /// Self: ``self ⊼ rhs`` + /// + /// Raises: + /// DDMemoryError: If the operation runs out of memory + #[pyo3(signature = (rhs, /))] + fn nand(&self, py: Python, rhs: &Self) -> PyResult { + py.allow_threads(move || self.0.nand(&rhs.0)).try_into() + } + /// Compute the negated disjunction ``self ⊽ rhs``. + /// + /// Locking behavior: acquires the manager's lock for shared access. + /// + /// Args: + /// rhs (Self): Right-hand side operand. Must belong to the same manager + /// as ``self`` + /// + /// Returns: + /// Self: ``self ⊽ rhs`` + /// + /// Raises: + /// DDMemoryError: If the operation runs out of memory + #[pyo3(signature = (rhs, /))] + fn nor(&self, py: Python, rhs: &Self) -> PyResult { + py.allow_threads(move || self.0.nor(&rhs.0)).try_into() + } + /// Compute the equivalence ``self ↔ rhs``. + /// + /// Locking behavior: acquires the manager's lock for shared access. + /// + /// Args: + /// rhs (Self): Right-hand side operand. Must belong to the same manager + /// as ``self`` + /// + /// Returns: + /// Self: ``self ↔ rhs`` + /// + /// Raises: + /// DDMemoryError: If the operation runs out of memory + #[pyo3(signature = (rhs, /))] + fn equiv(&self, py: Python, rhs: &Self) -> PyResult { + py.allow_threads(move || self.0.equiv(&rhs.0)).try_into() + } + /// Compute the implication ``self → rhs`` (or ``f ≤ g``). + /// + /// Locking behavior: acquires the manager's lock for shared access. + /// + /// Args: + /// rhs (Self): Right-hand side operand. Must belong to the same manager + /// as ``self`` + /// + /// Returns: + /// Self: ``self → rhs`` + /// + /// Raises: + /// DDMemoryError: If the operation runs out of memory + #[pyo3(signature = (rhs, /))] + fn imp(&self, py: Python, rhs: &Self) -> PyResult { + py.allow_threads(move || self.0.imp(&rhs.0)).try_into() + } + /// Compute the strict implication ``self < rhs``. + /// + /// Locking behavior: acquires the manager's lock for shared access. + /// + /// Args: + /// rhs (Self): Right-hand side operand. Must belong to the same manager + /// as ``self`` + /// + /// Returns: + /// Self: ``self < rhs`` + /// + /// Raises: + /// DDMemoryError: If the operation runs out of memory + #[pyo3(signature = (rhs, /))] + fn imp_strict(&self, py: Python, rhs: &Self) -> PyResult { + py.allow_threads(move || self.0.imp_strict(&rhs.0)) + .try_into() + } + + /// Compute the ZBDD for the conditional ``t if self else e``. + /// + /// Locking behavior: acquires the manager's lock for shared access. + /// + /// Args: + /// t (Self): Then-case; must belong to the same manager as ``self`` + /// e (Self): Else-case; must belong to the same manager as ``self`` + /// + /// Returns: + /// Self: The Boolean function ``f(v: 𝔹ⁿ) = t(v) if self(v) else e(v)`` + /// + /// Raises: + /// DDMemoryError: If the operation runs out of memory + fn ite(&self, py: Python, t: &Self, e: &Self) -> PyResult { + py.allow_threads(move || self.0.ite(&t.0, &e.0)).try_into() + } + + /// Create a node at ``self``'s level with edges ``hi`` and ``lo``. + /// + /// ``self`` must be a singleton set at a level above the top level of + /// ``hi`` and ``lo``. + /// + /// Locking behavior: acquires the manager's lock for shared access. + /// + /// Args: + /// hi (Self): Edge for the case where the variable is true; must belong + /// to the same manager as ``self`` + /// lo (Self): Edge for the case where the variable is false; must + /// belong to the same manager as ``self`` + /// + /// Returns: + /// Self: The new ZBDD node + /// + /// Raises: + /// DDMemoryError: If the operation runs out of memory + fn make_node(&self, hi: &Self, lo: &Self) -> PyResult { + self.0 + .with_manager_shared(move |manager, var| { + let hi = hi.0.as_edge(manager); + let lo = lo.0.as_edge(manager); + let hi = manager.clone_edge(hi); + let lo = manager.clone_edge(lo); + let res = oxidd::zbdd::make_node(manager, var, hi, lo)?; + Ok(oxidd::zbdd::ZBDDFunction::from_edge(manager, res)) + }) + .try_into() + } + + /// Get the number of descendant nodes. + /// + /// Locking behavior: acquires the manager's lock for shared access. + /// + /// Returns: + /// int: The count of descendant nodes including the node referenced by + /// ``self`` and terminal nodes. + fn node_count(&self, py: Python) -> usize { + py.allow_threads(move || self.0.node_count()) + } + + /// Check for satisfiability. + /// + /// Locking behavior: acquires the manager's lock for shared access. + /// + /// Time complexity: O(1) + /// + /// Returns: + /// bool: Whether the Boolean function has at least one satisfying + /// assignment + fn satisfiable(&self) -> bool { + self.0.satisfiable() + } + /// Check for validity. + /// + /// Locking behavior: acquires the manager's lock for shared access. + /// + /// Returns: + /// bool: Whether all assignments satisfy the Boolean function + fn valid(&self) -> bool { + self.0.valid() + } + + /// Count the number of satisfying assignments. + /// + /// Locking behavior: acquires the manager's lock for shared access. + /// + /// Args: + /// vars (int): Assume that the function's domain has this many + /// variables. + /// + /// Returns: + /// float: (An approximation of) the number of satisfying assignments + fn sat_count_float(&self, py: Python, vars: LevelNo) -> f64 { + py.allow_threads(move || { + self.0 + .sat_count::>(vars, &mut Default::default()) + .0 + }) + } + + /// Pick a satisfying assignment. + /// + /// Locking behavior: acquires the manager's lock for shared access. + /// + /// Returns: + /// list[bool | None] | None: The satisfying assignment where the i-th + /// value means that the i-th variable is false, true, or "don't care," + /// respectively, or ``None`` if ``self`` is unsatisfiable + fn pick_cube(&self, py: Python) -> PyObject { + match py.allow_threads(move || self.0.pick_cube([], move |_, _, _| false)) { + Some(r) => PyList::new_bound( + py, + r.into_iter().map(|v| match v { + OptBool::None => ().into_py(py), + _ => (v != OptBool::False).into_py(py), + }), + ) + .into_py(py), + None => ().into_py(py), + } + } + /// Pick a satisfying assignment, represented as decision diagram. + /// + /// Locking behavior: acquires the manager's lock for shared access. + /// + /// Returns: + /// Self: The satisfying assignment as decision diagram, or ``⊥`` if + /// ``self`` is unsatisfiable + fn pick_cube_dd(&self, py: Python) -> PyResult { + py.allow_threads(move || self.0.pick_cube_dd(move |_, _, _| false)) + .try_into() + } + /// Pick a satisfying assignment as DD, with choices as of ``literal_set``. + /// + /// ``literal_set`` is a conjunction of literals. Whenever there is a choice + /// for a variable, it will be set to true if the variable has a positive + /// occurrence in ``literal_set``, and set to false if it occurs negated in + /// ``literal_set``. If the variable does not occur in ``literal_set``, then + /// it will be left as don't care if possible, otherwise an arbitrary (not + /// necessarily random) choice will be performed. + /// + /// Locking behavior: acquires the manager's lock for shared access. + /// + /// Args: + /// literal_set (Self): Conjunction of literals to determine the choice + /// for variables + /// + /// Returns: + /// Self: The satisfying assignment as decision diagram, or ``⊥`` if + /// ``self`` is unsatisfiable + /// + /// Raises: + /// DDMemoryError: If the operation runs out of memory + fn pick_cube_dd_set(&self, py: Python, literal_set: &Self) -> PyResult { + py.allow_threads(move || self.0.pick_cube_dd_set(&literal_set.0)) + .try_into() + } + + /// Evaluate this Boolean function with arguments ``args``. + /// + /// Locking behavior: acquires the manager's lock for shared access. + /// + /// Args: + /// args (Iterable[tuple[Self, bool]]): ``(variable, value)`` pairs + /// where variables must be handles for the respective decision + /// diagram levels, i.e., singleton sets. + /// Missing variables are assumed to be false. However, note that + /// the arguments may also determine the domain, e.g., in case of + /// ZBDDs. If variables are given multiple times, the last value + /// counts. Besides that, the order is irrelevant. + /// All variable handles must belong to the same manager as ``self`` + /// and must reference inner nodes. + /// + /// Returns: + /// bool: The result of applying the function ``self`` to ``args`` + fn eval(&self, args: &Bound) -> PyResult { + let mut fs = Vec::with_capacity(args.len().unwrap_or(0)); + for pair in args.iter()? { + let pair: Bound = pair?.downcast_into()?; + let f = pair.get_borrowed_item(0)?; + let f = f.downcast::()?.get().0.clone(); + let b = pair.get_borrowed_item(1)?.is_truthy()?; + fs.push((f, b)); + } + + Ok(self.0.eval(fs.iter().map(|(f, b)| (f, *b)))) + } +} diff --git a/crates/oxidd-ffi-python/stub_gen/mod.rs b/crates/oxidd-ffi-python/stub_gen/mod.rs new file mode 100644 index 0000000..dcb352a --- /dev/null +++ b/crates/oxidd-ffi-python/stub_gen/mod.rs @@ -0,0 +1,1195 @@ +//! Generate stub definitions with types from PyO3/Rust source code with +//! Google-style docstrings + +use std::collections::HashMap; +use std::fmt::{self, Write as _}; +use std::fs; +use std::io; +use std::path::Path; + +use anyhow::{bail, Result}; +use proc_macro2::TokenStream; +use quote::ToTokens; + +mod util; +use util::{identifier_to_string, Indent, OrdRc}; + +// spell-checker:ignore punct + +#[derive(Debug)] +struct Item { + name: String, + doc: String, + kind: ItemKind, +} + +#[derive(Debug)] +enum ItemKind { + Attribute { + ty: Type, + }, + Function { + kind: FunctionKind, + params: Vec, + return_type: Type, + }, + Class { + items: Vec, + bases: Vec>, + constructible: bool, + subclassable: bool, + impl_eq: bool, + impl_eq_int: bool, + impl_ord: bool, + impl_hash: bool, + }, +} + +#[derive(Clone, PartialEq, Eq, Debug)] +enum FunctionKind { + Function, + FunctionPassModule, + Method, + Constructor, + Getter, + Setter(String), + Classmethod, + Staticmethod, +} + +#[derive(Debug)] +struct Parameter { + name: String, + ty: Option, + default_value: Option, +} + +impl Parameter { + fn name_only(name: impl ToString) -> Self { + Self { + name: name.to_string(), + ty: None, + default_value: None, + } + } + + fn params_for( + name: &str, + kind: &FunctionKind, + rust: &syn::punctuated::Punctuated, + pyo3: Option<&TokenStream>, + py: Option<&str>, + ) -> Result> { + let mut params = Vec::with_capacity(rust.len() + 1); + + // If there is a signature attribute, then PyO3 and the Rust compiler + // make sure that the PyO3 signature and the Rust function signature + // agree. In this case, we only look at the PyO3 signature. Otherwise, + // we infer the parameters from the Rust signature. + if let Some(tokens) = pyo3 { + let mut iter = tokens.clone().into_iter(); + match kind { + FunctionKind::Method | FunctionKind::Getter | FunctionKind::Setter(_) => { + params.push(Self::name_only("self")) + } + FunctionKind::Constructor | FunctionKind::Classmethod => { + params.push(Self::name_only("cls")) + } + _ => {} + } + loop { + let mut kv = iter + .by_ref() + .take_while(|tok| !util::parse::is_punct(',', tok)); + let mut name = String::new(); + for tok in kv + .by_ref() + .take_while(|tok| !util::parse::is_punct('=', tok)) + { + write!(name, "{tok}")?; + } + if name.is_empty() { + break; + } + let mut v = String::new(); + for tok in kv { + write!(v, "{tok}")?; + } + params.push(Parameter { + name, + ty: None, + default_value: if v.is_empty() { None } else { Some(v) }, + }); + } + } else { + let mut add_positional_delimiter = true; + if *kind == FunctionKind::Constructor { + params.push(Self::name_only("cls")); + params.push(Self::name_only("/")); + add_positional_delimiter = false; + } + let mut iter = rust.iter(); + if *kind == FunctionKind::FunctionPassModule { + iter.next(); // skip over module parameter + } + for param in iter { + match param { + syn::FnArg::Receiver(_) => { + params.push(Self::name_only("self")); + if !name.starts_with("__") { + params.push(Self::name_only("/")); + add_positional_delimiter = false; + } + } + syn::FnArg::Typed(pat_type) => { + let syn::Pat::Ident(pat_ident) = &*pat_type.pat else { + bail!("expected Rust parameters to be given an identifier") + }; + if let syn::Type::Path(path) = &*pat_type.ty { + if let Some(last) = path.path.segments.last() { + if last.ident == "Python" { + continue; + } + } + } + let mut name = pat_ident.ident.to_string(); + if let Some(n) = name.strip_prefix('_') { + name = n.to_string(); + } + params.push(Self::name_only(name)); + } + } + } + if !params.is_empty() && add_positional_delimiter { + params.push(Self::name_only("/")); + } + } + + if let Some(sig) = py { + // Check that the text_signature matches the signature from above + // and add default arguments. + + let Some(sig) = sig.strip_prefix('(').and_then(|s| s.strip_suffix(')')) else { + bail!("text signatures must start with '(' and end with ')'") + }; + + let mut iter = sig.bytes().enumerate(); + let mut par_depth = 0u32; + let mut in_str = 0u8; + let mut in_esc = false; + let mut param_iter = params.iter_mut(); + loop { + let mut inner = iter + .by_ref() + .filter(|(_, c)| !c.is_ascii_whitespace()) + .take_while(|&(_, c)| { + match c { + b',' if par_depth == 0 && in_str == 0 => return false, + b'(' | b'[' | b'{' => par_depth += 1, + b')' | b']' | b'}' => par_depth -= 1, + b'"' if !in_esc => in_str ^= b'"', + b'\'' if !in_esc => in_str ^= b'\'', + b'\\' => { + in_esc = true; + return true; + } + _ => {} + } + true + }); + + let Some((name_start, _)) = inner.next() else { + if let Some(param) = param_iter.next() { + bail!( + "parameter '{}' is missing in text_signature '{sig}'", + param.name + ) + } + break; + }; + let name_end = 1 + match inner.by_ref().take_while(|&(_, c)| c != b'=').last() { + Some((e, _)) => e, + None => name_start, + }; + let name = sig.split_at(name_end).0.split_at(name_start).1; + if name == "$module" && *kind == FunctionKind::FunctionPassModule { + continue; + } + let Some(param) = param_iter.next() else { + bail!("additional parameter '{name}' in text_signature") + }; + if param.name != name.strip_prefix('$').unwrap_or(name) { + bail!( + "parameter names do not agree ('{}' vs. '{name}' in text_signature)", + param.name + ) + } + + if let Some((val_start, _)) = inner.next() { + let val_end = 1 + match inner.last() { + Some((e, _)) => e, + None => val_start, + }; + let val = sig.split_at(val_end).0.split_at(val_start).1; + param.default_value = Some(val.to_string()) + } + } + } + + Ok(params) + } +} + +impl fmt::Display for Parameter { + fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { + f.write_str(&self.name)?; + match (&self.ty, &self.default_value) { + (None, None) => Ok(()), + (Some(ty), None) => write!(f, ": {ty}"), + (None, Some(val)) => write!(f, "={val}"), + (Some(ty), Some(val)) => write!(f, ": {ty} = {val}"), + } + } +} + +#[derive(Clone, PartialEq, Eq, PartialOrd, Ord, Debug)] +enum Type { + Any, + Union(Vec), + Other(OrdRc, Vec), +} + +#[derive(Default)] +pub struct TypeEnv { + py: HashMap>, + rs: HashMap>, +} + +impl TypeEnv { + pub fn new() -> Self { + Self::default() + } + + pub fn register_python_type(&mut self, py_name: String) -> Result> { + let name = OrdRc::new(py_name.clone()); + if self.py.insert(py_name, name.clone()).is_some() { + bail!("Python type '{name}' already declared"); + } + Ok(name) + } + + pub fn register_rust_type(&mut self, rust_name: &str, py_name: OrdRc) -> Result<()> { + if self.rs.insert(rust_name.to_string(), py_name).is_some() { + bail!("Rust type '{rust_name}' already declared"); + } + Ok(()) + } + + fn get_py_type(&self, name: &str, args: Vec) -> Result { + match self.py.get(name) { + Some(info) => Ok(Type::Other(info.clone(), args)), + None => bail!("Unknown Python type '{name}'"), + } + } + + fn parse_py(&self, string: &str) -> Result { + #[derive(Clone, Copy)] + enum Token<'a> { + Ident(&'a str), + LBrack, + RBrack, + Comma, + Dot, + Or, + } + + let mut tokens = Vec::new(); + let mut remainder = string; + while let Some(pos) = remainder.find([' ', '\t', '[', ']', ',', '.', '|']) { + if pos != 0 { + let (before, s) = remainder.split_at(pos); + tokens.push(Token::Ident(before)); + remainder = s; + } + let (delim, after) = remainder.split_at(1); + remainder = after; + tokens.push(match delim { + "[" => Token::LBrack, + "]" => Token::RBrack, + "," => Token::Comma, + "." => Token::Dot, + "|" => Token::Or, + _ => continue, + }); + } + if !remainder.is_empty() { + tokens.push(Token::Ident(remainder)); + } + + /// Split tokens into two parts such that the first part is the longest + /// sequence from the start consisting only of `Token::Ident(..)` and + /// `Token::Dot` + fn get_identifier<'a>(tokens: &'a [Token<'a>]) -> (&'a [Token<'a>], &'a [Token<'a>]) { + let mut i = 0; + let mut second = tokens; + while let [Token::Ident(_) | Token::Dot, r @ ..] = second { + i += 1; + second = r; + } + (&tokens[..i], second) + } + + fn parse_args<'a>( + env: &TypeEnv, + tokens: &'a [Token<'a>], + ) -> Result<(Vec, &'a [Token<'a>])> { + let [Token::LBrack, tokens @ ..] = tokens else { + return Ok((Vec::new(), tokens)); + }; + let mut args = Vec::new(); + let mut tokens = tokens; + loop { + let (arg, t) = parse(env, tokens)?; + args.push(arg); + match t { + [Token::RBrack, tokens @ ..] | [Token::Comma, Token::RBrack, tokens @ ..] => { + return Ok((args, tokens)) + } + [Token::Comma, t @ ..] => tokens = t, + _ => bail!("expected ',' or ']'"), + } + } + } + + fn parse_single<'a>( + env: &TypeEnv, + tokens: &'a [Token<'a>], + ) -> Result<(Type, &'a [Token<'a>])> { + let (path, tokens) = get_identifier(tokens); + let [.., Token::Ident(ident)] = *path else { + bail!("") + }; + Ok(match ident { + "Any" => (Type::Any, tokens), + _ => { + let (args, tokens) = parse_args(env, tokens)?; + (env.get_py_type(ident, args)?, tokens) + } + }) + } + + fn parse<'a>(env: &TypeEnv, tokens: &'a [Token<'a>]) -> Result<(Type, &'a [Token<'a>])> { + let (ty, tokens) = parse_single(env, tokens)?; + let [Token::Or, tokens @ ..] = tokens else { + return Ok((ty, tokens)); + }; + let mut union = vec![ty]; + let mut tokens = tokens; + loop { + let (ty, t) = parse_single(env, tokens)?; + union.push(ty); + match t { + [Token::Or, t @ ..] => tokens = t, + _ => return Ok((Type::Union(union), t)), + } + } + } + + match parse(self, &tokens) { + Ok((ty, [])) => Ok(ty), + Ok(_) => bail!("Failed to parse Python type '{string}'"), + Err(err) => Err(err.context(format!("Failed to parse Python type '{string}'"))), + } + } + + /// Read a function/method signature from a docstring + /// + /// `item_name` is used for error reporting only + fn signature_from_doc( + &self, + doc: &str, + item_name: &str, + mut params: &mut [Parameter], + ) -> Result { + #[derive(Clone, Copy, PartialEq, Eq)] + enum State { + Init, + Args, + Returns, + } + let mut state = State::Init; + let mut return_type = None; + for line in doc.lines() { + match line { + "Args:" => { + state = State::Args; + continue; + } + "Returns:" => { + state = State::Returns; + continue; + } + "" => continue, + _ if state == State::Init => continue, + _ => {} + } + let Some(line) = line.strip_prefix(" ") else { + state = State::Init; + continue; + }; + + if state == State::Args { + if line.starts_with(' ') { + continue; + } + if let Some((arg_name, after)) = line.split_once('(') { + let arg_name = arg_name.trim_ascii_end(); + if !arg_name.is_empty() { + if let Some((ty, _)) = after.split_once(')') { + let ty = self.parse_py(ty)?; + loop { + let [p, pr @ ..] = params else { + bail!("Additional parameter '{arg_name}' documented for '{item_name}'") + }; + params = pr; + if arg_name == p.name { + p.ty = Some(ty); + break; + } + } + continue; + } + } + } + bail!("Failed to parse arguments in docstring for '{item_name}'"); + } + + debug_assert!(state == State::Returns); + return_type = Some(if line == "None" { + self.get_py_type("None", Vec::new())? + } else if let Some((ty, _)) = line.split_once(':') { + self.parse_py(ty)? + } else { + bail!("Failed to parse the return type in docstring for '{item_name}'"); + }); + state = State::Init; + } + + if let Some(ret) = return_type { + Ok(ret) + } else { + bail!("Missing return type documentation for '{item_name}'") + } + } + + /// Read an attribute/property type from a docstring + /// + /// `item_name` is used for error reporting only + fn attr_type_from_doc(&self, doc: &str, item_name: &str) -> Result { + if let Some((ty, _)) = doc.split_once(':') { + self.parse_py(ty) + } else { + bail!("Type annotation missing in docstring for '{item_name}'") + } + } +} + +impl fmt::Display for Type { + fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { + match self { + Type::Any => f.write_str("Any"), + Type::Union(ts) => { + if let [tr @ .., t] = &ts[..] { + for t in tr { + write!(f, "{t} | ")?; + } + t.fmt(f) + } else { + f.write_str("Never") + } + } + Type::Other(name, args) => { + f.write_str(name)?; + if let [arg, args @ ..] = &args[..] { + write!(f, "[{arg}")?; + for arg in args { + write!(f, ", {arg}")?; + } + f.write_str("]")?; + } + Ok(()) + } + } + } +} + +fn attr_matches(attribute: &syn::Attribute, name: &str) -> bool { + if let Some(segment) = attribute.meta.path().segments.last() { + if segment.ident == name { + return true; + } + } + false +} + +fn get_doc(attributes: &[syn::Attribute]) -> String { + let mut doc = String::new(); + for attr in attributes { + let syn::Meta::NameValue(meta) = &attr.meta else { + continue; + }; + + let path = &meta.path.segments; + if path.len() != 1 || path[0].ident != "doc" { + continue; + } + + let syn::Expr::Lit(syn::ExprLit { + lit: syn::Lit::Str(value), + .. + }) = &meta.value + else { + continue; + }; + + let value = value.value(); + doc.push_str(value.strip_prefix(" ").unwrap_or(&value)); + doc.push('\n'); + } + + doc +} + +pub struct StubGen { + items: Vec, + class_to_item: HashMap, + type_env: TypeEnv, +} + +impl StubGen { + pub fn new(type_env: TypeEnv) -> Self { + Self { + items: Vec::new(), + class_to_item: HashMap::new(), + type_env, + } + } + + /// Process a Rust `struct`/`enum` + fn process_class( + &mut self, + ident: &syn::Ident, + attributes: &[syn::Attribute], + ) -> Result { + let Some(pyclass) = attributes.iter().find(|a| attr_matches(a, "pyclass")) else { + return Ok(usize::MAX); + }; + + let doc = get_doc(attributes); + + let mut name = String::new(); + let mut bases = Vec::new(); + let mut subclassable = false; + let mut impl_eq = false; + let mut impl_eq_int = false; + let mut impl_ord = false; + let mut impl_hash = false; + if let syn::Meta::List(syn::MetaList { tokens, .. }) = &pyclass.meta { + util::parse::recognize_key_val(tokens.clone(), pyclass, |key, tokens| { + if key == "eq" { + impl_eq = true; + } else if key == "eq_int" { + impl_eq_int = true; + } else if key == "ord" { + impl_ord = true; + } else if key == "hash" { + impl_hash = true; + } else if key == "name" { + util::parse::expect_punct_opt('=', tokens.next(), pyclass)?; + name = util::parse::expect_string_opt(tokens.next(), pyclass)?; + } else if key == "extends" { + util::parse::expect_punct_opt('=', tokens.next(), pyclass)?; + let base_name = + util::parse::expect_ident_opt(tokens.next(), pyclass)?.to_string(); + let Some(base) = self.type_env.rs.get(&base_name) else { + bail!("Unknown Rust type '{base_name}' as base class for '{ident}'") + }; + bases.push(base.clone()); + } else if key == "subclass" { + subclassable = true; + } else { + return Ok(false); + } + Ok(true) + })?; + } + + if name.is_empty() { + name = identifier_to_string(ident); + } + self.type_env.register_python_type(name.clone())?; + + let id = self.items.len(); + if self.class_to_item.insert(ident.clone(), id).is_some() { + bail!("Python class '{name}' (Rust identifier '{ident}') was declared twice") + } + + self.items.push(Item { + name, + doc, + kind: ItemKind::Class { + items: Vec::new(), + bases, + constructible: false, + subclassable, + impl_eq, + impl_eq_int, + impl_ord, + impl_hash, + }, + }); + + Ok(id) + } + + fn process_method(env: &TypeEnv, item: &syn::ImplItemFn, last: Option<&Item>) -> Result { + let mut kind = FunctionKind::Method; + let mut name = String::new(); + let mut signature = None; + let mut text_signature = None; + for attr in &item.attrs { + let Some(syn::PathSegment { ident, .. }) = attr.meta.path().segments.last() else { + continue; + }; + + if ident == "pyo3" { + let syn::Meta::List(syn::MetaList { tokens, .. }) = &attr.meta else { + continue; + }; + util::parse::recognize_key_val(tokens.clone(), attr, |ident, tokens| { + if ident == "name" { + util::parse::expect_punct_opt('=', tokens.next(), attr)?; + name = util::parse::expect_string_opt(tokens.next(), attr)?; + } else if ident == "signature" { + util::parse::expect_punct_opt('=', tokens.next(), attr)?; + signature = Some(util::parse::expect_group_opt(tokens.next(), attr)?); + } else if ident == "text_signature" { + util::parse::expect_punct_opt('=', tokens.next(), attr)?; + text_signature = Some(util::parse::expect_string_opt(tokens.next(), attr)?); + } else { + return Ok(false); + } + Ok(true) + })?; + } else if ident == "getter" { + kind = FunctionKind::Getter; + if let syn::Meta::List(syn::MetaList { tokens, .. }) = &attr.meta { + name = util::parse::expect_ident_opt(tokens.clone().into_iter().next(), attr)? + .to_string(); + } + } else if ident == "setter" { + kind = FunctionKind::Setter( + if let syn::Meta::List(syn::MetaList { tokens, .. }) = &attr.meta { + util::parse::expect_ident_opt(tokens.clone().into_iter().next(), attr)? + .to_string() + } else { + ident.to_string() + }, + ); + } else if ident == "new" { + kind = FunctionKind::Constructor; + name = "__new__".into(); + } else if ident == "classmethod" { + kind = FunctionKind::Classmethod; + } else if ident == "staticmethod" { + kind = FunctionKind::Staticmethod; + } + } + let doc = get_doc(&item.attrs); + + let ident = &item.sig.ident; + if name.is_empty() { + name = identifier_to_string(ident); + } + + let (params, return_type) = match &kind { + FunctionKind::Getter => { + let r = env.attr_type_from_doc(&doc, &name)?; + let p = vec![Parameter::name_only("self"), Parameter::name_only("/")]; + (p, r) + } + FunctionKind::Setter(property_name) => { + // we rely on the type associated with the getter + let Some(ty) = last.and_then(|last| match &last.kind { + ItemKind::Function { + kind: FunctionKind::Getter, + return_type, + .. + } if last.name == *property_name => Some(return_type), + _ => None, + }) else { + bail!("Expected the respective getter directly before setter '{name}' (Rust identifier '{ident}')") + }; + + let r = env.get_py_type("None", Vec::new())?; + let p = vec![ + Parameter::name_only("self"), + Parameter { + name: "value".into(), + ty: Some(ty.clone()), + default_value: None, + }, + Parameter::name_only("/"), + ]; + // TODO: should we check that this signature agrees with the Rust signature? + + (p, r) + } + _ => { + let mut p = Parameter::params_for( + &name, + &kind, + &item.sig.inputs, + signature.as_ref(), + text_signature.as_deref(), + ) + .map_err(|err| { + err.context(format!( + "Failed to process parameters for method '{name}' (Rust identifier '{ident}')" + )) + })?; + let r = env.signature_from_doc(&doc, &name, &mut p[..])?; + (p, r) + } + }; + + Ok(Item { + name, + doc, + kind: ItemKind::Function { + kind, + params, + return_type, + }, + }) + } + + fn process_function(&mut self, function: &syn::ItemFn) -> Result<()> { + let mut name = String::new(); + let mut signature = None; + let mut text_signature = None; + let mut pass_module = false; + for attr in &function.attrs { + let Some(syn::PathSegment { ident, .. }) = attr.meta.path().segments.last() else { + continue; + }; + + if ident == "pyo3" { + let syn::Meta::List(syn::MetaList { tokens, .. }) = &attr.meta else { + continue; + }; + util::parse::recognize_key_val(tokens.clone(), attr, |ident, tokens| { + if ident == "name" { + util::parse::expect_punct_opt('=', tokens.next(), attr)?; + name = util::parse::expect_string_opt(tokens.next(), attr)?; + } else if ident == "signature" { + util::parse::expect_punct_opt('=', tokens.next(), attr)?; + signature = Some(util::parse::expect_group_opt(tokens.next(), attr)?); + } else if ident == "text_signature" { + util::parse::expect_punct_opt('=', tokens.next(), attr)?; + text_signature = Some(util::parse::expect_string_opt(tokens.next(), attr)?); + } else if ident == "pass_module" { + pass_module = true; + } else { + return Ok(false); + } + Ok(true) + })?; + } + } + let doc = get_doc(&function.attrs); + + let ident = &function.sig.ident; + if name.is_empty() { + name = identifier_to_string(ident); + } + + let mut params = Parameter::params_for( + &name, + &if pass_module { + FunctionKind::FunctionPassModule + } else { + FunctionKind::Function + }, + &function.sig.inputs, + signature.as_ref(), + text_signature.as_deref(), + ) + .map_err(|err| { + err.context(format!( + "Failed to process parameters for method '{name}' (Rust identifier '{ident}')" + )) + })?; + let return_type = self + .type_env + .signature_from_doc(&doc, &name, &mut params[..])?; + + self.items.push(Item { + name, + doc, + kind: ItemKind::Function { + kind: FunctionKind::Function, + params, + return_type, + }, + }); + + Ok(()) + } + + fn process_class_items(&mut self, class_id: usize, items: &[syn::ImplItem]) -> Result<()> { + let class = &mut self.items[class_id]; + let class_name = &class.name; + let ItemKind::Class { + items: class_items, + constructible, + .. + } = &mut class.kind + else { + panic!("class_id must refer to a class"); + }; + + for item in items { + class_items.push(match item { + syn::ImplItem::Const(item) => { + if !item.attrs.iter().any(|a| attr_matches(a, "classattr")) { + continue; + } + let name = identifier_to_string(&item.ident); + let doc = get_doc(&item.attrs); + let ty = self.type_env.attr_type_from_doc(&doc, &name)?; + + let kind = ItemKind::Attribute { ty }; + Item { name, doc, kind } + } + syn::ImplItem::Fn(item) => { + let f = Self::process_method(&self.type_env, item, class_items.last()) + .map_err(|err| { + err.context(format!( + "failed to process methods for Python class '{class_name}'" + )) + })?; + + *constructible |= matches!( + f, + Item { + kind: ItemKind::Function { + kind: FunctionKind::Constructor, + .. + }, + .. + } + ); + + f + } + _ => continue, + }); + } + + Ok(()) + } + + fn process_exception(&mut self, tokens: &TokenStream) -> Result<()> { + let mut iter = tokens.clone().into_iter(); + iter.by_ref() + .take_while(|tok| !util::parse::is_punct(',', tok)) + .count(); + let Some(proc_macro2::TokenTree::Ident(name)) = iter.next() else { + bail!("Missing identifier in create_exception!({tokens})") + }; + iter.next(); // skip ',' + let mut base = None; + for tok in &mut iter { + if let proc_macro2::TokenTree::Ident(b) = tok { + base = Some(b); + } else if util::parse::is_punct(',', &tok) { + break; + } + } + let Some(base) = base else { + bail!("Missing base in create_exception!({tokens})") + }; + let Some(base) = self.type_env.rs.get(&base.to_string()) else { + bail!("Unknown base '{base}' in create_exception!({tokens})") + }; + let mut doc = String::new(); + if let Some(proc_macro2::TokenTree::Literal(l)) = iter.next() { + match syn::Lit::new(l) { + syn::Lit::Str(l) => doc = l.value(), + _ => bail!( + "Expected a string literal as documentation in create_exception!({tokens})" + ), + } + } + + let base = base.clone(); + self.type_env.register_python_type(name.to_string())?; + self.items.push(Item { + name: name.to_string(), + doc, + kind: ItemKind::Class { + items: Vec::new(), + bases: vec![base], + constructible: true, + subclassable: true, + impl_eq: false, + impl_eq_int: false, + impl_ord: false, + impl_hash: false, + }, + }); + + Ok(()) + } + + fn process_items(&mut self, items: &[syn::Item]) -> Result<()> { + // Process all sorts of classes (without their methods) first to register their + // names + for item in items { + match item { + syn::Item::Mod(item_mod) => { + if let Some((_, items)) = &item_mod.content { + self.process_items(items)?; + } + } + syn::Item::Struct(item_struct) => { + self.process_class(&item_struct.ident, &item_struct.attrs)?; + // TODO: handle fields `#[pyo3(get, set, name = + // "custom_name")]` + } + syn::Item::Enum(item_enum) => { + self.process_class(&item_enum.ident, &item_enum.attrs)?; + // TODO: handle variants `#[pyo3(constructor = + // (radius=1.0))]` + } + syn::Item::Macro(mac) => { + if let Some(last) = mac.mac.path.segments.last() { + if last.ident == "create_exception" { + self.process_exception(&mac.mac.tokens)?; + } + }; + } + _ => {} + } + } + + for item in items { + match item { + syn::Item::Mod(item_mod) => { + if let Some((_, items)) = &item_mod.content { + self.process_items(items)?; + } + } + syn::Item::Fn(item_fn) => { + if item_fn.attrs.iter().any(|a| attr_matches(a, "pyfunction")) { + self.process_function(item_fn)?; + } + } + syn::Item::Impl(item_impl) => { + if !item_impl.attrs.iter().any(|a| attr_matches(a, "pymethods")) { + continue; + } + + if let syn::Type::Path(path) = &*item_impl.self_ty { + if let Some(ident) = path.path.get_ident() { + if let Some(id) = self.class_to_item.get(ident) { + self.process_class_items(*id, &item_impl.items)?; + continue; + } + + bail!("Did not find a #[pyclass] '{ident}'") + } + } + + bail!( + "Unexpected type '{}' in #[pymethods] impl", + item_impl.self_ty.to_token_stream() + ) + } + _ => {} + } + } + + Ok(()) + } + + pub fn process_files>( + &mut self, + paths: impl IntoIterator, + ) -> Result<()> { + let mut items = Vec::new(); + for p in paths { + items.extend(syn::parse_file(&fs::read_to_string(p)?)?.items); + } + self.process_items(&items) + } + + fn write_doc(writer: &mut W, doc: &str, indent: Indent) -> io::Result<()> { + let doc = doc.trim_ascii_end(); + let raw = if doc.contains('\\') { "r" } else { "" }; + let mut lines = doc.lines(); + let Some(line) = lines.next() else { + return Ok(()); + }; + + write!(writer, "{indent}{raw}\"\"\"{line}")?; + let Some(line) = lines.next() else { + return writeln!(writer, "\"\"\""); + }; + writeln!(writer)?; + match line { + "" => writeln!(writer)?, + _ => writeln!(writer, "{indent}{line}")?, + } + + for line in lines { + match line { + "" => writeln!(writer)?, + _ => writeln!(writer, "{indent}{line}")?, + } + } + writeln!(writer, "{indent}\"\"\"") + } + + fn write_items( + w: &mut W, + items: &[Item], + indent: Indent, + mut blanks_before: u32, + ) -> Result<()> { + for item in items { + for _ in 0..blanks_before { + writeln!(w)?; + } + + let name = &item.name; + let sub_indent = Indent(indent.0 + 1); + match &item.kind { + ItemKind::Attribute { ty } => { + writeln!(w, "{indent}{name}: {ty} = ...")?; + Self::write_doc(w, &item.doc, indent)?; + blanks_before = 0; + } + ItemKind::Function { + kind, + params, + return_type, + } => { + match kind { + FunctionKind::Getter => writeln!(w, "{indent}@property")?, + FunctionKind::Setter(name) => writeln!(w, "{indent}@{name}.setter")?, + FunctionKind::Classmethod | FunctionKind::Constructor => { + writeln!(w, "{indent}@classmethod")? + } + FunctionKind::Staticmethod => writeln!(w, "{indent}@staticmethod")?, + _ => {} + } + write!(w, "{indent}def {name}(")?; + if let [param, params @ ..] = ¶ms[..] { + write!(w, "{param}")?; + for param in params { + write!(w, ", {param}")?; + } + } + write!(w, ") -> {return_type}:")?; + if item.doc.is_empty() { + writeln!(w, " ...")?; + blanks_before = 0; + } else { + writeln!(w)?; + Self::write_doc(w, &item.doc, sub_indent)?; + blanks_before = 1; + } + } + ItemKind::Class { + items, + bases, + constructible, + subclassable, + impl_eq, + impl_eq_int, + impl_ord, + impl_hash, + } => { + if !*subclassable { + writeln!(w, "{indent}@final")?; + } + write!(w, "{indent}class {name}")?; + if let [base, bases @ ..] = &bases[..] { + write!(w, "({base}")?; + for base in bases { + write!(w, ", {base}")?; + } + write!(w, ")")?; + } + + if item.doc.is_empty() && items.is_empty() { + writeln!(w, ":")?; + blanks_before = 0; + continue; + } + writeln!(w, ":")?; + Self::write_doc(w, &item.doc, sub_indent)?; + + if !*constructible { + writeln!(w)?; + writeln!(w, "{sub_indent}@classmethod")?; + writeln!(w, "{sub_indent}def __new__(cls, _: Never) -> Self:")?; + writeln!(w, "{sub_indent} \"\"\"Private constructor.\"\"\"")?; + } + + if !items.is_empty() { + Self::write_items(w, items, sub_indent, 1)?; + } + + if *impl_eq || *impl_eq_int || *impl_ord || *impl_hash { + writeln!(w)?; + } + if *impl_eq || *impl_eq_int || *impl_ord { + writeln!( + w, + "{sub_indent}def __eq__(self, /, rhs: object) -> bool: ..." + )?; + writeln!( + w, + "{sub_indent}def __ne__(self, /, rhs: object) -> bool: ..." + )?; + } + if *impl_eq_int { + writeln!(w, "{sub_indent}def __int__(self, /) -> int: ...")?; + } + if *impl_ord { + for op in ["le", "lt", "ge", "gt"] { + writeln!( + w, + "{sub_indent}def __{op}__(self, /, rhs: Self) -> bool: ..." + )?; + } + } + if *impl_hash { + writeln!(w, "{sub_indent}def __hash__(self, /) -> int: ...")?; + } + + blanks_before = 2; + } + } + } + + Ok(()) + } + + pub fn write(&self, writer: &mut W) -> Result<()> { + Self::write_items(writer, &self.items, Indent(0), 1) + } +} diff --git a/crates/oxidd-ffi-python/stub_gen/util.rs b/crates/oxidd-ffi-python/stub_gen/util.rs new file mode 100644 index 0000000..aea8d6a --- /dev/null +++ b/crates/oxidd-ffi-python/stub_gen/util.rs @@ -0,0 +1,196 @@ +use std::fmt; +use std::rc::Rc; + +// spell-checker:ignore punct + +pub struct OrdRc(Rc); + +impl OrdRc { + pub fn new(value: T) -> Self { + Self(Rc::new(value)) + } +} + +impl Clone for OrdRc { + fn clone(&self) -> Self { + Self(self.0.clone()) + } +} +impl PartialEq for OrdRc { + fn eq(&self, other: &Self) -> bool { + Rc::ptr_eq(&self.0, &other.0) + } +} +impl Eq for OrdRc {} +impl PartialOrd for OrdRc { + fn partial_cmp(&self, other: &Self) -> Option { + Some(self.cmp(other)) + } +} +impl Ord for OrdRc { + fn cmp(&self, other: &Self) -> std::cmp::Ordering { + Rc::as_ptr(&self.0).cmp(&Rc::as_ptr(&other.0)) + } +} + +impl std::ops::Deref for OrdRc { + type Target = T; + fn deref(&self) -> &Self::Target { + self.0.deref() + } +} + +impl fmt::Debug for OrdRc { + fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { + self.0.fmt(f) + } +} +impl fmt::Display for OrdRc { + fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { + self.0.fmt(f) + } +} + +pub mod parse { + use anyhow::{bail, Result}; + use proc_macro2::{token_stream, Ident, TokenStream, TokenTree}; + use quote::ToTokens; + + pub fn expect_ident(tok: TokenTree, context: impl ToTokens) -> Result { + match tok { + TokenTree::Ident(ident) => Ok(ident), + _ => bail!( + "expected an identifier, got '{tok}' in '{}'", + context.to_token_stream() + ), + } + } + + pub fn expect_ident_opt(tok: Option, context: impl ToTokens) -> Result { + let Some(tok) = tok else { + bail!( + "expected an identifier at the end of '{}'", + context.to_token_stream() + ) + }; + expect_ident(tok, context) + } + + pub fn is_punct(punct: char, tok: &TokenTree) -> bool { + if let TokenTree::Punct(p) = tok { + if p.as_char() == punct { + return true; + } + } + false + } + + pub fn expect_punct_opt( + punct: char, + tok: Option, + context: impl ToTokens, + ) -> Result<()> { + if let Some(tok) = tok { + if is_punct(punct, &tok) { + return Ok(()); + } + bail!( + "expected '{punct}', got '{tok}' at the end of '{}'", + context.to_token_stream() + ) + } + bail!( + "expected '{punct}' at the end of '{}'", + context.to_token_stream() + ) + } + + pub fn expect_string_opt(tok: Option, context: impl ToTokens) -> Result { + if let Some(tok) = tok { + if let TokenTree::Literal(literal) = &tok { + let mut s = literal.to_string(); + if s.len() > 2 && s.as_bytes()[0] == b'"' && s.pop().unwrap() == '"' { + s.remove(0); + return Ok(s); + } + } + bail!( + "expected a string literal, got {tok} in {}", + context.to_token_stream() + ) + } + bail!( + "expected a string literal at the end of '{}'", + context.to_token_stream() + ) + } + + pub fn expect_group_opt(tok: Option, context: impl ToTokens) -> Result { + if let Some(tok) = tok { + if let TokenTree::Group(group) = &tok { + return Ok(group.stream()); + } + bail!( + "expected a token group, got {tok} in {}", + context.to_token_stream() + ) + } + bail!( + "expected a token group at the end of '{}'", + context.to_token_stream() + ) + } + + /// Recognize single keys or key-value pairs + /// + /// `recognizer` should return `Ok(true)` whenever it recognized and fully + /// consumed an entry (i.e., the next token is expected to be a ',' or the + /// end). If the key is unknown, it should return `Ok(false)`, then the + /// parser will skip to the next ','. + pub fn recognize_key_val( + tokens: TokenStream, + context: impl ToTokens + Copy, + mut recognizer: impl FnMut(Ident, &mut token_stream::IntoIter) -> Result, + ) -> Result<()> { + let mut tokens = tokens.into_iter(); + 'outer: while let Some(tok) = tokens.next() { + let recognized = recognizer(expect_ident(tok, context)?, &mut tokens)?; + if recognized { + if let Some(tok) = tokens.next() { + expect_punct_opt(',', Some(tok), context)?; + continue; + } + return Ok(()); + } + + // unknown, consume everything up to the next comma + for tok in &mut tokens { + if is_punct(',', &tok) { + continue 'outer; + } + } + return Ok(()); + } + Ok(()) + } +} + +#[derive(Clone, Copy)] +pub struct Indent(pub u32); + +impl fmt::Display for Indent { + fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { + for _ in 0..self.0 { + f.write_str(" ")?; + } + Ok(()) + } +} + +pub fn identifier_to_string(ident: &syn::Ident) -> String { + let mut s = ident.to_string(); + if s.starts_with("r#") { + s = s.split_off(2); + } + s +} diff --git a/crates/oxidd-ffi/Cargo.toml b/crates/oxidd-ffi/Cargo.toml index 4a239f4..3d6acfc 100644 --- a/crates/oxidd-ffi/Cargo.toml +++ b/crates/oxidd-ffi/Cargo.toml @@ -15,7 +15,7 @@ publish = false [lib] crate-type = ["cdylib", "staticlib"] - +doc = false [dependencies] oxidd-core = { workspace = true } diff --git a/justfile b/justfile index 1175ad3..ee73de2 100644 --- a/justfile +++ b/justfile @@ -1,4 +1,4 @@ -# spell-checker:ignore Werror,pydata +# spell-checker:ignore autodoc,pydata,stubtest,Werror # Print available recipes help: @@ -32,19 +32,30 @@ lint-cpp: fmt-py: ruff format -# Lint Python code using ruff and pyright +# Lint Python code using ruff, mypy, and pyright lint-py: ruff check ruff format --check + mypy + python3 -m mypy.stubtest oxidd._oxidd pyright # Generate documentation for the Python bindings using Sphinx (output: `target/python/doc`) doc-py: - sphinx-build bindings/python/doc target/python/doc - -# Test Python code using pytest and generate a coverage report in `target/python/coverage` + @# Generate _oxidd.pyi + cargo check -p oxidd-ffi-python + @# We want Sphinx autodoc to look at the type annotations of the .pyi file + @# (we cannot provide the annotations in the compiled module). Hence, we + @# make a fake oxidd package without the compiled module and `_oxidd.pyi` + @# as `_oxidd.py`. + mkdir -p target/python/autodoc/oxidd + cp bindings/python/oxidd/*.py target/python/autodoc/oxidd + cp bindings/python/oxidd/_oxidd.pyi target/python/autodoc/oxidd/_oxidd.py + PYTHONPATH=target/python/autodoc sphinx-build bindings/python/doc target/python/doc + +# Test Python code using pytest test-py: - pytest -v --cov=oxidd --cov-report=html:target/python/coverage + pytest --verbose # `fmt-rust` fmt: fmt-rust @@ -70,8 +81,7 @@ devtools-py-venv-warn: devtools-py: devtools-py-venv && devtools-py-venv-warn #!/bin/sh if [ "$VIRTUAL_ENV" = '' ]; then source .venv/bin/activate; fi - pip3 install --upgrade pip pyright ruff sphinx pydata-sphinx-theme pytest-cov - pip3 install --editable . + pip3 install --editable '.[dev,docs,test]' # Install all development tools devtools: devtools-py diff --git a/pyproject.toml b/pyproject.toml index 4d63313..fe37760 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -8,7 +8,7 @@ authors = [{ name = "OxiDD Contributors", email = "info@oxidd.net" }] maintainers = [{ name = "Nils Husung", email = "nils@oxidd.net" }] readme = "bindings/python/README.md" -dependencies = ["cffi ~= 1.12", "typing-extensions ~= 4.0"] +dependencies = ["typing-extensions ~= 4.0"] # see https://pypi.org/classifiers/ classifiers = [ @@ -25,6 +25,7 @@ classifiers = [ "Programming Language :: Python :: 3.10", "Programming Language :: Python :: 3.11", "Programming Language :: Python :: 3.12", + "Programming Language :: Python :: 3.13", "Programming Language :: Rust", "Topic :: Scientific/Engineering", @@ -38,68 +39,87 @@ Documentation = "https://oxidd.net/api/python/dev/getting-started.html" Repository = "https://github.com/OxiDD/oxidd" Issues = "https://github.com/OxiDD/oxidd/issues" +[project.optional-dependencies] +# spell-checker:ignore pydata +dev = ["mypy ~= 1.13", "pyright ~= 1.1", "ruff ~= 0.7"] +docs = ["Sphinx ~= 8.0", "pydata-sphinx-theme ~= 0.16"] +test = ["pytest >= 8.0"] + + [build-system] -requires = ["setuptools >= 61.0, <= 73.0", "setuptools_scm >= 8"] -build-backend = "setuptools.build_meta" +requires = ["maturin ~= 1.7.4"] +build-backend = "maturin" + +[tool.maturin] +# spell-checker:ignore auditwheel +python-source = "bindings/python" +include = ["bindings/python/oxidd/_oxidd.pyi"] +exclude = [ + "bindings/python/oxidd/tests/**", + "crates/oxidd-ffi-python/build.rs", + "crates/oxidd-ffi-python/stub_gen/**", +] +module-name = "oxidd._oxidd" +manifest-path = "crates/oxidd-ffi-python/Cargo.toml" +auditwheel = "check" -[tool.setuptools] -packages = ["oxidd"] -package-dir = { "" = "bindings/python" } -include-package-data = false [tool.pyright] include = ["bindings/python"] pythonVersion = "3.9" -typeCheckingMode = "standard" -strict = ["bindings/python/tests/**"] +typeCheckingMode = "strict" + +[tool.mypy] +packages = ["oxidd"] +python_version = "3.9" +strict = true [tool.ruff] target-version = "py39" [tool.ruff.lint] select = [ - # pycodestyle - "E", # Pyflakes "F", + # pycodestyle + "E", + # isort + "I", + # pep8-naming + "N", + # pydocstyle + "D", # pyupgrade "UP", - # flake8-bugbear + # flake8 "B", - # flake8-simplify + "FA", + "PIE", + "Q", + "RET", "SIM", - # isort - "I", + # pylint + "PLE", + # ruff + "RUF", +] +ignore = [ + "D203", # one-blank-line-before-class + "D213", # multi-line-summary-second-line + "D401", # non-imperative-mood + "D413", # blank-line-after-last-section + "D415", # ends-in-punctuation (we have ends-in-period) + "RUF001", # ambiguous-unicode-character-string + "RUF002", # ambiguous-unicode-character-docstring + "RUF003", # ambiguous-unicode-character-comment ] [tool.ruff.format] docstring-code-format = true -[tool.cibuildwheel] -# `python -m build --wheel` is the current PyPA recommendation and prints better -# error messages than `python -m pip wheel` -build-frontend = "build" - -# Skip all CPython versions >= 3.10 right away to avoid downloading additional -# Python versions (macOS, Windows). This is possible as we build abi3 modules. -build = ["cp39-*", "pp*"] -# Skip every target that is not tier 1 or 2, see -# https://doc.rust-lang.org/stable/rustc/platform-support.html -skip = ["*-musllinux_ppc64le", "*-musllinux_s390x"] - -environment.OXIDD_PYFFI_LINK_MODE = "static" -linux.environment.OXIDD_PYFFI_CONTAINER_BUILD = "1" - -# All Rust musl targets require musl 1.2 -musllinux-x86_64-image = "musllinux_1_2" -musllinux-i686-image = "musllinux_1_2" -musllinux-aarch64-image = "musllinux_1_2" - -# Ensure a clean build in the container (dev setups, should be a no-op in CI) -linux.before-all = "rm -rf build" +[tool.ruff.lint.per-file-ignores] +"_oxidd.pyi" = ["E501"] # ignore too long lines -test-requires = "pytest" -test-command = "pytest {project}/bindings/python/oxidd" [tool.pytest.ini_options] # spell-checker:ignore testpaths diff --git a/setup.py b/setup.py deleted file mode 100644 index 0c8e8c5..0000000 --- a/setup.py +++ /dev/null @@ -1,10 +0,0 @@ -from setuptools import setup - -setup( - setup_requires=["cffi ~= 1.12"], - cffi_modules=["bindings/python/build/ffi.py:ffi"], - # CFFI >= 1.12 uses `#define Py_LIMITED_API` on all platforms, so we only - # need to build one wheel to target multiple CPython versions. - # https://cffi.readthedocs.io/en/latest/cdef.html#ffibuilder-compile-etc-compiling-out-of-line-modules - options={"bdist_wheel": {"py_limited_api": "cp39"}}, -)