Add 'bdd_isvar', 'bdd_isithvar', and 'bdd_isnithvar' predicates

As requested by Anna Blume Jakobsen

makefile

@@ -90,6 +90,9 @@ test/adiar/bdd/evaluate:
 test/adiar/bdd/if_then_else:
 	make $(MAKE_FLAGS) test TEST_FOLDER=test/adiar/bdd TEST_NAME=if_then_else
 
+test/adiar/bdd/pred:
+	make $(MAKE_FLAGS) test TEST_FOLDER=test/adiar/bdd TEST_NAME=pred
+
 test/adiar/bdd/negate:
 	make $(MAKE_FLAGS) test TEST_FOLDER=test/adiar/bdd TEST_NAME=negate
 

src/adiar/bdd.h

@@ -915,6 +915,27 @@ namespace adiar
   //////////////////////////////////////////////////////////////////////////////
   bool bdd_istrue(const bdd& f);
 
+  //////////////////////////////////////////////////////////////////////////////
+  /// \brief Whether a BDD is a function dependent on a single variable.
+  ///
+  /// \see bdd_isithvar bdd_isnithvar
+  //////////////////////////////////////////////////////////////////////////////
+  bool bdd_isvar(const bdd& f);
+
+  //////////////////////////////////////////////////////////////////////////////
+  /// \brief Whether a BDD is the function of a single positive variable.
+  ///
+  /// \see bdd_isvar bdd_ithvar
+  //////////////////////////////////////////////////////////////////////////////
+  bool bdd_isithvar(const bdd& f);
+
+  //////////////////////////////////////////////////////////////////////////////
+  /// \brief Whether a BDD is the function of a single negative variable.
+  ///
+  /// \see bdd_isvar bdd_nithvar
+  //////////////////////////////////////////////////////////////////////////////
+  bool bdd_isnithvar(const bdd& f);
+
   //////////////////////////////////////////////////////////////////////////////
   /// \brief Whether the two BDDs represent the same function.
   //////////////////////////////////////////////////////////////////////////////

src/adiar/bdd/pred.cpp

@@ -1,5 +1,7 @@
 #include <adiar/bdd.h>
 
+#include <adiar/internal/io/node_stream.h>
+
 #include <adiar/internal/algorithms/pred.h>
 
 namespace adiar
@@ -29,6 +31,35 @@ namespace adiar
     return internal::dd_istrue(f);
   }
 
+  bool bdd_isvar(const bdd& f)
+  {
+    // Assuming the BDD is fully reduced (which it should be), then it can only
+    // be a single variable, if there are exactly two arcs to terminals.
+    return f.number_of_terminals() == 2u;
+  }
+
+  bool bdd_isithvar(const bdd& f)
+  {
+    if (!bdd_isvar(f)) { return false; }
+
+    internal::node_stream<> ns(f);
+    const bdd::node_type root = ns.pull();
+
+    return root.low()  == bdd::node_type::pointer_type(false)
+        && root.high() == bdd::node_type::pointer_type(true);
+  }
+
+  bool bdd_isnithvar(const bdd& f)
+  {
+    if (!bdd_isvar(f)) { return false; }
+
+    internal::node_stream<> ns(f);
+    const bdd::node_type root = ns.pull();
+
+    return root.low()  == bdd::node_type::pointer_type(true)
+        && root.high() == bdd::node_type::pointer_type(false);
+  }
+
   bool bdd_equal(const exec_policy &ep, const bdd &f, const bdd &g)
   {
     return internal::is_isomorphic(ep, f, g);

test/adiar/bdd/CMakeLists.txt

@@ -4,6 +4,7 @@ add_test(adiar-bdd-build        test_build.cpp)
 add_test(adiar-bdd-count        test_count.cpp)
 add_test(adiar-bdd-evaluate     test_evaluate.cpp)
 add_test(adiar-bdd-if_then_else test_if_then_else.cpp)
+add_test(adiar-bdd-pred         test_pred.cpp)
 add_test(adiar-bdd-negate       test_negate.cpp)
 add_test(adiar-bdd-quantify     test_quantify.cpp)
 add_test(adiar-bdd-restrict     test_restrict.cpp)

test/adiar/bdd/test_pred.cpp

@@ -0,0 +1,204 @@
+#include "../../test.h"
+
+go_bandit([]() {
+  describe("adiar/bdd/pred.cpp", []() {
+    shared_levelized_file<bdd::node_type> bdd_T;
+    /*
+    //           T
+    */
+
+    { // Garbage collect writer to free write-lock
+      node_writer nw(bdd_T);
+      nw << node(true);
+    }
+
+    shared_levelized_file<bdd::node_type> bdd_F;
+    /*
+    //           F
+    */
+
+    { // Garbage collect writer to free write-lock
+      node_writer nw(bdd_F);
+      nw << node(false);
+    }
+
+    const ptr_uint64 terminal_T(true);
+    const ptr_uint64 terminal_F(false);
+
+    shared_levelized_file<bdd::node_type> bdd_x0;
+    /*
+    //         1      ---- x0
+    //        / \
+    //        F T
+    */
+
+    { // Garbage collect writer to free write-lock
+      node_writer nw(bdd_x0);
+      nw << node(0, node::max_id, terminal_F, terminal_T);
+    }
+
+    shared_levelized_file<bdd::node_type> bdd_not_x0;
+    /*
+    //         1      ---- x0
+    //        / \
+    //        T F
+    */
+
+    { // Garbage collect writer to free write-lock
+      node_writer nw(bdd_not_x0);
+      nw << node(0, node::max_id, terminal_T, terminal_F);
+    }
+
+    shared_levelized_file<bdd::node_type> bdd_x1;
+    /*
+    //         1      ---- x1
+    //        / \
+    //        F T
+    */
+
+    { // Garbage collect writer to free write-lock
+      node_writer nw(bdd_x1);
+      nw << node(1, node::max_id, terminal_F, terminal_T);
+    }
+
+    shared_levelized_file<bdd::node_type> bdd_0and2;
+    /*
+    //         1      ---- x0
+    //        / \
+    //        F 2     ---- x2
+    //         / \
+    //         F T
+    */
+
+    { // Garbage collect writer to free write-lock
+      node_writer nw(bdd_0and2);
+
+      nw << node(2, node::max_id, terminal_F, terminal_T)
+         << node(0, node::max_id, terminal_F, ptr_uint64(2, ptr_uint64::max_id));
+    }
+
+    // -------------------------------------------------------------------------
+    // NOTE: For the overloads from <adiar/internal/dd_func.h>, please look in
+    //       'test/adiar/internal/test_dd_func.cpp'.
+    //
+    // NOTE: For `bdd_equal` and `bdd_unequal` look at
+    //       'test/adiar/internal/algorithms/test_pred.cpp'
+    //
+    // TODO: Move BDD variants over here?
+    // -------------------------------------------------------------------------
+
+    describe("bdd_isvar", [&]() {
+      it("rejects F terminal", [&]() {
+        AssertThat(bdd_isvar(bdd_F), Is().False());
+      });
+
+      it("rejects T terminal", [&]() {
+        AssertThat(bdd_isvar(bdd_T), Is().False());
+      });
+
+      it("accepts  x0 [file content]", [&]() {
+        AssertThat(bdd_isvar(bdd_x0), Is().True());
+      });
+
+      it("accepts  x0 [complement flag]", [&]() {
+        AssertThat(bdd_isvar(bdd(bdd_not_x0, true)), Is().True());
+      });
+
+      it("accepts ~x0 [file content]", [&]() {
+        AssertThat(bdd_isvar(bdd_not_x0), Is().True());
+      });
+
+      it("accepts ~x0 [complement flag]", [&]() {
+        AssertThat(bdd_isvar(bdd(bdd_x0, true)), Is().True());
+      });
+
+      it("accepts  x1 [file content]", [&]() {
+        AssertThat(bdd_isvar(bdd_x1), Is().True());
+      });
+
+      it("accepts ~x1 [complement flag]", [&]() {
+        AssertThat(bdd_isvar(bdd(bdd_x1, true)), Is().True());
+      });
+
+      it("rejects x0 & x2", [&]() {
+        AssertThat(bdd_isvar(bdd_0and2), Is().False());
+      });
+    });
+
+    describe("bdd_isithvar", [&]() {
+      it("rejects F terminal", [&]() {
+        AssertThat(bdd_isithvar(bdd_F), Is().False());
+      });
+
+      it("rejects T terminal", [&]() {
+        AssertThat(bdd_isithvar(bdd_T), Is().False());
+      });
+
+      it("accepts  x0 [file content]", [&]() {
+        AssertThat(bdd_isithvar(bdd_x0), Is().True());
+      });
+
+      it("accepts  x0 [complement flag]", [&]() {
+        AssertThat(bdd_isithvar(bdd(bdd_not_x0, true)), Is().True());
+      });
+
+      it("rejects ~x0 [file content]", [&]() {
+        AssertThat(bdd_isithvar(bdd_not_x0), Is().False());
+      });
+
+      it("rejects ~x0 [complement flag]", [&]() {
+        AssertThat(bdd_isithvar(bdd(bdd_x0, true)), Is().False());
+      });
+
+      it("accepts  x1 [file content]", [&]() {
+        AssertThat(bdd_isithvar(bdd_x1), Is().True());
+      });
+
+      it("rejects ~x1 [complement flag]", [&]() {
+        AssertThat(bdd_isithvar(bdd(bdd_x1, true)), Is().False());
+      });
+
+      it("rejects x0 & x2", [&]() {
+        AssertThat(bdd_isithvar(bdd_0and2), Is().False());
+      });
+    });
+
+    describe("bdd_isnithvar", [&]() {
+      it("rejects F terminal", [&]() {
+        AssertThat(bdd_isnithvar(bdd_F), Is().False());
+      });
+
+      it("rejects T terminal", [&]() {
+        AssertThat(bdd_isnithvar(bdd_T), Is().False());
+      });
+
+      it("rejects  x0 [file content]", [&]() {
+        AssertThat(bdd_isnithvar(bdd_x0), Is().False());
+      });
+
+      it("rejects  x0 [complement flag]", [&]() {
+        AssertThat(bdd_isnithvar(bdd(bdd_not_x0, true)), Is().False());
+      });
+
+      it("accepts ~x0 [file content]", [&]() {
+        AssertThat(bdd_isnithvar(bdd_not_x0), Is().True());
+      });
+
+      it("accepts ~x0 [complement flag]", [&]() {
+        AssertThat(bdd_isnithvar(bdd(bdd_x0, true)), Is().True());
+      });
+
+      it("rejects  x1 [file content]", [&]() {
+        AssertThat(bdd_isnithvar(bdd_x1), Is().False());
+      });
+
+      it("accepts ~x1 [complement flag]", [&]() {
+        AssertThat(bdd_isnithvar(bdd(bdd_x1, true)), Is().True());
+      });
+
+      it("rejects x0 & x2", [&]() {
+        AssertThat(bdd_isnithvar(bdd_0and2), Is().False());
+      });
+    });
+  });
+ });

test/test.cpp

@@ -95,6 +95,7 @@ go_bandit([]() {
 #include "adiar/bdd/test_count.cpp"
 #include "adiar/bdd/test_evaluate.cpp"
 #include "adiar/bdd/test_if_then_else.cpp"
+#include "adiar/bdd/test_pred.cpp"
 #include "adiar/bdd/test_negate.cpp"
 #include "adiar/bdd/test_quantify.cpp"
 #include "adiar/bdd/test_restrict.cpp"