Rename pick_cube_symbolic into pick_cube_dd

bindings/cpp/include/oxidd/bcdd.hpp

@@ -672,8 +672,8 @@ class bcdd_function {
   ///
   /// @returns  A satisfying assignment if there exists one. Otherwise (i.e., if
   ///           `f` is ⊥), ⊥ is returned.
-  [[nodiscard]] bcdd_function pick_cube_symbolic() const noexcept {
-    return capi::oxidd_bcdd_pick_cube_symbolic(_func);
+  [[nodiscard]] bcdd_function pick_cube_dd() const noexcept {
+    return capi::oxidd_bcdd_pick_cube_dd(_func);
   }
 
   /// Pick a satisfying assignment, represented as BCDD, using the literals in
@@ -691,8 +691,8 @@ class bcdd_function {
   /// @returns  A satisfying assignment if there exists one. Otherwise (i.e., if
   ///           `f` is ⊥), ⊥ is returned.
   [[nodiscard]] bcdd_function
-  pick_cube_symbolic_set(const bcdd_function &literal_set) const noexcept {
-    return capi::oxidd_bcdd_pick_cube_symbolic_set(_func, literal_set._func);
+  pick_cube_dd_set(const bcdd_function &literal_set) const noexcept {
+    return capi::oxidd_bcdd_pick_cube_dd_set(_func, literal_set._func);
   }
 
   /// Evaluate this Boolean function with arguments `args`

bindings/cpp/include/oxidd/bdd.hpp

@@ -676,8 +676,8 @@ class bdd_function {
   ///
   /// @returns  A satisfying assignment if there exists one. Otherwise (i.e., if
   ///           `f` is ⊥), ⊥ is returned.
-  [[nodiscard]] bdd_function pick_cube_symbolic() const noexcept {
-    return capi::oxidd_bdd_pick_cube_symbolic(_func);
+  [[nodiscard]] bdd_function pick_cube_dd() const noexcept {
+    return capi::oxidd_bdd_pick_cube_dd(_func);
   }
 
   /// Pick a satisfying assignment, represented as BDD, using the literals in
@@ -695,8 +695,8 @@ class bdd_function {
   /// @returns  A satisfying assignment if there exists one. Otherwise (i.e., if
   ///           `f` is ⊥), ⊥ is returned.
   [[nodiscard]] bdd_function
-  pick_cube_symbolic_set(const bdd_function &literal_set) const noexcept {
-    return capi::oxidd_bdd_pick_cube_symbolic_set(_func, literal_set._func);
+  pick_cube_dd_set(const bdd_function &literal_set) const noexcept {
+    return capi::oxidd_bdd_pick_cube_dd_set(_func, literal_set._func);
   }
 
   /// Evaluate this Boolean function with arguments `args`

bindings/cpp/include/oxidd/concepts.hpp

@@ -232,9 +232,9 @@ concept substitution = function_subst<typename S::function> &&
 /// - `f.pick_cube()` returns a satisfying `oxidd::util::assignment` if `f` is
 ///   satisfiable, or an empty `oxidd::util::assignment` otherwise. `f` must be
 ///   valid.
-/// - `f.pick_cube_symbolic()` returns a satisfying assignment as decision
-///   diagram if there is one or ⊥.
-/// - `f.pick_cube_symbolic_set(literal_set)` returns a satisfying assignment as
+/// - `f.pick_cube_dd()` returns a satisfying assignment as decision diagram if
+///   there is one or ⊥.
+/// - `f.pick_cube_dd_set(literal_set)` returns a satisfying assignment as
 ///   decision diagram if there is one or ⊥. Whenever there is a choice for a
 ///   variable, and the variable is defined in `literal_set`, the respective
 ///   polarity is used.
@@ -289,8 +289,8 @@ concept boolean_function =
       { f.sat_count_double(levels) } -> std::same_as<double>;
 
       { f.pick_cube() } -> std::same_as<util::assignment>;
-      { f.pick_cube_symbolic() } -> std::same_as<F>;
-      { f.pick_cube_symbolic_set(f) } -> std::same_as<F>;
+      { f.pick_cube_dd() } -> std::same_as<F>;
+      { f.pick_cube_dd_set(f) } -> std::same_as<F>;
 
       { f.eval(args) } -> std::same_as<bool>;
     } &&

bindings/cpp/include/oxidd/zbdd.hpp

@@ -637,8 +637,8 @@ class zbdd_function {
   ///
   /// @returns  A satisfying assignment if there exists one. Otherwise (i.e., if
   ///           `f` is ⊥), ⊥ is returned.
-  [[nodiscard]] zbdd_function pick_cube_symbolic() const noexcept {
-    return capi::oxidd_zbdd_pick_cube_symbolic(_func);
+  [[nodiscard]] zbdd_function pick_cube_dd() const noexcept {
+    return capi::oxidd_zbdd_pick_cube_dd(_func);
   }
 
   /// Pick a satisfying assignment, represented as ZBDD, using the literals in
@@ -656,8 +656,8 @@ class zbdd_function {
   /// @returns  A satisfying assignment if there exists one. Otherwise (i.e., if
   ///           `f` is ⊥), ⊥ is returned.
   [[nodiscard]] zbdd_function
-  pick_cube_symbolic_set(const zbdd_function &literal_set) const noexcept {
-    return capi::oxidd_zbdd_pick_cube_symbolic_set(_func, literal_set._func);
+  pick_cube_dd_set(const zbdd_function &literal_set) const noexcept {
+    return capi::oxidd_zbdd_pick_cube_dd_set(_func, literal_set._func);
   }
 
   /// Evaluate this Boolean function with arguments `args`

bindings/cpp/tests/boolean-function.cpp

@@ -315,12 +315,11 @@ template <boolean_function_manager M> class test_all_boolean_functions {
 
       /* pick_cube() etc. */ {
         // This is a stripped-down version of the Rust test; we only test that
-        // the results of `pick_cube()` and `pick_cube_symbolic()` agree
-        // (therefore, both can be represented as a conjunction of literals),
-        // and that they imply `f`.
+        // the results of `pick_cube()` and `pick_cube_dd()` agree (therefore,
+        // both can be represented as a conjunction of literals), and that they
+        // imply `f`.
         const util::assignment cube = f.pick_cube();
-        const explicit_b_func actual =
-            _dd_to_boolean_func.at(f.pick_cube_symbolic());
+        const explicit_b_func actual = _dd_to_boolean_func.at(f.pick_cube_dd());
 
         if (f_explicit == 0) {
           assert(actual == 0);
@@ -351,8 +350,8 @@ template <boolean_function_manager M> class test_all_boolean_functions {
             if ((pos & neg) != 0)
               continue;
 
-            const explicit_b_func actual = _dd_to_boolean_func.at(
-                f.pick_cube_symbolic_set(make_cube(pos, neg)));
+            const explicit_b_func actual =
+                _dd_to_boolean_func.at(f.pick_cube_dd_set(make_cube(pos, neg)));
 
             if (f_explicit == 0) {
               assert(actual == 0);

bindings/python/oxidd/bcdd.py

@@ -346,16 +346,16 @@ def pick_cube(self) -> Optional[util.Assignment]:
         return util.Assignment._from_raw(raw) if raw.len > 0 else None
 
     @override
-    def pick_cube_symbolic(self) -> Self:
-        return self.__class__._from_raw(_lib.oxidd_bcdd_pick_cube_symbolic(self._func))
+    def pick_cube_dd(self) -> Self:
+        return self.__class__._from_raw(_lib.oxidd_bcdd_pick_cube_dd(self._func))
 
     @override
-    def pick_cube_symbolic_set(self, literal_set: Self) -> Self:
+    def pick_cube_dd_set(self, literal_set: Self) -> Self:
         assert (
             self._func._p == literal_set._func._p
         ), "`self` and `literal_set` must belong to the same manager"
         return self.__class__._from_raw(
-            _lib.oxidd_bcdd_pick_cube_symbolic_set(self._func, literal_set._func)
+            _lib.oxidd_bcdd_pick_cube_dd_set(self._func, literal_set._func)
         )
 
     @override

bindings/python/oxidd/bdd.py

@@ -344,16 +344,16 @@ def pick_cube(self) -> Optional[util.Assignment]:
         return util.Assignment._from_raw(raw) if raw.len > 0 else None
 
     @override
-    def pick_cube_symbolic(self) -> Self:
-        return self.__class__._from_raw(_lib.oxidd_bdd_pick_cube_symbolic(self._func))
+    def pick_cube_dd(self) -> Self:
+        return self.__class__._from_raw(_lib.oxidd_bdd_pick_cube_dd(self._func))
 
     @override
-    def pick_cube_symbolic_set(self, literal_set: Self) -> Self:
+    def pick_cube_dd_set(self, literal_set: Self) -> Self:
         assert (
             self._func._p == literal_set._func._p
         ), "`self` and `literal_set` must belong to the same manager"
         return self.__class__._from_raw(
-            _lib.oxidd_bdd_pick_cube_symbolic_set(self._func, literal_set._func)
+            _lib.oxidd_bdd_pick_cube_dd_set(self._func, literal_set._func)
         )
 
     @override

bindings/python/oxidd/protocols.py

@@ -322,7 +322,7 @@ def pick_cube(self) -> Optional[Assignment]:
         raise NotImplementedError
 
     @abstractmethod
-    def pick_cube_symbolic(self) -> Self:
+    def pick_cube_dd(self) -> Self:
         """Pick a satisfying assignment, represented as decision diagram
 
         Returns ``⊥`` iff ``self`` is unsatisfiable.
@@ -332,7 +332,7 @@ def pick_cube_symbolic(self) -> Self:
         raise NotImplementedError
 
     @abstractmethod
-    def pick_cube_symbolic_set(self, literal_set: Self) -> Self:
+    def pick_cube_dd_set(self, literal_set: Self) -> Self:
         """Pick a satisfying assignment, represented as BDD, using the
         literals in ``literal_set`` if there is a choice
 

bindings/python/oxidd/tests/test_boolean_function.py

@@ -197,12 +197,12 @@ def basic(self):
             # pick_cube() etc.
 
             # This is a stripped-down version of the Rust test; we only test
-            # that the results of `pick_cube()` and `pick_cube_symbolic()` agree
+            # that the results of `pick_cube()` and `pick_cube_dd()` agree
             # (therefore, both can be represented as a conjunction of literals),
             # and that they imply `f`.
 
             cube = f.pick_cube()
-            actual = self._dd_to_boolean_func[f.pick_cube_symbolic()]
+            actual = self._dd_to_boolean_func[f.pick_cube_dd()]
 
             if f_explicit == 0:
                 assert actual == 0
@@ -228,7 +228,7 @@ def basic(self):
                         continue
 
                     actual = self._dd_to_boolean_func[
-                        f.pick_cube_symbolic_set(self.make_cube(pos, neg))
+                        f.pick_cube_dd_set(self.make_cube(pos, neg))
                     ]
                     for var, var_func in enumerate(self._var_functions):
                         if (actual & var_func) >> (1 << var) == actual & ~var_func:

bindings/python/oxidd/zbdd.py

@@ -317,16 +317,16 @@ def pick_cube(self) -> Optional[util.Assignment]:
         return util.Assignment._from_raw(raw) if raw.len > 0 else None
 
     @override
-    def pick_cube_symbolic(self) -> Self:
-        return self.__class__._from_raw(_lib.oxidd_zbdd_pick_cube_symbolic(self._func))
+    def pick_cube_dd(self) -> Self:
+        return self.__class__._from_raw(_lib.oxidd_zbdd_pick_cube_dd(self._func))
 
     @override
-    def pick_cube_symbolic_set(self, literal_set: Self) -> Self:
+    def pick_cube_dd_set(self, literal_set: Self) -> Self:
         assert (
             self._func._p == literal_set._func._p
         ), "`self` and `literal_set` must belong to the same manager"
         return self.__class__._from_raw(
-            _lib.oxidd_zbdd_pick_cube_symbolic_set(self._func, literal_set._func)
+            _lib.oxidd_zbdd_pick_cube_dd_set(self._func, literal_set._func)
         )
 
     @override

crates/oxidd-core/src/function.rs

@@ -663,12 +663,12 @@ pub trait BooleanFunction: Function {
     /// If `self` is `⊥`, then the return value will be `⊥`.
     ///
     /// Locking behavior: acquires the manager's lock for shared access.
-    fn pick_cube_symbolic(
+    fn pick_cube_dd(
         &self,
         choice: impl for<'id> FnMut(&Self::Manager<'id>, &EdgeOfFunc<'id, Self>, LevelNo) -> bool,
     ) -> AllocResult<Self> {
         self.with_manager_shared(|manager, edge| {
-            let res = Self::pick_cube_symbolic_edge(manager, edge, choice)?;
+            let res = Self::pick_cube_dd_edge(manager, edge, choice)?;
             Ok(Self::from_edge(manager, res))
         })
     }
@@ -692,10 +692,9 @@ pub trait BooleanFunction: Function {
     /// If `self` is `⊥`, then the return value will be `⊥`.
     ///
     /// Locking behavior: acquires the manager's lock for shared access.
-    fn pick_cube_symbolic_set(&self, literal_set: &Self) -> AllocResult<Self> {
+    fn pick_cube_dd_set(&self, literal_set: &Self) -> AllocResult<Self> {
         self.with_manager_shared(|manager, edge| {
-            let res =
-                Self::pick_cube_symbolic_set_edge(manager, edge, literal_set.as_edge(manager))?;
+            let res = Self::pick_cube_dd_set_edge(manager, edge, literal_set.as_edge(manager))?;
             Ok(Self::from_edge(manager, res))
         })
     }
@@ -710,15 +709,15 @@ pub trait BooleanFunction: Function {
     where
         I: ExactSizeIterator<Item = &'a EdgeOfFunc<'id, Self>>;
 
-    /// `Edge` version of [`Self::pick_cube_symbolic()`]
-    fn pick_cube_symbolic_edge<'id>(
+    /// `Edge` version of [`Self::pick_cube_dd()`]
+    fn pick_cube_dd_edge<'id>(
         manager: &Self::Manager<'id>,
         edge: &EdgeOfFunc<'id, Self>,
         choice: impl FnMut(&Self::Manager<'id>, &EdgeOfFunc<'id, Self>, LevelNo) -> bool,
     ) -> AllocResult<EdgeOfFunc<'id, Self>>;
 
-    /// `Edge` version of [`Self::pick_cube_symbolic_set()`]
-    fn pick_cube_symbolic_set_edge<'id>(
+    /// `Edge` version of [`Self::pick_cube_dd_set()`]
+    fn pick_cube_dd_set_edge<'id>(
         manager: &Self::Manager<'id>,
         edge: &EdgeOfFunc<'id, Self>,
         literal_set: &EdgeOfFunc<'id, Self>,

crates/oxidd-derive/src/function.rs

@@ -447,7 +447,7 @@ pub fn derive_boolean_function(input: syn::DeriveInput) -> TokenStream {
             Binary("imp"),
             Binary("imp_strict"),
             Ternary("ite"),
-            Binary("pick_cube_symbolic_set"),
+            Binary("pick_cube_dd_set"),
         ],
         |ctx| {
             let CustomMethodsCtx {
@@ -560,21 +560,21 @@ pub fn derive_boolean_function(input: syn::DeriveInput) -> TokenStream {
                 }
 
                 #[inline]
-                fn pick_cube_symbolic(
+                fn pick_cube_dd(
                     &self,
                     choice: impl for<'__id> ::std::ops::FnMut(&#manager_ty, &#edge_ty, ::oxidd_core::LevelNo) -> bool,
                 ) -> ::oxidd_core::util::AllocResult<Self> {
-                    let res = <#inner as #trait_path>::pick_cube_symbolic(&self.#field, choice)?;
+                    let res = <#inner as #trait_path>::pick_cube_dd(&self.#field, choice)?;
                     Ok(#from_res)
                 }
 
                 #[inline]
-                fn pick_cube_symbolic_edge<'__id>(
+                fn pick_cube_dd_edge<'__id>(
                     manager: &#manager_ty,
                     edge: &#edge_ty,
                     choice: impl ::std::ops::FnMut(&#manager_ty, &#edge_ty, ::oxidd_core::LevelNo) -> bool,
                 ) -> ::oxidd_core::util::AllocResult<#edge_ty> {
-                    <#inner as #trait_path>::pick_cube_symbolic_edge(manager, edge, choice)
+                    <#inner as #trait_path>::pick_cube_dd_edge(manager, edge, choice)
                 }
 
                 #[inline]

crates/oxidd-ffi/src/bcdd.rs

@@ -789,10 +789,8 @@ pub unsafe extern "C" fn oxidd_bcdd_pick_cube(f: bcdd_t) -> assignment_t {
 /// @returns  A satisfying assignment if there exists one. Otherwise (i.e., if
 ///           `f` is ⊥), ⊥ is returned.
 #[no_mangle]
-pub unsafe extern "C" fn oxidd_bcdd_pick_cube_symbolic(f: bcdd_t) -> bcdd_t {
-    f.get()
-        .and_then(|f| f.pick_cube_symbolic(|_, _, _| false))
-        .into()
+pub unsafe extern "C" fn oxidd_bcdd_pick_cube_dd(f: bcdd_t) -> bcdd_t {
+    f.get().and_then(|f| f.pick_cube_dd(|_, _, _| false)).into()
 }
 
 /// Pick a satisfying assignment, represented as BCDD, using the literals in
@@ -810,11 +808,8 @@ pub unsafe extern "C" fn oxidd_bcdd_pick_cube_symbolic(f: bcdd_t) -> bcdd_t {
 /// @returns  A satisfying assignment if there exists one. Otherwise (i.e., if
 ///           `f` is ⊥), ⊥ is returned.
 #[no_mangle]
-pub unsafe extern "C" fn oxidd_bcdd_pick_cube_symbolic_set(
-    f: bcdd_t,
-    literal_set: bcdd_t,
-) -> bcdd_t {
-    op2(f, literal_set, BCDDFunction::pick_cube_symbolic_set)
+pub unsafe extern "C" fn oxidd_bcdd_pick_cube_dd_set(f: bcdd_t, literal_set: bcdd_t) -> bcdd_t {
+    op2(f, literal_set, BCDDFunction::pick_cube_dd_set)
 }
 
 /// Pair of a BCDD function and a Boolean

crates/oxidd-ffi/src/bdd.rs

@@ -782,10 +782,8 @@ pub unsafe extern "C" fn oxidd_bdd_pick_cube(f: bdd_t) -> assignment_t {
 /// @returns  A satisfying assignment if there exists one. Otherwise (i.e., if
 ///           `f` is ⊥), ⊥ is returned.
 #[no_mangle]
-pub unsafe extern "C" fn oxidd_bdd_pick_cube_symbolic(f: bdd_t) -> bdd_t {
-    f.get()
-        .and_then(|f| f.pick_cube_symbolic(|_, _, _| false))
-        .into()
+pub unsafe extern "C" fn oxidd_bdd_pick_cube_dd(f: bdd_t) -> bdd_t {
+    f.get().and_then(|f| f.pick_cube_dd(|_, _, _| false)).into()
 }
 
 /// Pick a satisfying assignment, represented as BDD, using the literals in
@@ -803,8 +801,8 @@ pub unsafe extern "C" fn oxidd_bdd_pick_cube_symbolic(f: bdd_t) -> bdd_t {
 /// @returns  A satisfying assignment if there exists one. Otherwise (i.e., if
 ///           `f` is ⊥), ⊥ is returned.
 #[no_mangle]
-pub unsafe extern "C" fn oxidd_bdd_pick_cube_symbolic_set(f: bdd_t, literal_set: bdd_t) -> bdd_t {
-    op2(f, literal_set, BDDFunction::pick_cube_symbolic_set)
+pub unsafe extern "C" fn oxidd_bdd_pick_cube_dd_set(f: bdd_t, literal_set: bdd_t) -> bdd_t {
+    op2(f, literal_set, BDDFunction::pick_cube_dd_set)
 }
 
 /// Pair of a BDD function and a Boolean

crates/oxidd-ffi/src/zbdd.rs

@@ -715,10 +715,8 @@ pub unsafe extern "C" fn oxidd_zbdd_pick_cube(f: zbdd_t) -> assignment_t {
 /// @returns  A satisfying assignment if there exists one. Otherwise (i.e., if
 ///           `f` is ⊥), ⊥ is returned.
 #[no_mangle]
-pub unsafe extern "C" fn oxidd_zbdd_pick_cube_symbolic(f: zbdd_t) -> zbdd_t {
-    f.get()
-        .and_then(|f| f.pick_cube_symbolic(|_, _, _| false))
-        .into()
+pub unsafe extern "C" fn oxidd_zbdd_pick_cube_dd(f: zbdd_t) -> zbdd_t {
+    f.get().and_then(|f| f.pick_cube_dd(|_, _, _| false)).into()
 }
 
 /// Pick a satisfying assignment, represented as ZBDD, using the literals in
@@ -736,11 +734,8 @@ pub unsafe extern "C" fn oxidd_zbdd_pick_cube_symbolic(f: zbdd_t) -> zbdd_t {
 /// @returns  A satisfying assignment if there exists one. Otherwise (i.e., if
 ///           `f` is ⊥), ⊥ is returned.
 #[no_mangle]
-pub unsafe extern "C" fn oxidd_zbdd_pick_cube_symbolic_set(
-    f: zbdd_t,
-    literal_set: zbdd_t,
-) -> zbdd_t {
-    op2(f, literal_set, ZBDDFunction::pick_cube_symbolic_set)
+pub unsafe extern "C" fn oxidd_zbdd_pick_cube_dd_set(f: zbdd_t, literal_set: zbdd_t) -> zbdd_t {
+    op2(f, literal_set, ZBDDFunction::pick_cube_dd_set)
 }
 
 /// Pair of a ZBDD function and a Boolean