From cf6274b9751feb17dbdf08e901e5e33eded2e8b9 Mon Sep 17 00:00:00 2001 From: adwait Date: Sun, 12 Oct 2025 20:43:02 -0700 Subject: [PATCH 01/24] Add Python-bindings for parsing module - use PyO3 package in rust - expose the Expr class as a python dictionary - expose the parse function (with indexing using a Python int ExprRef) Signed-off-by: adwait --- .gitignore | 29 ++ Cargo.toml | 2 +- patronus/src/expr/context.rs | 18 ++ python/patronus_btor/Cargo.toml | 15 + python/patronus_btor/pyproject.toml | 17 ++ python/patronus_btor/setup.py | 16 + python/patronus_btor/src/lib.rs | 363 +++++++++++++++++++++++ python/patronus_btor/tests/test_quiz1.py | 71 +++++ 8 files changed, 530 insertions(+), 1 deletion(-) create mode 100644 python/patronus_btor/Cargo.toml create mode 100644 python/patronus_btor/pyproject.toml create mode 100644 python/patronus_btor/setup.py create mode 100644 python/patronus_btor/src/lib.rs create mode 100644 python/patronus_btor/tests/test_quiz1.py diff --git a/.gitignore b/.gitignore index 93c8763..4754a30 100644 --- a/.gitignore +++ b/.gitignore @@ -7,3 +7,32 @@ Cargo.lock /perf.data /perf.data.old replay.smt + + +# Python +__pycache__/ +*.pyc +*.pyo +*.pyd +*.pdb +*.egg-info/ +.eggs/ +dist/ +build/ +*.egg +.env +.python-version +venv/ +env/ +ENV/ +env.bak/ +venv.bak/ +.ipynb_checkpoints +.pytest_cache/ +.mypy_cache/ +.pyre/ +.pytype/ +.coverage + +# C extensions +*.so \ No newline at end of file diff --git a/Cargo.toml b/Cargo.toml index 638417c..d5c3205 100644 --- a/Cargo.toml +++ b/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/patronus_btor"] [workspace.package] edition = "2024" diff --git a/patronus/src/expr/context.rs b/patronus/src/expr/context.rs index fa936f2..2039112 100644 --- a/patronus/src/expr/context.rs +++ b/patronus/src/expr/context.rs @@ -142,6 +142,24 @@ impl Index 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 diff --git a/python/patronus_btor/Cargo.toml b/python/patronus_btor/Cargo.toml new file mode 100644 index 0000000..2197d1d --- /dev/null +++ b/python/patronus_btor/Cargo.toml @@ -0,0 +1,15 @@ +[package] +name = "patronus_btor" +version = "0.1.0" +edition = "2024" +description = "PyO3 bindings for Patronus BTOR parsing" +license = "BSD-3-Clause" + +[lib] +name = "patronus_btor" +crate-type = ["cdylib"] + +[dependencies] +pyo3 = { version = "0.22", features = ["extension-module"] } +patronus = { path = "../../patronus" } +baa = "0.17.1" diff --git a/python/patronus_btor/pyproject.toml b/python/patronus_btor/pyproject.toml new file mode 100644 index 0000000..4ce54e4 --- /dev/null +++ b/python/patronus_btor/pyproject.toml @@ -0,0 +1,17 @@ +[build-system] +requires = ["setuptools>=64", "wheel", "setuptools-rust>=1.8"] +build-backend = "setuptools.build_meta" + +[project] +name = "patronus-btor" +version = "0.1.0" +description = "PyO3 bindings for Patronus BTOR parsing" +readme = "README.md" +requires-python = ">=3.8" +authors = [{ name = "Patronus Authors" }] +license = { text = "BSD-3-Clause" } +classifiers = [ + "Programming Language :: Rust", + "Programming Language :: Python", + "License :: OSI Approved :: BSD License" +] diff --git a/python/patronus_btor/setup.py b/python/patronus_btor/setup.py new file mode 100644 index 0000000..993b120 --- /dev/null +++ b/python/patronus_btor/setup.py @@ -0,0 +1,16 @@ +from setuptools import setup +from setuptools_rust import Binding, RustExtension + +setup( + name="patronus-btor", + version="0.1.0", + description="PyO3 bindings for Patronus BTOR parsing", + rust_extensions=[ + RustExtension( + "patronus_btor", + path="Cargo.toml", + binding=Binding.PyO3, + ) + ], + zip_safe=False, +) diff --git a/python/patronus_btor/src/lib.rs b/python/patronus_btor/src/lib.rs new file mode 100644 index 0000000..f7cd38e --- /dev/null +++ b/python/patronus_btor/src/lib.rs @@ -0,0 +1,363 @@ +use pyo3::exceptions::{PyIOError, PyIndexError, PyValueError}; +use pyo3::prelude::*; +use baa::BitVecOps; +use patronus::btor2; +use patronus::expr::{Context, Expr, ExprRef}; +use patronus::system::TransitionSystem; + +#[pyclass] +pub struct Design { + ctx: Context, + sys: TransitionSystem, +} + +#[pymethods] +impl Design { + fn __len__(&self) -> usize { + self.ctx.num_exprs() + } + + fn __getitem__(&self, idx: isize, py: Python<'_>) -> PyResult { + let n = self.ctx.num_exprs() as isize; + let mut i = idx; + if i < 0 { + i += n; + } + if i < 0 || i >= n { + return Err(PyIndexError::new_err(format!( + "index {idx} out of range for length {n}" + ))); + } + let idx_u = i as usize; + let r = ExprRef::from_index(idx_u); + let e = self.ctx.get_expr(r); + let d = expr_to_dict(py, e, &self.ctx)?; + Ok(d) + } + + // Optional convenience: number of roots of various categories + #[pyo3(name = "num_states")] + fn num_states_py(&self) -> usize { + self.sys.states.len() + } + + #[pyo3(name = "num_inputs")] + fn num_inputs_py(&self) -> usize { + self.sys.inputs.len() + } + + #[pyo3(name = "num_outputs")] + fn num_outputs_py(&self) -> usize { + self.sys.outputs.len() + } + + // Optional: names available at the system level + #[pyo3(name = "name")] + fn name_py(&self) -> String { + self.sys.name.clone() + } + + // Convenience lists for Python traversal + #[pyo3(name = "inputs")] + fn inputs_py(&self) -> Vec { + self.sys + .inputs + .iter() + .map(|&e| self.ctx.expr_index(e)) + .collect() + } + + #[pyo3(name = "states")] + fn states_py(&self) -> Vec { + self.sys + .states + .iter() + .map(|s| self.ctx.expr_index(s.symbol)) + .collect() + } + + #[pyo3(name = "outputs")] + fn outputs_py(&self) -> Vec { + self.sys + .outputs + .iter() + .map(|o| self.ctx.expr_index(o.expr)) + .collect() + } + + #[pyo3(name = "find_symbol")] + fn find_symbol_py(&self, name: &str) -> Option { + let map = self.sys.get_name_map(&self.ctx); + map.get(name).map(|&e| self.ctx.expr_index(e)) + } +} + +#[pyfunction] +pub fn parse(path: &str) -> PyResult { + // Robust path: avoid panics from parse_file_with_ctx File::open(...).expect(...) + let contents = std::fs::read_to_string(path) + .map_err(|e| PyIOError::new_err(format!("I/O error reading '{path}': {e}")))?; + let mut ctx = Context::default(); + let name = std::path::Path::new(path) + .file_stem() + .and_then(|s| s.to_str()); + match btor2::parse_str(&mut ctx, &contents, name) { + Some(sys) => Ok(Design { ctx, sys }), + None => Err(PyValueError::new_err(format!( + "Parse failed for BTOR file: {path}" + ))), + } +} + +#[pymodule] +fn patronus_btor(_py: Python<'_>, m: &pyo3::Bound<'_, pyo3::types::PyModule>) -> PyResult<()> { + m.add_class::()?; + m.add_function(wrap_pyfunction!(parse, m)?)?; + Ok(()) +} + +// Helpers + +fn expr_to_dict(py: Python<'_>, e: &Expr, ctx: &Context) -> PyResult { + let d = pyo3::types::PyDict::new_bound(py); + + macro_rules! set { + ($k:expr, $v:expr) => { + d.set_item($k, $v)? + }; + } + macro_rules! idx { + ($r:expr) => { + ctx.expr_index($r) + }; + } + + match e { + // Bit-Vector Expressions + Expr::BVSymbol { name, width } => { + set!("kind", "BVSymbol"); + set!("name", ctx[*name].as_str()); + set!("width", *width as u64); + } + Expr::BVLiteral(v) => { + set!("kind", "BVLiteral"); + let w = v.width(); + let value = v.get(ctx); + // mimic serialize.rs formatting + let s = if w <= 8 { + format!("{}'b{}", w, value.to_bit_str()) + } else { + format!("{}'x{}", w, value.to_hex_str()) + }; + set!("width", w as u64); + set!("value", s); + // Also expose numeric hex without width prefix for convenience + set!("hex", value.to_hex_str()); + } + // unary with explicit fields + Expr::BVZeroExt { e, by, width } => { + set!("kind", "BVZeroExt"); + set!("e", idx!(*e)); + set!("by", *by as u64); + set!("width", *width as u64); + } + Expr::BVSignExt { e, by, width } => { + set!("kind", "BVSignExt"); + set!("e", idx!(*e)); + set!("by", *by as u64); + set!("width", *width as u64); + } + Expr::BVSlice { e, hi, lo } => { + set!("kind", "BVSlice"); + set!("e", idx!(*e)); + set!("hi", *hi as u64); + set!("lo", *lo as u64); + } + Expr::BVNot(e, width) => { + set!("kind", "BVNot"); + set!("e", idx!(*e)); + set!("width", *width as u64); + } + Expr::BVNegate(e, width) => { + set!("kind", "BVNegate"); + set!("e", idx!(*e)); + set!("width", *width as u64); + } + // binary logical/compare/arithmetic + Expr::BVEqual(a, b) => { + set!("kind", "BVEqual"); + set!("a", idx!(*a)); + set!("b", idx!(*b)); + } + Expr::BVImplies(a, b) => { + set!("kind", "BVImplies"); + set!("a", idx!(*a)); + set!("b", idx!(*b)); + } + Expr::BVGreater(a, b) => { + set!("kind", "BVGreater"); + set!("a", idx!(*a)); + set!("b", idx!(*b)); + } + Expr::BVGreaterSigned(a, b, width) => { + set!("kind", "BVGreaterSigned"); + set!("a", idx!(*a)); + set!("b", idx!(*b)); + set!("width", *width as u64); + } + Expr::BVGreaterEqual(a, b) => { + set!("kind", "BVGreaterEqual"); + set!("a", idx!(*a)); + set!("b", idx!(*b)); + } + Expr::BVGreaterEqualSigned(a, b, width) => { + set!("kind", "BVGreaterEqualSigned"); + set!("a", idx!(*a)); + set!("b", idx!(*b)); + set!("width", *width as u64); + } + Expr::BVConcat(a, b, width) => { + set!("kind", "BVConcat"); + set!("a", idx!(*a)); + set!("b", idx!(*b)); + set!("width", *width as u64); + } + Expr::BVAnd(a, b, width) => { + set!("kind", "BVAnd"); + set!("a", idx!(*a)); + set!("b", idx!(*b)); + set!("width", *width as u64); + } + Expr::BVOr(a, b, width) => { + set!("kind", "BVOr"); + set!("a", idx!(*a)); + set!("b", idx!(*b)); + set!("width", *width as u64); + } + Expr::BVXor(a, b, width) => { + set!("kind", "BVXor"); + set!("a", idx!(*a)); + set!("b", idx!(*b)); + set!("width", *width as u64); + } + Expr::BVShiftLeft(a, b, width) => { + set!("kind", "BVShiftLeft"); + set!("a", idx!(*a)); + set!("b", idx!(*b)); + set!("width", *width as u64); + } + Expr::BVArithmeticShiftRight(a, b, width) => { + set!("kind", "BVArithmeticShiftRight"); + set!("a", idx!(*a)); + set!("b", idx!(*b)); + set!("width", *width as u64); + } + Expr::BVShiftRight(a, b, width) => { + set!("kind", "BVShiftRight"); + set!("a", idx!(*a)); + set!("b", idx!(*b)); + set!("width", *width as u64); + } + Expr::BVAdd(a, b, width) => { + set!("kind", "BVAdd"); + set!("a", idx!(*a)); + set!("b", idx!(*b)); + set!("width", *width as u64); + } + Expr::BVMul(a, b, width) => { + set!("kind", "BVMul"); + set!("a", idx!(*a)); + set!("b", idx!(*b)); + set!("width", *width as u64); + } + Expr::BVSignedDiv(a, b, width) => { + set!("kind", "BVSignedDiv"); + set!("a", idx!(*a)); + set!("b", idx!(*b)); + set!("width", *width as u64); + } + Expr::BVUnsignedDiv(a, b, width) => { + set!("kind", "BVUnsignedDiv"); + set!("a", idx!(*a)); + set!("b", idx!(*b)); + set!("width", *width as u64); + } + Expr::BVSignedMod(a, b, width) => { + set!("kind", "BVSignedMod"); + set!("a", idx!(*a)); + set!("b", idx!(*b)); + set!("width", *width as u64); + } + Expr::BVSignedRem(a, b, width) => { + set!("kind", "BVSignedRem"); + set!("a", idx!(*a)); + set!("b", idx!(*b)); + set!("width", *width as u64); + } + Expr::BVUnsignedRem(a, b, width) => { + set!("kind", "BVUnsignedRem"); + set!("a", idx!(*a)); + set!("b", idx!(*b)); + set!("width", *width as u64); + } + Expr::BVSub(a, b, width) => { + set!("kind", "BVSub"); + set!("a", idx!(*a)); + set!("b", idx!(*b)); + set!("width", *width as u64); + } + Expr::BVArrayRead { array, index, width } => { + set!("kind", "BVArrayRead"); + set!("array", idx!(*array)); + set!("index", idx!(*index)); + set!("width", *width as u64); + } + Expr::BVIte { cond, tru, fals } => { + set!("kind", "BVIte"); + set!("cond", idx!(*cond)); + set!("tru", idx!(*tru)); + set!("fals", idx!(*fals)); + } + + // Array Expressions + Expr::ArraySymbol { + name, + index_width, + data_width, + } => { + set!("kind", "ArraySymbol"); + set!("name", ctx[*name].as_str()); + set!("index_width", *index_width as u64); + set!("data_width", *data_width as u64); + } + Expr::ArrayConstant { + e, + index_width, + data_width, + } => { + set!("kind", "ArrayConstant"); + set!("e", idx!(*e)); + set!("index_width", *index_width as u64); + set!("data_width", *data_width as u64); + } + Expr::ArrayEqual(a, b) => { + set!("kind", "ArrayEqual"); + set!("a", idx!(*a)); + set!("b", idx!(*b)); + } + Expr::ArrayStore { array, index, data } => { + set!("kind", "ArrayStore"); + set!("array", idx!(*array)); + set!("index", idx!(*index)); + set!("data", idx!(*data)); + } + Expr::ArrayIte { cond, tru, fals } => { + set!("kind", "ArrayIte"); + set!("cond", idx!(*cond)); + set!("tru", idx!(*tru)); + set!("fals", idx!(*fals)); + } + } + + Ok(d.into_py(py)) +} diff --git a/python/patronus_btor/tests/test_quiz1.py b/python/patronus_btor/tests/test_quiz1.py new file mode 100644 index 0000000..0ea2866 --- /dev/null +++ b/python/patronus_btor/tests/test_quiz1.py @@ -0,0 +1,71 @@ +import pathlib +import pytest + +from patronus_btor import parse + + +def repo_root() -> pathlib.Path: + # this file: repo/python/patronus_btor/tests/test_quiz1.py + # parents[0]=tests, [1]=patronus_btor, [2]=python, [3]=repo root + return pathlib.Path(__file__).resolve().parents[3] + + +def test_parse_and_index_quiz1(): + btor_path = repo_root() / "inputs" / "chiseltest" / "Quiz1.btor" + assert btor_path.is_file(), f"missing BTOR test input at {btor_path}" + + design = parse(str(btor_path)) + n = len(design) + assert n > 0 + + # Index access for a handful of nodes should return a dict with at least a 'kind' + sample_count = min(n, 50) + saw_symbol = False + saw_literal = False + saw_op_with_children = False + + for i in range(sample_count): + node = design[i] + assert isinstance(node, dict), f"node {i} is not a dict" + assert "kind" in node, f"node {i} missing 'kind'" + k = node["kind"] + + if k == "BVSymbol" or k == "ArraySymbol": + assert "name" in node and isinstance(node["name"], str) + saw_symbol = True + + if k == "BVLiteral": + assert "width" in node and "value" in node + saw_literal = True + + # Check a few common ops have integer child refs + if k in {"BVAdd", "BVAnd", "BVOr", "BVEqual", "BVNot", "BVIte", "BVSlice"}: + # Determine expected child fields + if k in {"BVAdd", "BVAnd", "BVOr", "BVEqual"}: + assert isinstance(node["a"], int) and isinstance(node["b"], int) + saw_op_with_children = True + elif k == "BVNot": + assert isinstance(node["e"], int) + saw_op_with_children = True + elif k == "BVIte": + assert isinstance(node["cond"], int) + assert isinstance(node["tru"], int) + assert isinstance(node["fals"], int) + saw_op_with_children = True + elif k == "BVSlice": + assert isinstance(node["e"], int) + assert isinstance(node["hi"], int) + assert isinstance(node["lo"], int) + saw_op_with_children = True + + assert saw_symbol, "did not encounter any symbol nodes in the first batch" + assert saw_literal, "did not encounter any literal nodes in the first batch" + assert saw_op_with_children, "did not encounter any ops with children in the first batch" + + +def test_out_of_range_index_raises(): + # Use a tiny BTOR file to parse, then index out of bounds + btor_path = repo_root() / "inputs" / "chiseltest" / "Quiz1.btor" + design = parse(str(btor_path)) + with pytest.raises(IndexError): + _ = design[len(design)] From 9be9d34ee7cbbda7f17eb09704bc65b67f75f17c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Kevin=20L=C3=A4ufer?= Date: Wed, 15 Oct 2025 13:47:48 -0400 Subject: [PATCH 02/24] python binding: make part of workspace, rename to patronus --- .gitignore | 26 ++-------------- Cargo.toml | 4 ++- patronus/Cargo.toml | 2 +- python/Cargo.toml | 16 ++++++++++ python/patronus_btor/Cargo.toml | 15 --------- python/patronus_btor/pyproject.toml | 17 ---------- python/patronus_btor/setup.py | 16 ---------- python/pyproject.toml | 31 +++++++++++++++++++ python/{patronus_btor => }/src/lib.rs | 21 ++++++++----- .../{patronus_btor => }/tests/test_quiz1.py | 11 +++---- 10 files changed, 70 insertions(+), 89 deletions(-) create mode 100644 python/Cargo.toml delete mode 100644 python/patronus_btor/Cargo.toml delete mode 100644 python/patronus_btor/pyproject.toml delete mode 100644 python/patronus_btor/setup.py create mode 100644 python/pyproject.toml rename python/{patronus_btor => }/src/lib.rs (96%) rename python/{patronus_btor => }/tests/test_quiz1.py (85%) diff --git a/.gitignore b/.gitignore index 4754a30..7bc8c8f 100644 --- a/.gitignore +++ b/.gitignore @@ -11,28 +11,6 @@ replay.smt # Python __pycache__/ -*.pyc -*.pyo -*.pyd -*.pdb -*.egg-info/ -.eggs/ -dist/ -build/ -*.egg -.env -.python-version -venv/ -env/ -ENV/ -env.bak/ -venv.bak/ -.ipynb_checkpoints -.pytest_cache/ -.mypy_cache/ -.pyre/ -.pytype/ -.coverage -# C extensions -*.so \ No newline at end of file +# UV lock files +uv.lock diff --git a/Cargo.toml b/Cargo.toml index d5c3205..34c2973 100644 --- a/Cargo.toml +++ b/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", "python/patronus_btor"] +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" diff --git a/patronus/Cargo.toml b/patronus/Cargo.toml index b06a21a..2e7a70f 100644 --- a/patronus/Cargo.toml +++ b/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"] diff --git a/python/Cargo.toml b/python/Cargo.toml new file mode 100644 index 0000000..9f5e9dd --- /dev/null +++ b/python/Cargo.toml @@ -0,0 +1,16 @@ +[package] +name = "patronus_py" +description = "PyO3 bindings for Patronus" +version.workspace = true +rust-version.workspace = true +edition.workspace = true +license.workspace = true + +[lib] +name = "patronus" +crate-type = ["cdylib"] + +[dependencies] +pyo3 = { version = "0.26.0" } +patronus = { path = "../patronus" } +baa.workspace = true diff --git a/python/patronus_btor/Cargo.toml b/python/patronus_btor/Cargo.toml deleted file mode 100644 index 2197d1d..0000000 --- a/python/patronus_btor/Cargo.toml +++ /dev/null @@ -1,15 +0,0 @@ -[package] -name = "patronus_btor" -version = "0.1.0" -edition = "2024" -description = "PyO3 bindings for Patronus BTOR parsing" -license = "BSD-3-Clause" - -[lib] -name = "patronus_btor" -crate-type = ["cdylib"] - -[dependencies] -pyo3 = { version = "0.22", features = ["extension-module"] } -patronus = { path = "../../patronus" } -baa = "0.17.1" diff --git a/python/patronus_btor/pyproject.toml b/python/patronus_btor/pyproject.toml deleted file mode 100644 index 4ce54e4..0000000 --- a/python/patronus_btor/pyproject.toml +++ /dev/null @@ -1,17 +0,0 @@ -[build-system] -requires = ["setuptools>=64", "wheel", "setuptools-rust>=1.8"] -build-backend = "setuptools.build_meta" - -[project] -name = "patronus-btor" -version = "0.1.0" -description = "PyO3 bindings for Patronus BTOR parsing" -readme = "README.md" -requires-python = ">=3.8" -authors = [{ name = "Patronus Authors" }] -license = { text = "BSD-3-Clause" } -classifiers = [ - "Programming Language :: Rust", - "Programming Language :: Python", - "License :: OSI Approved :: BSD License" -] diff --git a/python/patronus_btor/setup.py b/python/patronus_btor/setup.py deleted file mode 100644 index 993b120..0000000 --- a/python/patronus_btor/setup.py +++ /dev/null @@ -1,16 +0,0 @@ -from setuptools import setup -from setuptools_rust import Binding, RustExtension - -setup( - name="patronus-btor", - version="0.1.0", - description="PyO3 bindings for Patronus BTOR parsing", - rust_extensions=[ - RustExtension( - "patronus_btor", - path="Cargo.toml", - binding=Binding.PyO3, - ) - ], - zip_safe=False, -) diff --git a/python/pyproject.toml b/python/pyproject.toml new file mode 100644 index 0000000..6c13c6a --- /dev/null +++ b/python/pyproject.toml @@ -0,0 +1,31 @@ +[project] +name = "patronus" +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", +] diff --git a/python/patronus_btor/src/lib.rs b/python/src/lib.rs similarity index 96% rename from python/patronus_btor/src/lib.rs rename to python/src/lib.rs index f7cd38e..123f60a 100644 --- a/python/patronus_btor/src/lib.rs +++ b/python/src/lib.rs @@ -1,9 +1,9 @@ +use ::patronus::btor2; +use ::patronus::expr::{Context, Expr, ExprRef}; +use ::patronus::system::TransitionSystem; +use baa::BitVecOps; use pyo3::exceptions::{PyIOError, PyIndexError, PyValueError}; use pyo3::prelude::*; -use baa::BitVecOps; -use patronus::btor2; -use patronus::expr::{Context, Expr, ExprRef}; -use patronus::system::TransitionSystem; #[pyclass] pub struct Design { @@ -110,7 +110,8 @@ pub fn parse(path: &str) -> PyResult { } #[pymodule] -fn patronus_btor(_py: Python<'_>, m: &pyo3::Bound<'_, pyo3::types::PyModule>) -> PyResult<()> { +#[pyo3(name = "patronus")] +fn patronus(_py: Python<'_>, m: &pyo3::Bound<'_, pyo3::types::PyModule>) -> PyResult<()> { m.add_class::()?; m.add_function(wrap_pyfunction!(parse, m)?)?; Ok(()) @@ -119,7 +120,7 @@ fn patronus_btor(_py: Python<'_>, m: &pyo3::Bound<'_, pyo3::types::PyModule>) -> // Helpers fn expr_to_dict(py: Python<'_>, e: &Expr, ctx: &Context) -> PyResult { - let d = pyo3::types::PyDict::new_bound(py); + let d = pyo3::types::PyDict::new(py); macro_rules! set { ($k:expr, $v:expr) => { @@ -306,7 +307,11 @@ fn expr_to_dict(py: Python<'_>, e: &Expr, ctx: &Context) -> PyResult { set!("b", idx!(*b)); set!("width", *width as u64); } - Expr::BVArrayRead { array, index, width } => { + Expr::BVArrayRead { + array, + index, + width, + } => { set!("kind", "BVArrayRead"); set!("array", idx!(*array)); set!("index", idx!(*index)); @@ -359,5 +364,5 @@ fn expr_to_dict(py: Python<'_>, e: &Expr, ctx: &Context) -> PyResult { } } - Ok(d.into_py(py)) + Ok(d.into()) } diff --git a/python/patronus_btor/tests/test_quiz1.py b/python/tests/test_quiz1.py similarity index 85% rename from python/patronus_btor/tests/test_quiz1.py rename to python/tests/test_quiz1.py index 0ea2866..d4337e2 100644 --- a/python/patronus_btor/tests/test_quiz1.py +++ b/python/tests/test_quiz1.py @@ -1,17 +1,14 @@ import pathlib import pytest -from patronus_btor import parse +from patronus import parse -def repo_root() -> pathlib.Path: - # this file: repo/python/patronus_btor/tests/test_quiz1.py - # parents[0]=tests, [1]=patronus_btor, [2]=python, [3]=repo root - return pathlib.Path(__file__).resolve().parents[3] +repo_root = (pathlib.Path(__file__) / '..' / '..' / '..').resolve() def test_parse_and_index_quiz1(): - btor_path = repo_root() / "inputs" / "chiseltest" / "Quiz1.btor" + btor_path = repo_root / "inputs" / "chiseltest" / "Quiz1.btor" assert btor_path.is_file(), f"missing BTOR test input at {btor_path}" design = parse(str(btor_path)) @@ -65,7 +62,7 @@ def test_parse_and_index_quiz1(): def test_out_of_range_index_raises(): # Use a tiny BTOR file to parse, then index out of bounds - btor_path = repo_root() / "inputs" / "chiseltest" / "Quiz1.btor" + btor_path = repo_root / "inputs" / "chiseltest" / "Quiz1.btor" design = parse(str(btor_path)) with pytest.raises(IndexError): _ = design[len(design)] From 6175217d3a5e94b4992c752f5efc74f0d1e11bae Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Kevin=20L=C3=A4ufer?= Date: Wed, 15 Oct 2025 13:55:44 -0400 Subject: [PATCH 03/24] ci: add python binding tests --- .github/workflows/test.yml | 25 +++++++++++++++++++++++++ 1 file changed, 25 insertions(+) diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml index 695cb44..4e45ce4 100644 --- a/.github/workflows/test.yml +++ b/.github/workflows/test.yml @@ -201,6 +201,31 @@ 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 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 From 999c0088632072c54a2087c2f9d7501b6a6fbe31 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Kevin=20L=C3=A4ufer?= Date: Wed, 15 Oct 2025 13:58:20 -0400 Subject: [PATCH 04/24] add uv lock --- .gitignore | 3 - python/uv.lock | 150 +++++++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 150 insertions(+), 3 deletions(-) create mode 100644 python/uv.lock diff --git a/.gitignore b/.gitignore index 7bc8c8f..ae14c3c 100644 --- a/.gitignore +++ b/.gitignore @@ -11,6 +11,3 @@ replay.smt # Python __pycache__/ - -# UV lock files -uv.lock diff --git a/python/uv.lock b/python/uv.lock new file mode 100644 index 0000000..50b6771 --- /dev/null +++ b/python/uv.lock @@ -0,0 +1,150 @@ +version = 1 +revision = 3 +requires-python = ">=3.9" + +[[package]] +name = "colorama" +version = "0.4.6" +source = { registry = "https://pypi.org/simple" } +sdist = { url = "https://files.pythonhosted.org/packages/d8/53/6f443c9a4a8358a93a6792e2acffb9d9d5cb0a5cfd8802644b7b1c9a02e4/colorama-0.4.6.tar.gz", hash = "sha256:08695f5cb7ed6e0531a20572697297273c47b8cae5a63ffc6d6ed5c201be6e44", size = 27697, upload-time = "2022-10-25T02:36:22.414Z" } +wheels = [ + { url = "https://files.pythonhosted.org/packages/d1/d6/3965ed04c63042e047cb6a3e6ed1a63a35087b6a609aa3a15ed8ac56c221/colorama-0.4.6-py2.py3-none-any.whl", hash = "sha256:4f1d9991f5acc0ca119f9d443620b77f9d6b33703e51011c16baf57afb285fc6", size = 25335, upload-time = "2022-10-25T02:36:20.889Z" }, +] + +[[package]] +name = "exceptiongroup" +version = "1.3.0" +source = { registry = "https://pypi.org/simple" } +dependencies = [ + { name = "typing-extensions", marker = "python_full_version < '3.13'" }, +] +sdist = { url = "https://files.pythonhosted.org/packages/0b/9f/a65090624ecf468cdca03533906e7c69ed7588582240cfe7cc9e770b50eb/exceptiongroup-1.3.0.tar.gz", hash = "sha256:b241f5885f560bc56a59ee63ca4c6a8bfa46ae4ad651af316d4e81817bb9fd88", size = 29749, upload-time = "2025-05-10T17:42:51.123Z" } +wheels = [ + { url = "https://files.pythonhosted.org/packages/36/f4/c6e662dade71f56cd2f3735141b265c3c79293c109549c1e6933b0651ffc/exceptiongroup-1.3.0-py3-none-any.whl", hash = "sha256:4d111e6e0c13d0644cad6ddaa7ed0261a0b36971f6d23e7ec9b4b9097da78a10", size = 16674, upload-time = "2025-05-10T17:42:49.33Z" }, +] + +[[package]] +name = "iniconfig" +version = "2.1.0" +source = { registry = "https://pypi.org/simple" } +sdist = { url = "https://files.pythonhosted.org/packages/f2/97/ebf4da567aa6827c909642694d71c9fcf53e5b504f2d96afea02718862f3/iniconfig-2.1.0.tar.gz", hash = "sha256:3abbd2e30b36733fee78f9c7f7308f2d0050e88f0087fd25c2645f63c773e1c7", size = 4793, upload-time = "2025-03-19T20:09:59.721Z" } +wheels = [ + { url = "https://files.pythonhosted.org/packages/2c/e1/e6716421ea10d38022b952c159d5161ca1193197fb744506875fbb87ea7b/iniconfig-2.1.0-py3-none-any.whl", hash = "sha256:9deba5723312380e77435581c6bf4935c94cbfab9b1ed33ef8d238ea168eb760", size = 6050, upload-time = "2025-03-19T20:10:01.071Z" }, +] + +[[package]] +name = "packaging" +version = "25.0" +source = { registry = "https://pypi.org/simple" } +sdist = { url = "https://files.pythonhosted.org/packages/a1/d4/1fc4078c65507b51b96ca8f8c3ba19e6a61c8253c72794544580a7b6c24d/packaging-25.0.tar.gz", hash = "sha256:d443872c98d677bf60f6a1f2f8c1cb748e8fe762d2bf9d3148b5599295b0fc4f", size = 165727, upload-time = "2025-04-19T11:48:59.673Z" } +wheels = [ + { url = "https://files.pythonhosted.org/packages/20/12/38679034af332785aac8774540895e234f4d07f7545804097de4b666afd8/packaging-25.0-py3-none-any.whl", hash = "sha256:29572ef2b1f17581046b3a2227d5c611fb25ec70ca1ba8554b24b0e69331a484", size = 66469, upload-time = "2025-04-19T11:48:57.875Z" }, +] + +[[package]] +name = "patronus" +source = { editable = "." } + +[package.dev-dependencies] +dev = [ + { name = "pytest" }, +] + +[package.metadata] + +[package.metadata.requires-dev] +dev = [{ name = "pytest", specifier = ">=8.4.2" }] + +[[package]] +name = "pluggy" +version = "1.6.0" +source = { registry = "https://pypi.org/simple" } +sdist = { url = "https://files.pythonhosted.org/packages/f9/e2/3e91f31a7d2b083fe6ef3fa267035b518369d9511ffab804f839851d2779/pluggy-1.6.0.tar.gz", hash = "sha256:7dcc130b76258d33b90f61b658791dede3486c3e6bfb003ee5c9bfb396dd22f3", size = 69412, upload-time = "2025-05-15T12:30:07.975Z" } +wheels = [ + { url = "https://files.pythonhosted.org/packages/54/20/4d324d65cc6d9205fabedc306948156824eb9f0ee1633355a8f7ec5c66bf/pluggy-1.6.0-py3-none-any.whl", hash = "sha256:e920276dd6813095e9377c0bc5566d94c932c33b27a3e3945d8389c374dd4746", size = 20538, upload-time = "2025-05-15T12:30:06.134Z" }, +] + +[[package]] +name = "pygments" +version = "2.19.2" +source = { registry = "https://pypi.org/simple" } +sdist = { url = "https://files.pythonhosted.org/packages/b0/77/a5b8c569bf593b0140bde72ea885a803b82086995367bf2037de0159d924/pygments-2.19.2.tar.gz", hash = "sha256:636cb2477cec7f8952536970bc533bc43743542f70392ae026374600add5b887", size = 4968631, upload-time = "2025-06-21T13:39:12.283Z" } +wheels = [ + { url = "https://files.pythonhosted.org/packages/c7/21/705964c7812476f378728bdf590ca4b771ec72385c533964653c68e86bdc/pygments-2.19.2-py3-none-any.whl", hash = "sha256:86540386c03d588bb81d44bc3928634ff26449851e99741617ecb9037ee5ec0b", size = 1225217, upload-time = "2025-06-21T13:39:07.939Z" }, +] + +[[package]] +name = "pytest" +version = "8.4.2" +source = { registry = "https://pypi.org/simple" } +dependencies = [ + { name = "colorama", marker = "sys_platform == 'win32'" }, + { name = "exceptiongroup", marker = "python_full_version < '3.11'" }, + { name = "iniconfig" }, + { name = "packaging" }, + { name = "pluggy" }, + { name = "pygments" }, + { name = "tomli", marker = "python_full_version < '3.11'" }, +] +sdist = { url = "https://files.pythonhosted.org/packages/a3/5c/00a0e072241553e1a7496d638deababa67c5058571567b92a7eaa258397c/pytest-8.4.2.tar.gz", hash = "sha256:86c0d0b93306b961d58d62a4db4879f27fe25513d4b969df351abdddb3c30e01", size = 1519618, upload-time = "2025-09-04T14:34:22.711Z" } +wheels = [ + { url = "https://files.pythonhosted.org/packages/a8/a4/20da314d277121d6534b3a980b29035dcd51e6744bd79075a6ce8fa4eb8d/pytest-8.4.2-py3-none-any.whl", hash = "sha256:872f880de3fc3a5bdc88a11b39c9710c3497a547cfa9320bc3c5e62fbf272e79", size = 365750, upload-time = "2025-09-04T14:34:20.226Z" }, +] + +[[package]] +name = "tomli" +version = "2.3.0" +source = { registry = "https://pypi.org/simple" } +sdist = { url = "https://files.pythonhosted.org/packages/52/ed/3f73f72945444548f33eba9a87fc7a6e969915e7b1acc8260b30e1f76a2f/tomli-2.3.0.tar.gz", hash = "sha256:64be704a875d2a59753d80ee8a533c3fe183e3f06807ff7dc2232938ccb01549", size = 17392, upload-time = "2025-10-08T22:01:47.119Z" } +wheels = [ + { url = "https://files.pythonhosted.org/packages/b3/2e/299f62b401438d5fe1624119c723f5d877acc86a4c2492da405626665f12/tomli-2.3.0-cp311-cp311-macosx_10_9_x86_64.whl", hash = "sha256:88bd15eb972f3664f5ed4b57c1634a97153b4bac4479dcb6a495f41921eb7f45", size = 153236, upload-time = "2025-10-08T22:01:00.137Z" }, + { url = "https://files.pythonhosted.org/packages/86/7f/d8fffe6a7aefdb61bced88fcb5e280cfd71e08939da5894161bd71bea022/tomli-2.3.0-cp311-cp311-macosx_11_0_arm64.whl", hash = "sha256:883b1c0d6398a6a9d29b508c331fa56adbcdff647f6ace4dfca0f50e90dfd0ba", size = 148084, upload-time = "2025-10-08T22:01:01.63Z" }, + { url = "https://files.pythonhosted.org/packages/47/5c/24935fb6a2ee63e86d80e4d3b58b222dafaf438c416752c8b58537c8b89a/tomli-2.3.0-cp311-cp311-manylinux2014_aarch64.manylinux_2_17_aarch64.manylinux_2_28_aarch64.whl", hash = "sha256:d1381caf13ab9f300e30dd8feadb3de072aeb86f1d34a8569453ff32a7dea4bf", size = 234832, upload-time = "2025-10-08T22:01:02.543Z" }, + { url = "https://files.pythonhosted.org/packages/89/da/75dfd804fc11e6612846758a23f13271b76d577e299592b4371a4ca4cd09/tomli-2.3.0-cp311-cp311-manylinux2014_x86_64.manylinux_2_17_x86_64.manylinux_2_28_x86_64.whl", hash = "sha256:a0e285d2649b78c0d9027570d4da3425bdb49830a6156121360b3f8511ea3441", size = 242052, upload-time = "2025-10-08T22:01:03.836Z" }, + { url = "https://files.pythonhosted.org/packages/70/8c/f48ac899f7b3ca7eb13af73bacbc93aec37f9c954df3c08ad96991c8c373/tomli-2.3.0-cp311-cp311-musllinux_1_2_aarch64.whl", hash = "sha256:0a154a9ae14bfcf5d8917a59b51ffd5a3ac1fd149b71b47a3a104ca4edcfa845", size = 239555, upload-time = "2025-10-08T22:01:04.834Z" }, + { url = "https://files.pythonhosted.org/packages/ba/28/72f8afd73f1d0e7829bfc093f4cb98ce0a40ffc0cc997009ee1ed94ba705/tomli-2.3.0-cp311-cp311-musllinux_1_2_x86_64.whl", hash = "sha256:74bf8464ff93e413514fefd2be591c3b0b23231a77f901db1eb30d6f712fc42c", size = 245128, upload-time = "2025-10-08T22:01:05.84Z" }, + { url = "https://files.pythonhosted.org/packages/b6/eb/a7679c8ac85208706d27436e8d421dfa39d4c914dcf5fa8083a9305f58d9/tomli-2.3.0-cp311-cp311-win32.whl", hash = "sha256:00b5f5d95bbfc7d12f91ad8c593a1659b6387b43f054104cda404be6bda62456", size = 96445, upload-time = "2025-10-08T22:01:06.896Z" }, + { url = "https://files.pythonhosted.org/packages/0a/fe/3d3420c4cb1ad9cb462fb52967080575f15898da97e21cb6f1361d505383/tomli-2.3.0-cp311-cp311-win_amd64.whl", hash = "sha256:4dc4ce8483a5d429ab602f111a93a6ab1ed425eae3122032db7e9acf449451be", size = 107165, upload-time = "2025-10-08T22:01:08.107Z" }, + { url = "https://files.pythonhosted.org/packages/ff/b7/40f36368fcabc518bb11c8f06379a0fd631985046c038aca08c6d6a43c6e/tomli-2.3.0-cp312-cp312-macosx_10_13_x86_64.whl", hash = "sha256:d7d86942e56ded512a594786a5ba0a5e521d02529b3826e7761a05138341a2ac", size = 154891, upload-time = "2025-10-08T22:01:09.082Z" }, + { url = "https://files.pythonhosted.org/packages/f9/3f/d9dd692199e3b3aab2e4e4dd948abd0f790d9ded8cd10cbaae276a898434/tomli-2.3.0-cp312-cp312-macosx_11_0_arm64.whl", hash = "sha256:73ee0b47d4dad1c5e996e3cd33b8a76a50167ae5f96a2607cbe8cc773506ab22", size = 148796, upload-time = "2025-10-08T22:01:10.266Z" }, + { url = "https://files.pythonhosted.org/packages/60/83/59bff4996c2cf9f9387a0f5a3394629c7efa5ef16142076a23a90f1955fa/tomli-2.3.0-cp312-cp312-manylinux2014_aarch64.manylinux_2_17_aarch64.manylinux_2_28_aarch64.whl", hash = "sha256:792262b94d5d0a466afb5bc63c7daa9d75520110971ee269152083270998316f", size = 242121, upload-time = "2025-10-08T22:01:11.332Z" }, + { url = "https://files.pythonhosted.org/packages/45/e5/7c5119ff39de8693d6baab6c0b6dcb556d192c165596e9fc231ea1052041/tomli-2.3.0-cp312-cp312-manylinux2014_x86_64.manylinux_2_17_x86_64.manylinux_2_28_x86_64.whl", hash = "sha256:4f195fe57ecceac95a66a75ac24d9d5fbc98ef0962e09b2eddec5d39375aae52", size = 250070, upload-time = "2025-10-08T22:01:12.498Z" }, + { url = "https://files.pythonhosted.org/packages/45/12/ad5126d3a278f27e6701abde51d342aa78d06e27ce2bb596a01f7709a5a2/tomli-2.3.0-cp312-cp312-musllinux_1_2_aarch64.whl", hash = "sha256:e31d432427dcbf4d86958c184b9bfd1e96b5b71f8eb17e6d02531f434fd335b8", size = 245859, upload-time = "2025-10-08T22:01:13.551Z" }, + { url = "https://files.pythonhosted.org/packages/fb/a1/4d6865da6a71c603cfe6ad0e6556c73c76548557a8d658f9e3b142df245f/tomli-2.3.0-cp312-cp312-musllinux_1_2_x86_64.whl", hash = "sha256:7b0882799624980785240ab732537fcfc372601015c00f7fc367c55308c186f6", size = 250296, upload-time = "2025-10-08T22:01:14.614Z" }, + { url = "https://files.pythonhosted.org/packages/a0/b7/a7a7042715d55c9ba6e8b196d65d2cb662578b4d8cd17d882d45322b0d78/tomli-2.3.0-cp312-cp312-win32.whl", hash = "sha256:ff72b71b5d10d22ecb084d345fc26f42b5143c5533db5e2eaba7d2d335358876", size = 97124, upload-time = "2025-10-08T22:01:15.629Z" }, + { url = "https://files.pythonhosted.org/packages/06/1e/f22f100db15a68b520664eb3328fb0ae4e90530887928558112c8d1f4515/tomli-2.3.0-cp312-cp312-win_amd64.whl", hash = "sha256:1cb4ed918939151a03f33d4242ccd0aa5f11b3547d0cf30f7c74a408a5b99878", size = 107698, upload-time = "2025-10-08T22:01:16.51Z" }, + { url = "https://files.pythonhosted.org/packages/89/48/06ee6eabe4fdd9ecd48bf488f4ac783844fd777f547b8d1b61c11939974e/tomli-2.3.0-cp313-cp313-macosx_10_13_x86_64.whl", hash = "sha256:5192f562738228945d7b13d4930baffda67b69425a7f0da96d360b0a3888136b", size = 154819, upload-time = "2025-10-08T22:01:17.964Z" }, + { url = "https://files.pythonhosted.org/packages/f1/01/88793757d54d8937015c75dcdfb673c65471945f6be98e6a0410fba167ed/tomli-2.3.0-cp313-cp313-macosx_11_0_arm64.whl", hash = "sha256:be71c93a63d738597996be9528f4abe628d1adf5e6eb11607bc8fe1a510b5dae", size = 148766, upload-time = "2025-10-08T22:01:18.959Z" }, + { url = "https://files.pythonhosted.org/packages/42/17/5e2c956f0144b812e7e107f94f1cc54af734eb17b5191c0bbfb72de5e93e/tomli-2.3.0-cp313-cp313-manylinux2014_aarch64.manylinux_2_17_aarch64.manylinux_2_28_aarch64.whl", hash = "sha256:c4665508bcbac83a31ff8ab08f424b665200c0e1e645d2bd9ab3d3e557b6185b", size = 240771, upload-time = "2025-10-08T22:01:20.106Z" }, + { url = "https://files.pythonhosted.org/packages/d5/f4/0fbd014909748706c01d16824eadb0307115f9562a15cbb012cd9b3512c5/tomli-2.3.0-cp313-cp313-manylinux2014_x86_64.manylinux_2_17_x86_64.manylinux_2_28_x86_64.whl", hash = "sha256:4021923f97266babc6ccab9f5068642a0095faa0a51a246a6a02fccbb3514eaf", size = 248586, upload-time = "2025-10-08T22:01:21.164Z" }, + { url = "https://files.pythonhosted.org/packages/30/77/fed85e114bde5e81ecf9bc5da0cc69f2914b38f4708c80ae67d0c10180c5/tomli-2.3.0-cp313-cp313-musllinux_1_2_aarch64.whl", hash = "sha256:a4ea38c40145a357d513bffad0ed869f13c1773716cf71ccaa83b0fa0cc4e42f", size = 244792, upload-time = "2025-10-08T22:01:22.417Z" }, + { url = "https://files.pythonhosted.org/packages/55/92/afed3d497f7c186dc71e6ee6d4fcb0acfa5f7d0a1a2878f8beae379ae0cc/tomli-2.3.0-cp313-cp313-musllinux_1_2_x86_64.whl", hash = "sha256:ad805ea85eda330dbad64c7ea7a4556259665bdf9d2672f5dccc740eb9d3ca05", size = 248909, upload-time = "2025-10-08T22:01:23.859Z" }, + { url = "https://files.pythonhosted.org/packages/f8/84/ef50c51b5a9472e7265ce1ffc7f24cd4023d289e109f669bdb1553f6a7c2/tomli-2.3.0-cp313-cp313-win32.whl", hash = "sha256:97d5eec30149fd3294270e889b4234023f2c69747e555a27bd708828353ab606", size = 96946, upload-time = "2025-10-08T22:01:24.893Z" }, + { url = "https://files.pythonhosted.org/packages/b2/b7/718cd1da0884f281f95ccfa3a6cc572d30053cba64603f79d431d3c9b61b/tomli-2.3.0-cp313-cp313-win_amd64.whl", hash = "sha256:0c95ca56fbe89e065c6ead5b593ee64b84a26fca063b5d71a1122bf26e533999", size = 107705, upload-time = "2025-10-08T22:01:26.153Z" }, + { url = "https://files.pythonhosted.org/packages/19/94/aeafa14a52e16163008060506fcb6aa1949d13548d13752171a755c65611/tomli-2.3.0-cp314-cp314-macosx_10_13_x86_64.whl", hash = "sha256:cebc6fe843e0733ee827a282aca4999b596241195f43b4cc371d64fc6639da9e", size = 154244, upload-time = "2025-10-08T22:01:27.06Z" }, + { url = "https://files.pythonhosted.org/packages/db/e4/1e58409aa78eefa47ccd19779fc6f36787edbe7d4cd330eeeedb33a4515b/tomli-2.3.0-cp314-cp314-macosx_11_0_arm64.whl", hash = "sha256:4c2ef0244c75aba9355561272009d934953817c49f47d768070c3c94355c2aa3", size = 148637, upload-time = "2025-10-08T22:01:28.059Z" }, + { url = "https://files.pythonhosted.org/packages/26/b6/d1eccb62f665e44359226811064596dd6a366ea1f985839c566cd61525ae/tomli-2.3.0-cp314-cp314-manylinux2014_aarch64.manylinux_2_17_aarch64.manylinux_2_28_aarch64.whl", hash = "sha256:c22a8bf253bacc0cf11f35ad9808b6cb75ada2631c2d97c971122583b129afbc", size = 241925, upload-time = "2025-10-08T22:01:29.066Z" }, + { url = "https://files.pythonhosted.org/packages/70/91/7cdab9a03e6d3d2bb11beae108da5bdc1c34bdeb06e21163482544ddcc90/tomli-2.3.0-cp314-cp314-manylinux2014_x86_64.manylinux_2_17_x86_64.manylinux_2_28_x86_64.whl", hash = "sha256:0eea8cc5c5e9f89c9b90c4896a8deefc74f518db5927d0e0e8d4a80953d774d0", size = 249045, upload-time = "2025-10-08T22:01:31.98Z" }, + { url = "https://files.pythonhosted.org/packages/15/1b/8c26874ed1f6e4f1fcfeb868db8a794cbe9f227299402db58cfcc858766c/tomli-2.3.0-cp314-cp314-musllinux_1_2_aarch64.whl", hash = "sha256:b74a0e59ec5d15127acdabd75ea17726ac4c5178ae51b85bfe39c4f8a278e879", size = 245835, upload-time = "2025-10-08T22:01:32.989Z" }, + { url = "https://files.pythonhosted.org/packages/fd/42/8e3c6a9a4b1a1360c1a2a39f0b972cef2cc9ebd56025168c4137192a9321/tomli-2.3.0-cp314-cp314-musllinux_1_2_x86_64.whl", hash = "sha256:b5870b50c9db823c595983571d1296a6ff3e1b88f734a4c8f6fc6188397de005", size = 253109, upload-time = "2025-10-08T22:01:34.052Z" }, + { url = "https://files.pythonhosted.org/packages/22/0c/b4da635000a71b5f80130937eeac12e686eefb376b8dee113b4a582bba42/tomli-2.3.0-cp314-cp314-win32.whl", hash = "sha256:feb0dacc61170ed7ab602d3d972a58f14ee3ee60494292d384649a3dc38ef463", size = 97930, upload-time = "2025-10-08T22:01:35.082Z" }, + { url = "https://files.pythonhosted.org/packages/b9/74/cb1abc870a418ae99cd5c9547d6bce30701a954e0e721821df483ef7223c/tomli-2.3.0-cp314-cp314-win_amd64.whl", hash = "sha256:b273fcbd7fc64dc3600c098e39136522650c49bca95df2d11cf3b626422392c8", size = 107964, upload-time = "2025-10-08T22:01:36.057Z" }, + { url = "https://files.pythonhosted.org/packages/54/78/5c46fff6432a712af9f792944f4fcd7067d8823157949f4e40c56b8b3c83/tomli-2.3.0-cp314-cp314t-macosx_10_13_x86_64.whl", hash = "sha256:940d56ee0410fa17ee1f12b817b37a4d4e4dc4d27340863cc67236c74f582e77", size = 163065, upload-time = "2025-10-08T22:01:37.27Z" }, + { url = "https://files.pythonhosted.org/packages/39/67/f85d9bd23182f45eca8939cd2bc7050e1f90c41f4a2ecbbd5963a1d1c486/tomli-2.3.0-cp314-cp314t-macosx_11_0_arm64.whl", hash = "sha256:f85209946d1fe94416debbb88d00eb92ce9cd5266775424ff81bc959e001acaf", size = 159088, upload-time = "2025-10-08T22:01:38.235Z" }, + { url = "https://files.pythonhosted.org/packages/26/5a/4b546a0405b9cc0659b399f12b6adb750757baf04250b148d3c5059fc4eb/tomli-2.3.0-cp314-cp314t-manylinux2014_aarch64.manylinux_2_17_aarch64.manylinux_2_28_aarch64.whl", hash = "sha256:a56212bdcce682e56b0aaf79e869ba5d15a6163f88d5451cbde388d48b13f530", size = 268193, upload-time = "2025-10-08T22:01:39.712Z" }, + { url = "https://files.pythonhosted.org/packages/42/4f/2c12a72ae22cf7b59a7fe75b3465b7aba40ea9145d026ba41cb382075b0e/tomli-2.3.0-cp314-cp314t-manylinux2014_x86_64.manylinux_2_17_x86_64.manylinux_2_28_x86_64.whl", hash = "sha256:c5f3ffd1e098dfc032d4d3af5c0ac64f6d286d98bc148698356847b80fa4de1b", size = 275488, upload-time = "2025-10-08T22:01:40.773Z" }, + { url = "https://files.pythonhosted.org/packages/92/04/a038d65dbe160c3aa5a624e93ad98111090f6804027d474ba9c37c8ae186/tomli-2.3.0-cp314-cp314t-musllinux_1_2_aarch64.whl", hash = "sha256:5e01decd096b1530d97d5d85cb4dff4af2d8347bd35686654a004f8dea20fc67", size = 272669, upload-time = "2025-10-08T22:01:41.824Z" }, + { url = "https://files.pythonhosted.org/packages/be/2f/8b7c60a9d1612a7cbc39ffcca4f21a73bf368a80fc25bccf8253e2563267/tomli-2.3.0-cp314-cp314t-musllinux_1_2_x86_64.whl", hash = "sha256:8a35dd0e643bb2610f156cca8db95d213a90015c11fee76c946aa62b7ae7e02f", size = 279709, upload-time = "2025-10-08T22:01:43.177Z" }, + { url = "https://files.pythonhosted.org/packages/7e/46/cc36c679f09f27ded940281c38607716c86cf8ba4a518d524e349c8b4874/tomli-2.3.0-cp314-cp314t-win32.whl", hash = "sha256:a1f7f282fe248311650081faafa5f4732bdbfef5d45fe3f2e702fbc6f2d496e0", size = 107563, upload-time = "2025-10-08T22:01:44.233Z" }, + { url = "https://files.pythonhosted.org/packages/84/ff/426ca8683cf7b753614480484f6437f568fd2fda2edbdf57a2d3d8b27a0b/tomli-2.3.0-cp314-cp314t-win_amd64.whl", hash = "sha256:70a251f8d4ba2d9ac2542eecf008b3c8a9fc5c3f9f02c56a9d7952612be2fdba", size = 119756, upload-time = "2025-10-08T22:01:45.234Z" }, + { url = "https://files.pythonhosted.org/packages/77/b8/0135fadc89e73be292b473cb820b4f5a08197779206b33191e801feeae40/tomli-2.3.0-py3-none-any.whl", hash = "sha256:e95b1af3c5b07d9e643909b5abbec77cd9f1217e6d0bca72b0234736b9fb1f1b", size = 14408, upload-time = "2025-10-08T22:01:46.04Z" }, +] + +[[package]] +name = "typing-extensions" +version = "4.15.0" +source = { registry = "https://pypi.org/simple" } +sdist = { url = "https://files.pythonhosted.org/packages/72/94/1a15dd82efb362ac84269196e94cf00f187f7ed21c242792a923cdb1c61f/typing_extensions-4.15.0.tar.gz", hash = "sha256:0cea48d173cc12fa28ecabc3b837ea3cf6f38c6d1136f85cbaaf598984861466", size = 109391, upload-time = "2025-08-25T13:49:26.313Z" } +wheels = [ + { url = "https://files.pythonhosted.org/packages/18/67/36e9267722cc04a6b9f15c7f3441c2363321a3ea07da7ae0c0707beb2a9c/typing_extensions-4.15.0-py3-none-any.whl", hash = "sha256:f0fa19c6845758ab08074a0cfa8b7aecb71c999ca73d62883bc25cc018c4e548", size = 44614, upload-time = "2025-08-25T13:49:24.86Z" }, +] From 2ec43446fd79ff0323cac2eb29b668a9f09dd811 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Kevin=20L=C3=A4ufer?= Date: Wed, 15 Oct 2025 14:41:22 -0400 Subject: [PATCH 05/24] uv: add cache keys --- python/pyproject.toml | 3 +++ 1 file changed, 3 insertions(+) diff --git a/python/pyproject.toml b/python/pyproject.toml index 6c13c6a..e23fe06 100644 --- a/python/pyproject.toml +++ b/python/pyproject.toml @@ -29,3 +29,6 @@ features = ["pyo3/extension-module"] dev = [ "pytest>=8.4.2", ] + +[tool.uv] +cache-keys = [{file = "pyproject.toml"}, {file = "Cargo.toml"}, {file = "src/*.rs"}] \ No newline at end of file From fbb6e951551c03a55278e567125b995a7088731b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Kevin=20L=C3=A4ufer?= Date: Wed, 15 Oct 2025 14:53:28 -0400 Subject: [PATCH 06/24] parse and serialize transition system --- python/src/lib.rs | 395 +++++-------------------------------- python/tests/test_btor2.py | 34 ++++ python/tests/test_quiz1.py | 68 ------- 3 files changed, 86 insertions(+), 411 deletions(-) create mode 100644 python/tests/test_btor2.py delete mode 100644 python/tests/test_quiz1.py diff --git a/python/src/lib.rs b/python/src/lib.rs index 123f60a..70b351f 100644 --- a/python/src/lib.rs +++ b/python/src/lib.rs @@ -1,368 +1,77 @@ use ::patronus::btor2; -use ::patronus::expr::{Context, Expr, ExprRef}; -use ::patronus::system::TransitionSystem; -use baa::BitVecOps; -use pyo3::exceptions::{PyIOError, PyIndexError, PyValueError}; +use ::patronus::expr::SerializableIrNode; +use pyo3::exceptions::PyValueError; use pyo3::prelude::*; +use std::ops::{Deref, DerefMut}; +use std::sync::{LazyLock, RwLock, RwLockWriteGuard}; -#[pyclass] -pub struct Design { - ctx: Context, - sys: TransitionSystem, -} - -#[pymethods] -impl Design { - fn __len__(&self) -> usize { - self.ctx.num_exprs() - } - - fn __getitem__(&self, idx: isize, py: Python<'_>) -> PyResult { - let n = self.ctx.num_exprs() as isize; - let mut i = idx; - if i < 0 { - i += n; - } - if i < 0 || i >= n { - return Err(PyIndexError::new_err(format!( - "index {idx} out of range for length {n}" - ))); - } - let idx_u = i as usize; - let r = ExprRef::from_index(idx_u); - let e = self.ctx.get_expr(r); - let d = expr_to_dict(py, e, &self.ctx)?; - Ok(d) - } +/// 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> = + LazyLock::new(|| RwLock::new(::patronus::expr::Context::default())); - // Optional convenience: number of roots of various categories - #[pyo3(name = "num_states")] - fn num_states_py(&self) -> usize { - self.sys.states.len() - } - - #[pyo3(name = "num_inputs")] - fn num_inputs_py(&self) -> usize { - self.sys.inputs.len() - } +#[pyclass] +pub struct TransitionSystem(::patronus::system::TransitionSystem); - #[pyo3(name = "num_outputs")] - fn num_outputs_py(&self) -> usize { - self.sys.outputs.len() - } +/// Exposes the Context object to python +#[pyclass] +pub struct Context(::patronus::expr::Context); - // Optional: names available at the system level - #[pyo3(name = "name")] - fn name_py(&self) -> String { - self.sys.name.clone() +#[pymethods] +impl TransitionSystem { + #[getter] + fn name(&self) -> &str { + &self.0.name } - // Convenience lists for Python traversal - #[pyo3(name = "inputs")] - fn inputs_py(&self) -> Vec { - self.sys - .inputs - .iter() - .map(|&e| self.ctx.expr_index(e)) - .collect() + fn __str__(&self) -> String { + self.0 + .serialize_to_str(DEFAULT_CONTEXT.read().unwrap().deref()) } +} - #[pyo3(name = "states")] - fn states_py(&self) -> Vec { - self.sys - .states - .iter() - .map(|s| self.ctx.expr_index(s.symbol)) - .collect() - } +enum ContextGuardMut<'a> { + Local(&'a mut Context), + Shared(RwLockWriteGuard<'a, ::patronus::expr::Context>), +} - #[pyo3(name = "outputs")] - fn outputs_py(&self) -> Vec { - self.sys - .outputs - .iter() - .map(|o| self.ctx.expr_index(o.expr)) - .collect() +impl<'a> From> for ContextGuardMut<'a> { + fn from(value: Option<&'a mut Context>) -> Self { + value + .map(|ctx| Self::Local(ctx)) + .unwrap_or_else(|| Self::Shared(DEFAULT_CONTEXT.write().unwrap())) } +} - #[pyo3(name = "find_symbol")] - fn find_symbol_py(&self, name: &str) -> Option { - let map = self.sys.get_name_map(&self.ctx); - map.get(name).map(|&e| self.ctx.expr_index(e)) +impl<'a> ContextGuardMut<'a> { + fn deref_mut(&mut self) -> &mut ::patronus::expr::Context { + match self { + ContextGuardMut::Local(ctx) => &mut ctx.0, + ContextGuardMut::Shared(guard) => guard.deref_mut(), + } } } #[pyfunction] -pub fn parse(path: &str) -> PyResult { - // Robust path: avoid panics from parse_file_with_ctx File::open(...).expect(...) - let contents = std::fs::read_to_string(path) - .map_err(|e| PyIOError::new_err(format!("I/O error reading '{path}': {e}")))?; - let mut ctx = Context::default(); - let name = std::path::Path::new(path) - .file_stem() - .and_then(|s| s.to_str()); - match btor2::parse_str(&mut ctx, &contents, name) { - Some(sys) => Ok(Design { ctx, sys }), - None => Err(PyValueError::new_err(format!( - "Parse failed for BTOR file: {path}" - ))), +#[pyo3(signature = (content, name=None, ctx=None))] +pub fn parse_btor2_str( + content: &str, + name: Option<&str>, + ctx: Option<&mut Context>, +) -> PyResult { + let mut ctx_guard: ContextGuardMut = ctx.into(); + let ctx = ctx_guard.deref_mut(); + match btor2::parse_str(ctx, &content, name) { + Some(sys) => Ok(TransitionSystem(sys)), + None => Err(PyValueError::new_err("failed to parse btor")), } } #[pymodule] #[pyo3(name = "patronus")] fn patronus(_py: Python<'_>, m: &pyo3::Bound<'_, pyo3::types::PyModule>) -> PyResult<()> { - m.add_class::()?; - m.add_function(wrap_pyfunction!(parse, m)?)?; + m.add_class::()?; + m.add_function(wrap_pyfunction!(parse_btor2_str, m)?)?; Ok(()) } - -// Helpers - -fn expr_to_dict(py: Python<'_>, e: &Expr, ctx: &Context) -> PyResult { - let d = pyo3::types::PyDict::new(py); - - macro_rules! set { - ($k:expr, $v:expr) => { - d.set_item($k, $v)? - }; - } - macro_rules! idx { - ($r:expr) => { - ctx.expr_index($r) - }; - } - - match e { - // Bit-Vector Expressions - Expr::BVSymbol { name, width } => { - set!("kind", "BVSymbol"); - set!("name", ctx[*name].as_str()); - set!("width", *width as u64); - } - Expr::BVLiteral(v) => { - set!("kind", "BVLiteral"); - let w = v.width(); - let value = v.get(ctx); - // mimic serialize.rs formatting - let s = if w <= 8 { - format!("{}'b{}", w, value.to_bit_str()) - } else { - format!("{}'x{}", w, value.to_hex_str()) - }; - set!("width", w as u64); - set!("value", s); - // Also expose numeric hex without width prefix for convenience - set!("hex", value.to_hex_str()); - } - // unary with explicit fields - Expr::BVZeroExt { e, by, width } => { - set!("kind", "BVZeroExt"); - set!("e", idx!(*e)); - set!("by", *by as u64); - set!("width", *width as u64); - } - Expr::BVSignExt { e, by, width } => { - set!("kind", "BVSignExt"); - set!("e", idx!(*e)); - set!("by", *by as u64); - set!("width", *width as u64); - } - Expr::BVSlice { e, hi, lo } => { - set!("kind", "BVSlice"); - set!("e", idx!(*e)); - set!("hi", *hi as u64); - set!("lo", *lo as u64); - } - Expr::BVNot(e, width) => { - set!("kind", "BVNot"); - set!("e", idx!(*e)); - set!("width", *width as u64); - } - Expr::BVNegate(e, width) => { - set!("kind", "BVNegate"); - set!("e", idx!(*e)); - set!("width", *width as u64); - } - // binary logical/compare/arithmetic - Expr::BVEqual(a, b) => { - set!("kind", "BVEqual"); - set!("a", idx!(*a)); - set!("b", idx!(*b)); - } - Expr::BVImplies(a, b) => { - set!("kind", "BVImplies"); - set!("a", idx!(*a)); - set!("b", idx!(*b)); - } - Expr::BVGreater(a, b) => { - set!("kind", "BVGreater"); - set!("a", idx!(*a)); - set!("b", idx!(*b)); - } - Expr::BVGreaterSigned(a, b, width) => { - set!("kind", "BVGreaterSigned"); - set!("a", idx!(*a)); - set!("b", idx!(*b)); - set!("width", *width as u64); - } - Expr::BVGreaterEqual(a, b) => { - set!("kind", "BVGreaterEqual"); - set!("a", idx!(*a)); - set!("b", idx!(*b)); - } - Expr::BVGreaterEqualSigned(a, b, width) => { - set!("kind", "BVGreaterEqualSigned"); - set!("a", idx!(*a)); - set!("b", idx!(*b)); - set!("width", *width as u64); - } - Expr::BVConcat(a, b, width) => { - set!("kind", "BVConcat"); - set!("a", idx!(*a)); - set!("b", idx!(*b)); - set!("width", *width as u64); - } - Expr::BVAnd(a, b, width) => { - set!("kind", "BVAnd"); - set!("a", idx!(*a)); - set!("b", idx!(*b)); - set!("width", *width as u64); - } - Expr::BVOr(a, b, width) => { - set!("kind", "BVOr"); - set!("a", idx!(*a)); - set!("b", idx!(*b)); - set!("width", *width as u64); - } - Expr::BVXor(a, b, width) => { - set!("kind", "BVXor"); - set!("a", idx!(*a)); - set!("b", idx!(*b)); - set!("width", *width as u64); - } - Expr::BVShiftLeft(a, b, width) => { - set!("kind", "BVShiftLeft"); - set!("a", idx!(*a)); - set!("b", idx!(*b)); - set!("width", *width as u64); - } - Expr::BVArithmeticShiftRight(a, b, width) => { - set!("kind", "BVArithmeticShiftRight"); - set!("a", idx!(*a)); - set!("b", idx!(*b)); - set!("width", *width as u64); - } - Expr::BVShiftRight(a, b, width) => { - set!("kind", "BVShiftRight"); - set!("a", idx!(*a)); - set!("b", idx!(*b)); - set!("width", *width as u64); - } - Expr::BVAdd(a, b, width) => { - set!("kind", "BVAdd"); - set!("a", idx!(*a)); - set!("b", idx!(*b)); - set!("width", *width as u64); - } - Expr::BVMul(a, b, width) => { - set!("kind", "BVMul"); - set!("a", idx!(*a)); - set!("b", idx!(*b)); - set!("width", *width as u64); - } - Expr::BVSignedDiv(a, b, width) => { - set!("kind", "BVSignedDiv"); - set!("a", idx!(*a)); - set!("b", idx!(*b)); - set!("width", *width as u64); - } - Expr::BVUnsignedDiv(a, b, width) => { - set!("kind", "BVUnsignedDiv"); - set!("a", idx!(*a)); - set!("b", idx!(*b)); - set!("width", *width as u64); - } - Expr::BVSignedMod(a, b, width) => { - set!("kind", "BVSignedMod"); - set!("a", idx!(*a)); - set!("b", idx!(*b)); - set!("width", *width as u64); - } - Expr::BVSignedRem(a, b, width) => { - set!("kind", "BVSignedRem"); - set!("a", idx!(*a)); - set!("b", idx!(*b)); - set!("width", *width as u64); - } - Expr::BVUnsignedRem(a, b, width) => { - set!("kind", "BVUnsignedRem"); - set!("a", idx!(*a)); - set!("b", idx!(*b)); - set!("width", *width as u64); - } - Expr::BVSub(a, b, width) => { - set!("kind", "BVSub"); - set!("a", idx!(*a)); - set!("b", idx!(*b)); - set!("width", *width as u64); - } - Expr::BVArrayRead { - array, - index, - width, - } => { - set!("kind", "BVArrayRead"); - set!("array", idx!(*array)); - set!("index", idx!(*index)); - set!("width", *width as u64); - } - Expr::BVIte { cond, tru, fals } => { - set!("kind", "BVIte"); - set!("cond", idx!(*cond)); - set!("tru", idx!(*tru)); - set!("fals", idx!(*fals)); - } - - // Array Expressions - Expr::ArraySymbol { - name, - index_width, - data_width, - } => { - set!("kind", "ArraySymbol"); - set!("name", ctx[*name].as_str()); - set!("index_width", *index_width as u64); - set!("data_width", *data_width as u64); - } - Expr::ArrayConstant { - e, - index_width, - data_width, - } => { - set!("kind", "ArrayConstant"); - set!("e", idx!(*e)); - set!("index_width", *index_width as u64); - set!("data_width", *data_width as u64); - } - Expr::ArrayEqual(a, b) => { - set!("kind", "ArrayEqual"); - set!("a", idx!(*a)); - set!("b", idx!(*b)); - } - Expr::ArrayStore { array, index, data } => { - set!("kind", "ArrayStore"); - set!("array", idx!(*array)); - set!("index", idx!(*index)); - set!("data", idx!(*data)); - } - Expr::ArrayIte { cond, tru, fals } => { - set!("kind", "ArrayIte"); - set!("cond", idx!(*cond)); - set!("tru", idx!(*tru)); - set!("fals", idx!(*fals)); - } - } - - Ok(d.into()) -} diff --git a/python/tests/test_btor2.py b/python/tests/test_btor2.py new file mode 100644 index 0000000..a460414 --- /dev/null +++ b/python/tests/test_btor2.py @@ -0,0 +1,34 @@ +import pathlib +import pytest +from patronus import * + + +repo_root = (pathlib.Path(__file__) / '..' / '..' / '..').resolve() + +COUNT_2 = """ +1 sort bitvec 3 +2 zero 1 +3 state 1 +4 init 1 3 2 +5 one 1 +6 add 1 3 5 +7 next 1 3 6 +8 ones 1 +9 sort bitvec 1 +10 eq 9 3 8 +11 bad 10 +""" + +def test_parse_and_serialize_count2(): + filename = repo_root / "inputs" / "chiseltest" / "Quiz1.btor" + sys = parse_btor2_str(COUNT_2, "count2") + assert sys.name == "count2" + + expected_system = """ +count2 +bad _bad_0 : bv<1> = eq(_state_0, 3'b111) +state _state_0 : bv<3> + [init] 3'b000 + [next] add(_state_0, 3'b001) + """ + assert expected_system.strip() == str(sys).strip() diff --git a/python/tests/test_quiz1.py b/python/tests/test_quiz1.py deleted file mode 100644 index d4337e2..0000000 --- a/python/tests/test_quiz1.py +++ /dev/null @@ -1,68 +0,0 @@ -import pathlib -import pytest - -from patronus import parse - - -repo_root = (pathlib.Path(__file__) / '..' / '..' / '..').resolve() - - -def test_parse_and_index_quiz1(): - btor_path = repo_root / "inputs" / "chiseltest" / "Quiz1.btor" - assert btor_path.is_file(), f"missing BTOR test input at {btor_path}" - - design = parse(str(btor_path)) - n = len(design) - assert n > 0 - - # Index access for a handful of nodes should return a dict with at least a 'kind' - sample_count = min(n, 50) - saw_symbol = False - saw_literal = False - saw_op_with_children = False - - for i in range(sample_count): - node = design[i] - assert isinstance(node, dict), f"node {i} is not a dict" - assert "kind" in node, f"node {i} missing 'kind'" - k = node["kind"] - - if k == "BVSymbol" or k == "ArraySymbol": - assert "name" in node and isinstance(node["name"], str) - saw_symbol = True - - if k == "BVLiteral": - assert "width" in node and "value" in node - saw_literal = True - - # Check a few common ops have integer child refs - if k in {"BVAdd", "BVAnd", "BVOr", "BVEqual", "BVNot", "BVIte", "BVSlice"}: - # Determine expected child fields - if k in {"BVAdd", "BVAnd", "BVOr", "BVEqual"}: - assert isinstance(node["a"], int) and isinstance(node["b"], int) - saw_op_with_children = True - elif k == "BVNot": - assert isinstance(node["e"], int) - saw_op_with_children = True - elif k == "BVIte": - assert isinstance(node["cond"], int) - assert isinstance(node["tru"], int) - assert isinstance(node["fals"], int) - saw_op_with_children = True - elif k == "BVSlice": - assert isinstance(node["e"], int) - assert isinstance(node["hi"], int) - assert isinstance(node["lo"], int) - saw_op_with_children = True - - assert saw_symbol, "did not encounter any symbol nodes in the first batch" - assert saw_literal, "did not encounter any literal nodes in the first batch" - assert saw_op_with_children, "did not encounter any ops with children in the first batch" - - -def test_out_of_range_index_raises(): - # Use a tiny BTOR file to parse, then index out of bounds - btor_path = repo_root / "inputs" / "chiseltest" / "Quiz1.btor" - design = parse(str(btor_path)) - with pytest.raises(IndexError): - _ = design[len(design)] From f62a4947007c9bd949a0e35487c3e1e7e3e6daa9 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Kevin=20L=C3=A4ufer?= Date: Wed, 15 Oct 2025 15:00:40 -0400 Subject: [PATCH 07/24] move context management to its own module --- python/src/ctx.rs | 60 +++++++++++++++++++++++++++++++++++++++++++++++ python/src/lib.rs | 43 +++++---------------------------- 2 files changed, 66 insertions(+), 37 deletions(-) create mode 100644 python/src/ctx.rs diff --git a/python/src/ctx.rs b/python/src/ctx.rs new file mode 100644 index 0000000..1b7386a --- /dev/null +++ b/python/src/ctx.rs @@ -0,0 +1,60 @@ +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> = + 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> { + Local(&'a mut Context), + Shared(RwLockWriteGuard<'a, ::patronus::expr::Context>), +} + +impl<'a> From> 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> ContextGuardWrite<'a> { + pub fn deref_mut(&mut self) -> &mut ::patronus::expr::Context { + match self { + Self::Local(ctx) => &mut ctx.0, + Self::Shared(guard) => guard.deref_mut(), + } + } +} + +pub(crate) enum ContextGuardRead<'a> { + Local(&'a Context), + Shared(RwLockReadGuard<'a, ::patronus::expr::Context>), +} + +impl<'a> From> for ContextGuardRead<'a> { + fn from(value: Option<&'a mut Context>) -> Self { + value + .map(|ctx| Self::Local(ctx)) + .unwrap_or_else(|| Self::default()) + } +} + +impl<'a> ContextGuardRead<'a> { + pub fn default() -> Self { + Self::Shared(DEFAULT_CONTEXT.read().unwrap()) + } + pub fn deref(&self) -> &::patronus::expr::Context { + match self { + Self::Local(ctx) => &ctx.0, + Self::Shared(guard) => guard.deref(), + } + } +} diff --git a/python/src/lib.rs b/python/src/lib.rs index 70b351f..7d6ac4d 100644 --- a/python/src/lib.rs +++ b/python/src/lib.rs @@ -1,23 +1,15 @@ +mod ctx; +pub use ctx::Context; +use ctx::{ContextGuardRead, ContextGuardWrite}; + use ::patronus::btor2; use ::patronus::expr::SerializableIrNode; use pyo3::exceptions::PyValueError; use pyo3::prelude::*; -use std::ops::{Deref, DerefMut}; -use std::sync::{LazyLock, RwLock, 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> = - LazyLock::new(|| RwLock::new(::patronus::expr::Context::default())); #[pyclass] pub struct TransitionSystem(::patronus::system::TransitionSystem); -/// Exposes the Context object to python -#[pyclass] -pub struct Context(::patronus::expr::Context); - #[pymethods] impl TransitionSystem { #[getter] @@ -26,30 +18,7 @@ impl TransitionSystem { } fn __str__(&self) -> String { - self.0 - .serialize_to_str(DEFAULT_CONTEXT.read().unwrap().deref()) - } -} - -enum ContextGuardMut<'a> { - Local(&'a mut Context), - Shared(RwLockWriteGuard<'a, ::patronus::expr::Context>), -} - -impl<'a> From> for ContextGuardMut<'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> ContextGuardMut<'a> { - fn deref_mut(&mut self) -> &mut ::patronus::expr::Context { - match self { - ContextGuardMut::Local(ctx) => &mut ctx.0, - ContextGuardMut::Shared(guard) => guard.deref_mut(), - } + self.0.serialize_to_str(ContextGuardRead::default().deref()) } } @@ -60,7 +29,7 @@ pub fn parse_btor2_str( name: Option<&str>, ctx: Option<&mut Context>, ) -> PyResult { - let mut ctx_guard: ContextGuardMut = ctx.into(); + let mut ctx_guard: ContextGuardWrite = ctx.into(); let ctx = ctx_guard.deref_mut(); match btor2::parse_str(ctx, &content, name) { Some(sys) => Ok(TransitionSystem(sys)), From 5a0a8a0ab17323d8f71ffa70614cf0fb2f9968f7 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Kevin=20L=C3=A4ufer?= Date: Wed, 15 Oct 2025 15:42:23 -0400 Subject: [PATCH 08/24] expose more transition system properties --- patronus/src/system/transition_system.rs | 2 +- python/src/ctx.rs | 49 ++++++++----- python/src/lib.rs | 91 ++++++++++++++++++++++-- python/tests/test_btor2.py | 14 +++- 4 files changed, 130 insertions(+), 26 deletions(-) diff --git a/patronus/src/system/transition_system.rs b/patronus/src/system/transition_system.rs index ca19348..55aaca5 100644 --- a/patronus/src/system/transition_system.rs +++ b/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, diff --git a/python/src/ctx.rs b/python/src/ctx.rs index 1b7386a..9dd2823 100644 --- a/python/src/ctx.rs +++ b/python/src/ctx.rs @@ -13,47 +13,62 @@ static DEFAULT_CONTEXT: LazyLock> = pub struct Context(::patronus::expr::Context); pub(crate) enum ContextGuardWrite<'a> { - Local(&'a mut Context), + // TODO: reintroduce local context support! + // Local(&'a mut Context), Shared(RwLockWriteGuard<'a, ::patronus::expr::Context>), } -impl<'a> From> 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())) +// TODO: reintroduce local context support! +// impl<'a> From> 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 { - Self::Local(ctx) => &mut ctx.0, + // TODO: reintroduce local context support! + // Self::Local(ctx) => &mut ctx.0, Self::Shared(guard) => guard.deref_mut(), } } } pub(crate) enum ContextGuardRead<'a> { - Local(&'a Context), + // TODO: reintroduce local context support! + // Local(&'a Context), Shared(RwLockReadGuard<'a, ::patronus::expr::Context>), } -impl<'a> From> for ContextGuardRead<'a> { - fn from(value: Option<&'a mut Context>) -> Self { - value - .map(|ctx| Self::Local(ctx)) - .unwrap_or_else(|| Self::default()) +// TODO: reintroduce local context support! +// impl<'a> From> 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 default() -> Self { - Self::Shared(DEFAULT_CONTEXT.read().unwrap()) - } pub fn deref(&self) -> &::patronus::expr::Context { match self { - Self::Local(ctx) => &ctx.0, + // TODO: reintroduce local context support! + // Self::Local(ctx) => &ctx.0, Self::Shared(guard) => guard.deref(), } } diff --git a/python/src/lib.rs b/python/src/lib.rs index 7d6ac4d..802538d 100644 --- a/python/src/lib.rs +++ b/python/src/lib.rs @@ -7,6 +7,62 @@ use ::patronus::expr::SerializableIrNode; use pyo3::exceptions::PyValueError; use pyo3::prelude::*; +#[pyclass] +pub struct ExprRef(::patronus::expr::ExprRef); + +#[pymethods] +impl ExprRef { + fn __str__(&self) -> String { + self.0.serialize_to_str(ContextGuardRead::default().deref()) + } +} + +#[pyclass] +pub struct Output(::patronus::system::Output); + +#[pymethods] +impl Output { + #[getter] + fn name(&self) -> String { + ContextGuardRead::default().deref()[self.0.name].to_string() + } + + #[getter] + fn expr(&self) -> ExprRef { + ExprRef(self.0.expr) + } +} + +#[pyclass] +pub struct State(::patronus::system::State); + +#[pymethods] +impl State { + #[getter] + fn symbol(&self) -> ExprRef { + ExprRef(self.0.symbol) + } + + #[getter] + fn name(&self) -> String { + ContextGuardRead::default() + .deref() + .get_symbol_name(self.0.symbol) + .unwrap() + .to_string() + } + + #[getter] + fn next(&self) -> Option { + self.0.next.map(|e| ExprRef(e)) + } + + #[getter] + fn init(&self) -> Option { + self.0.init.map(|e| ExprRef(e)) + } +} + #[pyclass] pub struct TransitionSystem(::patronus::system::TransitionSystem); @@ -17,19 +73,40 @@ impl TransitionSystem { &self.0.name } + #[getter] + fn inputs(&self) -> Vec { + self.0.inputs.iter().map(|e| ExprRef(*e)).collect() + } + + #[getter] + fn outputs(&self) -> Vec { + self.0.outputs.iter().map(|e| Output(*e)).collect() + } + + #[getter] + fn states(&self) -> Vec { + self.0.states.iter().map(|e| State(*e)).collect() + } + + #[getter] + fn bad_states(&self) -> Vec { + self.0.bad_states.iter().map(|e| ExprRef(*e)).collect() + } + + #[getter] + fn constraints(&self) -> Vec { + self.0.constraints.iter().map(|e| ExprRef(*e)).collect() + } + fn __str__(&self) -> String { self.0.serialize_to_str(ContextGuardRead::default().deref()) } } #[pyfunction] -#[pyo3(signature = (content, name=None, ctx=None))] -pub fn parse_btor2_str( - content: &str, - name: Option<&str>, - ctx: Option<&mut Context>, -) -> PyResult { - let mut ctx_guard: ContextGuardWrite = ctx.into(); +#[pyo3(signature = (content, name=None))] +pub fn parse_btor2_str(content: &str, name: Option<&str>) -> PyResult { + let mut ctx_guard = ContextGuardWrite::default(); let ctx = ctx_guard.deref_mut(); match btor2::parse_str(ctx, &content, name) { Some(sys) => Ok(TransitionSystem(sys)), diff --git a/python/tests/test_btor2.py b/python/tests/test_btor2.py index a460414..1584abc 100644 --- a/python/tests/test_btor2.py +++ b/python/tests/test_btor2.py @@ -20,7 +20,6 @@ """ def test_parse_and_serialize_count2(): - filename = repo_root / "inputs" / "chiseltest" / "Quiz1.btor" sys = parse_btor2_str(COUNT_2, "count2") assert sys.name == "count2" @@ -32,3 +31,16 @@ def test_parse_and_serialize_count2(): [next] add(_state_0, 3'b001) """ assert expected_system.strip() == str(sys).strip() + +def test_transition_system_fields(): + sys = parse_btor2_str(COUNT_2, "count2") + assert sys.inputs == [] + assert sys.constraints == [] + assert [str(e) for e in sys.bad_states] == ["eq(_state_0, 3'b111)"] + assert len(sys.states) == 1 + state = sys.states[0] + assert state.name == "_state_0" + assert str(state.symbol) == "_state_0" + assert str(state.init) == "3'b000" + assert str(state.next) == "add(_state_0, 3'b001)" + From 55f3ee91442c067faeccabdb1c113c6b7e8534f4 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Kevin=20L=C3=A4ufer?= Date: Wed, 15 Oct 2025 16:40:47 -0400 Subject: [PATCH 09/24] wip: simulation --- python/src/lib.rs | 17 +++++++++++++++++ python/src/sim.rs | 4 ++++ python/tests/test_btor2.py | 17 +++++++++++++++++ 3 files changed, 38 insertions(+) create mode 100644 python/src/sim.rs diff --git a/python/src/lib.rs b/python/src/lib.rs index 802538d..1036f28 100644 --- a/python/src/lib.rs +++ b/python/src/lib.rs @@ -1,4 +1,7 @@ mod ctx; +mod sim; + +use std::path::{PathBuf}; pub use ctx::Context; use ctx::{ContextGuardRead, ContextGuardWrite}; @@ -114,10 +117,24 @@ pub fn parse_btor2_str(content: &str, name: Option<&str>) -> PyResult PyResult { + let mut ctx_guard = ContextGuardWrite::default(); + let ctx = ctx_guard.deref_mut(); + match btor2::parse_file_with_ctx(filename, ctx) { + Some(sys) => Ok(TransitionSystem(sys)), + None => Err(PyValueError::new_err("failed to parse btor")), + } +} + #[pymodule] #[pyo3(name = "patronus")] fn patronus(_py: Python<'_>, m: &pyo3::Bound<'_, pyo3::types::PyModule>) -> PyResult<()> { m.add_class::()?; + m.add_class::()?; + m.add_class::()?; + m.add_class::()?; m.add_function(wrap_pyfunction!(parse_btor2_str, m)?)?; + m.add_function(wrap_pyfunction!(parse_btor2_file, m)?)?; Ok(()) } diff --git a/python/src/sim.rs b/python/src/sim.rs new file mode 100644 index 0000000..6981579 --- /dev/null +++ b/python/src/sim.rs @@ -0,0 +1,4 @@ +use pyo3::prelude::*; + +#[pyclass] +struct Simulator(Box>); \ No newline at end of file diff --git a/python/tests/test_btor2.py b/python/tests/test_btor2.py index 1584abc..148e0a4 100644 --- a/python/tests/test_btor2.py +++ b/python/tests/test_btor2.py @@ -43,4 +43,21 @@ def test_transition_system_fields(): assert str(state.symbol) == "_state_0" assert str(state.init) == "3'b000" assert str(state.next) == "add(_state_0, 3'b001)" + assert len(sys.outputs) == 0 +def test_transition_system_simulation(): + sys = parse_btor2_file(repo_root / "inputs" / "unittest" / "swap.btor") + sim = Interpreter(sys) + a, b = sys['a'], sys['b'] + + sim.init('zero') + assert sim[a] == 0, "a@0" + assert sim[b] == 1, "b@0" + + sim.step() + assert sim[a] == 1 + assert sim[b] == 0 + + sim.step() + assert sim[a] == 0 + assert sim[b] == 1 From 97550e687b74580a5378bf4606be1bc666f8460e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Kevin=20L=C3=A4ufer?= Date: Wed, 15 Oct 2025 16:56:40 -0400 Subject: [PATCH 10/24] wip: simulation --- python/Cargo.toml | 3 ++- python/src/lib.rs | 15 ++++++++++++++- python/src/sim.rs | 30 +++++++++++++++++++++++++++++- python/tests/test_btor2.py | 4 ++-- 4 files changed, 47 insertions(+), 5 deletions(-) diff --git a/python/Cargo.toml b/python/Cargo.toml index 9f5e9dd..1a48541 100644 --- a/python/Cargo.toml +++ b/python/Cargo.toml @@ -11,6 +11,7 @@ name = "patronus" crate-type = ["cdylib"] [dependencies] -pyo3 = { version = "0.26.0" } +pyo3 = { version = "0.26.0" , features = ["num-bigint"]} patronus = { path = "../patronus" } baa.workspace = true +bigint = "4.4.3" diff --git a/python/src/lib.rs b/python/src/lib.rs index 1036f28..d16ed0a 100644 --- a/python/src/lib.rs +++ b/python/src/lib.rs @@ -1,9 +1,10 @@ mod ctx; mod sim; -use std::path::{PathBuf}; pub use ctx::Context; use ctx::{ContextGuardRead, ContextGuardWrite}; +pub use sim::{Simulator, interpreter}; +use std::path::PathBuf; use ::patronus::btor2; use ::patronus::expr::SerializableIrNode; @@ -104,6 +105,17 @@ impl TransitionSystem { fn __str__(&self) -> String { self.0.serialize_to_str(ContextGuardRead::default().deref()) } + + /// look up states + fn __getitem__(&self, key: &str) -> Option { + let ctx_guard = ContextGuardRead::default(); + let ctx = ctx_guard.deref(); + self.0 + .states + .iter() + .find(|s| ctx.get_symbol_name(s.symbol).unwrap() == key) + .map(|s| State(*s)) + } } #[pyfunction] @@ -136,5 +148,6 @@ fn patronus(_py: Python<'_>, m: &pyo3::Bound<'_, pyo3::types::PyModule>) -> PyRe m.add_class::()?; m.add_function(wrap_pyfunction!(parse_btor2_str, m)?)?; m.add_function(wrap_pyfunction!(parse_btor2_file, m)?)?; + m.add_function(wrap_pyfunction!(interpreter, m)?)?; Ok(()) } diff --git a/python/src/sim.rs b/python/src/sim.rs index 6981579..bea3975 100644 --- a/python/src/sim.rs +++ b/python/src/sim.rs @@ -1,4 +1,32 @@ +use crate::TransitionSystem; +use crate::ctx::ContextGuardRead; +use patronus::expr::ExprRef; +use patronus::sim::InitKind; use pyo3::prelude::*; #[pyclass] -struct Simulator(Box>); \ No newline at end of file +pub struct Simulator(::patronus::sim::Interpreter); + +#[pymethods] +impl Simulator { + pub fn init(&mut self) { + use patronus::sim::Simulator; + self.0.init(InitKind::Zero); + } + + pub fn step(&mut self) { + use patronus::sim::Simulator; + self.0.step(); + } + + // fn __getitem__(&self, key: ExprRef) -> Option { + // + // } +} + +#[pyfunction] +#[pyo3(name = "Interpreter")] +pub fn interpreter(sys: &TransitionSystem) -> Simulator { + let interp = ::patronus::sim::Interpreter::new(ContextGuardRead::default().deref(), &sys.0); + Simulator(interp) +} diff --git a/python/tests/test_btor2.py b/python/tests/test_btor2.py index 148e0a4..2810c6e 100644 --- a/python/tests/test_btor2.py +++ b/python/tests/test_btor2.py @@ -48,9 +48,9 @@ def test_transition_system_fields(): def test_transition_system_simulation(): sys = parse_btor2_file(repo_root / "inputs" / "unittest" / "swap.btor") sim = Interpreter(sys) - a, b = sys['a'], sys['b'] + a, b = sys['a'].symbol, sys['b'].symbol - sim.init('zero') + sim.init() assert sim[a] == 0, "a@0" assert sim[b] == 1, "b@0" From 8eeb21aa7e66a5019dccf24a81ad414db72bbcb0 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Kevin=20L=C3=A4ufer?= Date: Thu, 16 Oct 2025 16:24:34 -0400 Subject: [PATCH 11/24] python: simple sim working --- python/Cargo.toml | 4 ++-- python/src/lib.rs | 3 +++ python/src/sim.rs | 19 ++++++++++++++----- 3 files changed, 19 insertions(+), 7 deletions(-) diff --git a/python/Cargo.toml b/python/Cargo.toml index 1a48541..6dfa06a 100644 --- a/python/Cargo.toml +++ b/python/Cargo.toml @@ -13,5 +13,5 @@ crate-type = ["cdylib"] [dependencies] pyo3 = { version = "0.26.0" , features = ["num-bigint"]} patronus = { path = "../patronus" } -baa.workspace = true -bigint = "4.4.3" +baa = { version = "0.17.1", features = ["rand1", "bigint"] } +num-bigint = "0.4.6" diff --git a/python/src/lib.rs b/python/src/lib.rs index d16ed0a..43a453e 100644 --- a/python/src/lib.rs +++ b/python/src/lib.rs @@ -12,6 +12,7 @@ use pyo3::exceptions::PyValueError; use pyo3::prelude::*; #[pyclass] +#[derive(Clone)] pub struct ExprRef(::patronus::expr::ExprRef); #[pymethods] @@ -22,6 +23,7 @@ impl ExprRef { } #[pyclass] +#[derive(Clone)] pub struct Output(::patronus::system::Output); #[pymethods] @@ -38,6 +40,7 @@ impl Output { } #[pyclass] +#[derive(Clone)] pub struct State(::patronus::system::State); #[pymethods] diff --git a/python/src/sim.rs b/python/src/sim.rs index bea3975..cb5197b 100644 --- a/python/src/sim.rs +++ b/python/src/sim.rs @@ -1,6 +1,7 @@ -use crate::TransitionSystem; use crate::ctx::ContextGuardRead; -use patronus::expr::ExprRef; +use crate::{ExprRef, TransitionSystem}; +use baa::{BitVecOps, Value}; +use num_bigint::BigInt; use patronus::sim::InitKind; use pyo3::prelude::*; @@ -19,9 +20,17 @@ impl Simulator { self.0.step(); } - // fn __getitem__(&self, key: ExprRef) -> Option { - // - // } + /// access the value of an expression + fn __getitem__(&self, key: ExprRef) -> Option { + use patronus::sim::Simulator; + let value = self.0.get(key.0); + match value { + Value::Array(_) => { + todo!("Array support!") + } + Value::BitVec(bv) => Some(bv.to_big_int()), + } + } } #[pyfunction] From 2829600ad2f771b3feacd004a38527f07688952b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Kevin=20L=C3=A4ufer?= Date: Thu, 16 Oct 2025 16:48:16 -0400 Subject: [PATCH 12/24] expr: build a simple expression --- python/src/expr.rs | 64 ++++++++++++++++++++++++++++++++++++++ python/src/lib.rs | 16 +++------- python/tests/test_btor2.py | 6 ++++ 3 files changed, 75 insertions(+), 11 deletions(-) create mode 100644 python/src/expr.rs diff --git a/python/src/expr.rs b/python/src/expr.rs new file mode 100644 index 0000000..8ef9ef2 --- /dev/null +++ b/python/src/expr.rs @@ -0,0 +1,64 @@ +use crate::ctx::{ContextGuardRead, ContextGuardWrite}; +use ::patronus::expr::SerializableIrNode; +use patronus::expr::{TypeCheck, WidthInt}; +use pyo3::exceptions::PyTypeError; +use pyo3::prelude::*; + +#[pyclass] +#[derive(Clone)] +pub struct ExprRef(pub(crate) patronus::expr::ExprRef); + +#[pymethods] +impl ExprRef { + fn __str__(&self) -> String { + self.0.serialize_to_str(ContextGuardRead::default().deref()) + } + + fn __lt__(&self, other: &Self) -> PyResult { + match (self.width(), other.width()) { + (Some(left), Some(right)) if left == right => { + // we default to signed, just like z3 + // a < b <=> b > a + Ok(ExprRef( + ContextGuardWrite::default() + .deref_mut() + .greater_signed(other.0, self.0), + )) + } + _ => Err(PyTypeError::new_err( + "Can only compare two bit vectors of the same width", + )), + } + } + + fn __gt__(&self, other: &Self) -> PyResult { + match (self.width(), other.width()) { + (Some(left), Some(right)) if left == right => { + // we default to signed, just like z3 + Ok(ExprRef( + ContextGuardWrite::default() + .deref_mut() + .greater_signed(self.0, other.0), + )) + } + _ => Err(PyTypeError::new_err( + "Can only compare two bit vectors of the same width", + )), + } + } + + fn width(&self) -> Option { + let c = ContextGuardRead::default(); + c.deref()[self.0].get_bv_type(c.deref()) + } +} + +#[pyfunction] +#[pyo3(name = "BitVec")] +pub fn bit_vec(name: &str, width: WidthInt) -> ExprRef { + ExprRef( + ContextGuardWrite::default() + .deref_mut() + .bv_symbol(name, width), + ) +} diff --git a/python/src/lib.rs b/python/src/lib.rs index 43a453e..c1ec5cc 100644 --- a/python/src/lib.rs +++ b/python/src/lib.rs @@ -1,8 +1,10 @@ mod ctx; +mod expr; mod sim; pub use ctx::Context; use ctx::{ContextGuardRead, ContextGuardWrite}; +pub use expr::{ExprRef, bit_vec}; pub use sim::{Simulator, interpreter}; use std::path::PathBuf; @@ -11,17 +13,6 @@ use ::patronus::expr::SerializableIrNode; use pyo3::exceptions::PyValueError; use pyo3::prelude::*; -#[pyclass] -#[derive(Clone)] -pub struct ExprRef(::patronus::expr::ExprRef); - -#[pymethods] -impl ExprRef { - fn __str__(&self) -> String { - self.0.serialize_to_str(ContextGuardRead::default().deref()) - } -} - #[pyclass] #[derive(Clone)] pub struct Output(::patronus::system::Output); @@ -151,6 +142,9 @@ fn patronus(_py: Python<'_>, m: &pyo3::Bound<'_, pyo3::types::PyModule>) -> PyRe m.add_class::()?; m.add_function(wrap_pyfunction!(parse_btor2_str, m)?)?; m.add_function(wrap_pyfunction!(parse_btor2_file, m)?)?; + // sim m.add_function(wrap_pyfunction!(interpreter, m)?)?; + // expr + m.add_function(wrap_pyfunction!(bit_vec, m)?)?; Ok(()) } diff --git a/python/tests/test_btor2.py b/python/tests/test_btor2.py index 2810c6e..ca7c143 100644 --- a/python/tests/test_btor2.py +++ b/python/tests/test_btor2.py @@ -61,3 +61,9 @@ def test_transition_system_simulation(): sim.step() assert sim[a] == 0 assert sim[b] == 1 + +def test_expression_builder(): + # we are emulating the Z3 API as much as possible + a = BitVec('a', 3) + b = BitVec('b', 3) + assert str(a < b) == "sgt(b, a)" From d78eb86d6bb1bb822551aae638be38882f3e2de1 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Kevin=20L=C3=A4ufer?= Date: Thu, 16 Oct 2025 17:01:42 -0400 Subject: [PATCH 13/24] wip: TransitionSystem construction from python --- python/src/lib.rs | 52 ++++++++++++++++++++++++++++++++++++++ python/tests/test_btor2.py | 10 ++++++++ 2 files changed, 62 insertions(+) diff --git a/python/src/lib.rs b/python/src/lib.rs index c1ec5cc..b86c62d 100644 --- a/python/src/lib.rs +++ b/python/src/lib.rs @@ -66,26 +66,78 @@ pub struct TransitionSystem(::patronus::system::TransitionSystem); #[pymethods] impl TransitionSystem { + #[new] + #[pyo3(signature = (name, inputs=None, states=None, outputs=None, bad_states=None, constraints=None))] + fn create( + name: &str, + inputs: Option>, + states: Option>, + outputs: Option>, + bad_states: Option>, + constraints: Option>, + ) -> Self { + Self(::patronus::system::TransitionSystem { + name: name.to_string(), + states: states + .map(|v| v.into_iter().map(|e| e.0).collect()) + .unwrap_or_default(), + inputs: inputs + .map(|v| v.into_iter().map(|e| e.0).collect()) + .unwrap_or_default(), + outputs: outputs + .map(|v| v.into_iter().map(|e| e.0).collect()) + .unwrap_or_default(), + bad_states: bad_states + .map(|v| v.into_iter().map(|e| e.0).collect()) + .unwrap_or_default(), + constraints: constraints + .map(|v| v.into_iter().map(|e| e.0).collect()) + .unwrap_or_default(), + names: Default::default(), + }) + } + #[getter] fn name(&self) -> &str { &self.0.name } + #[setter(name)] + fn set_name(&mut self, name: &str) { + self.0.name = name.to_string(); + } + #[getter] fn inputs(&self) -> Vec { self.0.inputs.iter().map(|e| ExprRef(*e)).collect() } + #[setter(inputs)] + fn set_inputs(&mut self, inputs: Vec) { + // TODO: validate that all inputs are symbols! + self.0.inputs = inputs.into_iter().map(|e| e.0).collect(); + } + #[getter] fn outputs(&self) -> Vec { self.0.outputs.iter().map(|e| Output(*e)).collect() } + #[setter(outputs)] + fn set_outputs(&mut self, outputs: Vec) { + self.0.outputs = outputs.into_iter().map(|e| e.0).collect(); + } + #[getter] fn states(&self) -> Vec { self.0.states.iter().map(|e| State(*e)).collect() } + #[setter(states)] + fn set_states(&mut self, states: Vec) { + self.0.states = states.into_iter().map(|e| e.0).collect(); + } + #[getter] fn bad_states(&self) -> Vec { self.0.bad_states.iter().map(|e| ExprRef(*e)).collect() diff --git a/python/tests/test_btor2.py b/python/tests/test_btor2.py index ca7c143..ec85290 100644 --- a/python/tests/test_btor2.py +++ b/python/tests/test_btor2.py @@ -67,3 +67,13 @@ def test_expression_builder(): a = BitVec('a', 3) b = BitVec('b', 3) assert str(a < b) == "sgt(b, a)" + + +def test_transition_system_builder(): + sys = TransitionSystem("test") + sys.inputs = [BitVec('en', 1)] + sys.states = [State('count_s', init=BitVecVal(0, 8), next=If(BitVec('en', 1), BitVec('count_s') + BitVecVal(1, 8), BitVec('count_s', 8)))] + sys.outputs = [Output('count', BitVec('count_s', 8))] + sys.bad_states.append(BitVec('count_s') == BitVecVal(123, 8)) + expected_system = "" + assert str(sys) == expected_system From 13375a42e8a54925dfab466b78da3d3bbf3aaab9 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Kevin=20L=C3=A4ufer?= Date: Fri, 17 Oct 2025 13:48:48 -0400 Subject: [PATCH 14/24] python: add more expression builder functions --- python/src/expr.rs | 115 ++++++++++++++++++++++++++++--------- python/src/lib.rs | 4 +- python/tests/test_btor2.py | 9 +-- 3 files changed, 96 insertions(+), 32 deletions(-) diff --git a/python/src/expr.rs b/python/src/expr.rs index 8ef9ef2..39afcdd 100644 --- a/python/src/expr.rs +++ b/python/src/expr.rs @@ -1,13 +1,39 @@ use crate::ctx::{ContextGuardRead, ContextGuardWrite}; use ::patronus::expr::SerializableIrNode; +use baa::BitVecValue; +use num_bigint::BigInt; use patronus::expr::{TypeCheck, WidthInt}; use pyo3::exceptions::PyTypeError; use pyo3::prelude::*; +use std::fmt::format; #[pyclass] #[derive(Clone)] pub struct ExprRef(pub(crate) patronus::expr::ExprRef); +/// Helper for binary ops that require a and b to be bitvectors of the same width +fn bv_bin_op( + a: &ExprRef, + b: &ExprRef, + op_str: &str, + op: fn( + &mut patronus::expr::Context, + patronus::expr::ExprRef, + patronus::expr::ExprRef, + ) -> patronus::expr::ExprRef, +) -> PyResult { + match (a.width(), b.width()) { + (Some(left), Some(right)) if left == right => { + let mut guard = ContextGuardWrite::default(); + let res = op(guard.deref_mut(), a.0, b.0); + Ok(ExprRef(res)) + } + _ => Err(PyTypeError::new_err(format!( + "Can only apply {op_str} two bit vectors of the same width" + ))), + } +} + #[pymethods] impl ExprRef { fn __str__(&self) -> String { @@ -15,36 +41,54 @@ impl ExprRef { } fn __lt__(&self, other: &Self) -> PyResult { - match (self.width(), other.width()) { - (Some(left), Some(right)) if left == right => { - // we default to signed, just like z3 - // a < b <=> b > a - Ok(ExprRef( - ContextGuardWrite::default() - .deref_mut() - .greater_signed(other.0, self.0), - )) - } - _ => Err(PyTypeError::new_err( - "Can only compare two bit vectors of the same width", - )), - } + // we default to signed, just like z3 + // a < b <=> b > a + bv_bin_op(self, other, "less than", |ctx, a, b| { + ctx.greater_signed(b, a) + }) } fn __gt__(&self, other: &Self) -> PyResult { - match (self.width(), other.width()) { - (Some(left), Some(right)) if left == right => { - // we default to signed, just like z3 - Ok(ExprRef( - ContextGuardWrite::default() - .deref_mut() - .greater_signed(self.0, other.0), - )) - } - _ => Err(PyTypeError::new_err( - "Can only compare two bit vectors of the same width", - )), - } + // we default to signed, just like z3 + bv_bin_op(self, other, "greater than", |ctx, a, b| { + ctx.greater_signed(a, b) + }) + } + + fn __add__(&self, other: &Self) -> PyResult { + bv_bin_op(self, other, "add", |ctx, a, b| ctx.add(a, b)) + } + + fn __sub__(&self, other: &Self) -> PyResult { + bv_bin_op(self, other, "sub", |ctx, a, b| ctx.sub(a, b)) + } + + fn __mul__(&self, other: &Self) -> PyResult { + bv_bin_op(self, other, "mul", |ctx, a, b| ctx.mul(a, b)) + } + + fn __or__(&self, other: &Self) -> PyResult { + bv_bin_op(self, other, "or", |ctx, a, b| ctx.or(a, b)) + } + + fn __and__(&self, other: &Self) -> PyResult { + bv_bin_op(self, other, "and", |ctx, a, b| ctx.and(a, b)) + } + + fn __xor__(&self, other: &Self) -> PyResult { + bv_bin_op(self, other, "xor", |ctx, a, b| ctx.xor(a, b)) + } + + fn __inv__(&self) -> PyResult { + Ok(ExprRef( + ContextGuardWrite::default().deref_mut().not(self.0), + )) + } + + fn __neg__(&self) -> PyResult { + Ok(ExprRef( + ContextGuardWrite::default().deref_mut().negate(self.0), + )) } fn width(&self) -> Option { @@ -62,3 +106,20 @@ pub fn bit_vec(name: &str, width: WidthInt) -> ExprRef { .bv_symbol(name, width), ) } + +#[pyfunction] +#[pyo3(name = "BitVecVal")] +pub fn bit_vec_val(value: BigInt, width: WidthInt) -> ExprRef { + let value = BitVecValue::from_big_int(&value, width); + ExprRef(ContextGuardWrite::default().deref_mut().bv_lit(&value)) +} + +#[pyfunction] +#[pyo3(name = "If")] +pub fn if_expr(cond: ExprRef, tru: ExprRef, fals: ExprRef) -> ExprRef { + ExprRef( + ContextGuardWrite::default() + .deref_mut() + .ite(cond.0, tru.0, fals.0), + ) +} diff --git a/python/src/lib.rs b/python/src/lib.rs index b86c62d..a743d9c 100644 --- a/python/src/lib.rs +++ b/python/src/lib.rs @@ -4,7 +4,7 @@ mod sim; pub use ctx::Context; use ctx::{ContextGuardRead, ContextGuardWrite}; -pub use expr::{ExprRef, bit_vec}; +pub use expr::*; pub use sim::{Simulator, interpreter}; use std::path::PathBuf; @@ -198,5 +198,7 @@ fn patronus(_py: Python<'_>, m: &pyo3::Bound<'_, pyo3::types::PyModule>) -> PyRe m.add_function(wrap_pyfunction!(interpreter, m)?)?; // expr m.add_function(wrap_pyfunction!(bit_vec, m)?)?; + m.add_function(wrap_pyfunction!(bit_vec_val, m)?)?; + m.add_function(wrap_pyfunction!(if_expr, m)?)?; Ok(()) } diff --git a/python/tests/test_btor2.py b/python/tests/test_btor2.py index ec85290..6b49c7e 100644 --- a/python/tests/test_btor2.py +++ b/python/tests/test_btor2.py @@ -71,9 +71,10 @@ def test_expression_builder(): def test_transition_system_builder(): sys = TransitionSystem("test") - sys.inputs = [BitVec('en', 1)] - sys.states = [State('count_s', init=BitVecVal(0, 8), next=If(BitVec('en', 1), BitVec('count_s') + BitVecVal(1, 8), BitVec('count_s', 8)))] - sys.outputs = [Output('count', BitVec('count_s', 8))] - sys.bad_states.append(BitVec('count_s') == BitVecVal(123, 8)) + en, count_s = BitVec('en', 1), BitVec('count_s', 8) + sys.inputs = [en] + sys.states = [State('count_s', init=BitVecVal(0, 8), next=If(en, count_s + BitVecVal(1, 8), count_s))] + sys.outputs = [Output('count', count_s)] + sys.bad_states.append(count_s == BitVecVal(123, 8)) expected_system = "" assert str(sys) == expected_system From a03f9bdd9831c109332696be4a1c960e2c4d4693 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Kevin=20L=C3=A4ufer?= Date: Fri, 17 Oct 2025 14:11:58 -0400 Subject: [PATCH 15/24] python: we can now build a transition system --- python/src/expr.rs | 4 +++ python/src/lib.rs | 63 ++++++++++++++++++++++++++++++++++++-- python/tests/test_btor2.py | 16 ++++++++-- 3 files changed, 78 insertions(+), 5 deletions(-) diff --git a/python/src/expr.rs b/python/src/expr.rs index 39afcdd..6643052 100644 --- a/python/src/expr.rs +++ b/python/src/expr.rs @@ -55,6 +55,10 @@ impl ExprRef { }) } + fn __eq__(&self, other: &Self) -> PyResult { + bv_bin_op(self, other, "equal", |ctx, a, b| ctx.equal(a, b)) + } + fn __add__(&self, other: &Self) -> PyResult { bv_bin_op(self, other, "add", |ctx, a, b| ctx.add(a, b)) } diff --git a/python/src/lib.rs b/python/src/lib.rs index a743d9c..9138556 100644 --- a/python/src/lib.rs +++ b/python/src/lib.rs @@ -9,8 +9,8 @@ pub use sim::{Simulator, interpreter}; use std::path::PathBuf; use ::patronus::btor2; -use ::patronus::expr::SerializableIrNode; -use pyo3::exceptions::PyValueError; +use ::patronus::expr::{SerializableIrNode, TypeCheck, WidthInt}; +use pyo3::exceptions::{PyRuntimeError, PyValueError}; use pyo3::prelude::*; #[pyclass] @@ -19,6 +19,15 @@ pub struct Output(::patronus::system::Output); #[pymethods] impl Output { + #[new] + fn create(name: &str, expr: ExprRef) -> Self { + let output = ::patronus::system::Output { + name: ContextGuardWrite::default().deref_mut().string(name.into()), + expr: expr.0, + }; + Self(output) + } + #[getter] fn name(&self) -> String { ContextGuardRead::default().deref()[self.0.name].to_string() @@ -36,6 +45,46 @@ pub struct State(::patronus::system::State); #[pymethods] impl State { + #[new] + #[pyo3(signature = (name, width=None, init=None, next=None))] + fn create( + name: &str, + width: Option, + init: Option, + next: Option, + ) -> PyResult { + let mut ctx_guard = ContextGuardWrite::default(); + let ctx = ctx_guard.deref_mut(); + let init_width = init.as_ref().and_then(|i| ctx[i.0].get_bv_type(ctx)); + let next_width = next.as_ref().and_then(|n| ctx[n.0].get_bv_type(ctx)); + let width = width.or(init_width).or(next_width); + if let Some(width) = width { + if let Some(iw) = init_width + && iw != width + { + Err(PyRuntimeError::new_err(format!( + "Width of init expression ({iw}) does not match width of {name} ({width})" + ))) + } else if let Some(nw) = next_width + && nw != width + { + Err(PyRuntimeError::new_err(format!( + "Width of next expression ({nw}) does not match width of {name} ({width})" + ))) + } else { + let symbol = ctx.bv_symbol(name, width); + let state = ::patronus::system::State { + symbol, + init: init.map(|i| i.0), + next: next.map(|n| n.0), + }; + Ok(Self(state)) + } + } else { + Err(PyRuntimeError::new_err("No width provided!")) + } + } + #[getter] fn symbol(&self) -> ExprRef { ExprRef(self.0.symbol) @@ -143,11 +192,21 @@ impl TransitionSystem { self.0.bad_states.iter().map(|e| ExprRef(*e)).collect() } + #[setter(bad_states)] + fn set_bad_states(&mut self, bad_states: Vec) { + self.0.bad_states = bad_states.into_iter().map(|e| e.0).collect(); + } + #[getter] fn constraints(&self) -> Vec { self.0.constraints.iter().map(|e| ExprRef(*e)).collect() } + #[setter(constraints)] + fn set_constraints(&mut self, constraints: Vec) { + self.0.constraints = constraints.into_iter().map(|e| e.0).collect(); + } + fn __str__(&self) -> String { self.0.serialize_to_str(ContextGuardRead::default().deref()) } diff --git a/python/tests/test_btor2.py b/python/tests/test_btor2.py index 6b49c7e..084151a 100644 --- a/python/tests/test_btor2.py +++ b/python/tests/test_btor2.py @@ -75,6 +75,16 @@ def test_transition_system_builder(): sys.inputs = [en] sys.states = [State('count_s', init=BitVecVal(0, 8), next=If(en, count_s + BitVecVal(1, 8), count_s))] sys.outputs = [Output('count', count_s)] - sys.bad_states.append(count_s == BitVecVal(123, 8)) - expected_system = "" - assert str(sys) == expected_system + # TODO: there is a big pitfall here: you cannot just `append` to the bad_states, inputs, etc. because we use + # a getter / setter approach + sys.bad_states = [count_s == BitVecVal(123, 8)] + expected_system = """ +test +input en : bv<1> +output count : bv<8> = count_s +bad %20 : bv<1> = eq(count, 8'b01111011) +state count_s : bv<8> + [init] 8'b00000000 + [next] ite(en, add(count, 8'b00000001), count) + """ + assert str(sys).strip() == expected_system.strip() From 2748963520ff322359fa3d801b8053a4da730c96 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Kevin=20L=C3=A4ufer?= Date: Fri, 17 Oct 2025 15:58:56 -0400 Subject: [PATCH 16/24] python: smt solver interface --- python/Cargo.toml | 1 + python/src/expr.rs | 3 +- python/src/lib.rs | 4 + python/src/smt.rs | 185 ++++++++++++++++++++ python/tests/{test_btor2.py => test_all.py} | 20 +++ 5 files changed, 211 insertions(+), 2 deletions(-) create mode 100644 python/src/smt.rs rename python/tests/{test_btor2.py => test_all.py} (84%) diff --git a/python/Cargo.toml b/python/Cargo.toml index 6dfa06a..13c881c 100644 --- a/python/Cargo.toml +++ b/python/Cargo.toml @@ -15,3 +15,4 @@ 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 diff --git a/python/src/expr.rs b/python/src/expr.rs index 6643052..590de90 100644 --- a/python/src/expr.rs +++ b/python/src/expr.rs @@ -5,10 +5,9 @@ use num_bigint::BigInt; use patronus::expr::{TypeCheck, WidthInt}; use pyo3::exceptions::PyTypeError; use pyo3::prelude::*; -use std::fmt::format; #[pyclass] -#[derive(Clone)] +#[derive(Clone, Copy)] pub struct ExprRef(pub(crate) patronus::expr::ExprRef); /// Helper for binary ops that require a and b to be bitvectors of the same width diff --git a/python/src/lib.rs b/python/src/lib.rs index 9138556..b203a54 100644 --- a/python/src/lib.rs +++ b/python/src/lib.rs @@ -1,11 +1,13 @@ mod ctx; mod expr; mod sim; +mod smt; pub use ctx::Context; use ctx::{ContextGuardRead, ContextGuardWrite}; pub use expr::*; pub use sim::{Simulator, interpreter}; +pub use smt::*; use std::path::PathBuf; use ::patronus::btor2; @@ -259,5 +261,7 @@ fn patronus(_py: Python<'_>, m: &pyo3::Bound<'_, pyo3::types::PyModule>) -> PyRe m.add_function(wrap_pyfunction!(bit_vec, m)?)?; m.add_function(wrap_pyfunction!(bit_vec_val, m)?)?; m.add_function(wrap_pyfunction!(if_expr, m)?)?; + // smt + m.add_function(wrap_pyfunction!(solver, m)?)?; Ok(()) } diff --git a/python/src/smt.rs b/python/src/smt.rs new file mode 100644 index 0000000..67aab84 --- /dev/null +++ b/python/src/smt.rs @@ -0,0 +1,185 @@ +use crate::ExprRef; +use crate::ctx::{ContextGuardRead, ContextGuardWrite}; +use baa::{BitVecOps, Value}; +use num_bigint::BigInt; +use patronus::expr::{Context, ForEachChild, TypeCheck}; +use patronus::mc::get_smt_value; +use patronus::smt::*; +use pyo3::exceptions::PyRuntimeError; +use pyo3::prelude::*; +use rustc_hash::{FxHashMap, FxHashSet}; +use std::fs::File; + +#[pyclass] +pub struct SolverCtx { + underlying: SmtLibSolverCtx, + declared_symbols: Vec>, +} + +impl SolverCtx { + fn new(underlying: SmtLibSolverCtx) -> Self { + Self { + underlying, + declared_symbols: vec![FxHashMap::default()], + } + } + + fn symbol_by_name(&self, name: &str) -> Option { + // from inner to outer + for map in self.declared_symbols.iter().rev() { + if let Some(symbol) = map.get(name) { + return Some(*symbol); + } + } + None + } +} + +fn find_symbols(ctx: &Context, e: patronus::expr::ExprRef) -> FxHashSet { + let mut out = FxHashSet::default(); + patronus::expr::traversal::bottom_up(ctx, e, |ctx, e, _| { + if ctx[e].is_symbol() { + out.insert(e); + } + }); + out +} + +#[pymethods] +impl SolverCtx { + #[pyo3(signature = (*assertions))] + fn check(&mut self, assertions: Vec) -> PyResult { + if !assertions.is_empty() { + self.push()?; + for a in assertions.iter() { + self.add(*a)?; + } + } + let r = self + .underlying + .check_sat() + .map(CheckSatResult) + .map_err(convert_smt_err)?; + if !assertions.is_empty() { + self.pop()?; + } + Ok(r) + } + + fn push(&mut self) -> PyResult<()> { + self.underlying.push().map_err(convert_smt_err)?; + self.declared_symbols.push(FxHashMap::default()); + Ok(()) + } + + fn pop(&mut self) -> PyResult<()> { + self.underlying.pop().map_err(convert_smt_err)?; + self.declared_symbols.pop(); + Ok(()) + } + + fn add(&mut self, assertion: ExprRef) -> PyResult<()> { + let ctx_guard = ContextGuardRead::default(); + let ctx = ctx_guard.deref(); + let a = assertion.0; + // scan the expression for any unknown symbols and declare them + let symbols = find_symbols(ctx, a); + for symbol in symbols.into_iter() { + let tpe = ctx[symbol].get_type(ctx); + let name = ctx[symbol].get_symbol_name(ctx).unwrap(); + if let Some(existing) = self.symbol_by_name(name) { + // check for compatible type for existing symbols + let existing_tpe = ctx[existing].get_type(ctx); + if existing_tpe != tpe { + return Err(PyRuntimeError::new_err(format!( + "There is already a symbol `{name}` with incompatible type {existing_tpe} != {tpe}" + ))); + } + } else { + // declare if symbol does not exist + self.underlying + .declare_const(ctx, symbol) + .map_err(convert_smt_err)?; + self.declared_symbols + .last_mut() + .unwrap() + .insert(name.to_string(), symbol); + } + } + + self.underlying.assert(ctx, a).map_err(convert_smt_err)?; + Ok(()) + } + + fn model(&mut self) -> PyResult { + let mut ctx_guard = ContextGuardWrite::default(); + let ctx = ctx_guard.deref_mut(); + let mut entries = vec![]; + for s in self.declared_symbols.iter().flat_map(|m| m.values()) { + let value = get_smt_value(ctx, &mut self.underlying, *s).map_err(convert_smt_err)?; + entries.push((*s, value)); + } + Ok(Model(entries)) + } +} + +#[pyclass] +pub struct Model(Vec<(patronus::expr::ExprRef, Value)>); + +#[pymethods] +impl Model { + fn __str__(&self) -> String { + "TODO".to_string() + } + + fn __len__(&self) -> usize { + self.0.len() + } + + fn __getitem__(&self, symbol: ExprRef) -> Option { + self.0 + .iter() + .find(|(e, _)| *e == symbol.0) + .map(|(_, value)| match value { + Value::Array(_) => { + todo!("Array support!") + } + Value::BitVec(bv) => bv.to_big_int(), + }) + } +} + +#[pyclass] +pub struct CheckSatResult(CheckSatResponse); + +#[pymethods] +impl CheckSatResult { + fn __str__(&self) -> String { + match self.0 { + CheckSatResponse::Sat => "sat".to_string(), + CheckSatResponse::Unsat => "unsat".to_string(), + CheckSatResponse::Unknown => "unknonw".to_string(), + } + } +} + +#[pyfunction] +#[pyo3(name = "Solver")] +pub fn solver(name: &str) -> PyResult { + match name.to_ascii_lowercase().as_str() { + "z3" => Ok(SolverCtx::new(Z3.start(None).map_err(convert_smt_err)?)), + "bitwuzla" => Ok(SolverCtx::new( + BITWUZLA.start(None).map_err(convert_smt_err)?, + )), + "yices" | "yices2" | "yices2-smt" => { + Ok(SolverCtx::new(YICES2.start(None).map_err(convert_smt_err)?)) + } + _ => Err(PyRuntimeError::new_err(format!( + "Unknonw or unsupported solver: {name}" + ))), + } +} + +fn convert_smt_err(e: Error) -> PyErr { + PyRuntimeError::new_err(format!("smt: {e}")) +} diff --git a/python/tests/test_btor2.py b/python/tests/test_all.py similarity index 84% rename from python/tests/test_btor2.py rename to python/tests/test_all.py index 084151a..684e710 100644 --- a/python/tests/test_btor2.py +++ b/python/tests/test_all.py @@ -88,3 +88,23 @@ def test_transition_system_builder(): [next] ite(en, add(count, 8'b00000001), count) """ assert str(sys).strip() == expected_system.strip() + + +def test_call_smt_solver(): + a = BitVec('a', 3) + b = BitVec('b', 3) + s = Solver('z3') + r = s.check(a < b) + assert str(r) == "sat" + + r = s.check(a < b, a > b) + assert str(r) == "unsat" + + # to generate a model, we need to actually add the assertion! + s.add(a < b) + s.check() + m = s.model() + assert len(m) == 2 + assert isinstance(m[a], int) + assert isinstance(m[b], int) + assert m[a] < m[b] From 056f015f1bb194db2b52253e445fd80a170a5a86 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Kevin=20L=C3=A4ufer?= Date: Mon, 20 Oct 2025 09:05:24 -0400 Subject: [PATCH 17/24] smt stuff and copyright and split tests --- patronus/src/smt/solver.rs | 9 +++++ python/src/ctx.rs | 4 +++ python/src/expr.rs | 4 +++ python/src/lib.rs | 6 ++++ python/src/sim.rs | 4 +++ python/src/smt.rs | 4 +++ python/tests/{test_all.py => test_lib.py} | 42 ++++------------------- python/tests/test_sim.py | 28 +++++++++++++++ python/tests/test_smt.py | 29 ++++++++++++++++ 9 files changed, 95 insertions(+), 35 deletions(-) rename python/tests/{test_all.py => test_lib.py} (69%) create mode 100644 python/tests/test_sim.py create mode 100644 python/tests/test_smt.py diff --git a/patronus/src/smt/solver.rs b/patronus/src/smt/solver.rs index 52a6ef2..5e3c748 100644 --- a/patronus/src/smt/solver.rs +++ b/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::*; diff --git a/python/src/ctx.rs b/python/src/ctx.rs index 9dd2823..3348496 100644 --- a/python/src/ctx.rs +++ b/python/src/ctx.rs @@ -1,3 +1,7 @@ +// Copyright 2025 Cornell University +// released under BSD 3-Clause License +// author: Kevin Laeufer + use pyo3::prelude::*; use std::ops::{Deref, DerefMut}; use std::sync::{LazyLock, RwLock, RwLockReadGuard, RwLockWriteGuard}; diff --git a/python/src/expr.rs b/python/src/expr.rs index 590de90..0ddcfdf 100644 --- a/python/src/expr.rs +++ b/python/src/expr.rs @@ -1,3 +1,7 @@ +// Copyright 2025 Cornell University +// released under BSD 3-Clause License +// author: Kevin Laeufer + use crate::ctx::{ContextGuardRead, ContextGuardWrite}; use ::patronus::expr::SerializableIrNode; use baa::BitVecValue; diff --git a/python/src/lib.rs b/python/src/lib.rs index b203a54..80f9d7e 100644 --- a/python/src/lib.rs +++ b/python/src/lib.rs @@ -1,3 +1,9 @@ +// Copyright 2025 The Regents of the University of California +// Copyright 2025 Cornell University +// released under BSD 3-Clause License +// author: Kevin Laeufer +// author: Adwait Godbole + mod ctx; mod expr; mod sim; diff --git a/python/src/sim.rs b/python/src/sim.rs index cb5197b..9447005 100644 --- a/python/src/sim.rs +++ b/python/src/sim.rs @@ -1,3 +1,7 @@ +// Copyright 2025 Cornell University +// released under BSD 3-Clause License +// author: Kevin Laeufer + use crate::ctx::ContextGuardRead; use crate::{ExprRef, TransitionSystem}; use baa::{BitVecOps, Value}; diff --git a/python/src/smt.rs b/python/src/smt.rs index 67aab84..996a035 100644 --- a/python/src/smt.rs +++ b/python/src/smt.rs @@ -1,3 +1,7 @@ +// Copyright 2025 Cornell University +// released under BSD 3-Clause License +// author: Kevin Laeufer + use crate::ExprRef; use crate::ctx::{ContextGuardRead, ContextGuardWrite}; use baa::{BitVecOps, Value}; diff --git a/python/tests/test_all.py b/python/tests/test_lib.py similarity index 69% rename from python/tests/test_all.py rename to python/tests/test_lib.py index 684e710..2dd307d 100644 --- a/python/tests/test_all.py +++ b/python/tests/test_lib.py @@ -1,3 +1,9 @@ +# Copyright 2025 Cornell University +# Copyright 2025 The Regents of the University of California +# released under BSD 3-Clause License +# author: Kevin Laeufer +# author: Adwait Godbole + import pathlib import pytest from patronus import * @@ -45,22 +51,6 @@ def test_transition_system_fields(): assert str(state.next) == "add(_state_0, 3'b001)" assert len(sys.outputs) == 0 -def test_transition_system_simulation(): - sys = parse_btor2_file(repo_root / "inputs" / "unittest" / "swap.btor") - sim = Interpreter(sys) - a, b = sys['a'].symbol, sys['b'].symbol - - sim.init() - assert sim[a] == 0, "a@0" - assert sim[b] == 1, "b@0" - - sim.step() - assert sim[a] == 1 - assert sim[b] == 0 - - sim.step() - assert sim[a] == 0 - assert sim[b] == 1 def test_expression_builder(): # we are emulating the Z3 API as much as possible @@ -82,7 +72,7 @@ def test_transition_system_builder(): test input en : bv<1> output count : bv<8> = count_s -bad %20 : bv<1> = eq(count, 8'b01111011) +bad %18 : bv<1> = eq(count, 8'b01111011) state count_s : bv<8> [init] 8'b00000000 [next] ite(en, add(count, 8'b00000001), count) @@ -90,21 +80,3 @@ def test_transition_system_builder(): assert str(sys).strip() == expected_system.strip() -def test_call_smt_solver(): - a = BitVec('a', 3) - b = BitVec('b', 3) - s = Solver('z3') - r = s.check(a < b) - assert str(r) == "sat" - - r = s.check(a < b, a > b) - assert str(r) == "unsat" - - # to generate a model, we need to actually add the assertion! - s.add(a < b) - s.check() - m = s.model() - assert len(m) == 2 - assert isinstance(m[a], int) - assert isinstance(m[b], int) - assert m[a] < m[b] diff --git a/python/tests/test_sim.py b/python/tests/test_sim.py new file mode 100644 index 0000000..31e3bc8 --- /dev/null +++ b/python/tests/test_sim.py @@ -0,0 +1,28 @@ +# Copyright 2025 Cornell University +# released under BSD 3-Clause License +# author: Kevin Laeufer + +import pathlib +import pytest +from patronus import * + +repo_root = (pathlib.Path(__file__) / '..' / '..' / '..').resolve() + + + +def test_transition_system_simulation(): + sys = parse_btor2_file(repo_root / "inputs" / "unittest" / "swap.btor") + sim = Interpreter(sys) + a, b = sys['a'].symbol, sys['b'].symbol + + sim.init() + assert sim[a] == 0, "a@0" + assert sim[b] == 1, "b@0" + + sim.step() + assert sim[a] == 1 + assert sim[b] == 0 + + sim.step() + assert sim[a] == 0 + assert sim[b] == 1 diff --git a/python/tests/test_smt.py b/python/tests/test_smt.py new file mode 100644 index 0000000..bc1d7b1 --- /dev/null +++ b/python/tests/test_smt.py @@ -0,0 +1,29 @@ +# Copyright 2025 Cornell University +# released under BSD 3-Clause License +# author: Kevin Laeufer + +import pathlib +import pytest +from patronus import * + +repo_root = (pathlib.Path(__file__) / '..' / '..' / '..').resolve() + +def test_call_smt_solver(): + a = BitVec('a', 3) + b = BitVec('b', 3) + s = Solver('z3') + r = s.check(a < b) + assert str(r) == "sat" + + r = s.check(a < b, a > b) + assert str(r) == "unsat" + + # to generate a model, we need to actually add the assertion! + s.add(a < b) + s.check() + m = s.model() + assert len(m) == 2 + assert isinstance(m[a], int) + assert isinstance(m[b], int) + assert m[a] < m[b] + From 7f0d67723ed71507237b38ed662039e04792b4ad Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Kevin=20L=C3=A4ufer?= Date: Mon, 20 Oct 2025 10:26:11 -0400 Subject: [PATCH 18/24] wip: BMC --- patronus/src/smt.rs | 2 +- python/src/lib.rs | 10 ++++++++++ python/src/mc.rs | 43 ++++++++++++++++++++++++++++++++++++++++ python/src/smt.rs | 43 +++++++++++++++++++++++++++++++--------- python/tests/test_lib.py | 5 +++++ python/tests/test_mc.py | 16 +++++++++++++++ python/tests/test_smt.py | 16 +++++++++++++++ 7 files changed, 125 insertions(+), 10 deletions(-) create mode 100644 python/src/mc.rs create mode 100644 python/tests/test_mc.py diff --git a/patronus/src/smt.rs b/patronus/src/smt.rs index e1f84b3..49606c9 100644 --- a/patronus/src/smt.rs +++ b/patronus/src/smt.rs @@ -7,6 +7,6 @@ mod parser; mod serialize; mod solver; -pub use parser::{parse_command, parse_expr}; +pub use parser::{parse_command, parse_expr, SmtParserError}; pub use serialize::serialize_cmd; pub use solver::*; diff --git a/python/src/lib.rs b/python/src/lib.rs index 80f9d7e..2383180 100644 --- a/python/src/lib.rs +++ b/python/src/lib.rs @@ -6,12 +6,14 @@ mod ctx; mod expr; +mod mc; mod sim; mod smt; pub use ctx::Context; use ctx::{ContextGuardRead, ContextGuardWrite}; pub use expr::*; +pub use mc::*; pub use sim::{Simulator, interpreter}; pub use smt::*; use std::path::PathBuf; @@ -229,6 +231,10 @@ impl TransitionSystem { .find(|s| ctx.get_symbol_name(s.symbol).unwrap() == key) .map(|s| State(*s)) } + + fn to_btor2_str(&self) -> String { + btor2::serialize_to_str(ContextGuardRead::default().deref(), &self.0) + } } #[pyfunction] @@ -269,5 +275,9 @@ fn patronus(_py: Python<'_>, m: &pyo3::Bound<'_, pyo3::types::PyModule>) -> PyRe m.add_function(wrap_pyfunction!(if_expr, m)?)?; // smt m.add_function(wrap_pyfunction!(solver, m)?)?; + m.add_function(wrap_pyfunction!(parse_smtlib_expr, m)?)?; + // mc + m.add_class::()?; + m.add_class::()?; Ok(()) } diff --git a/python/src/mc.rs b/python/src/mc.rs new file mode 100644 index 0000000..71e64ef --- /dev/null +++ b/python/src/mc.rs @@ -0,0 +1,43 @@ +// Copyright 2025 Cornell University +// released under BSD 3-Clause License +// author: Kevin Laeufer + +use crate::ctx::{ContextGuardRead, ContextGuardWrite}; +use crate::smt::{convert_smt_err, name_to_solver}; +use crate::{ExprRef, TransitionSystem}; +use patronus::smt::SmtLibSolver; +use pyo3::exceptions::PyRuntimeError; +use pyo3::prelude::*; +use std::fs::File; + +#[pyclass] +pub struct SmtModelChecker(::patronus::mc::SmtModelChecker); + +#[pyclass] +pub struct ModelCheckResult(::patronus::mc::ModelCheckResult); + +#[pymethods] +impl SmtModelChecker { + #[new] + #[pyo3(signature = (solver, check_constraints=true, check_bad_states_individually=false, save_smt_replay=false))] + fn create( + solver: &str, + check_constraints: bool, + check_bad_states_individually: bool, + save_smt_replay: bool, + ) -> PyResult { + let solver = name_to_solver(solver)?; + let opts = patronus::mc::SmtModelCheckerOptions { + check_constraints, + check_bad_states_individually, + save_smt_replay, + }; + let checker = patronus::mc::SmtModelChecker::new(solver, opts); + Ok(Self(checker)) + } + + fn check(&self, sys: &TransitionSystem, k_max: u64) -> PyResult { + Err(PyRuntimeError::new_err("TODO")) + // self.0.check(ContextGuardWrite::default().deref_mut(), &sys.0, k_max).map(ModelCheckResult).map_err(convert_smt_err) + } +} diff --git a/python/src/smt.rs b/python/src/smt.rs index 996a035..f878a4e 100644 --- a/python/src/smt.rs +++ b/python/src/smt.rs @@ -6,7 +6,7 @@ use crate::ExprRef; use crate::ctx::{ContextGuardRead, ContextGuardWrite}; use baa::{BitVecOps, Value}; use num_bigint::BigInt; -use patronus::expr::{Context, ForEachChild, TypeCheck}; +use patronus::expr::{Context, TypeCheck}; use patronus::mc::get_smt_value; use patronus::smt::*; use pyo3::exceptions::PyRuntimeError; @@ -170,20 +170,45 @@ impl CheckSatResult { #[pyfunction] #[pyo3(name = "Solver")] pub fn solver(name: &str) -> PyResult { + let solver = name_to_solver(name)?; + Ok(SolverCtx::new(solver.start(None).map_err(convert_smt_err)?)) +} + +pub(crate) fn name_to_solver(name: &str) -> PyResult { match name.to_ascii_lowercase().as_str() { - "z3" => Ok(SolverCtx::new(Z3.start(None).map_err(convert_smt_err)?)), - "bitwuzla" => Ok(SolverCtx::new( - BITWUZLA.start(None).map_err(convert_smt_err)?, - )), - "yices" | "yices2" | "yices2-smt" => { - Ok(SolverCtx::new(YICES2.start(None).map_err(convert_smt_err)?)) - } + "z3" => Ok(Z3), + "bitwuzla" => Ok(BITWUZLA), + "yices" | "yices2" | "yices2-smt" => Ok(YICES2), _ => Err(PyRuntimeError::new_err(format!( "Unknonw or unsupported solver: {name}" ))), } } -fn convert_smt_err(e: Error) -> PyErr { +#[pyfunction] +#[pyo3(signature = (value, symbols=None))] +pub fn parse_smtlib_expr( + value: &str, + symbols: Option>, +) -> PyResult { + let symbols = symbols + .unwrap_or_default() + .into_iter() + .map(|(k, v)| (k, v.0)) + .collect(); + parse_expr( + ContextGuardWrite::default().deref_mut(), + &symbols, + value.as_bytes(), + ) + .map_err(convert_smt_parse_err) + .map(ExprRef) +} + +pub(crate) fn convert_smt_err(e: Error) -> PyErr { + PyRuntimeError::new_err(format!("smt: {e}")) +} + +fn convert_smt_parse_err(e: SmtParserError) -> PyErr { PyRuntimeError::new_err(format!("smt: {e}")) } diff --git a/python/tests/test_lib.py b/python/tests/test_lib.py index 2dd307d..b2af2f9 100644 --- a/python/tests/test_lib.py +++ b/python/tests/test_lib.py @@ -38,6 +38,11 @@ def test_parse_and_serialize_count2(): """ assert expected_system.strip() == str(sys).strip() +@pytest.mark.skip(reason="btor2 serialization is not yet implemented in paronus") +def btor2_serialize(): + sys = parse_btor2_str(COUNT_2, "count2") + assert sys.to_btor2_str().strip() == COUNT_2.strip() + def test_transition_system_fields(): sys = parse_btor2_str(COUNT_2, "count2") assert sys.inputs == [] diff --git a/python/tests/test_mc.py b/python/tests/test_mc.py new file mode 100644 index 0000000..34fd614 --- /dev/null +++ b/python/tests/test_mc.py @@ -0,0 +1,16 @@ +# Copyright 2025 Cornell University +# released under BSD 3-Clause License +# author: Kevin Laeufer + +import pathlib +import pytest +from patronus import * + +repo_root = (pathlib.Path(__file__) / '..' / '..' / '..').resolve() + + + +def test_transition_system_model_checking(): + sys = parse_btor2_file(repo_root / "inputs" / "unittest" / "swap.btor") + mc = SmtModelChecker('z3') + mc.check(sys, 4) \ No newline at end of file diff --git a/python/tests/test_smt.py b/python/tests/test_smt.py index bc1d7b1..8f46044 100644 --- a/python/tests/test_smt.py +++ b/python/tests/test_smt.py @@ -27,3 +27,19 @@ def test_call_smt_solver(): assert isinstance(m[b], int) assert m[a] < m[b] + +def test_parse_smt_lib_expr(): + symbols = { + 'x_0': BitVec('x_0', 32), + 'y_0': BitVec('y_0', 32), + 'x_1': BitVec('x_1', 32), + } + a = parse_smtlib_expr("(= x_1 (bvadd x_0 y_0))", symbols) + assert str(a) == "eq(x_1, add(x_0, y_0))" + + +@pytest.mark.skip(reason="parsing commands is not implemented yet") +def test_parse_smt_lib_commands(): + parse_smtlib_cmd("(set-logic QF_BV)") + parse_smtlib_cmd("(set-option :produce-models true)") + parse_smtlib_cmd("(declare-const x_0 (_ BitVec 32))") From 297e72f519d40d668edbc6663f97b0711e5426de Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Kevin=20L=C3=A4ufer?= Date: Mon, 20 Oct 2025 11:41:05 -0400 Subject: [PATCH 19/24] python: model checker --- patronus/src/mc/smt.rs | 6 ++++++ patronus/src/smt.rs | 2 +- python/src/mc.rs | 8 ++++++-- 3 files changed, 13 insertions(+), 3 deletions(-) diff --git a/patronus/src/mc/smt.rs b/patronus/src/mc/smt.rs index 79e909c..171410c 100644 --- a/patronus/src/mc/smt.rs +++ b/patronus/src/mc/smt.rs @@ -42,6 +42,12 @@ impl> SmtModelChecker { k_max: u64, ) -> Result { 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 { diff --git a/patronus/src/smt.rs b/patronus/src/smt.rs index 49606c9..3cc3bfd 100644 --- a/patronus/src/smt.rs +++ b/patronus/src/smt.rs @@ -7,6 +7,6 @@ mod parser; mod serialize; mod solver; -pub use parser::{parse_command, parse_expr, SmtParserError}; +pub use parser::{SmtParserError, parse_command, parse_expr}; pub use serialize::serialize_cmd; pub use solver::*; diff --git a/python/src/mc.rs b/python/src/mc.rs index 71e64ef..ff06c7d 100644 --- a/python/src/mc.rs +++ b/python/src/mc.rs @@ -37,7 +37,11 @@ impl SmtModelChecker { } fn check(&self, sys: &TransitionSystem, k_max: u64) -> PyResult { - Err(PyRuntimeError::new_err("TODO")) - // self.0.check(ContextGuardWrite::default().deref_mut(), &sys.0, k_max).map(ModelCheckResult).map_err(convert_smt_err) + let mut ctx_guard = ContextGuardWrite::default(); + let ctx = ctx_guard.deref_mut(); + self.0 + .check(ctx, &sys.0, k_max) + .map(ModelCheckResult) + .map_err(convert_smt_err) } } From 5c52a41790fa563babd071e3e25117a8d061d68a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Kevin=20L=C3=A4ufer?= Date: Mon, 20 Oct 2025 13:20:59 -0400 Subject: [PATCH 20/24] ci: install solvers --- .github/workflows/test.yml | 2 ++ 1 file changed, 2 insertions(+) diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml index 4e45ce4..c9d898f 100644 --- a/.github/workflows/test.yml +++ b/.github/workflows/test.yml @@ -215,6 +215,8 @@ jobs: 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: From c4111d4d50bc5d43b11379d5ddb753197a776614 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Kevin=20L=C3=A4ufer?= Date: Mon, 20 Oct 2025 14:06:51 -0400 Subject: [PATCH 21/24] python: expose simplify --- python/src/expr.rs | 80 ++++++++++++++++++++++++++++++++++++--- python/src/lib.rs | 44 +++++++++++++++++++++ python/src/mc.rs | 44 +++++++++++++++++---- python/tests/test_expr.py | 20 ++++++++++ python/tests/test_lib.py | 4 +- python/tests/test_mc.py | 18 ++++++++- 6 files changed, 195 insertions(+), 15 deletions(-) create mode 100644 python/tests/test_expr.py diff --git a/python/src/expr.rs b/python/src/expr.rs index 0ddcfdf..688d5ac 100644 --- a/python/src/expr.rs +++ b/python/src/expr.rs @@ -6,9 +6,12 @@ use crate::ctx::{ContextGuardRead, ContextGuardWrite}; use ::patronus::expr::SerializableIrNode; use baa::BitVecValue; use num_bigint::BigInt; -use patronus::expr::{TypeCheck, WidthInt}; -use pyo3::exceptions::PyTypeError; +use patronus::expr::{SparseExprMap, TypeCheck, WidthInt}; +use pyo3::exceptions::{PyRuntimeError, PyTypeError}; use pyo3::prelude::*; +use pyo3::types::PySlice; +use std::ops::DerefMut; +use std::sync::{LazyLock, RwLock}; #[pyclass] #[derive(Clone, Copy)] @@ -39,10 +42,14 @@ fn bv_bin_op( #[pymethods] impl ExprRef { - fn __str__(&self) -> String { + pub(crate) fn __str__(&self) -> String { self.0.serialize_to_str(ContextGuardRead::default().deref()) } + fn __repr__(&self) -> String { + self.__str__() + } + fn __lt__(&self, other: &Self) -> PyResult { // we default to signed, just like z3 // a < b <=> b > a @@ -58,7 +65,7 @@ impl ExprRef { }) } - fn __eq__(&self, other: &Self) -> PyResult { + fn equals(&self, other: &Self) -> PyResult { bv_bin_op(self, other, "equal", |ctx, a, b| ctx.equal(a, b)) } @@ -86,7 +93,7 @@ impl ExprRef { bv_bin_op(self, other, "xor", |ctx, a, b| ctx.xor(a, b)) } - fn __inv__(&self) -> PyResult { + fn __invert__(&self) -> PyResult { Ok(ExprRef( ContextGuardWrite::default().deref_mut().not(self.0), )) @@ -98,10 +105,45 @@ impl ExprRef { )) } + // TODO: find a way to accept "invalid" slices + // fn __getitem__<'py>(&self, index: Bound<'py, PySlice>)-> PyResult { + // let mut guard = ContextGuardWrite::default(); + // let ctx = guard.deref_mut(); + // if let Some(width) = ctx[self.0].get_bv_type(ctx) { + // let indices = index.as_borrowed().indices(width as isize)?; + // Ok(ExprRef(ctx.slice(self.0, indices.stop as WidthInt, indices.start as WidthInt))) + // } else { + // Err(PyRuntimeError::new_err("Can only slice bit vectors!")) + // } + // + // } + fn width(&self) -> Option { let c = ContextGuardRead::default(); c.deref()[self.0].get_bv_type(c.deref()) } + + /// Compares reference equality. + /// This is different from the Z3 API where `==` builds an SMT expressoion + fn __eq__(&self, other: &Self) -> bool { + self.0 == other.0 + } +} + +/// Simplifier that is used by default for all operations. +/// Python usage is expected to be less performance critical, so using a single global +/// simplifier seems acceptable and will simplify use. +static DEFAULT_SIMPLIFIER: LazyLock< + RwLock<::patronus::expr::Simplifier>>>, +> = LazyLock::new(|| RwLock::new(::patronus::expr::Simplifier::new(SparseExprMap::default()))); + +#[pyfunction] +pub fn simplify(e: ExprRef) -> ExprRef { + let mut guard = DEFAULT_SIMPLIFIER.write().unwrap(); + let r = guard + .deref_mut() + .simplify(ContextGuardWrite::default().deref_mut(), e.0); + ExprRef(r) } #[pyfunction] @@ -130,3 +172,31 @@ pub fn if_expr(cond: ExprRef, tru: ExprRef, fals: ExprRef) -> ExprRef { .ite(cond.0, tru.0, fals.0), ) } + +#[pyfunction] +#[pyo3(name = "SignExt")] +pub fn sext(n: WidthInt, a: ExprRef) -> ExprRef { + ExprRef(ContextGuardWrite::default().deref_mut().sign_extend(a.0, n)) +} + +#[pyfunction] +#[pyo3(name = "ZeroExt")] +pub fn zext(n: WidthInt, a: ExprRef) -> ExprRef { + ExprRef(ContextGuardWrite::default().deref_mut().zero_extend(a.0, n)) +} + +#[pyfunction] +#[pyo3(name = "Extract")] +pub fn extract(high: WidthInt, low: WidthInt, a: ExprRef) -> ExprRef { + slice(high, low, a) +} + +#[pyfunction] +#[pyo3(name = "Slice")] +pub fn slice(high: WidthInt, low: WidthInt, a: ExprRef) -> ExprRef { + ExprRef( + ContextGuardWrite::default() + .deref_mut() + .slice(a.0, high, low), + ) +} diff --git a/python/src/lib.rs b/python/src/lib.rs index 2383180..2dab6a5 100644 --- a/python/src/lib.rs +++ b/python/src/lib.rs @@ -177,6 +177,19 @@ impl TransitionSystem { self.0.inputs = inputs.into_iter().map(|e| e.0).collect(); } + fn add_input(&mut self, symbol: ExprRef) -> PyResult<()> { + let is_symbol = ContextGuardRead::default().deref()[symbol.0].is_symbol(); + if !is_symbol { + Err(PyRuntimeError::new_err(format!( + "{} is not a symbol", + symbol.__str__() + ))) + } else { + self.0.inputs.push(symbol.0); + Ok(()) + } + } + #[getter] fn outputs(&self) -> Vec { self.0.outputs.iter().map(|e| Output(*e)).collect() @@ -187,6 +200,14 @@ impl TransitionSystem { self.0.outputs = outputs.into_iter().map(|e| e.0).collect(); } + fn add_output(&mut self, name: String, expr: ExprRef) { + let name_id = ContextGuardWrite::default().deref_mut().string(name.into()); + self.0.outputs.push(::patronus::system::Output { + name: name_id, + expr: expr.0, + }); + } + #[getter] fn states(&self) -> Vec { self.0.states.iter().map(|e| State(*e)).collect() @@ -202,6 +223,18 @@ impl TransitionSystem { self.0.bad_states.iter().map(|e| ExprRef(*e)).collect() } + fn add_bad_state(&mut self, name: String, expr: ExprRef) { + self.0.bad_states.push(expr.0); + let name_id = ContextGuardWrite::default().deref_mut().string(name.into()); + self.0.names[expr.0] = Some(name_id); + } + + fn add_assertion(&mut self, name: &str, expr: ExprRef) { + let not_name = format!("not_{name}"); + let not_expr = ContextGuardWrite::default().deref_mut().not(expr.0); + self.add_bad_state(not_name, ExprRef(not_expr)); + } + #[setter(bad_states)] fn set_bad_states(&mut self, bad_states: Vec) { self.0.bad_states = bad_states.into_iter().map(|e| e.0).collect(); @@ -217,6 +250,12 @@ impl TransitionSystem { self.0.constraints = constraints.into_iter().map(|e| e.0).collect(); } + fn add_constraint(&mut self, name: String, expr: ExprRef) { + self.0.constraints.push(expr.0); + let name_id = ContextGuardWrite::default().deref_mut().string(name.into()); + self.0.names[expr.0] = Some(name_id); + } + fn __str__(&self) -> String { self.0.serialize_to_str(ContextGuardRead::default().deref()) } @@ -273,6 +312,11 @@ fn patronus(_py: Python<'_>, m: &pyo3::Bound<'_, pyo3::types::PyModule>) -> PyRe m.add_function(wrap_pyfunction!(bit_vec, m)?)?; m.add_function(wrap_pyfunction!(bit_vec_val, m)?)?; m.add_function(wrap_pyfunction!(if_expr, m)?)?; + m.add_function(wrap_pyfunction!(simplify, m)?)?; + m.add_function(wrap_pyfunction!(zext, m)?)?; + m.add_function(wrap_pyfunction!(sext, m)?)?; + m.add_function(wrap_pyfunction!(extract, m)?)?; + m.add_function(wrap_pyfunction!(slice, m)?)?; // smt m.add_function(wrap_pyfunction!(solver, m)?)?; m.add_function(wrap_pyfunction!(parse_smtlib_expr, m)?)?; diff --git a/python/src/mc.rs b/python/src/mc.rs index ff06c7d..7faea45 100644 --- a/python/src/mc.rs +++ b/python/src/mc.rs @@ -2,20 +2,15 @@ // released under BSD 3-Clause License // author: Kevin Laeufer -use crate::ctx::{ContextGuardRead, ContextGuardWrite}; +use crate::ctx::ContextGuardWrite; use crate::smt::{convert_smt_err, name_to_solver}; -use crate::{ExprRef, TransitionSystem}; +use crate::{Model, TransitionSystem}; use patronus::smt::SmtLibSolver; -use pyo3::exceptions::PyRuntimeError; use pyo3::prelude::*; -use std::fs::File; #[pyclass] pub struct SmtModelChecker(::patronus::mc::SmtModelChecker); -#[pyclass] -pub struct ModelCheckResult(::patronus::mc::ModelCheckResult); - #[pymethods] impl SmtModelChecker { #[new] @@ -45,3 +40,38 @@ impl SmtModelChecker { .map_err(convert_smt_err) } } + +#[pyclass] +pub struct ModelCheckResult(::patronus::mc::ModelCheckResult); + +#[pymethods] +impl ModelCheckResult { + fn __str__(&self) -> String { + match &self.0 { + patronus::mc::ModelCheckResult::Success => "unsat".to_string(), + patronus::mc::ModelCheckResult::Fail(_) => "sat".to_string(), + } + } + + fn __len__(&self) -> usize { + match &self.0 { + patronus::mc::ModelCheckResult::Success => 0, + patronus::mc::ModelCheckResult::Fail(w) => w.inputs.len(), + } + } + + #[getter] + fn inits(&self) -> Option { + match &self.0 { + patronus::mc::ModelCheckResult::Success => None, + patronus::mc::ModelCheckResult::Fail(w) => { + todo!() + } + } + } + + #[getter] + fn inputs(&self) -> Vec { + todo!() + } +} diff --git a/python/tests/test_expr.py b/python/tests/test_expr.py new file mode 100644 index 0000000..873165e --- /dev/null +++ b/python/tests/test_expr.py @@ -0,0 +1,20 @@ +# Copyright 2025 Cornell University +# released under BSD 3-Clause License +# author: Kevin Laeufer + +from patronus import * + +def test_simplify(): + # by default this uses a global simplifier + true = BitVecVal(1, 1) + false = BitVecVal(0,1) + a = BitVec('a', 1) + assert simplify((~a) & a) == false + assert simplify((~a) | a) == true + + assert simplify(SignExt(1, false)) == BitVecVal(0b00, 2) + assert simplify(SignExt(1, true)) == BitVecVal(0b11, 2) + + assert simplify(BitVecVal(0, 4).equals(Extract(8, 5, ZeroExt(4, BitVec('a', 5))))) == true + + diff --git a/python/tests/test_lib.py b/python/tests/test_lib.py index b2af2f9..0adbf2d 100644 --- a/python/tests/test_lib.py +++ b/python/tests/test_lib.py @@ -72,12 +72,12 @@ def test_transition_system_builder(): sys.outputs = [Output('count', count_s)] # TODO: there is a big pitfall here: you cannot just `append` to the bad_states, inputs, etc. because we use # a getter / setter approach - sys.bad_states = [count_s == BitVecVal(123, 8)] + sys.add_bad_state('count_is_123', count_s.equals(BitVecVal(123, 8))) expected_system = """ test input en : bv<1> output count : bv<8> = count_s -bad %18 : bv<1> = eq(count, 8'b01111011) +bad count_is_123 : bv<1> = eq(count, 8'b01111011) state count_s : bv<8> [init] 8'b00000000 [next] ite(en, add(count, 8'b00000001), count) diff --git a/python/tests/test_mc.py b/python/tests/test_mc.py index 34fd614..9bcbd70 100644 --- a/python/tests/test_mc.py +++ b/python/tests/test_mc.py @@ -13,4 +13,20 @@ def test_transition_system_model_checking(): sys = parse_btor2_file(repo_root / "inputs" / "unittest" / "swap.btor") mc = SmtModelChecker('z3') - mc.check(sys, 4) \ No newline at end of file + # there are no assertions in this circuit, so it cannot fail + assert str(mc.check(sys, 4)) == "unsat" + + # add an assertion + a = next(s.symbol for s in sys.states if str(s.symbol) == 'a') + b = next(s.symbol for s in sys.states if str(s.symbol) == 'b') + sys.add_assertion("a_is_0", a.equals(BitVecVal(0, 8))) + r = mc.check(sys, 4) + assert str(r) == "sat" + + # check model + assert len(r) == 2, "fail in step 2" + + # check initial values + # TODO! + # assert r[a] == BitVecVal(0, 8) + # assert r[b] == BitVecVal(1, 8) \ No newline at end of file From 2ff8f770735b177d9a5c0bd43229dc05b7b8391e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Kevin=20L=C3=A4ufer?= Date: Mon, 20 Oct 2025 14:16:15 -0400 Subject: [PATCH 22/24] python: rename to patronpy --- python/Cargo.toml | 4 ++-- python/pyproject.toml | 2 +- python/src/expr.rs | 3 +-- python/src/lib.rs | 28 ++++++++++++++-------------- python/src/mc.rs | 2 +- python/tests/test_expr.py | 2 +- python/tests/test_lib.py | 2 +- python/tests/test_mc.py | 2 +- python/tests/test_sim.py | 2 +- python/tests/test_smt.py | 2 +- python/uv.lock | 2 +- 11 files changed, 25 insertions(+), 26 deletions(-) diff --git a/python/Cargo.toml b/python/Cargo.toml index 13c881c..6194b72 100644 --- a/python/Cargo.toml +++ b/python/Cargo.toml @@ -1,5 +1,5 @@ [package] -name = "patronus_py" +name = "patronpy" description = "PyO3 bindings for Patronus" version.workspace = true rust-version.workspace = true @@ -7,7 +7,7 @@ edition.workspace = true license.workspace = true [lib] -name = "patronus" +name = "patronpy" crate-type = ["cdylib"] [dependencies] diff --git a/python/pyproject.toml b/python/pyproject.toml index e23fe06..43693fb 100644 --- a/python/pyproject.toml +++ b/python/pyproject.toml @@ -1,5 +1,5 @@ [project] -name = "patronus" +name = "patronpy" requires-python = ">=3.9" dynamic = ["version"] license = "BSD-3-Clause" diff --git a/python/src/expr.rs b/python/src/expr.rs index 688d5ac..a463ed9 100644 --- a/python/src/expr.rs +++ b/python/src/expr.rs @@ -7,9 +7,8 @@ use ::patronus::expr::SerializableIrNode; use baa::BitVecValue; use num_bigint::BigInt; use patronus::expr::{SparseExprMap, TypeCheck, WidthInt}; -use pyo3::exceptions::{PyRuntimeError, PyTypeError}; +use pyo3::exceptions::PyTypeError; use pyo3::prelude::*; -use pyo3::types::PySlice; use std::ops::DerefMut; use std::sync::{LazyLock, RwLock}; diff --git a/python/src/lib.rs b/python/src/lib.rs index 2dab6a5..e982c62 100644 --- a/python/src/lib.rs +++ b/python/src/lib.rs @@ -18,20 +18,20 @@ pub use sim::{Simulator, interpreter}; pub use smt::*; use std::path::PathBuf; -use ::patronus::btor2; -use ::patronus::expr::{SerializableIrNode, TypeCheck, WidthInt}; +use patronus::btor2; +use patronus::expr::{SerializableIrNode, TypeCheck, WidthInt}; use pyo3::exceptions::{PyRuntimeError, PyValueError}; use pyo3::prelude::*; #[pyclass] #[derive(Clone)] -pub struct Output(::patronus::system::Output); +pub struct Output(patronus::system::Output); #[pymethods] impl Output { #[new] fn create(name: &str, expr: ExprRef) -> Self { - let output = ::patronus::system::Output { + let output = patronus::system::Output { name: ContextGuardWrite::default().deref_mut().string(name.into()), expr: expr.0, }; @@ -51,7 +51,7 @@ impl Output { #[pyclass] #[derive(Clone)] -pub struct State(::patronus::system::State); +pub struct State(patronus::system::State); #[pymethods] impl State { @@ -83,7 +83,7 @@ impl State { ))) } else { let symbol = ctx.bv_symbol(name, width); - let state = ::patronus::system::State { + let state = patronus::system::State { symbol, init: init.map(|i| i.0), next: next.map(|n| n.0), @@ -111,17 +111,17 @@ impl State { #[getter] fn next(&self) -> Option { - self.0.next.map(|e| ExprRef(e)) + self.0.next.map(ExprRef) } #[getter] fn init(&self) -> Option { - self.0.init.map(|e| ExprRef(e)) + self.0.init.map(ExprRef) } } #[pyclass] -pub struct TransitionSystem(::patronus::system::TransitionSystem); +pub struct TransitionSystem(patronus::system::TransitionSystem); #[pymethods] impl TransitionSystem { @@ -135,7 +135,7 @@ impl TransitionSystem { bad_states: Option>, constraints: Option>, ) -> Self { - Self(::patronus::system::TransitionSystem { + Self(patronus::system::TransitionSystem { name: name.to_string(), states: states .map(|v| v.into_iter().map(|e| e.0).collect()) @@ -202,7 +202,7 @@ impl TransitionSystem { fn add_output(&mut self, name: String, expr: ExprRef) { let name_id = ContextGuardWrite::default().deref_mut().string(name.into()); - self.0.outputs.push(::patronus::system::Output { + self.0.outputs.push(patronus::system::Output { name: name_id, expr: expr.0, }); @@ -281,7 +281,7 @@ impl TransitionSystem { pub fn parse_btor2_str(content: &str, name: Option<&str>) -> PyResult { let mut ctx_guard = ContextGuardWrite::default(); let ctx = ctx_guard.deref_mut(); - match btor2::parse_str(ctx, &content, name) { + match btor2::parse_str(ctx, content, name) { Some(sys) => Ok(TransitionSystem(sys)), None => Err(PyValueError::new_err("failed to parse btor")), } @@ -298,8 +298,8 @@ pub fn parse_btor2_file(filename: PathBuf) -> PyResult { } #[pymodule] -#[pyo3(name = "patronus")] -fn patronus(_py: Python<'_>, m: &pyo3::Bound<'_, pyo3::types::PyModule>) -> PyResult<()> { +#[pyo3(name = "patronpy")] +fn patronpy(_py: Python<'_>, m: &pyo3::Bound<'_, pyo3::types::PyModule>) -> PyResult<()> { m.add_class::()?; m.add_class::()?; m.add_class::()?; diff --git a/python/src/mc.rs b/python/src/mc.rs index 7faea45..49056fc 100644 --- a/python/src/mc.rs +++ b/python/src/mc.rs @@ -64,7 +64,7 @@ impl ModelCheckResult { fn inits(&self) -> Option { match &self.0 { patronus::mc::ModelCheckResult::Success => None, - patronus::mc::ModelCheckResult::Fail(w) => { + patronus::mc::ModelCheckResult::Fail(_w) => { todo!() } } diff --git a/python/tests/test_expr.py b/python/tests/test_expr.py index 873165e..783c71e 100644 --- a/python/tests/test_expr.py +++ b/python/tests/test_expr.py @@ -2,7 +2,7 @@ # released under BSD 3-Clause License # author: Kevin Laeufer -from patronus import * +from patronpy import * def test_simplify(): # by default this uses a global simplifier diff --git a/python/tests/test_lib.py b/python/tests/test_lib.py index 0adbf2d..d365c65 100644 --- a/python/tests/test_lib.py +++ b/python/tests/test_lib.py @@ -6,7 +6,7 @@ import pathlib import pytest -from patronus import * +from patronpy import * repo_root = (pathlib.Path(__file__) / '..' / '..' / '..').resolve() diff --git a/python/tests/test_mc.py b/python/tests/test_mc.py index 9bcbd70..1df4ca9 100644 --- a/python/tests/test_mc.py +++ b/python/tests/test_mc.py @@ -4,7 +4,7 @@ import pathlib import pytest -from patronus import * +from patronpy import * repo_root = (pathlib.Path(__file__) / '..' / '..' / '..').resolve() diff --git a/python/tests/test_sim.py b/python/tests/test_sim.py index 31e3bc8..411ed4c 100644 --- a/python/tests/test_sim.py +++ b/python/tests/test_sim.py @@ -4,7 +4,7 @@ import pathlib import pytest -from patronus import * +from patronpy import * repo_root = (pathlib.Path(__file__) / '..' / '..' / '..').resolve() diff --git a/python/tests/test_smt.py b/python/tests/test_smt.py index 8f46044..3f3d161 100644 --- a/python/tests/test_smt.py +++ b/python/tests/test_smt.py @@ -4,7 +4,7 @@ import pathlib import pytest -from patronus import * +from patronpy import * repo_root = (pathlib.Path(__file__) / '..' / '..' / '..').resolve() diff --git a/python/uv.lock b/python/uv.lock index 50b6771..7383028 100644 --- a/python/uv.lock +++ b/python/uv.lock @@ -42,7 +42,7 @@ wheels = [ ] [[package]] -name = "patronus" +name = "patronpy" source = { editable = "." } [package.dev-dependencies] From 5d979a51e9153289157b96413463a885a8714675 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Kevin=20L=C3=A4ufer?= Date: Mon, 20 Oct 2025 14:18:53 -0400 Subject: [PATCH 23/24] ci: add python release --- .github/workflows/release.yml | 101 ++++++++++++++++++++++++++++++++++ 1 file changed, 101 insertions(+) create mode 100644 .github/workflows/release.yml diff --git a/.github/workflows/release.yml b/.github/workflows/release.yml new file mode 100644 index 0000000..575a597 --- /dev/null +++ b/.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-*/* From 3cda29c2c262d7aca0085fc691b132b43a7bf62c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Kevin=20L=C3=A4ufer?= Date: Mon, 20 Oct 2025 14:23:09 -0400 Subject: [PATCH 24/24] rename to pypatronus --- python/Cargo.toml | 4 ++-- python/pyproject.toml | 2 +- python/src/lib.rs | 4 ++-- python/tests/test_expr.py | 2 +- python/tests/test_lib.py | 2 +- python/tests/test_mc.py | 2 +- python/tests/test_sim.py | 2 +- python/tests/test_smt.py | 2 +- python/uv.lock | 28 ++++++++++++++-------------- 9 files changed, 24 insertions(+), 24 deletions(-) diff --git a/python/Cargo.toml b/python/Cargo.toml index 6194b72..eb30890 100644 --- a/python/Cargo.toml +++ b/python/Cargo.toml @@ -1,5 +1,5 @@ [package] -name = "patronpy" +name = "pypatronus" description = "PyO3 bindings for Patronus" version.workspace = true rust-version.workspace = true @@ -7,7 +7,7 @@ edition.workspace = true license.workspace = true [lib] -name = "patronpy" +name = "pypatronus" crate-type = ["cdylib"] [dependencies] diff --git a/python/pyproject.toml b/python/pyproject.toml index 43693fb..ecda27d 100644 --- a/python/pyproject.toml +++ b/python/pyproject.toml @@ -1,5 +1,5 @@ [project] -name = "patronpy" +name = "pypatronus" requires-python = ">=3.9" dynamic = ["version"] license = "BSD-3-Clause" diff --git a/python/src/lib.rs b/python/src/lib.rs index e982c62..762d85f 100644 --- a/python/src/lib.rs +++ b/python/src/lib.rs @@ -298,8 +298,8 @@ pub fn parse_btor2_file(filename: PathBuf) -> PyResult { } #[pymodule] -#[pyo3(name = "patronpy")] -fn patronpy(_py: Python<'_>, m: &pyo3::Bound<'_, pyo3::types::PyModule>) -> PyResult<()> { +#[pyo3(name = "pypatronus")] +fn pypatronus(_py: Python<'_>, m: &pyo3::Bound<'_, pyo3::types::PyModule>) -> PyResult<()> { m.add_class::()?; m.add_class::()?; m.add_class::()?; diff --git a/python/tests/test_expr.py b/python/tests/test_expr.py index 783c71e..03d1226 100644 --- a/python/tests/test_expr.py +++ b/python/tests/test_expr.py @@ -2,7 +2,7 @@ # released under BSD 3-Clause License # author: Kevin Laeufer -from patronpy import * +from pypatronus import * def test_simplify(): # by default this uses a global simplifier diff --git a/python/tests/test_lib.py b/python/tests/test_lib.py index d365c65..3ae0de6 100644 --- a/python/tests/test_lib.py +++ b/python/tests/test_lib.py @@ -6,7 +6,7 @@ import pathlib import pytest -from patronpy import * +from pypatronus import * repo_root = (pathlib.Path(__file__) / '..' / '..' / '..').resolve() diff --git a/python/tests/test_mc.py b/python/tests/test_mc.py index 1df4ca9..4ae350b 100644 --- a/python/tests/test_mc.py +++ b/python/tests/test_mc.py @@ -4,7 +4,7 @@ import pathlib import pytest -from patronpy import * +from pypatronus import * repo_root = (pathlib.Path(__file__) / '..' / '..' / '..').resolve() diff --git a/python/tests/test_sim.py b/python/tests/test_sim.py index 411ed4c..c134f68 100644 --- a/python/tests/test_sim.py +++ b/python/tests/test_sim.py @@ -4,7 +4,7 @@ import pathlib import pytest -from patronpy import * +from pypatronus import * repo_root = (pathlib.Path(__file__) / '..' / '..' / '..').resolve() diff --git a/python/tests/test_smt.py b/python/tests/test_smt.py index 3f3d161..5a0f498 100644 --- a/python/tests/test_smt.py +++ b/python/tests/test_smt.py @@ -4,7 +4,7 @@ import pathlib import pytest -from patronpy import * +from pypatronus import * repo_root = (pathlib.Path(__file__) / '..' / '..' / '..').resolve() diff --git a/python/uv.lock b/python/uv.lock index 7383028..1f6a851 100644 --- a/python/uv.lock +++ b/python/uv.lock @@ -41,20 +41,6 @@ wheels = [ { url = "https://files.pythonhosted.org/packages/20/12/38679034af332785aac8774540895e234f4d07f7545804097de4b666afd8/packaging-25.0-py3-none-any.whl", hash = "sha256:29572ef2b1f17581046b3a2227d5c611fb25ec70ca1ba8554b24b0e69331a484", size = 66469, upload-time = "2025-04-19T11:48:57.875Z" }, ] -[[package]] -name = "patronpy" -source = { editable = "." } - -[package.dev-dependencies] -dev = [ - { name = "pytest" }, -] - -[package.metadata] - -[package.metadata.requires-dev] -dev = [{ name = "pytest", specifier = ">=8.4.2" }] - [[package]] name = "pluggy" version = "1.6.0" @@ -73,6 +59,20 @@ wheels = [ { url = "https://files.pythonhosted.org/packages/c7/21/705964c7812476f378728bdf590ca4b771ec72385c533964653c68e86bdc/pygments-2.19.2-py3-none-any.whl", hash = "sha256:86540386c03d588bb81d44bc3928634ff26449851e99741617ecb9037ee5ec0b", size = 1225217, upload-time = "2025-06-21T13:39:07.939Z" }, ] +[[package]] +name = "pypatronus" +source = { editable = "." } + +[package.dev-dependencies] +dev = [ + { name = "pytest" }, +] + +[package.metadata] + +[package.metadata.requires-dev] +dev = [{ name = "pytest", specifier = ">=8.4.2" }] + [[package]] name = "pytest" version = "8.4.2"