From baf235aeeb8c6c97f391326fba09e978d4ea07df Mon Sep 17 00:00:00 2001
From: Christoph Jabs <christoph.jabs@helsinki.fi>
Date: Sun, 9 Mar 2025 10:01:51 +0200
Subject: [PATCH] feat(pyapi): include bimander encoding

---
 .../python/rustsat/encodings/am1/__init__.pyi  | 10 +++++++++-
 pyapi/src/encodings/am1.rs                     | 18 ++++++++++++++++--
 2 files changed, 25 insertions(+), 3 deletions(-)

diff --git a/pyapi/python/rustsat/encodings/am1/__init__.pyi b/pyapi/python/rustsat/encodings/am1/__init__.pyi
index 2933ab19..bfac2a83 100644
--- a/pyapi/python/rustsat/encodings/am1/__init__.pyi
+++ b/pyapi/python/rustsat/encodings/am1/__init__.pyi
@@ -1,7 +1,15 @@
 from rustsat import Lit, Cnf, VarManager
 from typing import List, final
 
-__all__ = ["Bitwise", "Commander", "Ladder", "Pairwise"]
+__all__ = ["Bimander", "Bitwise", "Commander", "Ladder", "Pairwise"]
+
+@final
+class Bimander:
+    def __new__(cls, lits: List[Lit]) -> "Bimander": ...
+    def n_lits(self) -> int: ...
+    def n_clauses(self) -> int: ...
+    def n_vars(self) -> int: ...
+    def encode(self, var_manager: VarManager) -> Cnf: ...
 
 @final
 class Bitwise:
diff --git a/pyapi/src/encodings/am1.rs b/pyapi/src/encodings/am1.rs
index 71f3c7e2..2d980ad7 100644
--- a/pyapi/src/encodings/am1.rs
+++ b/pyapi/src/encodings/am1.rs
@@ -5,8 +5,8 @@ use pyo3::prelude::*;
 use rustsat::{
     encodings::{
         am1::{
-            Bitwise as RsBitwise, Commander as RsCommander, Encode, Ladder as RsLadder,
-            Pairwise as RsPairwise,
+            Bimander as RsBimander, Bitwise as RsBitwise, Commander as RsCommander, Encode,
+            Ladder as RsLadder, Pairwise as RsPairwise,
         },
         EncodeStats,
     },
@@ -68,6 +68,20 @@ macro_rules! implement_pyapi {
     };
 }
 
+/// Implementation of the bimander at-most-1 encoding.
+///
+/// The sub encoding is fixed to [`Pairwise`] and the size of the splits to 4.
+///
+/// # References
+///
+/// - Van-Hau Nguyen and Son Thay Mai: _A New Method to Encode the At-Most-One Constraint into SAT,
+///   SOICT 2015.
+#[pyclass]
+#[repr(transparent)]
+pub struct Bimander(RsBimander);
+
+implement_pyapi!(Bimander, RsBimander);
+
 /// Implementations of the bitwise at-most-1 encoding.
 ///
 /// # References