Test C++ API

.project-words.txt

@@ -80,6 +80,7 @@ noreturn
 OxiDD
 pointee
 postprocess
+precompute
 ptrdiff
 RAII
 realloc

bindings/cpp/include/oxidd/util.hpp

@@ -85,7 +85,7 @@ template <typename T> class slice {
 
   /// Construct a slice from a std::vector<T>
   template <typename A>
-  slice(const std::vector<T, A> &vec) : _data(vec.data()), _len(vec.len()) {}
+  slice(const std::vector<T, A> &vec) : _data(vec.data()), _len(vec.size()) {}
 
   /// Construct a slice from a std::array<T>
   template <size_t N>
@@ -94,8 +94,7 @@ template <typename T> class slice {
 
   /// Construct a slice from a C array
   template <size_t N>
-  constexpr slice(const T (&array)[N])
-      : _data(array.data()), _len(array.len()) {}
+  constexpr slice(const T (&array)[N]) : _data(array), _len(N) {}
 
   /// Construct a slice from a std::initializer_list<T>
   constexpr slice(const std::initializer_list<T> &list)

bindings/cpp/include/oxidd/zbdd.hpp

@@ -342,6 +342,17 @@ class zbdd_function {
     return capi::oxidd_zbdd_cofactor_true(_func);
   }
 
+  /// Get the ZBDD Boolean function v for the singleton set {v}
+  ///
+  /// `this` must be a singleton set.
+  ///
+  /// Locking behavior: acquires a shared manager lock.
+  ///
+  /// @returns  The ZBDD Boolean function v
+  zbdd_function var_boolean_function() const noexcept {
+    return capi::oxidd_zbdd_var_boolean_function(_func);
+  }
+
   /// Compute the ZBDD for the negation `¬this`
   ///
   /// Locking behavior: acquires a shared manager lock.

bindings/cpp/tests/boolean-function.cpp

@@ -1,21 +1,312 @@
 #undef NDEBUG // enable runtime assertions regardless of the build type
 
+#include <bit>
+#include <cstdint>
+#include <limits>
+#include <unordered_map>
+#include <vector>
+
 #include <oxidd/bcdd.hpp>
 #include <oxidd/bdd.hpp>
 #include <oxidd/concepts.hpp>
 #include <oxidd/zbdd.hpp>
 
 using namespace oxidd;
 using namespace oxidd::concepts;
+using oxidd::util::slice;
+
+// spell-checker:ignore nvars
+
+using explicit_b_func = uint32_t;
+
+/// C++ translation `TestAllBooleanFunctions` form
+/// `crates/oxidd/tests/boolean_function.rs`
+template <boolean_function_manager M> class test_all_boolean_functions {
+  M _mgr;
+  slice<typename M::function> _vars;
+  /// Stores all possible Boolean functions with `vars.size()` vars
+  std::vector<typename M::function> _boolean_functions;
+  std::unordered_map<typename M::function, explicit_b_func> _dd_to_boolean_func;
+
+public:
+  test_all_boolean_functions(const M &mgr, slice<typename M::function> vars,
+                             slice<typename M::function> var_handles)
+      : _mgr(mgr), _vars(vars) {
+    assert(vars.size() == var_handles.size());
+    assert(std::bit_width(
+               (unsigned)std::numeric_limits<explicit_b_func>::digits) >=
+               vars.size() &&
+           "too many variables");
+    // actually, only 3 are possible in a feasible amount of time
+
+    const unsigned nvars = vars.size();
+    const unsigned num_assignments = 1 << nvars;
+    const explicit_b_func num_functions = 1 << num_assignments;
+    _boolean_functions.reserve(num_functions);
+    _dd_to_boolean_func.reserve(num_functions);
+
+    std::vector<std::pair<typename M::function, bool>> args;
+    args.reserve(nvars);
+    for (const typename M::function &var : var_handles)
+      args.emplace_back(var, false);
+
+    for (explicit_b_func explicit_f = 0; explicit_f < num_functions;
+         ++explicit_f) {
+      // naïve DD construction from the on-set
+      typename M::function f = _mgr.f();
+      for (unsigned assignment = 0; assignment < num_assignments;
+           ++assignment) {
+        if ((explicit_f & (1 << assignment)) == 0)
+          continue; // not part of the on-set
+        typename M::function cube = _mgr.t();
+
+        for (unsigned var = 0; var < nvars; ++var) {
+          typename M::function v = _vars[var];
+          if ((assignment & (1 << var)) == 0)
+            v = ~v;
+          cube &= v;
+          assert(!cube.is_invalid());
+        }
+
+        f |= cube;
+        assert(!f.is_invalid());
+      }
+
+      // check that evaluating the function yields the desired values
+      for (unsigned assignment = 0; assignment < num_assignments;
+           ++assignment) {
+        const bool expected = (explicit_f & (1 << assignment)) != 0;
+        for (unsigned var = 0; var < nvars; ++var)
+          args[var].second = (assignment & (1 << var)) != 0;
+        const bool actual = f.eval(args);
+        assert(actual == expected);
+        assert(f.sat_count_double(nvars) == std::popcount(explicit_f));
+      }
+
+      _boolean_functions.push_back(f);
+      const auto [_, inserted] =
+          _dd_to_boolean_func.emplace(std::move(f), explicit_f);
+      assert(inserted &&
+             "two different Boolean functions have the same representation");
+    }
+  }
+
+  /// Test basic operations on all Boolean function with the given variable set
+  void basic() const {
+    const unsigned nvars = _vars.size();
+    const unsigned num_assignments = 1 << nvars;
+    const explicit_b_func num_functions = 1 << num_assignments;
+    const explicit_b_func func_mask = num_functions - 1;
+
+    // false & true
+    assert(_mgr.f() == _boolean_functions.front());
+    assert(_mgr.t() == _boolean_functions.back());
+
+    // vars
+    for (unsigned var = 0; var < nvars; ++var) {
+      explicit_b_func expected = 0;
+      for (unsigned assignment = 0; assignment < num_assignments; ++assignment)
+        expected |= ((assignment >> var) & 1) << assignment;
+      const explicit_b_func actual = _dd_to_boolean_func.at(_vars[var]);
+      assert(actual == expected);
+    }
+
+    // arity >= 1
+    for (explicit_b_func f_explicit = 0; f_explicit < num_functions;
+         ++f_explicit) {
+      const typename M::function &f = _boolean_functions[f_explicit];
+
+      /* not */ {
+        const explicit_b_func expected = ~f_explicit & func_mask;
+        const explicit_b_func actual = _dd_to_boolean_func.at(~f);
+        assert(actual == expected);
+      }
+
+      // arity >= 2
+      for (explicit_b_func g_explicit = 0; g_explicit < num_functions;
+           ++g_explicit) {
+        const typename M::function &g = _boolean_functions[g_explicit];
+
+        /* and */ {
+          const explicit_b_func expected = f_explicit & g_explicit;
+          const explicit_b_func actual = _dd_to_boolean_func.at(f & g);
+          assert(actual == expected);
+        }
+        /* or */ {
+          const explicit_b_func expected = f_explicit | g_explicit;
+          const explicit_b_func actual = _dd_to_boolean_func.at(f | g);
+          assert(actual == expected);
+        }
+        /* xor */ {
+          const explicit_b_func expected = f_explicit ^ g_explicit;
+          const explicit_b_func actual = _dd_to_boolean_func.at(f ^ g);
+          assert(actual == expected);
+        }
+        /* equiv */ {
+          const explicit_b_func expected =
+              ~(f_explicit ^ g_explicit) & func_mask;
+          const explicit_b_func actual = _dd_to_boolean_func.at(f.equiv(g));
+          assert(actual == expected);
+        }
+        /* nand */ {
+          const explicit_b_func expected =
+              ~(f_explicit & g_explicit) & func_mask;
+          const explicit_b_func actual = _dd_to_boolean_func.at(f.nand(g));
+          assert(actual == expected);
+        }
+        /* nor */ {
+          const explicit_b_func expected =
+              ~(f_explicit | g_explicit) & func_mask;
+          const explicit_b_func actual = _dd_to_boolean_func.at(f.nor(g));
+          assert(actual == expected);
+        }
+        /* implication */ {
+          const explicit_b_func expected =
+              (~f_explicit | g_explicit) & func_mask;
+          const explicit_b_func actual = _dd_to_boolean_func.at(f.imp(g));
+          assert(actual == expected);
+        }
+        /* strict implication */ {
+          const explicit_b_func expected = ~f_explicit & g_explicit;
+          const explicit_b_func actual =
+              _dd_to_boolean_func.at(f.imp_strict(g));
+          assert(actual == expected);
+        }
+
+        // arity >= 3
+        for (explicit_b_func h_explicit = 0; h_explicit < num_functions;
+             ++h_explicit) {
+          const typename M::function &h = _boolean_functions[h_explicit];
+
+          /* ite */ {
+            const explicit_b_func expected =
+                (f_explicit & g_explicit) | (~f_explicit & h_explicit);
+            const explicit_b_func actual = _dd_to_boolean_func.at(f.ite(g, h));
+            assert(actual == expected);
+          }
+        }
+      }
+    }
+  }
+
+  /// Test quantification operations on all Boolean function with the given
+  /// variable set
+  void quant()
+    requires(boolean_function_quant<typename M::function>)
+  {
+    const unsigned nvars = _vars.size();
+    const unsigned num_assignments = 1 << nvars;
+    const explicit_b_func num_functions = 1 << num_assignments;
+    const explicit_b_func func_mask = num_functions - 1;
+
+    // Example for 3 vars: [0b01010101, 0b00110011, 0b00001111]
+    std::vector<explicit_b_func> var_functions;
+    var_functions.reserve(nvars);
+    for (unsigned i = 0; i < nvars; ++i) {
+      explicit_b_func f = 0;
+      for (unsigned assignment = 0; assignment < num_assignments; ++assignment)
+        f |= ((explicit_b_func)((assignment >> i) & 1)) << assignment;
+      var_functions.push_back(f);
+    }
+
+    // TODO: restrict (once we have it in the C/C++ API)
+
+    // quantification
+    std::vector<explicit_b_func> assignment_to_mask(num_assignments);
+    for (unsigned var_set = 0; var_set < num_assignments; ++var_set) {
+      typename M::function dd_var_set = _mgr.t();
+      for (unsigned i = 0; i < nvars; ++i) {
+        if (var_set & (1 << i))
+          dd_var_set &= _vars[i];
+      }
+
+      // precompute `assignment_to_mask`
+      for (unsigned assignment = 0; assignment < num_assignments;
+           ++assignment) {
+        explicit_b_func mask = func_mask;
+        for (unsigned i = 0; i < nvars; ++i) {
+          if ((var_set >> i) & 1)
+            continue;
+          const explicit_b_func f = var_functions[i];
+          mask &= (assignment >> i) & 1 ? f : ~f;
+        }
+        assignment_to_mask[assignment] = mask;
+      }
+
+      for (explicit_b_func f_explicit = 0; f_explicit < num_functions;
+           ++f_explicit) {
+        const typename M::function &f = _boolean_functions[f_explicit];
+
+        explicit_b_func exist_expected = 0, forall_expected = 0,
+                        unique_expected = 0;
+        for (unsigned assignment = 0; assignment < num_assignments;
+             ++assignment) {
+          const explicit_b_func mask = assignment_to_mask[assignment];
+
+          // or of all bits under mask
+          const explicit_b_func exist_bit = (f_explicit & mask) != 0;
+          // and of all bits under mask
+          const explicit_b_func forall_bit = (f_explicit & mask) == mask;
+          // xor of all bits under mask
+          const explicit_b_func unique_bit =
+              std::popcount(f_explicit & mask) & 1;
+
+          exist_expected |= exist_bit << assignment;
+          forall_expected |= forall_bit << assignment;
+          unique_expected |= unique_bit << assignment;
+        }
+
+        const explicit_b_func exist_actual =
+            _dd_to_boolean_func.at(f.exist(dd_var_set));
+        assert(exist_actual == exist_expected);
+
+        const explicit_b_func forall_actual =
+            _dd_to_boolean_func.at(f.forall(dd_var_set));
+        assert(forall_actual == forall_expected);
+
+        const explicit_b_func unique_actual =
+            _dd_to_boolean_func.at(f.unique(dd_var_set));
+        assert(unique_actual == unique_expected);
+      }
+    }
+  }
+};
+
+void bdd_all_boolean_functions_2vars_t1() {
+  bdd_manager mgr(65536, 1024, 1);
+  bdd_function vars[] = {mgr.new_var(), mgr.new_var()};
+  test_all_boolean_functions test(mgr, vars, vars);
+  test.basic();
+  test.quant();
+}
+
+void bcdd_all_boolean_functions_2vars_t1() {
+  bcdd_manager mgr(65536, 1024, 1);
+  bcdd_function vars[] = {mgr.new_var(), mgr.new_var()};
+  test_all_boolean_functions test(mgr, vars, vars);
+  test.basic();
+  test.quant();
+}
+
+void zbdd_all_boolean_functions_2vars_t1() {
+  zbdd_manager mgr(65536, 1024, 1);
+  zbdd_function singletons[] = {mgr.new_singleton(), mgr.new_singleton()};
+  zbdd_function vars[] = {singletons[0].var_boolean_function(),
+                          singletons[1].var_boolean_function()};
+  test_all_boolean_functions test(mgr, vars, singletons);
+  test.basic();
+}
 
 int main() {
   static_assert(boolean_function_manager<bdd_manager>);
   static_assert(boolean_function_manager<bcdd_manager>);
   static_assert(boolean_function_manager<zbdd_manager>);
 
-  static_assert(boolean_function<bdd_function>);
-  static_assert(boolean_function<bcdd_function>);
+  static_assert(boolean_function_quant<bdd_function>);
+  static_assert(boolean_function_quant<bcdd_function>);
   static_assert(boolean_function<zbdd_function>);
 
-  // TODO
+  bdd_all_boolean_functions_2vars_t1();
+  bcdd_all_boolean_functions_2vars_t1();
+  zbdd_all_boolean_functions_2vars_t1();
 }

crates/oxidd-ffi/src/zbdd.rs

@@ -229,6 +229,28 @@ pub unsafe extern "C" fn oxidd_zbdd_new_singleton(manager: oxidd_zbdd_manager_t)
         .with_manager_exclusive(|manager| ZBDDFunction::new_singleton(manager).into())
 }
 
+/// Get the ZBDD Boolean function v for the singleton set {v}
+///
+/// `var` must be a singleton set.
+///
+/// Locking behavior: acquires a shared manager lock.
+///
+/// @param  singleton  The singleton set {v}
+///
+/// @returns  The ZBDD Boolean function v
+#[no_mangle]
+pub unsafe extern "C" fn oxidd_zbdd_var_boolean_function(singleton: oxidd_zbdd_t) -> oxidd_zbdd_t {
+    let res = singleton.get().and_then(|singleton| {
+        singleton.with_manager_shared(|manager, edge| {
+            Ok(ZBDDFunction::from_edge(
+                manager,
+                oxidd::zbdd::var_boolean_function(manager, edge)?,
+            ))
+        })
+    });
+    res.into()
+}
+
 /// Create a new ZBDD node at the level of `var` with the given `hi` and `lo`
 /// edges
 ///
@@ -238,7 +260,7 @@ pub unsafe extern "C" fn oxidd_zbdd_new_singleton(manager: oxidd_zbdd_manager_t)
 ///
 /// Locking behavior: acquires a shared manager lock.
 ///
-/// @returns  The ZBDD set referencing the new node.
+/// @returns  The ZBDD set referencing the new node
 #[no_mangle]
 pub unsafe extern "C" fn oxidd_zbdd_make_node(
     var: oxidd_zbdd_t,