From 3926ec6151acb2137d84f4d905bbbf764b042978 Mon Sep 17 00:00:00 2001 From: Christoph Jabs Date: Thu, 19 Dec 2024 16:06:20 +0200 Subject: [PATCH 1/9] fix(pyapi): confusing parameter names --- pyapi/rustsat/encodings/__init__.pyi | 6 +++--- pyapi/src/encodings.rs | 18 +++++++++--------- 2 files changed, 12 insertions(+), 12 deletions(-) diff --git a/pyapi/rustsat/encodings/__init__.pyi b/pyapi/rustsat/encodings/__init__.pyi index 91aa0c9b..df21dbe9 100644 --- a/pyapi/rustsat/encodings/__init__.pyi +++ b/pyapi/rustsat/encodings/__init__.pyi @@ -8,7 +8,7 @@ class Totalizer: def n_lits(self) -> int: ... def n_clauses(self) -> int: ... def n_vars(self) -> int: ... - def encode_ub(self, max_ub: int, min_ub: int, var_manager: VarManager) -> Cnf: ... + def encode_ub(self, min_ub: int, max_ub: int, var_manager: VarManager) -> Cnf: ... def enforce_ub(self, ub) -> List[Lit]: ... @final @@ -18,7 +18,7 @@ class GeneralizedTotalizer: def weight_sum(self) -> int: ... def n_clauses(self) -> int: ... def n_vars(self) -> int: ... - def encode_ub(self, max_ub: int, min_ub: int, var_manager: VarManager) -> Cnf: ... + def encode_ub(self, min_ub: int, max_ub: int, var_manager: VarManager) -> Cnf: ... def enforce_ub(self, ub) -> List[Lit]: ... @final @@ -27,5 +27,5 @@ class DynamicPolyWatchdog: def weight_sum(self) -> int: ... def n_clauses(self) -> int: ... def n_vars(self) -> int: ... - def encode_ub(self, max_ub: int, min_ub: int, var_manager: VarManager) -> Cnf: ... + def encode_ub(self, min_ub: int, max_ub: int, var_manager: VarManager) -> Cnf: ... def enforce_ub(self, ub) -> List[Lit]: ... diff --git a/pyapi/src/encodings.rs b/pyapi/src/encodings.rs index 6dfbb959..126acff5 100644 --- a/pyapi/src/encodings.rs +++ b/pyapi/src/encodings.rs @@ -89,19 +89,19 @@ impl Totalizer { } /// Incrementally builds the totalizer encoding to that upper bounds - /// in the range `max_ub..=min_ub` can be enforced. New variables will + /// in the range `min_ub..=max_ub` can be enforced. New variables will /// be taken from `var_manager`. fn encode_ub( &mut self, - max_ub: usize, min_ub: usize, + max_ub: usize, var_manager: &mut VarManager, ) -> PyResult { let mut cnf = RsCnf::new(); let var_manager: &mut BasicVarManager = var_manager.into(); handle_oom!(self .0 - .encode_ub_change(max_ub..=min_ub, &mut cnf, var_manager)); + .encode_ub_change(min_ub..=max_ub, &mut cnf, var_manager)); Ok(cnf.into()) } @@ -171,19 +171,19 @@ impl GeneralizedTotalizer { } /// Incrementally builds the GTE encoding to that upper bounds - /// in the range `max_ub..=min_ub` can be enforced. New variables will + /// in the range `min_ub..=max_ub` can be enforced. New variables will /// be taken from `var_manager`. fn encode_ub( &mut self, - max_ub: usize, min_ub: usize, + max_ub: usize, var_manager: &mut VarManager, ) -> PyResult { let mut cnf = RsCnf::new(); let var_manager: &mut BasicVarManager = var_manager.into(); handle_oom!(self .0 - .encode_ub_change(max_ub..=min_ub, &mut cnf, var_manager)); + .encode_ub_change(min_ub..=max_ub, &mut cnf, var_manager)); Ok(cnf.into()) } @@ -248,19 +248,19 @@ impl DynamicPolyWatchdog { } /// Incrementally builds the DPW encoding to that upper bounds - /// in the range `max_ub..=min_ub` can be enforced. New variables will + /// in the range `min_ub..=max_ub` can be enforced. New variables will /// be taken from `var_manager`. fn encode_ub( &mut self, - max_ub: usize, min_ub: usize, + max_ub: usize, var_manager: &mut VarManager, ) -> PyResult { let mut cnf = RsCnf::new(); let var_manager: &mut BasicVarManager = var_manager.into(); handle_oom!(self .0 - .encode_ub_change(max_ub..=min_ub, &mut cnf, var_manager)); + .encode_ub_change(min_ub..=max_ub, &mut cnf, var_manager)); Ok(cnf.into()) } From a0e8dd4f19917dc44fc1c6dd4d63b2ff47199150 Mon Sep 17 00:00:00 2001 From: Christoph Jabs Date: Thu, 19 Dec 2024 16:06:47 +0200 Subject: [PATCH 2/9] feat(pyapi): include `BinaryAdder` encoding --- pyapi/rustsat/encodings/__init__.pyi | 17 ++++ pyapi/src/encodings.rs | 124 ++++++++++++++++++++++++++- pyapi/src/lib.rs | 3 +- 3 files changed, 142 insertions(+), 2 deletions(-) diff --git a/pyapi/rustsat/encodings/__init__.pyi b/pyapi/rustsat/encodings/__init__.pyi index df21dbe9..20c86ba9 100644 --- a/pyapi/rustsat/encodings/__init__.pyi +++ b/pyapi/rustsat/encodings/__init__.pyi @@ -29,3 +29,20 @@ class DynamicPolyWatchdog: def n_vars(self) -> int: ... def encode_ub(self, min_ub: int, max_ub: int, var_manager: VarManager) -> Cnf: ... def enforce_ub(self, ub) -> List[Lit]: ... + +@final +class BinaryAdder: + def __new__(cls, wlits: List[tuple[int, Lit]]) -> BinaryAdder: ... + def weight_sum(self) -> int: ... + def n_clauses(self) -> int: ... + def n_vars(self) -> int: ... + def encode_ub(self, min_ub: int, max_ub: int, var_manager: VarManager) -> Cnf: ... + def enforce_ub(self, ub) -> List[Lit]: ... + def encode_lb(self, min_lb: int, max_lb: int, var_manager: VarManager) -> Cnf: ... + def enforce_lb(self, lb) -> List[Lit]: ... + def encode_lb(self, min_lb: int, max_lb: int, var_manager: VarManager) -> Cnf: ... + def enforce_lb(self, lb) -> List[Lit]: ... + def encode_both( + self, min_bound: int, max_bound: int, var_manager: VarManager + ) -> Cnf: ... + def enforce_eq(self, val) -> List[Lit]: ... diff --git a/pyapi/src/encodings.rs b/pyapi/src/encodings.rs index 126acff5..b50bf2a3 100644 --- a/pyapi/src/encodings.rs +++ b/pyapi/src/encodings.rs @@ -9,7 +9,8 @@ use rustsat::{ Encode as CardEncode, }, pb::{ - BoundUpper as PbBU, BoundUpperIncremental as PbBUI, DbGte, + BinaryAdder as RsAdder, BoundBoth, BoundBothIncremental, BoundLower, + BoundLowerIncremental, BoundUpper as PbBU, BoundUpperIncremental as PbBUI, DbGte, DynamicPolyWatchdog as RsDpw, Encode as PbEncode, }, EncodeStats, Error, @@ -271,3 +272,124 @@ impl DynamicPolyWatchdog { Ok(assumps.into_iter().map(Into::into).collect()) } } + +/// Implementation of the binary adder encoding first described in \[1\]. +/// The implementation follows the description in \[2\]. +/// +/// ## References +/// +/// - \[1\] Joose P. Warners: _A linear-time transformation of linear inequalities into conjunctive +/// normal form_, Inf. Process. Lett. 1998. +/// - \[2\] Niklas Eén and Niklas Sörensson: _Translating Pseudo-Boolean Constraints into SAT_, +/// JSAT 2006. +#[pyclass] +#[repr(transparent)] +pub struct BinaryAdder(RsAdder); + +impl From for BinaryAdder { + fn from(value: RsAdder) -> Self { + Self(value) + } +} + +impl From for RsAdder { + fn from(value: BinaryAdder) -> Self { + value.0 + } +} + +#[pymethods] +impl BinaryAdder { + #[new] + fn new(lits: Vec<(Lit, usize)>) -> Self { + let lits: Vec<(RsLit, usize)> = unsafe { std::mem::transmute(lits) }; + RsAdder::from_iter(lits).into() + } + + /// Gets the sum of weights in the encoding + fn weight_sum(&self) -> usize { + self.0.weight_sum() + } + + /// Gets the number of clauses in the encoding + fn n_clauses(&self) -> usize { + self.0.n_clauses() + } + + /// Gets the number of variables in the encoding + fn n_vars(&self) -> u32 { + self.0.n_vars() + } + + /// Incrementally builds the DPW encoding to that upper bounds + /// in the range `min_ub..=max_ub` can be enforced. New variables will + /// be taken from `var_manager`. + fn encode_ub( + &mut self, + min_ub: usize, + max_ub: usize, + var_manager: &mut VarManager, + ) -> PyResult { + let mut cnf = RsCnf::new(); + let var_manager: &mut BasicVarManager = var_manager.into(); + handle_oom!(self + .0 + .encode_ub_change(min_ub..=max_ub, &mut cnf, var_manager)); + Ok(cnf.into()) + } + + /// Gets assumptions to enforce the given upper bound. Make sure that + /// the required encoding is built first. + fn enforce_ub(&self, ub: usize) -> PyResult> { + let assumps = self.0.enforce_ub(ub).map_err(convert_error)?; + Ok(assumps.into_iter().map(Into::into).collect()) + } + + /// Incrementally builds the Adder encoding to that lower bounds + /// in the range `min_lb..=max_lb` can be enforced. New variables will + /// be taken from `var_manager`. + fn encode_lb( + &mut self, + min_lb: usize, + max_lb: usize, + var_manager: &mut VarManager, + ) -> PyResult { + let mut cnf = RsCnf::new(); + let var_manager: &mut BasicVarManager = var_manager.into(); + handle_oom!(self + .0 + .encode_lb_change(min_lb..=max_lb, &mut cnf, var_manager)); + Ok(cnf.into()) + } + + /// Gets assumptions to enforce the given lower bound. Make sure that + /// the required encoding is built first. + fn enforce_lb(&self, lb: usize) -> PyResult> { + let assumps = self.0.enforce_lb(lb).map_err(convert_error)?; + Ok(assumps.into_iter().map(Into::into).collect()) + } + + /// Incrementally builds the Adder encoding to that both bounds + /// in the range `min_bound..=max_bound` can be enforced. New variables will + /// be taken from `var_manager`. + fn encode_both( + &mut self, + min_bound: usize, + max_bound: usize, + var_manager: &mut VarManager, + ) -> PyResult { + let mut cnf = RsCnf::new(); + let var_manager: &mut BasicVarManager = var_manager.into(); + handle_oom!(self + .0 + .encode_both_change(min_bound..=max_bound, &mut cnf, var_manager)); + Ok(cnf.into()) + } + + /// Gets assumptions to enforce the given equality bound. Make sure that + /// the required encoding is built first. + fn enforce_eq(&self, val: usize) -> PyResult> { + let assumps = self.0.enforce_eq(val).map_err(convert_error)?; + Ok(assumps.into_iter().map(Into::into).collect()) + } +} diff --git a/pyapi/src/lib.rs b/pyapi/src/lib.rs index c3ede98d..c8a70e46 100644 --- a/pyapi/src/lib.rs +++ b/pyapi/src/lib.rs @@ -23,7 +23,7 @@ mod instances; mod types; use crate::{ - encodings::{DynamicPolyWatchdog, GeneralizedTotalizer, Totalizer}, + encodings::{BinaryAdder, DynamicPolyWatchdog, GeneralizedTotalizer, Totalizer}, instances::{Cnf, VarManager}, types::{Clause, Lit}, }; @@ -46,6 +46,7 @@ fn rustsat(py: Python<'_>, m: &Bound<'_, PyModule>) -> PyResult<()> { encodings.add_class::()?; encodings.add_class::()?; encodings.add_class::()?; + encodings.add_class::()?; m.add("encodings", &encodings)?; // To import encodings. Fix from https://github.com/PyO3/pyo3/issues/759 From 6166100dfe64fa2d8fda0deb5a4765bb816a87d3 Mon Sep 17 00:00:00 2001 From: Christoph Jabs Date: Thu, 19 Dec 2024 16:44:53 +0200 Subject: [PATCH 3/9] feat(pyapi): restructure python API --- pyapi/examples/pyapi-dpw.py | 2 +- pyapi/pyproject.toml | 3 + pyapi/{ => python}/rustsat/__init__.py | 0 pyapi/{ => python}/rustsat/__init__.pyi | 0 .../rustsat/encodings/__init__.py | 0 .../rustsat/encodings/__init__.pyi} | 0 .../python/rustsat/encodings/card/__init__.py | 5 + .../rustsat/encodings/card/__init__.pyi | 12 + pyapi/python/rustsat/encodings/pb/__init__.py | 5 + .../rustsat/encodings/pb}/__init__.pyi | 12 - pyapi/python/rustsat/py.typed | 0 pyapi/src/encodings.rs | 395 +----------------- pyapi/src/encodings/card.rs | 111 +++++ pyapi/src/encodings/pb.rs | 311 ++++++++++++++ pyapi/src/lib.rs | 23 +- pyapi/stubtest-allowlist.txt | 2 + shell.nix | 1 + 17 files changed, 471 insertions(+), 411 deletions(-) rename pyapi/{ => python}/rustsat/__init__.py (100%) rename pyapi/{ => python}/rustsat/__init__.pyi (100%) rename pyapi/{ => python}/rustsat/encodings/__init__.py (100%) rename pyapi/{rustsat/py.typed => python/rustsat/encodings/__init__.pyi} (100%) create mode 100644 pyapi/python/rustsat/encodings/card/__init__.py create mode 100644 pyapi/python/rustsat/encodings/card/__init__.pyi create mode 100644 pyapi/python/rustsat/encodings/pb/__init__.py rename pyapi/{rustsat/encodings => python/rustsat/encodings/pb}/__init__.pyi (74%) create mode 100644 pyapi/python/rustsat/py.typed create mode 100644 pyapi/src/encodings/card.rs create mode 100644 pyapi/src/encodings/pb.rs diff --git a/pyapi/examples/pyapi-dpw.py b/pyapi/examples/pyapi-dpw.py index cd1e02d1..1e943651 100644 --- a/pyapi/examples/pyapi-dpw.py +++ b/pyapi/examples/pyapi-dpw.py @@ -1,5 +1,5 @@ from rustsat import Lit, VarManager -from rustsat.encodings import DynamicPolyWatchdog as Dpw +from rustsat.encodings.pb import DynamicPolyWatchdog as Dpw # Lit creates a literal object from an ipasir integer representation. The # encoding takes a list of (lit, weight) pairs as input. diff --git a/pyapi/pyproject.toml b/pyapi/pyproject.toml index 9a983bf4..fd84c5e9 100644 --- a/pyapi/pyproject.toml +++ b/pyapi/pyproject.toml @@ -5,3 +5,6 @@ requires-python = ">=3.7" [build-system] requires = ["maturin>=1.0,<2.0"] build-backend = "maturin" + +[tool.maturin] +python-source = "python" diff --git a/pyapi/rustsat/__init__.py b/pyapi/python/rustsat/__init__.py similarity index 100% rename from pyapi/rustsat/__init__.py rename to pyapi/python/rustsat/__init__.py diff --git a/pyapi/rustsat/__init__.pyi b/pyapi/python/rustsat/__init__.pyi similarity index 100% rename from pyapi/rustsat/__init__.pyi rename to pyapi/python/rustsat/__init__.pyi diff --git a/pyapi/rustsat/encodings/__init__.py b/pyapi/python/rustsat/encodings/__init__.py similarity index 100% rename from pyapi/rustsat/encodings/__init__.py rename to pyapi/python/rustsat/encodings/__init__.py diff --git a/pyapi/rustsat/py.typed b/pyapi/python/rustsat/encodings/__init__.pyi similarity index 100% rename from pyapi/rustsat/py.typed rename to pyapi/python/rustsat/encodings/__init__.pyi diff --git a/pyapi/python/rustsat/encodings/card/__init__.py b/pyapi/python/rustsat/encodings/card/__init__.py new file mode 100644 index 00000000..fd26067f --- /dev/null +++ b/pyapi/python/rustsat/encodings/card/__init__.py @@ -0,0 +1,5 @@ +from .rustsat.encodings.card import * + +__doc__ = rustsat.encodings.card.__doc__ +if hasattr(rustsat.encodings.card, "__all__"): + __all__ = rustsat.encodings.card.__all__ diff --git a/pyapi/python/rustsat/encodings/card/__init__.pyi b/pyapi/python/rustsat/encodings/card/__init__.pyi new file mode 100644 index 00000000..9420ec79 --- /dev/null +++ b/pyapi/python/rustsat/encodings/card/__init__.pyi @@ -0,0 +1,12 @@ +from rustsat import Lit, Cnf, VarManager +from typing import List, final + +@final +class Totalizer: + def __new__(cls, lits: List[Lit]) -> Totalizer: ... + def extend(self, lits: List[Lit]) -> None: ... + def n_lits(self) -> int: ... + def n_clauses(self) -> int: ... + def n_vars(self) -> int: ... + def encode_ub(self, min_ub: int, max_ub: int, var_manager: VarManager) -> Cnf: ... + def enforce_ub(self, ub) -> List[Lit]: ... diff --git a/pyapi/python/rustsat/encodings/pb/__init__.py b/pyapi/python/rustsat/encodings/pb/__init__.py new file mode 100644 index 00000000..fb339209 --- /dev/null +++ b/pyapi/python/rustsat/encodings/pb/__init__.py @@ -0,0 +1,5 @@ +from .rustsat.encodings.pb import * + +__doc__ = rustsat.encodings.pb.__doc__ +if hasattr(rustsat.encodings.pb, "__all__"): + __all__ = rustsat.encodings.pb.__all__ diff --git a/pyapi/rustsat/encodings/__init__.pyi b/pyapi/python/rustsat/encodings/pb/__init__.pyi similarity index 74% rename from pyapi/rustsat/encodings/__init__.pyi rename to pyapi/python/rustsat/encodings/pb/__init__.pyi index 20c86ba9..10553c63 100644 --- a/pyapi/rustsat/encodings/__init__.pyi +++ b/pyapi/python/rustsat/encodings/pb/__init__.pyi @@ -1,16 +1,6 @@ from rustsat import Lit, Cnf, VarManager from typing import List, final -@final -class Totalizer: - def __new__(cls, lits: List[Lit]) -> Totalizer: ... - def extend(self, lits: List[Lit]) -> None: ... - def n_lits(self) -> int: ... - def n_clauses(self) -> int: ... - def n_vars(self) -> int: ... - def encode_ub(self, min_ub: int, max_ub: int, var_manager: VarManager) -> Cnf: ... - def enforce_ub(self, ub) -> List[Lit]: ... - @final class GeneralizedTotalizer: def __new__(cls, wlits: List[tuple[int, Lit]]) -> GeneralizedTotalizer: ... @@ -40,8 +30,6 @@ class BinaryAdder: def enforce_ub(self, ub) -> List[Lit]: ... def encode_lb(self, min_lb: int, max_lb: int, var_manager: VarManager) -> Cnf: ... def enforce_lb(self, lb) -> List[Lit]: ... - def encode_lb(self, min_lb: int, max_lb: int, var_manager: VarManager) -> Cnf: ... - def enforce_lb(self, lb) -> List[Lit]: ... def encode_both( self, min_bound: int, max_bound: int, var_manager: VarManager ) -> Cnf: ... diff --git a/pyapi/python/rustsat/py.typed b/pyapi/python/rustsat/py.typed new file mode 100644 index 00000000..e69de29b diff --git a/pyapi/src/encodings.rs b/pyapi/src/encodings.rs index b50bf2a3..6fbd5f01 100644 --- a/pyapi/src/encodings.rs +++ b/pyapi/src/encodings.rs @@ -1,395 +1,4 @@ //! # Python API for RustSAT Encodings -use pyo3::prelude::*; - -use rustsat::{ - encodings::{ - card::{ - BoundUpper as CardBU, BoundUpperIncremental as CardBUI, DbTotalizer, - Encode as CardEncode, - }, - pb::{ - BinaryAdder as RsAdder, BoundBoth, BoundBothIncremental, BoundLower, - BoundLowerIncremental, BoundUpper as PbBU, BoundUpperIncremental as PbBUI, DbGte, - DynamicPolyWatchdog as RsDpw, Encode as PbEncode, - }, - EncodeStats, Error, - }, - instances::{BasicVarManager, Cnf as RsCnf}, - types::Lit as RsLit, -}; - -use crate::{ - handle_oom, - instances::{Cnf, VarManager}, - types::Lit, -}; - -#[allow(clippy::needless_pass_by_value)] -fn convert_error(err: Error) -> PyErr { - match err { - Error::NotEncoded => { - pyo3::exceptions::PyRuntimeError::new_err("not encoded to enforce bound") - } - Error::Unsat => pyo3::exceptions::PyValueError::new_err("encoding is unsat"), - } -} - -/// Implementation of the binary adder tree totalizer encoding \[1\]. -/// The implementation is incremental as extended in \[2\]. -/// The implementation is based on a node database. -/// For now, this implementation only supports upper bounding. -/// -/// # References -/// -/// - \[1\] Olivier Bailleux and Yacine Boufkhad: _Efficient CNF Encoding of Boolean Cardinality Constraints_, CP 2003. -/// - \[2\] Ruben Martins and Saurabh Joshi and Vasco Manquinho and Ines Lynce: _Incremental Cardinality Constraints for MaxSAT_, CP 2014. -#[pyclass] -#[repr(transparent)] -pub struct Totalizer(DbTotalizer); - -impl From for Totalizer { - fn from(value: DbTotalizer) -> Self { - Self(value) - } -} - -impl From for DbTotalizer { - fn from(value: Totalizer) -> Self { - value.0 - } -} - -#[pymethods] -impl Totalizer { - #[new] - fn new(lits: Vec) -> Self { - let lits: Vec = unsafe { std::mem::transmute(lits) }; - DbTotalizer::from_iter(lits).into() - } - - /// Adds additional input literals to the totalizer - fn extend(&mut self, lits: Vec) { - let lits: Vec = unsafe { std::mem::transmute(lits) }; - self.0.extend(lits); - } - - /// Gets the number of input literals in the encoding - fn n_lits(&self) -> usize { - self.0.n_lits() - } - - /// Gets the number of clauses in the encoding - fn n_clauses(&self) -> usize { - self.0.n_clauses() - } - - /// Gets the number of variables in the encoding - fn n_vars(&self) -> u32 { - self.0.n_vars() - } - - /// Incrementally builds the totalizer encoding to that upper bounds - /// in the range `min_ub..=max_ub` can be enforced. New variables will - /// be taken from `var_manager`. - fn encode_ub( - &mut self, - min_ub: usize, - max_ub: usize, - var_manager: &mut VarManager, - ) -> PyResult { - let mut cnf = RsCnf::new(); - let var_manager: &mut BasicVarManager = var_manager.into(); - handle_oom!(self - .0 - .encode_ub_change(min_ub..=max_ub, &mut cnf, var_manager)); - Ok(cnf.into()) - } - - /// Gets assumptions to enforce the given upper bound. Make sure that - /// the required encoding is built first. - fn enforce_ub(&self, ub: usize) -> PyResult> { - let assumps: Vec = - unsafe { std::mem::transmute(self.0.enforce_ub(ub).map_err(convert_error)?) }; - Ok(assumps) - } -} - -/// Implementation of the binary adder tree generalized totalizer encoding -/// \[1\]. The implementation is incremental. The implementation is recursive. -/// This encoding only support upper bounding. Lower bounding can be achieved by -/// negating the input literals. This is implemented in -/// [`super::simulators::Inverted`]. -/// The implementation is based on a node database. -/// -/// # References -/// -/// - \[1\] Saurabh Joshi and Ruben Martins and Vasco Manquinho: _Generalized -/// Totalizer Encoding for Pseudo-Boolean Constraints_, CP 2015. -#[pyclass] -#[repr(transparent)] -pub struct GeneralizedTotalizer(DbGte); - -impl From for GeneralizedTotalizer { - fn from(value: DbGte) -> Self { - Self(value) - } -} - -impl From for DbGte { - fn from(value: GeneralizedTotalizer) -> Self { - value.0 - } -} - -#[pymethods] -impl GeneralizedTotalizer { - #[new] - fn new(lits: Vec<(Lit, usize)>) -> Self { - let lits: Vec<(RsLit, usize)> = unsafe { std::mem::transmute(lits) }; - DbGte::from_iter(lits).into() - } - - /// Adds additional input literals to the generalized totalizer - fn extend(&mut self, lits: Vec<(Lit, usize)>) { - let lits: Vec<(RsLit, usize)> = unsafe { std::mem::transmute(lits) }; - self.0.extend(lits); - } - - /// Gets the sum of weights in the encoding - fn weight_sum(&self) -> usize { - self.0.weight_sum() - } - - /// Gets the number of clauses in the encoding - fn n_clauses(&self) -> usize { - self.0.n_clauses() - } - - /// Gets the number of variables in the encoding - fn n_vars(&self) -> u32 { - self.0.n_vars() - } - - /// Incrementally builds the GTE encoding to that upper bounds - /// in the range `min_ub..=max_ub` can be enforced. New variables will - /// be taken from `var_manager`. - fn encode_ub( - &mut self, - min_ub: usize, - max_ub: usize, - var_manager: &mut VarManager, - ) -> PyResult { - let mut cnf = RsCnf::new(); - let var_manager: &mut BasicVarManager = var_manager.into(); - handle_oom!(self - .0 - .encode_ub_change(min_ub..=max_ub, &mut cnf, var_manager)); - Ok(cnf.into()) - } - - /// Gets assumptions to enforce the given upper bound. Make sure that - /// the required encoding is built first. - fn enforce_ub(&self, ub: usize) -> PyResult> { - let assumps: Vec = - unsafe { std::mem::transmute(self.0.enforce_ub(ub).map_err(convert_error)?) }; - Ok(assumps) - } -} - -/// Implementation of the dynamic polynomial watchdog (DPW) encoding \[1\]. -/// -/// **Note**: -/// This implementation of the DPW encoding only supports incrementally -/// changing the bound, but not adding new input literals. Calling extend after -/// encoding resets the entire encoding and with the next encode and entirely -/// new encoding will be returned. -/// -/// ## References -/// -/// - \[1\] Tobias Paxian and Sven Reimer and Bernd Becker: _Dynamic Polynomial -/// Watchdog Encoding for Solving Weighted MaxSAT_, SAT 2018. -#[pyclass] -#[repr(transparent)] -pub struct DynamicPolyWatchdog(RsDpw); - -impl From for DynamicPolyWatchdog { - fn from(value: RsDpw) -> Self { - Self(value) - } -} - -impl From for RsDpw { - fn from(value: DynamicPolyWatchdog) -> Self { - value.0 - } -} - -#[pymethods] -impl DynamicPolyWatchdog { - #[new] - fn new(lits: Vec<(Lit, usize)>) -> Self { - let lits: Vec<(RsLit, usize)> = unsafe { std::mem::transmute(lits) }; - RsDpw::from_iter(lits).into() - } - - /// Gets the sum of weights in the encoding - fn weight_sum(&self) -> usize { - self.0.weight_sum() - } - - /// Gets the number of clauses in the encoding - fn n_clauses(&self) -> usize { - self.0.n_clauses() - } - - /// Gets the number of variables in the encoding - fn n_vars(&self) -> u32 { - self.0.n_vars() - } - - /// Incrementally builds the DPW encoding to that upper bounds - /// in the range `min_ub..=max_ub` can be enforced. New variables will - /// be taken from `var_manager`. - fn encode_ub( - &mut self, - min_ub: usize, - max_ub: usize, - var_manager: &mut VarManager, - ) -> PyResult { - let mut cnf = RsCnf::new(); - let var_manager: &mut BasicVarManager = var_manager.into(); - handle_oom!(self - .0 - .encode_ub_change(min_ub..=max_ub, &mut cnf, var_manager)); - Ok(cnf.into()) - } - - /// Gets assumptions to enforce the given upper bound. Make sure that - /// the required encoding is built first. - fn enforce_ub(&self, ub: usize) -> PyResult> { - let assumps = self.0.enforce_ub(ub).map_err(convert_error)?; - Ok(assumps.into_iter().map(Into::into).collect()) - } -} - -/// Implementation of the binary adder encoding first described in \[1\]. -/// The implementation follows the description in \[2\]. -/// -/// ## References -/// -/// - \[1\] Joose P. Warners: _A linear-time transformation of linear inequalities into conjunctive -/// normal form_, Inf. Process. Lett. 1998. -/// - \[2\] Niklas Eén and Niklas Sörensson: _Translating Pseudo-Boolean Constraints into SAT_, -/// JSAT 2006. -#[pyclass] -#[repr(transparent)] -pub struct BinaryAdder(RsAdder); - -impl From for BinaryAdder { - fn from(value: RsAdder) -> Self { - Self(value) - } -} - -impl From for RsAdder { - fn from(value: BinaryAdder) -> Self { - value.0 - } -} - -#[pymethods] -impl BinaryAdder { - #[new] - fn new(lits: Vec<(Lit, usize)>) -> Self { - let lits: Vec<(RsLit, usize)> = unsafe { std::mem::transmute(lits) }; - RsAdder::from_iter(lits).into() - } - - /// Gets the sum of weights in the encoding - fn weight_sum(&self) -> usize { - self.0.weight_sum() - } - - /// Gets the number of clauses in the encoding - fn n_clauses(&self) -> usize { - self.0.n_clauses() - } - - /// Gets the number of variables in the encoding - fn n_vars(&self) -> u32 { - self.0.n_vars() - } - - /// Incrementally builds the DPW encoding to that upper bounds - /// in the range `min_ub..=max_ub` can be enforced. New variables will - /// be taken from `var_manager`. - fn encode_ub( - &mut self, - min_ub: usize, - max_ub: usize, - var_manager: &mut VarManager, - ) -> PyResult { - let mut cnf = RsCnf::new(); - let var_manager: &mut BasicVarManager = var_manager.into(); - handle_oom!(self - .0 - .encode_ub_change(min_ub..=max_ub, &mut cnf, var_manager)); - Ok(cnf.into()) - } - - /// Gets assumptions to enforce the given upper bound. Make sure that - /// the required encoding is built first. - fn enforce_ub(&self, ub: usize) -> PyResult> { - let assumps = self.0.enforce_ub(ub).map_err(convert_error)?; - Ok(assumps.into_iter().map(Into::into).collect()) - } - - /// Incrementally builds the Adder encoding to that lower bounds - /// in the range `min_lb..=max_lb` can be enforced. New variables will - /// be taken from `var_manager`. - fn encode_lb( - &mut self, - min_lb: usize, - max_lb: usize, - var_manager: &mut VarManager, - ) -> PyResult { - let mut cnf = RsCnf::new(); - let var_manager: &mut BasicVarManager = var_manager.into(); - handle_oom!(self - .0 - .encode_lb_change(min_lb..=max_lb, &mut cnf, var_manager)); - Ok(cnf.into()) - } - - /// Gets assumptions to enforce the given lower bound. Make sure that - /// the required encoding is built first. - fn enforce_lb(&self, lb: usize) -> PyResult> { - let assumps = self.0.enforce_lb(lb).map_err(convert_error)?; - Ok(assumps.into_iter().map(Into::into).collect()) - } - - /// Incrementally builds the Adder encoding to that both bounds - /// in the range `min_bound..=max_bound` can be enforced. New variables will - /// be taken from `var_manager`. - fn encode_both( - &mut self, - min_bound: usize, - max_bound: usize, - var_manager: &mut VarManager, - ) -> PyResult { - let mut cnf = RsCnf::new(); - let var_manager: &mut BasicVarManager = var_manager.into(); - handle_oom!(self - .0 - .encode_both_change(min_bound..=max_bound, &mut cnf, var_manager)); - Ok(cnf.into()) - } - - /// Gets assumptions to enforce the given equality bound. Make sure that - /// the required encoding is built first. - fn enforce_eq(&self, val: usize) -> PyResult> { - let assumps = self.0.enforce_eq(val).map_err(convert_error)?; - Ok(assumps.into_iter().map(Into::into).collect()) - } -} +pub mod card; +pub mod pb; diff --git a/pyapi/src/encodings/card.rs b/pyapi/src/encodings/card.rs new file mode 100644 index 00000000..045ab930 --- /dev/null +++ b/pyapi/src/encodings/card.rs @@ -0,0 +1,111 @@ +//! # Python API for RustSAT Cardinality Encodings + +use pyo3::prelude::*; + +use rustsat::{ + encodings::{ + card::{ + BoundUpper as CardBU, BoundUpperIncremental as CardBUI, DbTotalizer, + Encode as CardEncode, + }, + EncodeStats, Error, + }, + instances::{BasicVarManager, Cnf as RsCnf}, + types::Lit as RsLit, +}; + +use crate::{ + handle_oom, + instances::{Cnf, VarManager}, + types::Lit, +}; + +#[allow(clippy::needless_pass_by_value)] +fn convert_error(err: Error) -> PyErr { + match err { + Error::NotEncoded => { + pyo3::exceptions::PyRuntimeError::new_err("not encoded to enforce bound") + } + Error::Unsat => pyo3::exceptions::PyValueError::new_err("encoding is unsat"), + } +} + +/// Implementation of the binary adder tree totalizer encoding \[1\]. +/// The implementation is incremental as extended in \[2\]. +/// The implementation is based on a node database. +/// For now, this implementation only supports upper bounding. +/// +/// # References +/// +/// - \[1\] Olivier Bailleux and Yacine Boufkhad: _Efficient CNF Encoding of Boolean Cardinality Constraints_, CP 2003. +/// - \[2\] Ruben Martins and Saurabh Joshi and Vasco Manquinho and Ines Lynce: _Incremental Cardinality Constraints for MaxSAT_, CP 2014. +#[pyclass] +#[repr(transparent)] +pub struct Totalizer(DbTotalizer); + +impl From for Totalizer { + fn from(value: DbTotalizer) -> Self { + Self(value) + } +} + +impl From for DbTotalizer { + fn from(value: Totalizer) -> Self { + value.0 + } +} + +#[pymethods] +impl Totalizer { + #[new] + fn new(lits: Vec) -> Self { + let lits: Vec = unsafe { std::mem::transmute(lits) }; + DbTotalizer::from_iter(lits).into() + } + + /// Adds additional input literals to the totalizer + fn extend(&mut self, lits: Vec) { + let lits: Vec = unsafe { std::mem::transmute(lits) }; + self.0.extend(lits); + } + + /// Gets the number of input literals in the encoding + fn n_lits(&self) -> usize { + self.0.n_lits() + } + + /// Gets the number of clauses in the encoding + fn n_clauses(&self) -> usize { + self.0.n_clauses() + } + + /// Gets the number of variables in the encoding + fn n_vars(&self) -> u32 { + self.0.n_vars() + } + + /// Incrementally builds the totalizer encoding to that upper bounds + /// in the range `min_ub..=max_ub` can be enforced. New variables will + /// be taken from `var_manager`. + fn encode_ub( + &mut self, + min_ub: usize, + max_ub: usize, + var_manager: &mut VarManager, + ) -> PyResult { + let mut cnf = RsCnf::new(); + let var_manager: &mut BasicVarManager = var_manager.into(); + handle_oom!(self + .0 + .encode_ub_change(min_ub..=max_ub, &mut cnf, var_manager)); + Ok(cnf.into()) + } + + /// Gets assumptions to enforce the given upper bound. Make sure that + /// the required encoding is built first. + fn enforce_ub(&self, ub: usize) -> PyResult> { + let assumps: Vec = + unsafe { std::mem::transmute(self.0.enforce_ub(ub).map_err(convert_error)?) }; + Ok(assumps) + } +} diff --git a/pyapi/src/encodings/pb.rs b/pyapi/src/encodings/pb.rs new file mode 100644 index 00000000..e63da067 --- /dev/null +++ b/pyapi/src/encodings/pb.rs @@ -0,0 +1,311 @@ +//! # Python API for RustSAT PB Encodings + +use pyo3::prelude::*; + +use rustsat::{ + encodings::{ + pb::{ + BinaryAdder as RsAdder, BoundBoth, BoundBothIncremental, BoundLower, + BoundLowerIncremental, BoundUpper as PbBU, BoundUpperIncremental as PbBUI, DbGte, + DynamicPolyWatchdog as RsDpw, Encode as PbEncode, + }, + EncodeStats, Error, + }, + instances::{BasicVarManager, Cnf as RsCnf}, + types::Lit as RsLit, +}; + +use crate::{ + handle_oom, + instances::{Cnf, VarManager}, + types::Lit, +}; + +#[allow(clippy::needless_pass_by_value)] +fn convert_error(err: Error) -> PyErr { + match err { + Error::NotEncoded => { + pyo3::exceptions::PyRuntimeError::new_err("not encoded to enforce bound") + } + Error::Unsat => pyo3::exceptions::PyValueError::new_err("encoding is unsat"), + } +} + +/// Implementation of the binary adder tree generalized totalizer encoding +/// \[1\]. The implementation is incremental. The implementation is recursive. +/// This encoding only support upper bounding. Lower bounding can be achieved by +/// negating the input literals. This is implemented in +/// [`super::simulators::Inverted`]. +/// The implementation is based on a node database. +/// +/// # References +/// +/// - \[1\] Saurabh Joshi and Ruben Martins and Vasco Manquinho: _Generalized +/// Totalizer Encoding for Pseudo-Boolean Constraints_, CP 2015. +#[pyclass] +#[repr(transparent)] +pub struct GeneralizedTotalizer(DbGte); + +impl From for GeneralizedTotalizer { + fn from(value: DbGte) -> Self { + Self(value) + } +} + +impl From for DbGte { + fn from(value: GeneralizedTotalizer) -> Self { + value.0 + } +} + +#[pymethods] +impl GeneralizedTotalizer { + #[new] + fn new(lits: Vec<(Lit, usize)>) -> Self { + let lits: Vec<(RsLit, usize)> = unsafe { std::mem::transmute(lits) }; + DbGte::from_iter(lits).into() + } + + /// Adds additional input literals to the generalized totalizer + fn extend(&mut self, lits: Vec<(Lit, usize)>) { + let lits: Vec<(RsLit, usize)> = unsafe { std::mem::transmute(lits) }; + self.0.extend(lits); + } + + /// Gets the sum of weights in the encoding + fn weight_sum(&self) -> usize { + self.0.weight_sum() + } + + /// Gets the number of clauses in the encoding + fn n_clauses(&self) -> usize { + self.0.n_clauses() + } + + /// Gets the number of variables in the encoding + fn n_vars(&self) -> u32 { + self.0.n_vars() + } + + /// Incrementally builds the GTE encoding to that upper bounds + /// in the range `min_ub..=max_ub` can be enforced. New variables will + /// be taken from `var_manager`. + fn encode_ub( + &mut self, + min_ub: usize, + max_ub: usize, + var_manager: &mut VarManager, + ) -> PyResult { + let mut cnf = RsCnf::new(); + let var_manager: &mut BasicVarManager = var_manager.into(); + handle_oom!(self + .0 + .encode_ub_change(min_ub..=max_ub, &mut cnf, var_manager)); + Ok(cnf.into()) + } + + /// Gets assumptions to enforce the given upper bound. Make sure that + /// the required encoding is built first. + fn enforce_ub(&self, ub: usize) -> PyResult> { + let assumps: Vec = + unsafe { std::mem::transmute(self.0.enforce_ub(ub).map_err(convert_error)?) }; + Ok(assumps) + } +} + +/// Implementation of the dynamic polynomial watchdog (DPW) encoding \[1\]. +/// +/// **Note**: +/// This implementation of the DPW encoding only supports incrementally +/// changing the bound, but not adding new input literals. Calling extend after +/// encoding resets the entire encoding and with the next encode and entirely +/// new encoding will be returned. +/// +/// ## References +/// +/// - \[1\] Tobias Paxian and Sven Reimer and Bernd Becker: _Dynamic Polynomial +/// Watchdog Encoding for Solving Weighted MaxSAT_, SAT 2018. +#[pyclass] +#[repr(transparent)] +pub struct DynamicPolyWatchdog(RsDpw); + +impl From for DynamicPolyWatchdog { + fn from(value: RsDpw) -> Self { + Self(value) + } +} + +impl From for RsDpw { + fn from(value: DynamicPolyWatchdog) -> Self { + value.0 + } +} + +#[pymethods] +impl DynamicPolyWatchdog { + #[new] + fn new(lits: Vec<(Lit, usize)>) -> Self { + let lits: Vec<(RsLit, usize)> = unsafe { std::mem::transmute(lits) }; + RsDpw::from_iter(lits).into() + } + + /// Gets the sum of weights in the encoding + fn weight_sum(&self) -> usize { + self.0.weight_sum() + } + + /// Gets the number of clauses in the encoding + fn n_clauses(&self) -> usize { + self.0.n_clauses() + } + + /// Gets the number of variables in the encoding + fn n_vars(&self) -> u32 { + self.0.n_vars() + } + + /// Incrementally builds the DPW encoding to that upper bounds + /// in the range `min_ub..=max_ub` can be enforced. New variables will + /// be taken from `var_manager`. + fn encode_ub( + &mut self, + min_ub: usize, + max_ub: usize, + var_manager: &mut VarManager, + ) -> PyResult { + let mut cnf = RsCnf::new(); + let var_manager: &mut BasicVarManager = var_manager.into(); + handle_oom!(self + .0 + .encode_ub_change(min_ub..=max_ub, &mut cnf, var_manager)); + Ok(cnf.into()) + } + + /// Gets assumptions to enforce the given upper bound. Make sure that + /// the required encoding is built first. + fn enforce_ub(&self, ub: usize) -> PyResult> { + let assumps = self.0.enforce_ub(ub).map_err(convert_error)?; + Ok(assumps.into_iter().map(Into::into).collect()) + } +} + +/// Implementation of the binary adder encoding first described in \[1\]. +/// The implementation follows the description in \[2\]. +/// +/// ## References +/// +/// - \[1\] Joose P. Warners: _A linear-time transformation of linear inequalities into conjunctive +/// normal form_, Inf. Process. Lett. 1998. +/// - \[2\] Niklas Eén and Niklas Sörensson: _Translating Pseudo-Boolean Constraints into SAT_, +/// JSAT 2006. +#[pyclass] +#[repr(transparent)] +pub struct BinaryAdder(RsAdder); + +impl From for BinaryAdder { + fn from(value: RsAdder) -> Self { + Self(value) + } +} + +impl From for RsAdder { + fn from(value: BinaryAdder) -> Self { + value.0 + } +} + +#[pymethods] +impl BinaryAdder { + #[new] + fn new(lits: Vec<(Lit, usize)>) -> Self { + let lits: Vec<(RsLit, usize)> = unsafe { std::mem::transmute(lits) }; + RsAdder::from_iter(lits).into() + } + + /// Gets the sum of weights in the encoding + fn weight_sum(&self) -> usize { + self.0.weight_sum() + } + + /// Gets the number of clauses in the encoding + fn n_clauses(&self) -> usize { + self.0.n_clauses() + } + + /// Gets the number of variables in the encoding + fn n_vars(&self) -> u32 { + self.0.n_vars() + } + + /// Incrementally builds the DPW encoding to that upper bounds + /// in the range `min_ub..=max_ub` can be enforced. New variables will + /// be taken from `var_manager`. + fn encode_ub( + &mut self, + min_ub: usize, + max_ub: usize, + var_manager: &mut VarManager, + ) -> PyResult { + let mut cnf = RsCnf::new(); + let var_manager: &mut BasicVarManager = var_manager.into(); + handle_oom!(self + .0 + .encode_ub_change(min_ub..=max_ub, &mut cnf, var_manager)); + Ok(cnf.into()) + } + + /// Gets assumptions to enforce the given upper bound. Make sure that + /// the required encoding is built first. + fn enforce_ub(&self, ub: usize) -> PyResult> { + let assumps = self.0.enforce_ub(ub).map_err(convert_error)?; + Ok(assumps.into_iter().map(Into::into).collect()) + } + + /// Incrementally builds the Adder encoding to that lower bounds + /// in the range `min_lb..=max_lb` can be enforced. New variables will + /// be taken from `var_manager`. + fn encode_lb( + &mut self, + min_lb: usize, + max_lb: usize, + var_manager: &mut VarManager, + ) -> PyResult { + let mut cnf = RsCnf::new(); + let var_manager: &mut BasicVarManager = var_manager.into(); + handle_oom!(self + .0 + .encode_lb_change(min_lb..=max_lb, &mut cnf, var_manager)); + Ok(cnf.into()) + } + + /// Gets assumptions to enforce the given lower bound. Make sure that + /// the required encoding is built first. + fn enforce_lb(&self, lb: usize) -> PyResult> { + let assumps = self.0.enforce_lb(lb).map_err(convert_error)?; + Ok(assumps.into_iter().map(Into::into).collect()) + } + + /// Incrementally builds the Adder encoding to that both bounds + /// in the range `min_bound..=max_bound` can be enforced. New variables will + /// be taken from `var_manager`. + fn encode_both( + &mut self, + min_bound: usize, + max_bound: usize, + var_manager: &mut VarManager, + ) -> PyResult { + let mut cnf = RsCnf::new(); + let var_manager: &mut BasicVarManager = var_manager.into(); + handle_oom!(self + .0 + .encode_both_change(min_bound..=max_bound, &mut cnf, var_manager)); + Ok(cnf.into()) + } + + /// Gets assumptions to enforce the given equality bound. Make sure that + /// the required encoding is built first. + fn enforce_eq(&self, val: usize) -> PyResult> { + let assumps = self.0.enforce_eq(val).map_err(convert_error)?; + Ok(assumps.into_iter().map(Into::into).collect()) + } +} diff --git a/pyapi/src/lib.rs b/pyapi/src/lib.rs index c8a70e46..5ae48d51 100644 --- a/pyapi/src/lib.rs +++ b/pyapi/src/lib.rs @@ -23,7 +23,10 @@ mod instances; mod types; use crate::{ - encodings::{BinaryAdder, DynamicPolyWatchdog, GeneralizedTotalizer, Totalizer}, + encodings::{ + card::Totalizer, + pb::{BinaryAdder, DynamicPolyWatchdog, GeneralizedTotalizer}, + }, instances::{Cnf, VarManager}, types::{Clause, Lit}, }; @@ -43,16 +46,26 @@ fn rustsat(py: Python<'_>, m: &Bound<'_, PyModule>) -> PyResult<()> { m.add_class::()?; let encodings = PyModule::new(py, "rustsat.encodings")?; - encodings.add_class::()?; - encodings.add_class::()?; - encodings.add_class::()?; - encodings.add_class::()?; + let card = PyModule::new(py, "rustsat.encodings.card")?; + card.add_class::()?; + let pb = PyModule::new(py, "rustsat.encodings.pb")?; + pb.add_class::()?; + pb.add_class::()?; + pb.add_class::()?; + encodings.add("card", &card)?; + encodings.add("pb", &pb)?; m.add("encodings", &encodings)?; // To import encodings. Fix from https://github.com/PyO3/pyo3/issues/759 py.import("sys")? .getattr("modules")? .set_item("rustsat.encodings", &encodings)?; + py.import("sys")? + .getattr("modules")? + .set_item("rustsat.encodings.pb", &pb)?; + py.import("sys")? + .getattr("modules")? + .set_item("rustsat.encodings.card", &card)?; Ok(()) } diff --git a/pyapi/stubtest-allowlist.txt b/pyapi/stubtest-allowlist.txt index 1b5184fc..3af5136c 100644 --- a/pyapi/stubtest-allowlist.txt +++ b/pyapi/stubtest-allowlist.txt @@ -1,2 +1,4 @@ rustsat.rustsat rustsat.encodings +rustsat.encodings.pb +rustsat.encodings.card diff --git a/shell.nix b/shell.nix index 974760b6..eacee064 100644 --- a/shell.nix +++ b/shell.nix @@ -14,6 +14,7 @@ in cargo-nextest release-plz jq + maturin ]; buildInputs = libs; RUSTC_VERSION = overrides.toolchain.channel; From ed44c62ee6d67a2aa84162de3712111d0c1f8cec Mon Sep 17 00:00:00 2001 From: Christoph Jabs Date: Fri, 20 Dec 2024 12:47:27 +0200 Subject: [PATCH 4/9] doc(pyapi): include type annotations --- pyapi/python/rustsat/__init__.pyi | 8 ++++---- pyapi/python/rustsat/encodings/card/__init__.pyi | 2 +- pyapi/python/rustsat/encodings/pb/__init__.pyi | 6 +++--- 3 files changed, 8 insertions(+), 8 deletions(-) diff --git a/pyapi/python/rustsat/__init__.pyi b/pyapi/python/rustsat/__init__.pyi index dc9cf6b2..cdcbebfe 100644 --- a/pyapi/python/rustsat/__init__.pyi +++ b/pyapi/python/rustsat/__init__.pyi @@ -2,12 +2,12 @@ from typing import List, final @final class Lit: - def __new__(cls, ipasir: int) -> Lit: ... + def __new__(cls, ipasir: int) -> "Lit": ... def to_ipasir(self) -> int: ... @final class Clause: - def __new__(cls, lits: List[Lit]) -> Clause: ... + def __new__(cls, lits: List[Lit]) -> "Clause": ... def is_unit(self) -> bool: ... def is_binary(self) -> bool: ... def add(self, lit: Lit) -> None: ... @@ -17,7 +17,7 @@ class Clause: @final class Cnf: - def __new__(cls, clauses: List[Clause]) -> Cnf: ... + def __new__(cls, clauses: List[Clause]) -> "Cnf": ... def add_clause(self, clause: Clause) -> None: ... def add_unit(self, unit: Lit) -> None: ... def add_binary(self, lit1: Lit, lit2: Lit) -> None: ... @@ -34,7 +34,7 @@ class Cnf: @final class VarManager: - def __new__(cls, n_used: int = 0) -> VarManager: ... + def __new__(cls, n_used: int = 0) -> "VarManager": ... def increase_used(self, n_used: int) -> None: ... def new_var(self) -> int: ... def n_used(self) -> int: ... diff --git a/pyapi/python/rustsat/encodings/card/__init__.pyi b/pyapi/python/rustsat/encodings/card/__init__.pyi index 9420ec79..625f45c1 100644 --- a/pyapi/python/rustsat/encodings/card/__init__.pyi +++ b/pyapi/python/rustsat/encodings/card/__init__.pyi @@ -3,7 +3,7 @@ from typing import List, final @final class Totalizer: - def __new__(cls, lits: List[Lit]) -> Totalizer: ... + def __new__(cls, lits: List[Lit]) -> "Totalizer": ... def extend(self, lits: List[Lit]) -> None: ... def n_lits(self) -> int: ... def n_clauses(self) -> int: ... diff --git a/pyapi/python/rustsat/encodings/pb/__init__.pyi b/pyapi/python/rustsat/encodings/pb/__init__.pyi index 10553c63..6b6fb3ee 100644 --- a/pyapi/python/rustsat/encodings/pb/__init__.pyi +++ b/pyapi/python/rustsat/encodings/pb/__init__.pyi @@ -3,7 +3,7 @@ from typing import List, final @final class GeneralizedTotalizer: - def __new__(cls, wlits: List[tuple[int, Lit]]) -> GeneralizedTotalizer: ... + def __new__(cls, wlits: List[tuple[int, Lit]]) -> "GeneralizedTotalizer": ... def extend(self, lits: List[Lit]) -> None: ... def weight_sum(self) -> int: ... def n_clauses(self) -> int: ... @@ -13,7 +13,7 @@ class GeneralizedTotalizer: @final class DynamicPolyWatchdog: - def __new__(cls, wlits: List[tuple[int, Lit]]) -> DynamicPolyWatchdog: ... + def __new__(cls, wlits: List[tuple[int, Lit]]) -> "DynamicPolyWatchdog": ... def weight_sum(self) -> int: ... def n_clauses(self) -> int: ... def n_vars(self) -> int: ... @@ -22,7 +22,7 @@ class DynamicPolyWatchdog: @final class BinaryAdder: - def __new__(cls, wlits: List[tuple[int, Lit]]) -> BinaryAdder: ... + def __new__(cls, wlits: List[tuple[int, Lit]]) -> "BinaryAdder": ... def weight_sum(self) -> int: ... def n_clauses(self) -> int: ... def n_vars(self) -> int: ... From 826a0d97f92a5c2cece3016dfd53eaf9faa7a5d2 Mon Sep 17 00:00:00 2001 From: Christoph Jabs Date: Fri, 20 Dec 2024 12:48:12 +0200 Subject: [PATCH 5/9] chore(pyapi): format python example --- pyapi/examples/pyapi-dpw.py | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/pyapi/examples/pyapi-dpw.py b/pyapi/examples/pyapi-dpw.py index 1e943651..58619798 100644 --- a/pyapi/examples/pyapi-dpw.py +++ b/pyapi/examples/pyapi-dpw.py @@ -4,16 +4,16 @@ # Lit creates a literal object from an ipasir integer representation. The # encoding takes a list of (lit, weight) pairs as input. input_lits = [ - (Lit(1), 5), - (Lit(-2), 4), - (Lit(3), 3), - (Lit(-4), 2), - (Lit(5), 1), + (Lit(1), 5), + (Lit(-2), 4), + (Lit(3), 3), + (Lit(-4), 2), + (Lit(5), 1), ] # Getting unused variables is handled by a VarManager. Create one that has 5 # variables already used. -vm = VarManager(n_used = 5) +vm = VarManager(n_used=5) dpw = Dpw(input_lits) @@ -26,8 +26,8 @@ # DIMACS format. for cl in cnf: for l in cl: - print(l.to_ipasir(), end=' ') - print('0') + print(l.to_ipasir(), end=" ") + print("0") # Get assumptions to enforce an upper bound of 4 on the input literals. The # assumptions are a list of literals. From 3e442439bd5548f38a98ad51554f75b9ea950099 Mon Sep 17 00:00:00 2001 From: Christoph Jabs Date: Fri, 20 Dec 2024 12:59:08 +0200 Subject: [PATCH 6/9] fix(pyapi): extend stubs to properly include submodules --- pyapi/python/rustsat/__init__.pyi | 2 ++ pyapi/python/rustsat/encodings/__init__.pyi | 1 + pyapi/stubtest-allowlist.txt | 3 --- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/pyapi/python/rustsat/__init__.pyi b/pyapi/python/rustsat/__init__.pyi index cdcbebfe..dc992dbb 100644 --- a/pyapi/python/rustsat/__init__.pyi +++ b/pyapi/python/rustsat/__init__.pyi @@ -1,5 +1,7 @@ from typing import List, final +from rustsat import encodings + @final class Lit: def __new__(cls, ipasir: int) -> "Lit": ... diff --git a/pyapi/python/rustsat/encodings/__init__.pyi b/pyapi/python/rustsat/encodings/__init__.pyi index e69de29b..1092ec86 100644 --- a/pyapi/python/rustsat/encodings/__init__.pyi +++ b/pyapi/python/rustsat/encodings/__init__.pyi @@ -0,0 +1 @@ +from rustsat.encodings import card, pb diff --git a/pyapi/stubtest-allowlist.txt b/pyapi/stubtest-allowlist.txt index 3af5136c..49c3011a 100644 --- a/pyapi/stubtest-allowlist.txt +++ b/pyapi/stubtest-allowlist.txt @@ -1,4 +1 @@ rustsat.rustsat -rustsat.encodings -rustsat.encodings.pb -rustsat.encodings.card From 5bbb88eb21a7622fcd2ddff6059acbc1ac80bb08 Mon Sep 17 00:00:00 2001 From: Christoph Jabs Date: Fri, 20 Dec 2024 14:57:40 +0200 Subject: [PATCH 7/9] refactor(pyapi): simplify pyapi with macros --- Cargo.lock | 16 + pyapi/Cargo.toml | 1 + .../python/rustsat/encodings/pb/__init__.pyi | 1 + pyapi/src/encodings/card.rs | 137 +++--- pyapi/src/encodings/pb.rs | 393 +++++++----------- 5 files changed, 250 insertions(+), 298 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index aa1465e6..c8a82059 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -740,6 +740,15 @@ dependencies = [ "rustc_version", ] +[[package]] +name = "inventory" +version = "0.3.16" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "e5d80fade88dd420ce0d9ab6f7c58ef2272dde38db874657950f827d4982c817" +dependencies = [ + "rustversion", +] + [[package]] name = "is-terminal" version = "0.4.13" @@ -1075,6 +1084,7 @@ checksum = "e484fd2c8b4cb67ab05a318f1fd6fa8f199fcc30819f08f07d200809dba26c15" dependencies = [ "cfg-if", "indoc", + "inventory", "libc", "memoffset", "once_cell", @@ -1385,6 +1395,12 @@ dependencies = [ "termcolor", ] +[[package]] +name = "rustversion" +version = "1.0.18" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "0e819f2bc632f285be6d7cd36e25940d45b2391dd6d9b939e79de557f7014248" + [[package]] name = "ryu" version = "1.0.18" diff --git a/pyapi/Cargo.toml b/pyapi/Cargo.toml index 3c26cf5c..cf6f43e1 100644 --- a/pyapi/Cargo.toml +++ b/pyapi/Cargo.toml @@ -19,6 +19,7 @@ pyo3 = { version = "0.23.3", features = [ "extension-module", "abi3", "abi3-py37", + "multiple-pymethods", ] } [build-dependencies] diff --git a/pyapi/python/rustsat/encodings/pb/__init__.pyi b/pyapi/python/rustsat/encodings/pb/__init__.pyi index 6b6fb3ee..9fc56e2a 100644 --- a/pyapi/python/rustsat/encodings/pb/__init__.pyi +++ b/pyapi/python/rustsat/encodings/pb/__init__.pyi @@ -23,6 +23,7 @@ class DynamicPolyWatchdog: @final class BinaryAdder: def __new__(cls, wlits: List[tuple[int, Lit]]) -> "BinaryAdder": ... + def extend(self, lits: List[Lit]) -> None: ... def weight_sum(self) -> int: ... def n_clauses(self) -> int: ... def n_vars(self) -> int: ... diff --git a/pyapi/src/encodings/card.rs b/pyapi/src/encodings/card.rs index 045ab930..554cdcb9 100644 --- a/pyapi/src/encodings/card.rs +++ b/pyapi/src/encodings/card.rs @@ -30,6 +30,76 @@ fn convert_error(err: Error) -> PyErr { } } +macro_rules! implement_pyapi { + ($type:ty, $rstype:ty) => { + impl From<$rstype> for $type { + fn from(value: $rstype) -> Self { + Self(value) + } + } + + impl From<$type> for $rstype { + fn from(value: $type) -> Self { + value.0 + } + } + + #[pymethods] + impl $type { + #[new] + fn new(lits: Vec) -> Self { + let lits: Vec = unsafe { std::mem::transmute(lits) }; + <$rstype>::from_iter(lits).into() + } + + /// Adds additional input literals to the encoding + fn extend(&mut self, lits: Vec) { + let lits: Vec = unsafe { std::mem::transmute(lits) }; + self.0.extend(lits); + } + + /// Gets the number of input literals in the encoding + fn n_lits(&self) -> usize { + self.0.n_lits() + } + + /// Gets the number of clauses in the encoding + fn n_clauses(&self) -> usize { + self.0.n_clauses() + } + + /// Gets the number of variables in the encoding + fn n_vars(&self) -> u32 { + self.0.n_vars() + } + + /// Incrementally builds the encoding to that upper bounds in the range + /// `min_ub..=max_ub` can be enforced. New variables will be taken from `var_manager`. + fn encode_ub( + &mut self, + min_ub: usize, + max_ub: usize, + var_manager: &mut VarManager, + ) -> PyResult { + let mut cnf = RsCnf::new(); + let var_manager: &mut BasicVarManager = var_manager.into(); + handle_oom!(self + .0 + .encode_ub_change(min_ub..=max_ub, &mut cnf, var_manager)); + Ok(cnf.into()) + } + + /// Gets assumptions to enforce the given upper bound. Make sure that the required + /// encoding is built first. + fn enforce_ub(&self, ub: usize) -> PyResult> { + let assumps: Vec = + unsafe { std::mem::transmute(self.0.enforce_ub(ub).map_err(convert_error)?) }; + Ok(assumps) + } + } + }; +} + /// Implementation of the binary adder tree totalizer encoding \[1\]. /// The implementation is incremental as extended in \[2\]. /// The implementation is based on a node database. @@ -43,69 +113,4 @@ fn convert_error(err: Error) -> PyErr { #[repr(transparent)] pub struct Totalizer(DbTotalizer); -impl From for Totalizer { - fn from(value: DbTotalizer) -> Self { - Self(value) - } -} - -impl From for DbTotalizer { - fn from(value: Totalizer) -> Self { - value.0 - } -} - -#[pymethods] -impl Totalizer { - #[new] - fn new(lits: Vec) -> Self { - let lits: Vec = unsafe { std::mem::transmute(lits) }; - DbTotalizer::from_iter(lits).into() - } - - /// Adds additional input literals to the totalizer - fn extend(&mut self, lits: Vec) { - let lits: Vec = unsafe { std::mem::transmute(lits) }; - self.0.extend(lits); - } - - /// Gets the number of input literals in the encoding - fn n_lits(&self) -> usize { - self.0.n_lits() - } - - /// Gets the number of clauses in the encoding - fn n_clauses(&self) -> usize { - self.0.n_clauses() - } - - /// Gets the number of variables in the encoding - fn n_vars(&self) -> u32 { - self.0.n_vars() - } - - /// Incrementally builds the totalizer encoding to that upper bounds - /// in the range `min_ub..=max_ub` can be enforced. New variables will - /// be taken from `var_manager`. - fn encode_ub( - &mut self, - min_ub: usize, - max_ub: usize, - var_manager: &mut VarManager, - ) -> PyResult { - let mut cnf = RsCnf::new(); - let var_manager: &mut BasicVarManager = var_manager.into(); - handle_oom!(self - .0 - .encode_ub_change(min_ub..=max_ub, &mut cnf, var_manager)); - Ok(cnf.into()) - } - - /// Gets assumptions to enforce the given upper bound. Make sure that - /// the required encoding is built first. - fn enforce_ub(&self, ub: usize) -> PyResult> { - let assumps: Vec = - unsafe { std::mem::transmute(self.0.enforce_ub(ub).map_err(convert_error)?) }; - Ok(assumps) - } -} +implement_pyapi!(Totalizer, DbTotalizer); diff --git a/pyapi/src/encodings/pb.rs b/pyapi/src/encodings/pb.rs index e63da067..1b808186 100644 --- a/pyapi/src/encodings/pb.rs +++ b/pyapi/src/encodings/pb.rs @@ -31,6 +31,164 @@ fn convert_error(err: Error) -> PyErr { } } +macro_rules! shared_pyapi { + (derive_from, $type:ty, $rstype:ty) => { + impl From<$rstype> for $type { + fn from(value: $rstype) -> Self { + Self(value) + } + } + + impl From<$type> for $rstype { + fn from(value: $type) -> Self { + value.0 + } + } + }; + (extend, $type:ty) => { + #[pymethods] + impl $type { + /// Adds additional input literals to the encoding + fn extend(&mut self, lits: Vec<(Lit, usize)>) { + let lits: Vec<(RsLit, usize)> = unsafe { std::mem::transmute(lits) }; + self.0.extend(lits); + } + } + }; + (base, $type:ty, $rstype:ty) => { + #[pymethods] + impl $type { + #[new] + fn new(lits: Vec<(Lit, usize)>) -> Self { + let lits: Vec<(RsLit, usize)> = unsafe { std::mem::transmute(lits) }; + <$rstype>::from_iter(lits).into() + } + + /// Gets the sum of weights in the encoding + fn weight_sum(&self) -> usize { + self.0.weight_sum() + } + + /// Gets the number of clauses in the encoding + fn n_clauses(&self) -> usize { + self.0.n_clauses() + } + + /// Gets the number of variables in the encoding + fn n_vars(&self) -> u32 { + self.0.n_vars() + } + } + }; + (ub, $type:ty) => { + #[pymethods] + impl $type { + /// Incrementally builds the encoding to that upper bounds in the range + /// `min_ub..=max_ub` can be enforced. New variables will be taken from `var_manager`. + fn encode_ub( + &mut self, + min_ub: usize, + max_ub: usize, + var_manager: &mut VarManager, + ) -> PyResult { + let mut cnf = RsCnf::new(); + let var_manager: &mut BasicVarManager = var_manager.into(); + handle_oom!(self + .0 + .encode_ub_change(min_ub..=max_ub, &mut cnf, var_manager)); + Ok(cnf.into()) + } + + /// Gets assumptions to enforce the given upper bound. Make sure that the required + /// encoding is built first. + fn enforce_ub(&self, ub: usize) -> PyResult> { + let assumps: Vec = + unsafe { std::mem::transmute(self.0.enforce_ub(ub).map_err(convert_error)?) }; + Ok(assumps) + } + } + }; + (lb, $type:ty) => { + #[pymethods] + impl $type { + /// Incrementally builds the encoding to that lower bounds in the range `min_lb..=max_lb` + /// can be enforced. New variables will be taken from `var_manager`. + fn encode_lb( + &mut self, + min_lb: usize, + max_lb: usize, + var_manager: &mut VarManager, + ) -> PyResult { + let mut cnf = RsCnf::new(); + let var_manager: &mut BasicVarManager = var_manager.into(); + handle_oom!(self + .0 + .encode_lb_change(min_lb..=max_lb, &mut cnf, var_manager)); + Ok(cnf.into()) + } + + /// Gets assumptions to enforce the given lower bound. Make sure that the required encoding + /// is built first. + fn enforce_lb(&self, lb: usize) -> PyResult> { + let assumps = self.0.enforce_lb(lb).map_err(convert_error)?; + Ok(assumps.into_iter().map(Into::into).collect()) + } + } + }; + (both, $type:ty) => { + #[pymethods] + impl $type { + /// Incrementally builds the encoding to that both bounds in the range + /// `min_bound..=max_bound` can be enforced. New variables will be taken from + /// `var_manager`. + fn encode_both( + &mut self, + min_bound: usize, + max_bound: usize, + var_manager: &mut VarManager, + ) -> PyResult { + let mut cnf = RsCnf::new(); + let var_manager: &mut BasicVarManager = var_manager.into(); + handle_oom!(self.0.encode_both_change( + min_bound..=max_bound, + &mut cnf, + var_manager + )); + Ok(cnf.into()) + } + + /// Gets assumptions to enforce the given equality bound. Make sure that the required + /// encoding is built first. + fn enforce_eq(&self, val: usize) -> PyResult> { + let assumps = self.0.enforce_eq(val).map_err(convert_error)?; + Ok(assumps.into_iter().map(Into::into).collect()) + } + } + }; +} + +macro_rules! implement_pyapi { + (ub, $type:ty, $rstype:ty) => { + shared_pyapi!(derive_from, $type, $rstype); + shared_pyapi!(base, $type, $rstype); + shared_pyapi!(extend, $type); + shared_pyapi!(ub, $type); + }; + (ub_noextend, $type:ty, $rstype:ty) => { + shared_pyapi!(derive_from, $type, $rstype); + shared_pyapi!(base, $type, $rstype); + shared_pyapi!(ub, $type); + }; + (both, $type:ty, $rstype:ty) => { + shared_pyapi!(derive_from, $type, $rstype); + shared_pyapi!(base, $type, $rstype); + shared_pyapi!(extend, $type); + shared_pyapi!(ub, $type); + shared_pyapi!(lb, $type); + shared_pyapi!(both, $type); + }; +} + /// Implementation of the binary adder tree generalized totalizer encoding /// \[1\]. The implementation is incremental. The implementation is recursive. /// This encoding only support upper bounding. Lower bounding can be achieved by @@ -46,72 +204,7 @@ fn convert_error(err: Error) -> PyErr { #[repr(transparent)] pub struct GeneralizedTotalizer(DbGte); -impl From for GeneralizedTotalizer { - fn from(value: DbGte) -> Self { - Self(value) - } -} - -impl From for DbGte { - fn from(value: GeneralizedTotalizer) -> Self { - value.0 - } -} - -#[pymethods] -impl GeneralizedTotalizer { - #[new] - fn new(lits: Vec<(Lit, usize)>) -> Self { - let lits: Vec<(RsLit, usize)> = unsafe { std::mem::transmute(lits) }; - DbGte::from_iter(lits).into() - } - - /// Adds additional input literals to the generalized totalizer - fn extend(&mut self, lits: Vec<(Lit, usize)>) { - let lits: Vec<(RsLit, usize)> = unsafe { std::mem::transmute(lits) }; - self.0.extend(lits); - } - - /// Gets the sum of weights in the encoding - fn weight_sum(&self) -> usize { - self.0.weight_sum() - } - - /// Gets the number of clauses in the encoding - fn n_clauses(&self) -> usize { - self.0.n_clauses() - } - - /// Gets the number of variables in the encoding - fn n_vars(&self) -> u32 { - self.0.n_vars() - } - - /// Incrementally builds the GTE encoding to that upper bounds - /// in the range `min_ub..=max_ub` can be enforced. New variables will - /// be taken from `var_manager`. - fn encode_ub( - &mut self, - min_ub: usize, - max_ub: usize, - var_manager: &mut VarManager, - ) -> PyResult { - let mut cnf = RsCnf::new(); - let var_manager: &mut BasicVarManager = var_manager.into(); - handle_oom!(self - .0 - .encode_ub_change(min_ub..=max_ub, &mut cnf, var_manager)); - Ok(cnf.into()) - } - - /// Gets assumptions to enforce the given upper bound. Make sure that - /// the required encoding is built first. - fn enforce_ub(&self, ub: usize) -> PyResult> { - let assumps: Vec = - unsafe { std::mem::transmute(self.0.enforce_ub(ub).map_err(convert_error)?) }; - Ok(assumps) - } -} +implement_pyapi!(ub, GeneralizedTotalizer, DbGte); /// Implementation of the dynamic polynomial watchdog (DPW) encoding \[1\]. /// @@ -129,65 +222,7 @@ impl GeneralizedTotalizer { #[repr(transparent)] pub struct DynamicPolyWatchdog(RsDpw); -impl From for DynamicPolyWatchdog { - fn from(value: RsDpw) -> Self { - Self(value) - } -} - -impl From for RsDpw { - fn from(value: DynamicPolyWatchdog) -> Self { - value.0 - } -} - -#[pymethods] -impl DynamicPolyWatchdog { - #[new] - fn new(lits: Vec<(Lit, usize)>) -> Self { - let lits: Vec<(RsLit, usize)> = unsafe { std::mem::transmute(lits) }; - RsDpw::from_iter(lits).into() - } - - /// Gets the sum of weights in the encoding - fn weight_sum(&self) -> usize { - self.0.weight_sum() - } - - /// Gets the number of clauses in the encoding - fn n_clauses(&self) -> usize { - self.0.n_clauses() - } - - /// Gets the number of variables in the encoding - fn n_vars(&self) -> u32 { - self.0.n_vars() - } - - /// Incrementally builds the DPW encoding to that upper bounds - /// in the range `min_ub..=max_ub` can be enforced. New variables will - /// be taken from `var_manager`. - fn encode_ub( - &mut self, - min_ub: usize, - max_ub: usize, - var_manager: &mut VarManager, - ) -> PyResult { - let mut cnf = RsCnf::new(); - let var_manager: &mut BasicVarManager = var_manager.into(); - handle_oom!(self - .0 - .encode_ub_change(min_ub..=max_ub, &mut cnf, var_manager)); - Ok(cnf.into()) - } - - /// Gets assumptions to enforce the given upper bound. Make sure that - /// the required encoding is built first. - fn enforce_ub(&self, ub: usize) -> PyResult> { - let assumps = self.0.enforce_ub(ub).map_err(convert_error)?; - Ok(assumps.into_iter().map(Into::into).collect()) - } -} +implement_pyapi!(ub_noextend, DynamicPolyWatchdog, RsDpw); /// Implementation of the binary adder encoding first described in \[1\]. /// The implementation follows the description in \[2\]. @@ -202,110 +237,4 @@ impl DynamicPolyWatchdog { #[repr(transparent)] pub struct BinaryAdder(RsAdder); -impl From for BinaryAdder { - fn from(value: RsAdder) -> Self { - Self(value) - } -} - -impl From for RsAdder { - fn from(value: BinaryAdder) -> Self { - value.0 - } -} - -#[pymethods] -impl BinaryAdder { - #[new] - fn new(lits: Vec<(Lit, usize)>) -> Self { - let lits: Vec<(RsLit, usize)> = unsafe { std::mem::transmute(lits) }; - RsAdder::from_iter(lits).into() - } - - /// Gets the sum of weights in the encoding - fn weight_sum(&self) -> usize { - self.0.weight_sum() - } - - /// Gets the number of clauses in the encoding - fn n_clauses(&self) -> usize { - self.0.n_clauses() - } - - /// Gets the number of variables in the encoding - fn n_vars(&self) -> u32 { - self.0.n_vars() - } - - /// Incrementally builds the DPW encoding to that upper bounds - /// in the range `min_ub..=max_ub` can be enforced. New variables will - /// be taken from `var_manager`. - fn encode_ub( - &mut self, - min_ub: usize, - max_ub: usize, - var_manager: &mut VarManager, - ) -> PyResult { - let mut cnf = RsCnf::new(); - let var_manager: &mut BasicVarManager = var_manager.into(); - handle_oom!(self - .0 - .encode_ub_change(min_ub..=max_ub, &mut cnf, var_manager)); - Ok(cnf.into()) - } - - /// Gets assumptions to enforce the given upper bound. Make sure that - /// the required encoding is built first. - fn enforce_ub(&self, ub: usize) -> PyResult> { - let assumps = self.0.enforce_ub(ub).map_err(convert_error)?; - Ok(assumps.into_iter().map(Into::into).collect()) - } - - /// Incrementally builds the Adder encoding to that lower bounds - /// in the range `min_lb..=max_lb` can be enforced. New variables will - /// be taken from `var_manager`. - fn encode_lb( - &mut self, - min_lb: usize, - max_lb: usize, - var_manager: &mut VarManager, - ) -> PyResult { - let mut cnf = RsCnf::new(); - let var_manager: &mut BasicVarManager = var_manager.into(); - handle_oom!(self - .0 - .encode_lb_change(min_lb..=max_lb, &mut cnf, var_manager)); - Ok(cnf.into()) - } - - /// Gets assumptions to enforce the given lower bound. Make sure that - /// the required encoding is built first. - fn enforce_lb(&self, lb: usize) -> PyResult> { - let assumps = self.0.enforce_lb(lb).map_err(convert_error)?; - Ok(assumps.into_iter().map(Into::into).collect()) - } - - /// Incrementally builds the Adder encoding to that both bounds - /// in the range `min_bound..=max_bound` can be enforced. New variables will - /// be taken from `var_manager`. - fn encode_both( - &mut self, - min_bound: usize, - max_bound: usize, - var_manager: &mut VarManager, - ) -> PyResult { - let mut cnf = RsCnf::new(); - let var_manager: &mut BasicVarManager = var_manager.into(); - handle_oom!(self - .0 - .encode_both_change(min_bound..=max_bound, &mut cnf, var_manager)); - Ok(cnf.into()) - } - - /// Gets assumptions to enforce the given equality bound. Make sure that - /// the required encoding is built first. - fn enforce_eq(&self, val: usize) -> PyResult> { - let assumps = self.0.enforce_eq(val).map_err(convert_error)?; - Ok(assumps.into_iter().map(Into::into).collect()) - } -} +implement_pyapi!(both, BinaryAdder, RsAdder); From 77d329b521ab5fc6ac379ce6c8ee8a1e000322c1 Mon Sep 17 00:00:00 2001 From: Christoph Jabs Date: Fri, 20 Dec 2024 15:07:06 +0200 Subject: [PATCH 8/9] feat(pyapi): include at-most-one encodings --- pyapi/python/rustsat/encodings/__init__.pyi | 2 +- .../python/rustsat/encodings/am1/__init__.py | 5 + .../python/rustsat/encodings/am1/__init__.pyi | 34 +++++ pyapi/src/encodings.rs | 1 + pyapi/src/encodings/am1.rs | 117 ++++++++++++++++++ pyapi/src/lib.rs | 10 ++ 6 files changed, 168 insertions(+), 1 deletion(-) create mode 100644 pyapi/python/rustsat/encodings/am1/__init__.py create mode 100644 pyapi/python/rustsat/encodings/am1/__init__.pyi create mode 100644 pyapi/src/encodings/am1.rs diff --git a/pyapi/python/rustsat/encodings/__init__.pyi b/pyapi/python/rustsat/encodings/__init__.pyi index 1092ec86..fc1ea710 100644 --- a/pyapi/python/rustsat/encodings/__init__.pyi +++ b/pyapi/python/rustsat/encodings/__init__.pyi @@ -1 +1 @@ -from rustsat.encodings import card, pb +from rustsat.encodings import card, pb, am1 diff --git a/pyapi/python/rustsat/encodings/am1/__init__.py b/pyapi/python/rustsat/encodings/am1/__init__.py new file mode 100644 index 00000000..e9d86d41 --- /dev/null +++ b/pyapi/python/rustsat/encodings/am1/__init__.py @@ -0,0 +1,5 @@ +from .rustsat.encodings.am1 import * + +__doc__ = rustsat.encodings.am1.__doc__ +if hasattr(rustsat.encodings.am1, "__all__"): + __all__ = rustsat.encodings.am1.__all__ diff --git a/pyapi/python/rustsat/encodings/am1/__init__.pyi b/pyapi/python/rustsat/encodings/am1/__init__.pyi new file mode 100644 index 00000000..8ed37316 --- /dev/null +++ b/pyapi/python/rustsat/encodings/am1/__init__.pyi @@ -0,0 +1,34 @@ +from rustsat import Lit, Cnf, VarManager +from typing import List, final + +@final +class Bitwise: + def __new__(cls, lits: List[Lit]) -> "Bitwise": ... + def n_lits(self) -> int: ... + def n_clauses(self) -> int: ... + def n_vars(self) -> int: ... + def encode(self, var_manager: VarManager) -> Cnf: ... + +@final +class Commander: + def __new__(cls, lits: List[Lit]) -> "Commander": ... + def n_lits(self) -> int: ... + def n_clauses(self) -> int: ... + def n_vars(self) -> int: ... + def encode(self, var_manager: VarManager) -> Cnf: ... + +@final +class Ladder: + def __new__(cls, lits: List[Lit]) -> "Ladder": ... + def n_lits(self) -> int: ... + def n_clauses(self) -> int: ... + def n_vars(self) -> int: ... + def encode(self, var_manager: VarManager) -> Cnf: ... + +@final +class Pairwise: + def __new__(cls, lits: List[Lit]) -> "Pairwise": ... + def n_lits(self) -> int: ... + def n_clauses(self) -> int: ... + def n_vars(self) -> int: ... + def encode(self, var_manager: VarManager) -> Cnf: ... diff --git a/pyapi/src/encodings.rs b/pyapi/src/encodings.rs index 6fbd5f01..17134a2e 100644 --- a/pyapi/src/encodings.rs +++ b/pyapi/src/encodings.rs @@ -1,4 +1,5 @@ //! # Python API for RustSAT Encodings +pub mod am1; pub mod card; pub mod pb; diff --git a/pyapi/src/encodings/am1.rs b/pyapi/src/encodings/am1.rs new file mode 100644 index 00000000..71f3c7e2 --- /dev/null +++ b/pyapi/src/encodings/am1.rs @@ -0,0 +1,117 @@ +//! # Python API for RustSAT At-Most-One Encodings + +use pyo3::prelude::*; + +use rustsat::{ + encodings::{ + am1::{ + Bitwise as RsBitwise, Commander as RsCommander, Encode, Ladder as RsLadder, + Pairwise as RsPairwise, + }, + EncodeStats, + }, + instances::{BasicVarManager, Cnf as RsCnf}, + types::Lit as RsLit, +}; + +use crate::{ + handle_oom, + instances::{Cnf, VarManager}, + types::Lit, +}; + +macro_rules! implement_pyapi { + ($type:ty, $rstype:ty) => { + impl From<$rstype> for $type { + fn from(value: $rstype) -> Self { + Self(value) + } + } + + impl From<$type> for $rstype { + fn from(value: $type) -> Self { + value.0 + } + } + + #[pymethods] + impl $type { + #[new] + fn new(lits: Vec) -> Self { + let lits: Vec = unsafe { std::mem::transmute(lits) }; + <$rstype>::from_iter(lits).into() + } + + /// Gets the number of input literals in the encoding + fn n_lits(&self) -> usize { + self.0.n_lits() + } + + /// Gets the number of clauses in the encoding + fn n_clauses(&self) -> usize { + self.0.n_clauses() + } + + /// Gets the number of variables in the encoding + fn n_vars(&self) -> u32 { + self.0.n_vars() + } + + /// Builds the encoding. New variables will be taken from `var_manager`. + fn encode(&mut self, var_manager: &mut VarManager) -> PyResult { + let mut cnf = RsCnf::new(); + let var_manager: &mut BasicVarManager = var_manager.into(); + handle_oom!(self.0.encode(&mut cnf, var_manager)); + Ok(cnf.into()) + } + } + }; +} + +/// Implementations of the bitwise at-most-1 encoding. +/// +/// # References +/// +/// - Steven D. Prestwich: _Negative Effects of Modeling Techniques on Search Performance_, in +/// Trends in Constraint Programming 2007. +#[pyclass] +#[repr(transparent)] +pub struct Bitwise(RsBitwise); + +implement_pyapi!(Bitwise, RsBitwise); + +/// Implementations of the commander at-most-1 encoding. +/// +/// The encoding uses 4 splits and the pairwise encoding as the sub encoding. +/// +/// # References +/// +/// - Will Klieber and Gihwon Kwon: _Efficient CNF Encoding for Selecting 1 from N Objects, CFV +/// 2007. +#[pyclass] +#[repr(transparent)] +pub struct Commander(RsCommander); + +implement_pyapi!(Commander, RsCommander); + +/// Implementations of the ladder at-most-1 encoding. +/// +/// # References +/// +/// - Ian P. Gent and Peter Nightingale: _A new Encoding of AllDifferent into SAT_, CP 2004. +#[pyclass] +#[repr(transparent)] +pub struct Ladder(RsLadder); + +implement_pyapi!(Ladder, RsLadder); + +/// Implementations of the pairwise at-most-1 encoding. +/// +/// # References +/// +/// - Steven D. Prestwich: _CNF Encodings_, in Handbook of Satisfiability 2021. +#[pyclass] +#[repr(transparent)] +pub struct Pairwise(RsPairwise); + +implement_pyapi!(Pairwise, RsPairwise); diff --git a/pyapi/src/lib.rs b/pyapi/src/lib.rs index 5ae48d51..e0fdb044 100644 --- a/pyapi/src/lib.rs +++ b/pyapi/src/lib.rs @@ -24,6 +24,7 @@ mod types; use crate::{ encodings::{ + am1::{Bitwise, Commander, Ladder, Pairwise}, card::Totalizer, pb::{BinaryAdder, DynamicPolyWatchdog, GeneralizedTotalizer}, }, @@ -52,8 +53,14 @@ fn rustsat(py: Python<'_>, m: &Bound<'_, PyModule>) -> PyResult<()> { pb.add_class::()?; pb.add_class::()?; pb.add_class::()?; + let am1 = PyModule::new(py, "rustsat.encodings.am1")?; + am1.add_class::()?; + am1.add_class::()?; + am1.add_class::()?; + am1.add_class::()?; encodings.add("card", &card)?; encodings.add("pb", &pb)?; + encodings.add("am1", &am1)?; m.add("encodings", &encodings)?; // To import encodings. Fix from https://github.com/PyO3/pyo3/issues/759 @@ -66,6 +73,9 @@ fn rustsat(py: Python<'_>, m: &Bound<'_, PyModule>) -> PyResult<()> { py.import("sys")? .getattr("modules")? .set_item("rustsat.encodings.card", &card)?; + py.import("sys")? + .getattr("modules")? + .set_item("rustsat.encodings.am1", &am1)?; Ok(()) } From 70190fe386d5a689a4172a833d884cfb58784f48 Mon Sep 17 00:00:00 2001 From: Christoph Jabs Date: Fri, 20 Dec 2024 15:08:03 +0200 Subject: [PATCH 9/9] doc(pyapi): omit "show source" button --- .github/workflows/pages.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/pages.yml b/.github/workflows/pages.yml index 38696b11..2eaafe9c 100644 --- a/.github/workflows/pages.yml +++ b/.github/workflows/pages.yml @@ -33,7 +33,7 @@ jobs: - name: Install Python package run: pip install --no-index --find-links target/wheels/ rustsat - name: Build Python API docs - run: pip install pdoc && pdoc -o _site/pyapi/ rustsat + run: pip install pdoc && pdoc -o _site/pyapi/ --no-show-source rustsat - name: Upload artifact # Automatically uploads an artifact from the './_site' directory by default uses: actions/upload-pages-artifact@v3