Merge pull request #15 from zhufangu/python-bindings

Add Python bindings for light and aggressive simplification functions

.github/workflows/CI.yml

@@ -0,0 +1,169 @@
+# This file is autogenerated by maturin v1.7.0
+# To update, run
+#
+#    maturin generate-ci github
+#
+name: CI
+
+on:
+  push:
+    branches:
+      - main
+      - master
+    tags:
+      - '*'
+  pull_request:
+  workflow_dispatch:
+
+permissions:
+  contents: read
+
+jobs:
+  linux:
+    runs-on: ${{ matrix.platform.runner }}
+    strategy:
+      matrix:
+        platform:
+          - runner: ubuntu-latest
+            target: x86_64
+          - runner: ubuntu-latest
+            target: x86
+          - runner: ubuntu-latest
+            target: aarch64
+          - runner: ubuntu-latest
+            target: armv7
+          - runner: ubuntu-latest
+            target: s390x
+          - runner: ubuntu-latest
+            target: ppc64le
+    steps:
+      - uses: actions/checkout@v4
+      - uses: actions/setup-python@v5
+        with:
+          python-version: 3.x
+      - name: Build wheels
+        uses: PyO3/maturin-action@v1
+        with:
+          target: ${{ matrix.platform.target }}
+          args: --release --out dist --find-interpreter
+          sccache: 'true'
+          manylinux: auto
+      - name: Upload wheels
+        uses: actions/upload-artifact@v4
+        with:
+          name: wheels-linux-${{ matrix.platform.target }}
+          path: dist
+
+  musllinux:
+    runs-on: ${{ matrix.platform.runner }}
+    strategy:
+      matrix:
+        platform:
+          - runner: ubuntu-latest
+            target: x86_64
+          - runner: ubuntu-latest
+            target: x86
+          - runner: ubuntu-latest
+            target: aarch64
+          - runner: ubuntu-latest
+            target: armv7
+    steps:
+      - uses: actions/checkout@v4
+      - uses: actions/setup-python@v5
+        with:
+          python-version: 3.x
+      - name: Build wheels
+        uses: PyO3/maturin-action@v1
+        with:
+          target: ${{ matrix.platform.target }}
+          args: --release --out dist --find-interpreter
+          sccache: 'true'
+          manylinux: musllinux_1_2
+      - name: Upload wheels
+        uses: actions/upload-artifact@v4
+        with:
+          name: wheels-musllinux-${{ matrix.platform.target }}
+          path: dist
+
+  windows:
+    runs-on: ${{ matrix.platform.runner }}
+    strategy:
+      matrix:
+        platform:
+          - runner: windows-latest
+            target: x64
+          - runner: windows-latest
+            target: x86
+    steps:
+      - uses: actions/checkout@v4
+      - uses: actions/setup-python@v5
+        with:
+          python-version: 3.x
+          architecture: ${{ matrix.platform.target }}
+      - name: Build wheels
+        uses: PyO3/maturin-action@v1
+        with:
+          target: ${{ matrix.platform.target }}
+          args: --release --out dist --find-interpreter
+          sccache: 'true'
+      - name: Upload wheels
+        uses: actions/upload-artifact@v4
+        with:
+          name: wheels-windows-${{ matrix.platform.target }}
+          path: dist
+
+  macos:
+    runs-on: ${{ matrix.platform.runner }}
+    strategy:
+      matrix:
+        platform:
+          - runner: macos-12
+            target: x86_64
+          - runner: macos-14
+            target: aarch64
+    steps:
+      - uses: actions/checkout@v4
+      - uses: actions/setup-python@v5
+        with:
+          python-version: 3.x
+      - name: Build wheels
+        uses: PyO3/maturin-action@v1
+        with:
+          target: ${{ matrix.platform.target }}
+          args: --release --out dist --find-interpreter
+          sccache: 'true'
+      - name: Upload wheels
+        uses: actions/upload-artifact@v4
+        with:
+          name: wheels-macos-${{ matrix.platform.target }}
+          path: dist
+
+  sdist:
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v4
+      - name: Build sdist
+        uses: PyO3/maturin-action@v1
+        with:
+          command: sdist
+          args: --out dist
+      - name: Upload sdist
+        uses: actions/upload-artifact@v4
+        with:
+          name: wheels-sdist
+          path: dist
+
+  release:
+    name: Release
+    runs-on: ubuntu-latest
+    if: "startsWith(github.ref, 'refs/tags/')"
+    needs: [linux, musllinux, windows, macos, sdist]
+    steps:
+      - uses: actions/download-artifact@v4
+      - name: Publish to PyPI
+        uses: PyO3/maturin-action@v1
+        env:
+          MATURIN_PYPI_TOKEN: ${{ secrets.PYPI_API_TOKEN }}
+        with:
+          command: upload
+          args: --non-interactive --skip-existing wheels-*/*

.gitignore

@@ -23,5 +23,9 @@ simplify
 # JetBrains IDE (RustRover/IdeaJ)
 .idea
 
+
+# Python virtual environment
+.env
+
 # Visual Studio Code
-.vscode
+.vscode

Cargo.toml

@@ -12,6 +12,11 @@ rand = "0.8.5"
 sequential-test = "0.2.4"
 z3 = {version="0.12", features = ["static-link-z3"]}
 z3-sys = {version="0.8", features = ["static-link-z3"]}
+pyo3 = { version = "0.15", features = ["extension-module"] }
 
 [dev-dependencies]
 ordered-float = "3.0.0"
+
+[lib]
+name = "simplify"
+crate-type = ["cdylib"]

README.md

@@ -55,5 +55,72 @@ To recompile and then simplify formula f against assumptions a, use
 For example,
 `cargo run -- -s "(or (and (= (v) (0)) (distinct (intersection) (x))) (and (> (v) (0)) (or (and (= (v) (vmax)) (or (< (+ (* (* (2) (A)) (intersection)) (^ (v) (2))) (+ (^ (vmax) (2)) (* (* (2) (A)) (x)))) (or (and (> (timeToRed) (0)) (= (+ (* (* (2) (A)) (intersection)) (^ (v) (2))) (+ (^ (vmax) (2)) (* (* (2) (A)) (x))))) (and (> (+ (* (* (2) (A)) (intersection)) (^ (v) (2))) (+ (^ (vmax) (2)) (* (* (2) (A)) (x)))) (or (> (B) (* (^ (v) (2)) (^ (+ (* (2) (intersection)) (* (-2) (x))) (-1)))) (< (* (2) (intersection)) (+ (* (timeToRed) (+ (v) (vmax))) (* (2) (x))))))))) (and (< (v) (vmax)) (or (< (intersection) (x)) (or (and (> (intersection) (x)) (or (> (* (* (2) (B)) (+ (intersection) (* (-1) (x)))) (^ (v) (2))) (< (* (intersection) (v)) (* (v) (+ (* (timeToRed) (v)) (x)))))) (and (> (timeToRed) (0)) (= (intersection) (x)))))))))" "(and (>= v 0) (and (> A 0) (and (> B 0) (and (> T 0) (> vmax 0)))))"`
 
+## Generating a Binary
+To generate a binary, in the folder algebraic_simplification_cesar, run
+`cargo build --release`.
+This creates the executable `simplify` in the folder `target`.
+
+## Calling Rust from Python
+Before you begin, ensure you have the following installed:
+- Python
+- Rust and Cargo (Rust's package manager)
+- Maturin (for building and publishing Rust crates as Python packages)
+
+### Step 1: Setting Up Environment
+
+Create a virtual environment:
+```
+python3 -m venv .env  
+source .env/bin/activate
+```
+### Step 2: Installing Maturin
+```
+pip install maturin
+```
+
+Inside the directory, now run `maturin init`. This will generate the new package source. When given the choice of bindings to use, select pyo3 bindings:
+```
+$ maturin init
+✔ 🤷 Which kind of bindings to use?
+  📖 Documentation: https://maturin.rs/bindings.html · pyo3
+  ✨ Done! Initialized project /your/path
+```
+
+### Step 3: Building and Installing the Python Module
+
+This will build the package and install it into the Python virtualenv previously created and activated. The package is then ready to be used from `python`:
+```
+maturin develop
+```
+
+An example output would be:
+```
+📦 Including license file "/path/to/project/LICENSE"
+🔗 Found pyo3 bindings
+🐍 Found CPython 3.12 at /path/to/project/.env/bin/python
+📡 Using build options features from pyproject.toml
+    Finished `dev` profile [unoptimized + debuginfo] target(s) in 0.21s
+📦 Built wheel for CPython 3.12 to /var/folders/.../algebraic_simplification_cesar-0.1.0-cp312-cp312-macosx_10_12_x86_64.whl
+✏️  Setting installed package as editable
+🛠 Installed algebraic_simplification_cesar-0.1.0
+```
+
+### Step 4: Using the Python Module
+
+Open a Python Shell:
+```
+python
+```
+Import and Use the Module:
+```
+import simplify
+simplify.aggressive_simplify("formula","assumption")
+```
+
+### References
+
+For more detailed information on using PyO3, refer to the [official PyO3 guide](https://github.com/PyO3/pyo3).
+
+
 ## More Information
 This tool was designed to collapse redundant cells resulting from performing [quanitifier elimination](https://reference.wolfram.com/language/ref/Resolve.html), but can work for other simplification applications as well. It is used by the [CESAR](https://arxiv.org/abs/2311.02833) tool.

pyproject.toml

@@ -0,0 +1,15 @@
+[build-system]
+requires = ["maturin>=1.7,<2.0"]
+build-backend = "maturin"
+
+[project]
+name = "algebraic_simplification_cesar"
+requires-python = ">=3.8"
+classifiers = [
+    "Programming Language :: Rust",
+    "Programming Language :: Python :: Implementation :: CPython",
+    "Programming Language :: Python :: Implementation :: PyPy",
+]
+dynamic = ["version"]
+[tool.maturin]
+features = ["pyo3/extension-module"]

src/lib.rs

@@ -0,0 +1,23 @@
+use pyo3::prelude::*;
+
+// Exposes the cesar module to the crate root
+pub mod cesar;
+
+#[pyfunction]
+fn light_simplify(expr: String, assumptions: String) -> PyResult<()> {
+    crate::cesar::simplify::light_simplify(expr, assumptions);
+    Ok(())
+}
+
+#[pyfunction]
+fn aggressive_simplify(expr: String, assumptions: String) -> PyResult<()> {
+    crate::cesar::simplify::aggressive_simplify(expr, assumptions);
+    Ok(())
+}
+
+#[pymodule]
+fn simplify(_py: Python, m: &PyModule) -> PyResult<()> {
+    m.add_function(wrap_pyfunction!(light_simplify, m)?)?;
+    m.add_function(wrap_pyfunction!(aggressive_simplify, m)?)?;
+    Ok(())
+}