Python: add BooleanFunction.sat_count using arbitrary precision int…

…egers

bindings/python/oxidd/protocols.py

@@ -367,9 +367,24 @@ def valid(self, /) -> bool:
         """
         raise NotImplementedError
 
+    @abstractmethod
+    def sat_count(self, /, vars: int) -> int:
+        """Count the exact number of satisfying assignments.
+
+        Uses arbitrary precision integers.
+
+        Locking behavior: acquires the manager's lock for shared access.
+
+        Args:
+            vars: Assume that the function's domain has this many variables.
+        """
+        raise NotImplementedError
+
     @abstractmethod
     def sat_count_float(self, /, vars: int) -> float:
-        """Count the number of satisfying assignments.
+        """Count the (approximate) number of satisfying assignments.
+
+        Uses floating point numbers.
 
         Locking behavior: acquires the manager's lock for shared access.
 

crates/oxidd-ffi-python/Cargo.toml

@@ -23,7 +23,10 @@ oxidd-core = { workspace = true }
 oxidd-dump = { workspace = true, features = ["dddmp", "dot"] }
 oxidd = { workspace = true, features = ["bdd", "bcdd", "zbdd"] }
 
-pyo3 = { version = "0.23.1", features = ["extension-module", "abi3-py39"] }
+pyo3 = { version = "0.23.1", features = ["extension-module", "abi3-py39", "num-bigint"] }
+
+# big integers
+num-bigint = "0.4"
 
 # fast hash function
 #

crates/oxidd-ffi-python/src/bcdd.rs

@@ -3,6 +3,7 @@
 use std::hash::BuildHasherDefault;
 use std::path::PathBuf;
 
+use num_bigint::BigUint;
 use pyo3::prelude::*;
 use pyo3::types::{PyBool, PyList, PyNone, PyTuple, PyType};
 use rustc_hash::FxHasher;
@@ -695,6 +696,23 @@ impl BCDDFunction {
         self.0.valid()
     }
 
+    /// Count the number of satisfying assignments.
+    ///
+    /// Locking behavior: acquires the manager's lock for shared access.
+    ///
+    /// Args:
+    ///     vars (int): Assume that the function's domain has this many
+    ///         variables.
+    ///
+    /// Returns:
+    ///     int: The exact number of satisfying assignments
+    fn sat_count(&self, py: Python, vars: LevelNo) -> BigUint {
+        py.allow_threads(move || {
+            self.0
+                .sat_count::<BigUint, BuildHasherDefault<FxHasher>>(vars, &mut Default::default())
+        })
+    }
+
     /// Count the number of satisfying assignments.
     ///
     /// Locking behavior: acquires the manager's lock for shared access.

crates/oxidd-ffi-python/src/bdd.rs

@@ -3,6 +3,7 @@
 use std::hash::BuildHasherDefault;
 use std::path::PathBuf;
 
+use num_bigint::BigUint;
 use pyo3::prelude::*;
 use pyo3::types::{PyBool, PyList, PyNone, PyTuple, PyType};
 use rustc_hash::FxHasher;
@@ -693,6 +694,23 @@ impl BDDFunction {
         self.0.valid()
     }
 
+    /// Count the number of satisfying assignments.
+    ///
+    /// Locking behavior: acquires the manager's lock for shared access.
+    ///
+    /// Args:
+    ///     vars (int): Assume that the function's domain has this many
+    ///         variables.
+    ///
+    /// Returns:
+    ///     int: The exact number of satisfying assignments
+    fn sat_count(&self, py: Python, vars: LevelNo) -> BigUint {
+        py.allow_threads(move || {
+            self.0
+                .sat_count::<BigUint, BuildHasherDefault<FxHasher>>(vars, &mut Default::default())
+        })
+    }
+
     /// Count the number of satisfying assignments.
     ///
     /// Locking behavior: acquires the manager's lock for shared access.

crates/oxidd-ffi-python/src/zbdd.rs

@@ -3,6 +3,7 @@
 use std::hash::BuildHasherDefault;
 use std::path::PathBuf;
 
+use num_bigint::BigUint;
 use pyo3::prelude::*;
 use pyo3::types::{PyBool, PyList, PyNone, PyTuple};
 use rustc_hash::FxHasher;
@@ -580,6 +581,23 @@ impl ZBDDFunction {
         self.0.valid()
     }
 
+    /// Count the number of satisfying assignments.
+    ///
+    /// Locking behavior: acquires the manager's lock for shared access.
+    ///
+    /// Args:
+    ///     vars (int): Assume that the function's domain has this many
+    ///         variables.
+    ///
+    /// Returns:
+    ///     int: The exact number of satisfying assignments
+    fn sat_count(&self, py: Python, vars: LevelNo) -> BigUint {
+        py.allow_threads(move || {
+            self.0
+                .sat_count::<BigUint, BuildHasherDefault<FxHasher>>(vars, &mut Default::default())
+        })
+    }
+
     /// Count the number of satisfying assignments.
     ///
     /// Locking behavior: acquires the manager's lock for shared access.