From 7a64d8c76ba99762c0594d5b428575468df26ae0 Mon Sep 17 00:00:00 2001 From: Maurice Laveaux Date: Tue, 24 Sep 2024 10:50:04 +0200 Subject: [PATCH] Expose function/node level via FFI --- bindings/cpp/include/oxidd/bcdd.hpp | 13 +++++++++++++ bindings/cpp/include/oxidd/bdd.hpp | 13 +++++++++++++ bindings/cpp/include/oxidd/zbdd.hpp | 15 ++++++++++++++- bindings/python/oxidd/bcdd.py | 9 ++++++++- bindings/python/oxidd/bdd.py | 9 ++++++++- bindings/python/oxidd/protocols.py | 15 +++++++++++++++ .../python/oxidd/tests/test_boolean_function.py | 3 +++ bindings/python/oxidd/util.py | 3 +++ bindings/python/oxidd/zbdd.py | 7 ++++++- crates/oxidd-ffi/src/bcdd.rs | 17 +++++++++++++++++ crates/oxidd-ffi/src/bdd.rs | 17 +++++++++++++++++ crates/oxidd-ffi/src/zbdd.rs | 17 +++++++++++++++++ 12 files changed, 134 insertions(+), 4 deletions(-) diff --git a/bindings/cpp/include/oxidd/bcdd.hpp b/bindings/cpp/include/oxidd/bcdd.hpp index d81d4e9..0dc0b17 100644 --- a/bindings/cpp/include/oxidd/bcdd.hpp +++ b/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::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. diff --git a/bindings/cpp/include/oxidd/bdd.hpp b/bindings/cpp/include/oxidd/bdd.hpp index d49b7fe..9887fb5 100644 --- a/bindings/cpp/include/oxidd/bdd.hpp +++ b/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::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. diff --git a/bindings/cpp/include/oxidd/zbdd.hpp b/bindings/cpp/include/oxidd/zbdd.hpp index cbe62db..d8b08dd 100644 --- a/bindings/cpp/include/oxidd/zbdd.hpp +++ b/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 ftrue(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::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. diff --git a/bindings/python/oxidd/bcdd.py b/bindings/python/oxidd/bcdd.py index f1d04c9..4c8df7b 100644 --- a/bindings/python/oxidd/bcdd.py +++ b/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)) diff --git a/bindings/python/oxidd/bdd.py b/bindings/python/oxidd/bdd.py index 472eb75..e924ff4 100644 --- a/bindings/python/oxidd/bdd.py +++ b/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)) diff --git a/bindings/python/oxidd/protocols.py b/bindings/python/oxidd/protocols.py index 1b6ee8f..e912252 100644 --- a/bindings/python/oxidd/protocols.py +++ b/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""" diff --git a/bindings/python/oxidd/tests/test_boolean_function.py b/bindings/python/oxidd/tests/test_boolean_function.py index 0877c04..3a8d6a1 100644 --- a/bindings/python/oxidd/tests/test_boolean_function.py +++ b/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 diff --git a/bindings/python/oxidd/util.py b/bindings/python/oxidd/util.py index 764dbd7..afcba1f 100644 --- a/bindings/python/oxidd/util.py +++ b/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""" diff --git a/bindings/python/oxidd/zbdd.py b/bindings/python/oxidd/zbdd.py index 4bd955b..121afe6 100644 --- a/bindings/python/oxidd/zbdd.py +++ b/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} diff --git a/crates/oxidd-ffi/src/bcdd.rs b/crates/oxidd-ffi/src/bcdd.rs index 7c0b916..dc1595a 100644 --- a/crates/oxidd-ffi/src/bcdd.rs +++ b/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. diff --git a/crates/oxidd-ffi/src/bdd.rs b/crates/oxidd-ffi/src/bdd.rs index 998f559..4864e5b 100644 --- a/crates/oxidd-ffi/src/bdd.rs +++ b/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. diff --git a/crates/oxidd-ffi/src/zbdd.rs b/crates/oxidd-ffi/src/zbdd.rs index 173c7d2..fbbd0e3 100644 --- a/crates/oxidd-ffi/src/zbdd.rs +++ b/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.