Expose function/node level via FFI

bindings/cpp/include/oxidd/bcdd.hpp

@@ -348,6 +348,19 @@ class bcdd_function {
     return capi::oxidd_bcdd_cofactor_true(_func);
   }
 
+  /// Get the level of the underlying node
+  ///
+  /// Locking behavior: acquires the manager's lock for shared access.
+  ///
+  /// Runtime complexity: O(1)
+  ///
+  /// @returns  The level of the underlying inner node or
+  ///           `std::numeric_limits<oxidd::level_no>::max()` for terminals and
+  ///           invalid functions.
+  [[nodiscard]] level_no_t level() const noexcept {
+    return capi::oxidd_bcdd_level(_func);
+  }
+
   /// Compute the BCDD for the negation `¬this`
   ///
   /// Locking behavior: acquires the manager's lock for shared access.

bindings/cpp/include/oxidd/bdd.hpp

@@ -351,6 +351,19 @@ class bdd_function {
     return capi::oxidd_bdd_cofactor_true(_func);
   }
 
+  /// Get the level of the underlying node
+  ///
+  /// Locking behavior: acquires the manager's lock for shared access.
+  ///
+  /// Runtime complexity: O(1)
+  ///
+  /// @returns  The level of the underlying inner node or
+  ///           `std::numeric_limits<oxidd::level_no>::max()` for terminals and
+  ///           invalid functions.
+  [[nodiscard]] level_no_t level() const noexcept {
+    return capi::oxidd_bdd_level(_func);
+  }
+
   /// Compute the BDD for the negation `¬this`
   ///
   /// Locking behavior: acquires the manager's lock for shared access.

bindings/cpp/include/oxidd/zbdd.hpp

@@ -306,7 +306,7 @@ class zbdd_function {
   /// @name ZBDD Construction Operations
   /// @{
 
-  /// Get the cofactors `(f_true, f_false)` of `f`
+  /// Get the cofactors `(f_true, f_false)`
   ///
   /// Let f(x₀, …, xₙ) be represented by `f`, where x₀ is (currently) the
   /// top-most variable. Then f<sub>true</sub>(x₁, …, xₙ) = f(⊤, x₁, …, xₙ) and
@@ -361,6 +361,19 @@ class zbdd_function {
     return capi::oxidd_zbdd_cofactor_true(_func);
   }
 
+  /// Get the level of the underlying node
+  ///
+  /// Locking behavior: acquires the manager's lock for shared access.
+  ///
+  /// Runtime complexity: O(1)
+  ///
+  /// @returns  The level of the underlying inner node or
+  ///           `std::numeric_limits<oxidd::level_no>::max()` for terminals and
+  ///           invalid functions.
+  [[nodiscard]] level_no_t level() const noexcept {
+    return capi::oxidd_zbdd_level(_func);
+  }
+
   /// Get the ZBDD Boolean function v for the singleton set {v}
   ///
   /// `this` must be a singleton set.

bindings/python/oxidd/bcdd.py

@@ -87,7 +87,9 @@ def __del__(self):
 
 
 class BCDDFunction(
-    protocols.BooleanFunctionQuant, protocols.FunctionSubst[BCDDSubstitution]
+    protocols.BooleanFunctionQuant,
+    protocols.FunctionSubst[BCDDSubstitution],
+    protocols.HasLevel,
 ):
     """Boolean function represented as a binary decision diagram with complement
     edges (BCDD)
@@ -177,6 +179,11 @@ def cofactor_true(self) -> Self:
     def cofactor_false(self) -> Self:
         return self.__class__._from_raw(_lib.oxidd_bcdd_cofactor_false(self._func))
 
+    @override
+    def level(self) -> Optional[int]:
+        val = _lib.oxidd_bcdd_level(self._func)
+        return val if val != util._LEVEL_NO_MAX else None
+
     @override
     def __invert__(self) -> Self:
         return self.__class__._from_raw(_lib.oxidd_bcdd_not(self._func))

bindings/python/oxidd/bdd.py

@@ -87,7 +87,9 @@ def __del__(self):
 
 
 class BDDFunction(
-    protocols.BooleanFunctionQuant, protocols.FunctionSubst[BDDSubstitution]
+    protocols.BooleanFunctionQuant,
+    protocols.FunctionSubst[BDDSubstitution],
+    protocols.HasLevel,
 ):
     """Boolean function represented as a simple binary decision diagram (BDD)
 
@@ -175,6 +177,11 @@ def cofactor_true(self) -> Self:
     def cofactor_false(self) -> Self:
         return self.__class__._from_raw(_lib.oxidd_bdd_cofactor_false(self._func))
 
+    @override
+    def level(self) -> Optional[int]:
+        val = _lib.oxidd_bdd_level(self._func)
+        return val if val != util._LEVEL_NO_MAX else None
+
     @override
     def __invert__(self) -> Self:
         return self.__class__._from_raw(_lib.oxidd_bdd_not(self._func))

bindings/python/oxidd/protocols.py

@@ -10,6 +10,7 @@
     "FunctionSubst",
     "BooleanFunction",
     "BooleanFunctionQuant",
+    "HasLevel",
 ]
 
 import collections.abc
@@ -112,6 +113,20 @@ def substitute(self, substitution: S) -> Self:
         raise NotImplementedError
 
 
+class HasLevel(Function, Protocol):
+    """Function whose decision diagram node is associated with a level"""
+
+    @abstractmethod
+    def level(self) -> Optional[int]:
+        """Get the level of the underlying node (``None`` for terminals)
+
+        Locking behavior: acquires the manager's lock for shared access.
+
+        Runtime complexity: O(1)
+        """
+        raise NotImplementedError
+
+
 class BooleanFunction(Function, Protocol):
     """Boolean function represented as decision diagram"""
 

bindings/python/oxidd/tests/test_boolean_function.py

@@ -416,9 +416,12 @@ def test_zbdd_all_boolean_functions_2vars_t1():
 def pick_cube(mgr: Union[oxidd.bdd.BDDManager, oxidd.bcdd.BCDDManager]):
     """Only works for B(C)DDs"""
     tt = mgr.true()
+    assert tt.level() is None
 
     x = mgr.new_var()
     y = mgr.new_var()
+    assert x.level() is not None
+    assert y.level() is not None
 
     c = tt.pick_cube()
     assert c is not None

bindings/python/oxidd/util.py

@@ -13,6 +13,9 @@
 #: CFFI allocator that does not zero the newly allocated region
 _alloc = _ffi.new_allocator(should_clear_after_alloc=False)
 
+#: Maximum numeric value of the Rust ``LevelNo`` type (used for terminals)
+_LEVEL_NO_MAX = (1 << 32) - 1
+
 
 class BooleanOperator(enum.IntEnum):
     """Binary operators on Boolean functions"""

bindings/python/oxidd/zbdd.py

@@ -87,7 +87,7 @@ def num_inner_nodes(self) -> int:
         return _lib.oxidd_zbdd_num_inner_nodes(self._mgr)
 
 
-class ZBDDFunction(protocols.BooleanFunction):
+class ZBDDFunction(protocols.BooleanFunction, protocols.HasLevel):
     """Boolean function 𝔹ⁿ → 𝔹 (or set of Boolean vectors 𝔹ⁿ) represented as
     zero-suppressed binary decision diagram
 
@@ -175,6 +175,11 @@ def cofactor_true(self) -> Self:
     def cofactor_false(self) -> Self:
         return self.__class__._from_raw(_lib.oxidd_zbdd_cofactor_false(self._func))
 
+    @override
+    def level(self) -> Optional[int]:
+        val = _lib.oxidd_zbdd_level(self._func)
+        return val if val != util._LEVEL_NO_MAX else None
+
     def var_boolean_function(self) -> Self:
         """Get the ZBDD Boolean function v for the singleton set {v}
 

crates/oxidd-ffi/src/bcdd.rs

@@ -354,6 +354,23 @@ pub unsafe extern "C" fn oxidd_bcdd_cofactor_false(f: bcdd_t) -> bcdd_t {
     }
 }
 
+/// Get the level of `f`'s underlying node (maximum value of `oxidd_level_no_t`
+/// for terminals and invalid functions)
+///
+/// Locking behavior: acquires the manager's lock for shared access.
+///
+/// Runtime complexity: O(1)
+///
+/// @returns  The level of the underlying node.
+#[no_mangle]
+pub unsafe extern "C" fn oxidd_bcdd_level(f: bcdd_t) -> LevelNo {
+    if let Ok(f) = f.get() {
+        f.with_manager_shared(|manager, edge| manager.get_node(edge).level())
+    } else {
+        LevelNo::MAX
+    }
+}
+
 /// Compute the BCDD for the negation `¬f`
 ///
 /// Locking behavior: acquires the manager's lock for shared access.

crates/oxidd-ffi/src/bdd.rs

@@ -351,6 +351,23 @@ pub unsafe extern "C" fn oxidd_bdd_cofactor_false(f: bdd_t) -> bdd_t {
     }
 }
 
+/// Get the level of `f`'s underlying node (maximum value of `oxidd_level_no_t`
+/// for terminals and invalid functions)
+///
+/// Locking behavior: acquires the manager's lock for shared access.
+///
+/// Runtime complexity: O(1)
+///
+/// @returns  The level of the underlying node.
+#[no_mangle]
+pub unsafe extern "C" fn oxidd_bdd_level(f: bdd_t) -> LevelNo {
+    if let Ok(f) = f.get() {
+        f.with_manager_shared(|manager, edge| manager.get_node(edge).level())
+    } else {
+        LevelNo::MAX
+    }
+}
+
 /// Compute the BDD for the negation `¬f`
 ///
 /// Locking behavior: acquires the manager's lock for shared access.

crates/oxidd-ffi/src/zbdd.rs

@@ -506,6 +506,23 @@ pub unsafe extern "C" fn oxidd_zbdd_true(manager: zbdd_manager_t) -> zbdd_t {
         .with_manager_shared(|manager| ZBDDFunction::t(manager).into())
 }
 
+/// Get the level of `f`'s underlying node (maximum value of `oxidd_level_no_t`
+/// for terminals and invalid functions)
+///
+/// Locking behavior: acquires the manager's lock for shared access.
+///
+/// Runtime complexity: O(1)
+///
+/// @returns  The level of the underlying node.
+#[no_mangle]
+pub unsafe extern "C" fn oxidd_zbdd_level(f: zbdd_t) -> LevelNo {
+    if let Ok(f) = f.get() {
+        f.with_manager_shared(|manager, edge| manager.get_node(edge).level())
+    } else {
+        LevelNo::MAX
+    }
+}
+
 /// Compute the ZBDD for the negation `¬f`
 ///
 /// Locking behavior: acquires the manager's lock for shared access.