Add Python-bindings for parsing module

.github/workflows/release.yml

@@ -0,0 +1,101 @@
+name: python release
+
+on:
+  push:
+    tags:
+      - "v[0-9]+.[0-9]+.[0-9]+"
+
+permissions:
+  contents: write
+
+jobs:
+  create-release:
+    name: create-release
+    runs-on: ubuntu-22.04
+    steps:
+      - uses: actions/checkout@v4
+      - name: Get the release version from the tag
+        if: env.VERSION == ''
+        run: echo "VERSION=${{ github.ref_name }}" >> $GITHUB_ENV
+    outputs:
+      version: ${{ env.VERSION }}
+
+  linux:
+    runs-on: ubuntu-22.04
+    needs: ["create-release"]
+
+    strategy:
+      matrix:
+        target: [x86_64, aarch64]
+    steps:
+      - uses: actions/checkout@v4
+      - uses: actions/setup-python@v5
+        with:
+          python-version: "3.10"
+      - name: Build wheels
+        uses: PyO3/maturin-action@v1
+        with:
+          target: ${{ matrix.target }}
+          args: --release --manifest-path python/Cargo.toml --out dist --find-interpreter
+          sccache: "true"
+          manylinux: auto
+      - name: Upload wheels
+        uses: actions/upload-artifact@v4
+        with:
+          name: wheels-linux-${{ matrix.target }}
+          path: dist
+
+  macos:
+    runs-on: macos-latest
+    needs: ["create-release"]
+    strategy:
+      matrix:
+        target: [x86_64, aarch64]
+    steps:
+      - uses: actions/checkout@v4
+      - uses: actions/setup-python@v5
+        with:
+          python-version: "3.10"
+      - name: Build wheels
+        uses: PyO3/maturin-action@v1
+        with:
+          target: ${{ matrix.target }}
+          args: --release --manifest-path python/Cargo.toml --out dist --find-interpreter
+          sccache: "true"
+      - name: Upload wheels
+        uses: actions/upload-artifact@v4
+        with:
+          name: wheels-macos-${{ matrix.target }}
+          path: dist
+
+  sdist:
+    # switch back to ubuntu-22.04 once this issue is resolved:
+    # https://github.com/PyO3/maturin-action/issues/291
+    runs-on: ubuntu-22.04
+    steps:
+      - uses: actions/checkout@v4
+      - name: Build sdist
+        uses: PyO3/maturin-action@v1
+        with:
+          command: sdist
+          args: --manifest-path python/Cargo.toml --out dist
+      - name: Upload sdist
+        uses: actions/upload-artifact@v4
+        with:
+          name: wheels-sdist
+          path: dist
+
+  release:
+    name: Release
+    runs-on: ubuntu-22.04
+    if: "startsWith(github.ref, 'refs/tags/')"
+    needs: [linux, 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-*/*

.github/workflows/test.yml

@@ -201,6 +201,33 @@ jobs:
       - name: run
         run: cargo run --release -p simplify -- inputs/smtlib/arbiter_array_cex_w32d32q16n4b34.smt2 out.smt
 
+  python:
+    name: Test Python Bindings
+    runs-on: ubuntu-24.04
+    timeout-minutes: 5
+    strategy:
+      matrix:
+        toolchain:
+          - stable
+        python:
+          - "3.10"
+
+    steps:
+      - name: Update Rust to ${{ matrix.toolchain }}
+        run: rustup update ${{ matrix.toolchain }} && rustup default ${{ matrix.toolchain }}
+      - name: Install z3, CVC5, boolector
+        run: sudo apt install -y z3 cvc5 boolector
+      - name: Install uv and set the Python version
+        uses: astral-sh/setup-uv@v6
+        with:
+          python-version: ${{ matrix.python }}
+      - uses: actions/checkout@v4
+      - name: Install the project
+        working-directory: python
+        run: uv sync --locked --all-extras --dev
+      - name: Test
+        working-directory: python
+        run: uv run pytest
 
   semver:
     name: Check Semantic Versioning of Patronus

.gitignore

@@ -7,3 +7,7 @@ Cargo.lock
 /perf.data
 /perf.data.old
 replay.smt
+
+
+# Python
+__pycache__/

Cargo.toml

@@ -1,6 +1,6 @@
 [workspace]
 resolver = "2"
-members = ["patronus", "patronus-egraphs", "patronus-dse", "tools/bmc", "tools/egraphs-cond-synth", "tools/sim", "tools/simplify", "tools/view"]
+members = ["patronus", "patronus-egraphs", "patronus-dse", "tools/bmc", "tools/egraphs-cond-synth", "tools/sim", "tools/simplify", "tools/view", "python"]
 
 [workspace.package]
 edition = "2024"
@@ -9,6 +9,8 @@ repository = "https://github.com/cucapra/patronus"
 readme = "Readme.md"
 license = "BSD-3-Clause"
 rust-version = "1.85.0"
+# used by main patronus library and python bindings
+version = "0.34.1"
 
 [workspace.dependencies]
 rustc-hash = "2.x"

patronus/Cargo.toml

@@ -1,6 +1,6 @@
 [package]
 name = "patronus"
-version = "0.34.1"
+version.workspace = true
 description = "Hardware bug-finding toolkit."
 homepage = "https://kevinlaeufer.com"
 keywords = ["RTL", "btor", "model-checking", "SMT", "bit-vector"]

patronus/src/expr/context.rs

@@ -142,6 +142,24 @@ impl Index<StringRef> for Context {
     }
 }
 
+impl Context {
+    /// Returns the number of interned expressions in this context.
+    pub fn num_exprs(&self) -> usize {
+        self.exprs.len()
+    }
+
+    /// Returns a reference to the expression for the given reference.
+    /// Panics if the reference is invalid (use indices in range 0..num_exprs()).
+    pub fn get_expr(&self, r: ExprRef) -> &Expr {
+        &self[r]
+    }
+
+    /// Returns the zero-based intern index of the given expression reference.
+    pub fn expr_index(&self, r: ExprRef) -> usize {
+        r.index()
+    }
+}
+
 /// Convenience methods to construct IR nodes.
 impl Context {
     // helper functions to construct expressions

patronus/src/mc/smt.rs

@@ -42,6 +42,12 @@ impl<S: Solver<std::fs::File>> SmtModelChecker<S> {
         k_max: u64,
     ) -> Result<ModelCheckResult> {
         assert!(k_max > 0 && k_max <= 2000, "unreasonable k_max={}", k_max);
+
+        // if there are no assertions, there cannot be an error!
+        if sys.bad_states.is_empty() {
+            return Ok(ModelCheckResult::Success);
+        }
+
         let replay_file = if self.opts.save_smt_replay {
             Some(std::fs::File::create("replay.smt")?)
         } else {

patronus/src/smt.rs

@@ -7,6 +7,6 @@ mod parser;
 mod serialize;
 mod solver;
 
-pub use parser::{parse_command, parse_expr};
+pub use parser::{SmtParserError, parse_command, parse_expr};
 pub use serialize::serialize_cmd;
 pub use solver::*;

patronus/src/smt/solver.rs

@@ -416,6 +416,15 @@ pub const YICES2: SmtLibSolver = SmtLibSolver {
     supports_const_array: false,
 };
 
+pub const Z3: SmtLibSolver = SmtLibSolver {
+    name: "z3",
+    args: &["-in"],
+    options: &[],
+    supports_uf: true,
+    supports_check_assuming: true,
+    supports_const_array: true,
+};
+
 #[cfg(test)]
 mod tests {
     use super::*;

patronus/src/system/transition_system.rs

@@ -5,7 +5,7 @@
 use crate::expr::{Context, ExprMap, ExprRef, SparseExprMap, StringRef};
 use rustc_hash::{FxHashMap, FxHashSet};
 
-#[derive(Debug, PartialEq, Eq, Clone, Hash)]
+#[derive(Debug, PartialEq, Eq, Clone, Hash, Copy)]
 pub struct State {
     pub symbol: ExprRef,
     pub init: Option<ExprRef>,

python/Cargo.toml

@@ -0,0 +1,18 @@
+[package]
+name = "pypatronus"
+description = "PyO3 bindings for Patronus"
+version.workspace = true
+rust-version.workspace = true
+edition.workspace = true
+license.workspace = true
+
+[lib]
+name = "pypatronus"
+crate-type = ["cdylib"]
+
+[dependencies]
+pyo3 = { version = "0.26.0" , features = ["num-bigint"]}
+patronus = { path = "../patronus" }
+baa = { version = "0.17.1", features = ["rand1", "bigint"] }
+num-bigint = "0.4.6"
+rustc-hash.workspace = true

python/pyproject.toml

@@ -0,0 +1,34 @@
+[project]
+name = "pypatronus"
+requires-python = ">=3.9"
+dynamic = ["version"]
+license = "BSD-3-Clause"
+description = "The hardware bug-finding toolkit for Python programmers."
+authors = [
+    { name = "Adwait Godbole", email = "adwait@berkeley.edu" },
+    { name = "Kevin Laeufer", email = "laeufer@cornell.edu" },
+]
+classifiers = [
+    "Programming Language :: Rust",
+    "Programming Language :: Python",
+    "License :: OSI Approved :: BSD License"
+]
+
+[project.urls]
+Homepage = "https://github.com/cucapra/patronus"
+Issues = "https://github.com/cucapra/patronus/issues"
+
+[build-system]
+requires = ["maturin>=1.5,<2.0"]
+build-backend = "maturin"
+
+[tool.maturin]
+features = ["pyo3/extension-module"]
+
+[dependency-groups]
+dev = [
+    "pytest>=8.4.2",
+]
+
+[tool.uv]
+cache-keys = [{file = "pyproject.toml"}, {file = "Cargo.toml"}, {file = "src/*.rs"}]

python/src/ctx.rs

@@ -0,0 +1,79 @@
+// Copyright 2025 Cornell University
+// released under BSD 3-Clause License
+// author: Kevin Laeufer <laeufer@cornell.edu>
+
+use pyo3::prelude::*;
+use std::ops::{Deref, DerefMut};
+use std::sync::{LazyLock, RwLock, RwLockReadGuard, RwLockWriteGuard};
+
+/// Context that is used by default for all operations.
+/// Python usage is expected to be less performance critical, so using a single global
+/// context seems acceptable and will simplify use.
+static DEFAULT_CONTEXT: LazyLock<RwLock<::patronus::expr::Context>> =
+    LazyLock::new(|| RwLock::new(::patronus::expr::Context::default()));
+
+/// Exposes the Context object to python
+#[pyclass]
+pub struct Context(::patronus::expr::Context);
+
+pub(crate) enum ContextGuardWrite<'a> {
+    // TODO: reintroduce local context support!
+    // Local(&'a mut Context),
+    Shared(RwLockWriteGuard<'a, ::patronus::expr::Context>),
+}
+
+// TODO: reintroduce local context support!
+// impl<'a> From<Option<&'a mut Context>> for ContextGuardWrite<'a> {
+//     fn from(value: Option<&'a mut Context>) -> Self {
+//         value
+//             .map(|ctx| Self::Local(ctx))
+//             .unwrap_or_else(|| Self::Shared(DEFAULT_CONTEXT.write().unwrap()))
+//     }
+// }
+
+impl<'a> Default for ContextGuardWrite<'a> {
+    fn default() -> Self {
+        Self::Shared(DEFAULT_CONTEXT.write().unwrap())
+    }
+}
+
+impl<'a> ContextGuardWrite<'a> {
+    pub fn deref_mut(&mut self) -> &mut ::patronus::expr::Context {
+        match self {
+            // TODO: reintroduce local context support!
+            // Self::Local(ctx) => &mut ctx.0,
+            Self::Shared(guard) => guard.deref_mut(),
+        }
+    }
+}
+
+pub(crate) enum ContextGuardRead<'a> {
+    // TODO: reintroduce local context support!
+    // Local(&'a Context),
+    Shared(RwLockReadGuard<'a, ::patronus::expr::Context>),
+}
+
+// TODO: reintroduce local context support!
+// impl<'a> From<Option<&'a mut Context>> for ContextGuardRead<'a> {
+//     fn from(value: Option<&'a mut Context>) -> Self {
+//         value
+//             .map(|ctx| Self::Local(ctx))
+//             .unwrap_or_else(|| Self::default())
+//     }
+// }
+
+impl<'a> Default for ContextGuardRead<'a> {
+    fn default() -> Self {
+        Self::Shared(DEFAULT_CONTEXT.read().unwrap())
+    }
+}
+
+impl<'a> ContextGuardRead<'a> {
+    pub fn deref(&self) -> &::patronus::expr::Context {
+        match self {
+            // TODO: reintroduce local context support!
+            // Self::Local(ctx) => &ctx.0,
+            Self::Shared(guard) => guard.deref(),
+        }
+    }
+}