diff --git a/src/adiar/bdd.h b/src/adiar/bdd.h
index 8d1ae737e..48caeef29 100644
--- a/src/adiar/bdd.h
+++ b/src/adiar/bdd.h
@@ -401,6 +401,21 @@ namespace adiar
   operator&(__bdd&&, __bdd&&);
   /// \endcond
 
+  //////////////////////////////////////////////////////////////////////////////////////////////////
+  /// \see bdd_and
+  //////////////////////////////////////////////////////////////////////////////////////////////////
+  __bdd
+  operator*(const bdd& lhs, const bdd& rhs);
+
+  /// \cond
+  __bdd
+  operator*(const bdd&, __bdd&&);
+  __bdd
+  operator*(__bdd&&, const bdd&);
+  __bdd
+  operator*(__bdd&&, __bdd&&);
+  /// \endcond
+
   //////////////////////////////////////////////////////////////////////////////////////////////////
   /// \brief Logical 'nand' operator.
   ///
@@ -448,6 +463,33 @@ namespace adiar
   operator|(__bdd&&, __bdd&&);
   /// \endcond
 
+  //////////////////////////////////////////////////////////////////////////////////////////////////
+  /// \see bdd_or
+  //////////////////////////////////////////////////////////////////////////////////////////////////
+  bdd
+  operator+(const bdd& f);
+
+  //////////////////////////////////////////////////////////////////////////////////////////////////
+  /// \see bdd_or
+  //////////////////////////////////////////////////////////////////////////////////////////////////
+  __bdd
+  operator+(__bdd&& f);
+
+  //////////////////////////////////////////////////////////////////////////////////////////////////
+  /// \see bdd_or
+  //////////////////////////////////////////////////////////////////////////////////////////////////
+  __bdd
+  operator+(const bdd& lhs, const bdd& rhs);
+
+  /// \cond
+  __bdd
+  operator+(const bdd&, __bdd&&);
+  __bdd
+  operator+(__bdd&&, const bdd&);
+  __bdd
+  operator+(__bdd&&, __bdd&&);
+  /// \endcond
+
   //////////////////////////////////////////////////////////////////////////////////////////////////
   /// \brief Logical 'nor' operator.
   ///
@@ -575,6 +617,32 @@ namespace adiar
   __bdd
   bdd_diff(const exec_policy& ep, const bdd& f, const bdd& g);
 
+  //////////////////////////////////////////////////////////////////////////////////////////////////
+  /// \see bdd_diff, bdd_not
+  //////////////////////////////////////////////////////////////////////////////////////////////////
+  bdd
+  operator-(const bdd& f);
+
+  /// \cond
+  __bdd
+  operator-(__bdd&& f);
+  /// \endcond
+
+  //////////////////////////////////////////////////////////////////////////////////////////////////
+  /// \see bdd_diff
+  //////////////////////////////////////////////////////////////////////////////////////////////////
+  __bdd
+  operator-(const bdd& lhs, const bdd& rhs);
+
+  /// \cond
+  __bdd
+  operator-(const bdd&, __bdd&&);
+  __bdd
+  operator-(__bdd&&, const bdd&);
+  __bdd
+  operator-(__bdd&&, __bdd&&);
+  /// \endcond
+
   //////////////////////////////////////////////////////////////////////////////////////////////////
   /// \brief Logical 'less than' operator.
   ///
diff --git a/src/adiar/bdd/bdd.cpp b/src/adiar/bdd/bdd.cpp
index 41b471b90..47e1d2cc4 100644
--- a/src/adiar/bdd/bdd.cpp
+++ b/src/adiar/bdd/bdd.cpp
@@ -11,7 +11,7 @@
 
 namespace adiar
 {
-  //////////////////////////////////////////////////////////////////////////////
+  //////////////////////////////////////////////////////////////////////////////////////////////////
   // '__bdd' Constructors
   __bdd::__bdd() = default;
 
@@ -27,7 +27,7 @@ namespace adiar
     : internal::__dd(dd)
   {}
 
-  //////////////////////////////////////////////////////////////////////////////
+  //////////////////////////////////////////////////////////////////////////////////////////////////
   // 'bdd' Constructors
   bdd::bdd(bool t)
     : bdd(bdd_terminal(t))
@@ -53,15 +53,9 @@ namespace adiar
     : internal::dd(internal::reduce<bdd_policy>(std::move(f)))
   {}
 
-  //////////////////////////////////////////////////////////////////////////////
+  //////////////////////////////////////////////////////////////////////////////////////////////////
   // Operators
-  bdd
-  operator~(__bdd&& in)
-  {
-    return ~bdd(std::move(in));
-  }
-
-#define __bdd_oper(out_t, op)                          \
+#define __BDD_OPER(out_t, op)                          \
   out_t operator op(__bdd&& lhs, __bdd&& rhs)          \
   {                                                    \
     return bdd(std::move(lhs)) op bdd(std::move(rhs)); \
@@ -77,10 +71,11 @@ namespace adiar
     return bdd(std::move(lhs)) op rhs;                 \
   }
 
-  __bdd_oper(__bdd, &) __bdd_oper(__bdd, |) __bdd_oper(__bdd, ^) __bdd_oper(bool, ==)
-    __bdd_oper(bool, !=)
+  //////////////////////////////////////////////////////////////////////////////
+  // Operators (Assignment)
 
-      bdd& bdd::operator=(const bdd & other)
+  bdd&
+  bdd::operator=(const bdd& other)
   {
     this->negate = other.negate;
     this->file   = other.file;
@@ -94,6 +89,54 @@ namespace adiar
     return (*this = internal::reduce<bdd_policy>(std::move(other)));
   }
 
+  //////////////////////////////////////////////////////////////////////////////
+  // Operators (Relational)
+
+  __BDD_OPER(bool, ==);
+
+  bool
+  operator==(const bdd& lhs, const bdd& rhs)
+  {
+    return bdd_equal(lhs, rhs);
+  }
+
+  __BDD_OPER(bool, !=);
+
+  bool
+  operator!=(const bdd& lhs, const bdd& rhs)
+  {
+    return bdd_unequal(lhs, rhs);
+  }
+
+  //////////////////////////////////////////////////////////////////////////////
+  // Operators (Bit)
+
+  bdd
+  operator~(const bdd& f)
+  {
+    return bdd_not(f);
+  }
+
+  bdd
+  operator~(bdd&& f)
+  {
+    return bdd_not(std::move(f));
+  }
+
+  bdd
+  operator~(__bdd&& in)
+  {
+    return ~bdd(std::move(in));
+  }
+
+  __BDD_OPER(__bdd, &);
+
+  __bdd
+  operator&(const bdd& lhs, const bdd& rhs)
+  {
+    return bdd_and(lhs, rhs);
+  }
+
   bdd&
   bdd::operator&=(const bdd& other)
   {
@@ -108,6 +151,14 @@ namespace adiar
     return (*this = std::move(temp));
   }
 
+  __BDD_OPER(__bdd, |);
+
+  __bdd
+  operator|(const bdd& lhs, const bdd& rhs)
+  {
+    return bdd_or(lhs, rhs);
+  }
+
   bdd&
   bdd::operator|=(const bdd& other)
   {
@@ -122,6 +173,14 @@ namespace adiar
     return (*this = std::move(temp));
   }
 
+  __BDD_OPER(__bdd, ^);
+
+  __bdd
+  operator^(const bdd& lhs, const bdd& rhs)
+  {
+    return bdd_xor(lhs, rhs);
+  }
+
   bdd&
   bdd::operator^=(const bdd& other)
   {
@@ -136,49 +195,100 @@ namespace adiar
     return (*this = std::move(temp));
   }
 
-  bool
-  operator==(const bdd& lhs, const bdd& rhs)
+  //////////////////////////////////////////////////////////////////////////////
+  // Operators (Set/Arithmetic)
+
+  __BDD_OPER(__bdd, +);
+
+  bdd
+  operator+(const bdd& f)
   {
-    return bdd_equal(lhs, rhs);
+    return f;
   }
 
-  bool
-  operator!=(const bdd& lhs, const bdd& rhs)
+  __bdd
+  operator+(__bdd&& f)
   {
-    return bdd_unequal(lhs, rhs);
+    return f;
   }
 
-  bdd
-  operator~(const bdd& f)
+  __bdd
+  operator+(const bdd& lhs, const bdd& rhs)
   {
-    return bdd_not(f);
+    return bdd_or(lhs, rhs);
+  }
+
+  bdd&
+  bdd::operator+=(const bdd& other)
+  {
+    return (*this = bdd_or(*this, other));
+  }
+
+  bdd&
+  bdd::operator+=(bdd&& other)
+  {
+    __bdd temp = bdd_or(*this, other);
+    other.deref();
+    return (*this = std::move(temp));
   }
 
+  __BDD_OPER(__bdd, -);
+
   bdd
-  operator~(bdd&& f)
+  operator-(const bdd& f)
   {
-    return bdd_not(std::forward<bdd>(f));
+    return bdd_not(f);
   }
 
   __bdd
-  operator&(const bdd& lhs, const bdd& rhs)
+  operator-(__bdd&& f)
   {
-    return bdd_and(lhs, rhs);
+    return bdd_not(std::move(f));
   }
 
   __bdd
-  operator|(const bdd& lhs, const bdd& rhs)
+  operator-(const bdd& lhs, const bdd& rhs)
   {
-    return bdd_or(lhs, rhs);
+    return bdd_diff(lhs, rhs);
+  }
+
+  bdd&
+  bdd::operator-=(const bdd& other)
+  {
+    return (*this = bdd_diff(*this, other));
+  }
+
+  bdd&
+  bdd::operator-=(bdd&& other)
+  {
+    __bdd temp = bdd_diff(*this, other);
+    other.deref();
+    return (*this = std::move(temp));
   }
 
+  __BDD_OPER(__bdd, *);
+
   __bdd
-  operator^(const bdd& lhs, const bdd& rhs)
+  operator*(const bdd& lhs, const bdd& rhs)
   {
-    return bdd_xor(lhs, rhs);
+    return bdd_and(lhs, rhs);
   }
 
-  //////////////////////////////////////////////////////////////////////////////
+  bdd&
+  bdd::operator*=(const bdd& other)
+  {
+    return (*this = bdd_and(*this, other));
+  }
+
+  bdd&
+  bdd::operator*=(bdd&& other)
+  {
+    __bdd temp = bdd_and(*this, other);
+    other.deref();
+    return (*this = std::move(temp));
+  }
+
+  //////////////////////////////////////////////////////////////////////////////////////////////////
   // Input variables
   bdd::label_type
   bdd_topvar(const bdd& f)
diff --git a/src/adiar/bdd/bdd.h b/src/adiar/bdd/bdd.h
index a6893b62f..a57b36b3c 100644
--- a/src/adiar/bdd/bdd.h
+++ b/src/adiar/bdd/bdd.h
@@ -183,6 +183,39 @@ namespace adiar
     bdd&
     operator^=(bdd&& other);
     /// \endcond
+
+    ////////////////////////////////////////////////////////////////////////////////////////////////
+    /// \see bdd_or
+    ////////////////////////////////////////////////////////////////////////////////////////////////
+    bdd&
+    operator+=(const bdd& other);
+
+    /// \cond
+    bdd&
+    operator+=(bdd&& other);
+    /// \endcond
+
+    ////////////////////////////////////////////////////////////////////////////////////////////////
+    /// \see bdd_diff
+    ////////////////////////////////////////////////////////////////////////////////////////////////
+    bdd&
+    operator-=(const bdd& other);
+
+    /// \cond
+    bdd&
+    operator-=(bdd&& other);
+    /// \endcond
+
+    ////////////////////////////////////////////////////////////////////////////////////////////////
+    /// \see bdd_and
+    ////////////////////////////////////////////////////////////////////////////////////////////////
+    bdd&
+    operator*=(const bdd& other);
+
+    /// \cond
+    bdd&
+    operator*=(bdd&& other);
+    /// \endcond
   };
 }
 
diff --git a/src/adiar/zdd.h b/src/adiar/zdd.h
index 920d1cc06..139a9c69a 100644
--- a/src/adiar/zdd.h
+++ b/src/adiar/zdd.h
@@ -473,6 +473,29 @@ namespace adiar
   operator|(__zdd&&, const zdd&);
   /// \endcond
 
+  //////////////////////////////////////////////////////////////////////////////////////////////////
+  /// \see zdd_union
+  //////////////////////////////////////////////////////////////////////////////////////////////////
+  zdd
+  operator+(const zdd& A);
+
+  /// \cond
+  __zdd
+  operator+(__zdd&& A);
+  /// \endcond
+
+  __zdd
+  operator+(const zdd& lhs, const zdd& rhs);
+
+  /// \cond
+  __zdd
+  operator+(__zdd&&, __zdd&&);
+  __zdd
+  operator+(const zdd&, __zdd&&);
+  __zdd
+  operator+(__zdd&&, const zdd&);
+  /// \endcond
+
   //////////////////////////////////////////////////////////////////////////////////////////////////
   /// \brief   The intersection of two families of sets.
   ///
@@ -499,7 +522,22 @@ namespace adiar
   __zdd
   operator&(const zdd&, __zdd&&);
   __zdd
-  operator&(__zdd&&, const __zdd&);
+  operator&(__zdd&&, const zdd&);
+  /// \endcond
+
+  //////////////////////////////////////////////////////////////////////////////////////////////////
+  /// \see zdd_intsec
+  //////////////////////////////////////////////////////////////////////////////////////////////////
+  __zdd
+  operator*(const zdd& lhs, const zdd& rhs);
+
+  /// \cond
+  __zdd
+  operator*(__zdd&&, __zdd&&);
+  __zdd
+  operator*(const zdd&, __zdd&&);
+  __zdd
+  operator*(__zdd&&, const zdd&);
   /// \endcond
 
   //////////////////////////////////////////////////////////////////////////////////////////////////
@@ -516,6 +554,17 @@ namespace adiar
   __zdd
   zdd_diff(const exec_policy& ep, const zdd& A, const zdd& B);
 
+  //////////////////////////////////////////////////////////////////////////////////////////////////
+  /// \see zdd_diff, zdd_complement
+  //////////////////////////////////////////////////////////////////////////////////////////////////
+  __zdd
+  operator-(const zdd& A);
+
+  /// \cond
+  __zdd
+  operator-(__zdd&& A);
+  /// \endcond
+
   //////////////////////////////////////////////////////////////////////////////////////////////////
   /// \see zdd_diff
   //////////////////////////////////////////////////////////////////////////////////////////////////
diff --git a/src/adiar/zdd/zdd.cpp b/src/adiar/zdd/zdd.cpp
index 6062d7d01..bab9075e0 100644
--- a/src/adiar/zdd/zdd.cpp
+++ b/src/adiar/zdd/zdd.cpp
@@ -17,7 +17,7 @@
 
 namespace adiar
 {
-  //////////////////////////////////////////////////////////////////////////////
+  //////////////////////////////////////////////////////////////////////////////////////////////////
   // '__zdd' Constructors
   __zdd::__zdd()
     : internal::__dd()
@@ -35,7 +35,7 @@ namespace adiar
     : internal::__dd(dd)
   {}
 
-  //////////////////////////////////////////////////////////////////////////////
+  //////////////////////////////////////////////////////////////////////////////////////////////////
   // 'zdd' Constructors
   zdd::zdd()
     : zdd(zdd_empty())
@@ -63,9 +63,9 @@ namespace adiar
     : internal::dd(internal::reduce<zdd_policy>(std::move(A)))
   {}
 
-  //////////////////////////////////////////////////////////////////////////////
+  //////////////////////////////////////////////////////////////////////////////////////////////////
   // Operators
-#define __zdd_oper(out_t, op)                          \
+#define __ZDD_OPER(out_t, op)                          \
   out_t operator op(__zdd&& lhs, __zdd&& rhs)          \
   {                                                    \
     return zdd(std::move(lhs)) op zdd(std::move(rhs)); \
@@ -81,12 +81,11 @@ namespace adiar
     return zdd(std::move(lhs)) op rhs;                 \
   }
 
-  __zdd_oper(__zdd, &) __zdd_oper(__zdd, |) __zdd_oper(__zdd, -)
-
-    __zdd_oper(bool, ==) __zdd_oper(bool, !=) __zdd_oper(bool, <=) __zdd_oper(bool, >=)
-      __zdd_oper(bool, <) __zdd_oper(bool, >)
+  //////////////////////////////////////////////////////////////////////////////
+  // Operators (Assignment)
 
-        zdd& zdd::operator=(const zdd & other)
+  zdd&
+  zdd::operator=(const zdd& other)
   {
     this->negate = other.negate;
     this->file   = other.file;
@@ -100,6 +99,60 @@ namespace adiar
     return (*this = internal::reduce<zdd_policy>(std::move(other)));
   }
 
+  //////////////////////////////////////////////////////////////////////////////
+  // Operators (Relational)
+
+  __ZDD_OPER(bool, ==);
+
+  bool
+  operator==(const zdd& lhs, const zdd& rhs)
+  {
+    return zdd_equal(lhs, rhs);
+  }
+
+  __ZDD_OPER(bool, !=);
+
+  bool
+  operator!=(const zdd& lhs, const zdd& rhs)
+  {
+    return zdd_unequal(lhs, rhs);
+  }
+
+  __ZDD_OPER(bool, <=);
+
+  bool
+  operator<=(const zdd& lhs, const zdd& rhs)
+  {
+    return zdd_subseteq(lhs, rhs);
+  }
+
+  __ZDD_OPER(bool, >=);
+
+  bool
+  operator>=(const zdd& lhs, const zdd& rhs)
+  {
+    return zdd_subseteq(rhs, lhs);
+  }
+
+  __ZDD_OPER(bool, <);
+
+  bool
+  operator<(const zdd& lhs, const zdd& rhs)
+  {
+    return zdd_subset(lhs, rhs);
+  }
+
+  __ZDD_OPER(bool, >);
+
+  bool
+  operator>(const zdd& lhs, const zdd& rhs)
+  {
+    return zdd_subset(rhs, lhs);
+  }
+
+  //////////////////////////////////////////////////////////////////////////////
+  // Operators (Bit)
+
   __zdd
   operator~(const zdd& A)
   {
@@ -112,6 +165,8 @@ namespace adiar
     return ~zdd(std::move(A));
   }
 
+  __ZDD_OPER(__zdd, &);
+
   __zdd
   operator&(const zdd& lhs, const zdd& rhs)
   {
@@ -132,6 +187,8 @@ namespace adiar
     return (*this = std::move(temp));
   }
 
+  __ZDD_OPER(__zdd, |);
+
   __zdd
   operator|(const zdd& lhs, const zdd& rhs)
   {
@@ -152,6 +209,23 @@ namespace adiar
     return (*this = std::move(temp));
   }
 
+  //////////////////////////////////////////////////////////////////////////////
+  // Operators (Set/Arithmetic)
+
+  __ZDD_OPER(__zdd, -);
+
+  __zdd
+  operator-(const zdd& A)
+  {
+    return zdd_complement(A);
+  }
+
+  __zdd
+  operator-(__zdd&& A)
+  {
+    return -zdd(std::move(A));
+  }
+
   __zdd
   operator-(const zdd& lhs, const zdd& rhs)
   {
@@ -172,43 +246,63 @@ namespace adiar
     return (*this = std::move(temp));
   }
 
-  bool
-  operator==(const zdd& lhs, const zdd& rhs)
+  __ZDD_OPER(__zdd, +);
+
+  zdd
+  operator+(const zdd& A)
   {
-    return zdd_equal(lhs, rhs);
+    return A;
   }
 
-  bool
-  operator!=(const zdd& lhs, const zdd& rhs)
+  __zdd
+  operator+(__zdd&& A)
   {
-    return zdd_unequal(lhs, rhs);
+    return A;
   }
 
-  bool
-  operator<=(const zdd& lhs, const zdd& rhs)
+  __zdd
+  operator+(const zdd& lhs, const zdd& rhs)
   {
-    return zdd_subseteq(lhs, rhs);
+    return zdd_union(lhs, rhs);
   }
 
-  bool
-  operator>=(const zdd& lhs, const zdd& rhs)
+  zdd&
+  zdd::operator+=(const zdd& other)
   {
-    return zdd_subseteq(rhs, lhs);
+    return (*this = zdd_union(*this, other));
   }
 
-  bool
-  operator<(const zdd& lhs, const zdd& rhs)
+  zdd&
+  zdd::operator+=(zdd&& other)
   {
-    return zdd_subset(lhs, rhs);
+    __zdd temp = zdd_union(*this, other);
+    other.deref();
+    return (*this = std::move(temp));
   }
 
-  bool
-  operator>(const zdd& lhs, const zdd& rhs)
+  __ZDD_OPER(__zdd, *);
+
+  __zdd
+  operator*(const zdd& lhs, const zdd& rhs)
   {
-    return zdd_subset(rhs, lhs);
+    return zdd_intsec(lhs, rhs);
   }
 
-  //////////////////////////////////////////////////////////////////////////////
+  zdd&
+  zdd::operator*=(const zdd& other)
+  {
+    return (*this = zdd_intsec(*this, other));
+  }
+
+  zdd&
+  zdd::operator*=(zdd&& other)
+  {
+    __zdd temp = zdd_intsec(*this, other);
+    other.deref();
+    return (*this = std::move(temp));
+  }
+
+  //////////////////////////////////////////////////////////////////////////////////////////////////
   // Input variables
   zdd::label_type
   zdd_topvar(const zdd& A)
diff --git a/src/adiar/zdd/zdd.h b/src/adiar/zdd/zdd.h
index 3fd9ed43d..7907eae4d 100644
--- a/src/adiar/zdd/zdd.h
+++ b/src/adiar/zdd/zdd.h
@@ -227,6 +227,17 @@ namespace adiar
     operator&=(zdd&& other);
     /// \endcond
 
+    ////////////////////////////////////////////////////////////////////////////////////////////////
+    /// \see zdd_union
+    ////////////////////////////////////////////////////////////////////////////////////////////////
+    zdd&
+    operator*=(const zdd& other);
+
+    /// \cond
+    zdd&
+    operator*=(zdd&& other);
+    /// \endcond
+
     ////////////////////////////////////////////////////////////////////////////////////////////////
     /// \see zdd_union
     ////////////////////////////////////////////////////////////////////////////////////////////////
@@ -238,6 +249,17 @@ namespace adiar
     operator|=(zdd&& other);
     /// \endcond
 
+    ////////////////////////////////////////////////////////////////////////////////////////////////
+    /// \see zdd_union
+    ////////////////////////////////////////////////////////////////////////////////////////////////
+    zdd&
+    operator+=(const zdd& other);
+
+    /// \cond
+    zdd&
+    operator+=(zdd&& other);
+    /// \endcond
+
     ////////////////////////////////////////////////////////////////////////////////////////////////
     /// \see zdd_diff
     ////////////////////////////////////////////////////////////////////////////////////////////////
diff --git a/test/adiar/bdd/test_bdd.cpp b/test/adiar/bdd/test_bdd.cpp
index 51fbbc8bf..fa205cce5 100644
--- a/test/adiar/bdd/test_bdd.cpp
+++ b/test/adiar/bdd/test_bdd.cpp
@@ -5,8 +5,8 @@ go_bandit([]() {
     shared_levelized_file<bdd::node_type> x0_nf;
 
     {
-      node_writer nw_0(x0_nf);
-      nw_0 << node(0, node::max_id, ptr_uint64(false), ptr_uint64(true));
+      node_writer nw(x0_nf);
+      nw << node(0, node::max_id, ptr_uint64(false), ptr_uint64(true));
     }
 
     bdd x0(x0_nf);
@@ -14,8 +14,8 @@ go_bandit([]() {
     shared_levelized_file<bdd::node_type> x1_nf;
 
     {
-      node_writer nw_1(x1_nf);
-      nw_1 << node(1, node::max_id, ptr_uint64(false), ptr_uint64(true));
+      node_writer nw(x1_nf);
+      nw << node(1, node::max_id, ptr_uint64(false), ptr_uint64(true));
     }
 
     bdd x1(x1_nf);
@@ -23,30 +23,26 @@ go_bandit([]() {
     shared_levelized_file<bdd::node_type> x0_and_x1_nf;
 
     {
-      node_writer nw_01(x0_and_x1_nf);
-
-      nw_01 << node(1, node::max_id, ptr_uint64(false), ptr_uint64(true));
-
-      nw_01 << node(0, node::max_id, ptr_uint64(false), ptr_uint64(1, ptr_uint64::max_id));
+      node_writer nw(x0_and_x1_nf);
+      nw << node(1, node::max_id, ptr_uint64(false), ptr_uint64(true))
+         << node(0, node::max_id, ptr_uint64(false), ptr_uint64(1, ptr_uint64::max_id));
     }
 
     bdd x0_and_x1(x0_and_x1_nf);
     bdd x0_nand_x1(x0_and_x1_nf, true);
 
     shared_levelized_file<bdd::node_type> terminal_T_nf;
-
     {
-      node_writer nw_T(terminal_T_nf);
-      nw_T << node(true);
+      node_writer nw(terminal_T_nf);
+      nw << node(true);
     }
 
     bdd terminal_T(terminal_T_nf);
 
     shared_levelized_file<bdd::node_type> terminal_F_nf;
-
     {
-      node_writer nw_F(terminal_F_nf);
-      nw_F << node(false);
+      node_writer nw(terminal_F_nf);
+      nw << node(false);
     }
 
     bdd terminal_F(terminal_F_nf);
@@ -128,97 +124,249 @@ go_bandit([]() {
          AssertThat(t2.is_negated(), Is().False());
        });
 
-    describe("operators", [&]() {
-      it("should check terminal_F != terminal_T",
-         [&]() { AssertThat(terminal_F, Is().Not().EqualTo(terminal_T)); });
+    describe("operator overloading", [&]() {
+      describe("==, !=", [&]() {
+        it("checks F != T", [&]() { AssertThat(terminal_F, Is().Not().EqualTo(terminal_T)); });
 
-      it("should check terminal_F != ~terminal_F",
-         [&]() { AssertThat(terminal_F, Is().Not().EqualTo(~terminal_F)); });
+        it("checks F != ~F", [&]() { AssertThat(terminal_F, Is().Not().EqualTo(~terminal_F)); });
 
-      it("should check terminal_F == ~terminal_T",
-         [&]() { AssertThat(terminal_F, Is().EqualTo(~terminal_T)); });
+        it("checks F != (x0 & x1)",
+           [&]() { AssertThat(terminal_F, Is().Not().EqualTo(x0_and_x1)); });
 
-      it("should check ~(x0 & x1) != (x0 & x1)",
-         [&]() { AssertThat(x0_and_x1, Is().Not().EqualTo(x0_nand_x1)); });
+        it("checks (x0 & x1) != T",
+           [&]() { AssertThat(x0_and_x1, Is().Not().EqualTo(terminal_T)); });
 
-      shared_levelized_file<bdd::node_type> x0_and_x1_nf2;
+        it("checks '(x0 & x1) != ~(x0 & x1)'",
+           [&]() { AssertThat(x0_and_x1, Is().Not().EqualTo(x0_nand_x1)); });
 
-      {
-        node_writer nw_01(x0_and_x1_nf2);
-
-        nw_01 << node(1, node::max_id, ptr_uint64(false), ptr_uint64(true));
-
-        nw_01 << node(0, node::max_id, ptr_uint64(false), ptr_uint64(1, ptr_uint64::max_id));
-      }
+        it("checks (x0 & x1) matches itself",
+           [&]() { AssertThat(x0_and_x1, Is().EqualTo(x0_and_x1)); });
 
-      it("should check (x0 & x1) == (x0 & x1)", [&]() {
-        bdd other(x0_and_x1_nf2);
-        AssertThat(x0_and_x1, Is().EqualTo(other));
+        it("checks (x0 & x1) matches a copy", [&]() {
+          shared_levelized_file<bdd::node_type> other_nf;
+          {
+            node_writer nw(other_nf);
+            nw << node(1, node::max_id, ptr_uint64(false), ptr_uint64(true))
+               << node(0, node::max_id, ptr_uint64(false), ptr_uint64(1, ptr_uint64::max_id));
+          }
+          const bdd other(other_nf);
+          AssertThat(x0_and_x1, Is().EqualTo(other));
+        });
       });
 
-      it("should compute x0 & x1", [&]() { AssertThat(x0_and_x1 == (x0 & x1), Is().True()); });
-
-      it("should compute bdd& in x0 ?= x1", [&]() {
-        bdd out1 = x0;
-        out1 &= x1;
-        AssertThat(out1 == (x0 & x1), Is().True());
-        AssertThat(out1 != (x0 & x1), Is().False());
-
-        bdd out2 = x0;
-        out2 |= x1;
-        AssertThat(out2 == (x0 | x1), Is().True());
-        AssertThat(out2 != (x0 | x1), Is().False());
-        AssertThat(out2 != (x0 & x1), Is().True());
-
-        bdd out3 = x0;
-        out3 ^= x1;
-        AssertThat(out3 == (x0 ^ x1), Is().True());
-        AssertThat(out3 != (x0 ^ x1), Is().False());
-        AssertThat(out3 != (x0 | x1), Is().True());
+      describe("~, &, |, ^", [&]() {
+        it("negates 'T' into 'F'", [&]() { AssertThat(terminal_F, Is().EqualTo(~terminal_T)); });
+
+        it("negates '(x0 & x1)' into ~(x0 & x1)'",
+           [&]() { AssertThat(~x0_and_x1, Is().EqualTo(x0_nand_x1)); });
+
+        it("negates '~(x0 & x1)' into '(x0 & x1)'",
+           [&]() { AssertThat(~x0_and_x1, Is().EqualTo(x0_nand_x1)); });
+
+        it("computes 'x0 & x1'", [&]() {
+          const bdd f = x0 & x1;
+          AssertThat(f, Is().EqualTo(x0_and_x1));
+        });
+
+        it("computes '~(~x0 | ~x1)'", [&]() {
+          const bdd f = ~(~x0 | ~x1);
+          AssertThat(f, Is().EqualTo(x0_and_x1));
+        });
+
+        it("computes 'x0 ^ x1' to be '(~x0 & x1) | (x0 & ~x1)'", [&]() {
+          const bdd f = x0 ^ x1;
+
+          const bdd g1 = ~x0 & x1;
+          const bdd g2 = x0 & ~x1;
+          const bdd g  = g1 | g2;
+
+          AssertThat(f, Is().EqualTo(g));
+        });
+
+        it("negates 'x0 & x1' __bdd&& into '~(x0 & x1)", [&]() {
+          AssertThat(x0_nand_x1 == ~(x0 & x1), Is().True());
+          AssertThat(x0_nand_x1 != ~(x0 & x1), Is().False());
+        });
+
+        it("resolves 'x0 ^ x1' to be '(~x0 & x1) | (x0 & ~x1)'", [&]() {
+          const bdd f = x0 ^ x1;
+          const bdd g = (~x0 & x1) | (x0 & ~x1);
+          AssertThat(f, Is().EqualTo(g));
+        });
+
+        it("accumulates with '&=(bdd&)' operator", [&]() {
+          bdd f = x0;
+          AssertThat(f == x0, Is().True());
+
+          f &= x1;
+          AssertThat(f == (x0 & x1), Is().True());
+
+          f &= terminal_F;
+          AssertThat(f == terminal_F, Is().True());
+        });
+
+        it("accumulates with '&=(__bdd&&)' operator", [&]() {
+          bdd f = terminal_T;
+          f &= x0 & x1;
+          AssertThat((x0 & x1) == f, Is().True());
+        });
+
+        it("accumulates with '|=(bdd&)' operator", [&]() {
+          bdd f = x0;
+          AssertThat(f == x0, Is().True());
+
+          f |= x1;
+          AssertThat(f == (x0 | x1), Is().True());
+
+          f |= terminal_T;
+          AssertThat(terminal_T == f, Is().True());
+        });
+
+        it("accumulates with '|=(__bdd&&)' operator", [&]() {
+          bdd f = terminal_F;
+          f |= x0 & x1;
+          AssertThat(f == (x0 & x1), Is().True());
+        });
+
+        it("accumulates with '^=(bdd&)' operator", [&]() {
+          bdd f = x0;
+          AssertThat(f == x0, Is().True());
+
+          f ^= x1;
+          AssertThat(f == (x0 ^ x1), Is().True());
+
+          f ^= x0;
+          AssertThat(f == x1, Is().True());
+        });
+
+        it("accumulates with '^=(__bdd&&)' operator", [&]() {
+          bdd f = terminal_T;
+          f ^= x0 & x1;
+          AssertThat(~(x0 & x1) == f, Is().True());
+        });
+
+        it("computes with __bdd&& operators [1]", [&]() {
+          const bdd f = ((x0 & ~x1) | (~x0 & x1)) ^ ((x1 ^ x0) & (~x0 & x1));
+          AssertThat(f == (x0 & ~x1), Is().True());
+          AssertThat((x0 & ~x1) == f, Is().True());
+        });
+
+        it("computes with __bdd&& operators [2]", [&]() {
+          const bdd f = ((x0 & ~x1) | (~x0 & x1)) ^ ((x1 ^ x0) & (~x0 & x1));
+          AssertThat(f == (x0 & ~x1), Is().True());
+          AssertThat((x0 & ~x1) == f, Is().True());
+        });
+
+        it("computes with __bdd&& and bdd& operators [1]", [&]() {
+          // Notice, that the two expressions with terminal_T and terminal_F
+          // shortcut with the operator for a bdd with the negation flag
+          // set correctly.
+          const bdd f = ((x0 & x1) | (~x0 & x1)) ^ ((terminal_T ^ x0) & (terminal_F | x1));
+          AssertThat(f == (x0 & x1), Is().True());
+          AssertThat((x0 & x1) == f, Is().True());
+        });
+
+        it("computes with __bdd&& and bdd& operators [2]", [&]() {
+          // The right-hand-side will evaluate to a bdd, since terminal_T negates.
+          const bdd f = ((~x0 | (x0 & x1)) ^ (terminal_T ^ (x1 ^ x0)));
+          AssertThat(f == (~x0 & x1), Is().True());
+          AssertThat((~x0 & x1) == f, Is().True());
+        });
       });
 
-      it("should negate __bdd&& in ~(x0 & x1)", [&]() {
-        AssertThat(x0_nand_x1 == ~(x0 & x1), Is().True());
-        AssertThat(x0_nand_x1 != ~(x0 & x1), Is().False());
-      });
-
-      it("should compute with __bdd&& operators", [&]() {
-        bdd out = ((x0 & ~x1) | (~x0 & x1)) ^ ((x1 ^ x0) & (~x0 & x1));
-        AssertThat((x0 & ~x1) == out, Is().True());
-        AssertThat((x0 & ~x1) != out, Is().False());
-      });
+      describe("==, !=", [&]() {
+        it("check two derivations of same __bdd&& [==]",
+           [&]() { AssertThat((x0 ^ x1) == ((x0 & ~x1) | (~x0 & x1)), Is().True()); });
 
-      it("should compute with __bdd&& and bdd& in operators [1]", [&]() {
-        // Notice, that the two expressions with terminal_T and terminal_F
-        // shortcut with the operator for a bdd with the negation flag
-        // set correctly.
-        bdd out = ((x0 & x1) | (~x0 & x1)) ^ ((terminal_T ^ x0) & (terminal_F | x1));
-        AssertThat((x0 & x1) == out, Is().True());
-        AssertThat((x0 & x1) != out, Is().False());
-      });
+        it("check two derivations of same __bdd&& [!=]",
+           [&]() { AssertThat((x0 ^ x1) != ((x0 & ~x1) | (~x0 & x1)), Is().False()); });
 
-      it("should compute with __bdd&& and bdd& in operators [2]", [&]() {
-        // The right-hand-side will evaluate to a bdd, since terminal_F negates.
-        bdd out = ((~x0 | (x0 & x1)) ^ (terminal_T ^ (x1 ^ x0)));
-        AssertThat((~x0 & x1) == out, Is().True());
-        AssertThat((~x0 & x1) != out, Is().False());
-      });
-
-      it("should x0 ?= __bdd&&", [&]() {
-        bdd out = x0;
-        out &= x0 & x1;
-        AssertThat((x0 & x1) == out, Is().True());
-        AssertThat((x0 & x1) != out, Is().False());
-      });
+        it("checks two derivations of different __bdd&& [==]",
+           [&]() { AssertThat((x0 | x1) == ((x0 & x1) | (~x0 & x1)), Is().False()); });
 
-      it("should check two derivations of same __bdd&&", [&]() {
-        AssertThat((x0 ^ x1) == ((x0 & ~x1) | (~x0 & x1)), Is().True());
-        AssertThat((x0 ^ x1) != ((x0 & ~x1) | (~x0 & x1)), Is().False());
+        it("checks two derivations of different __bdd&& [!=]",
+           [&]() { AssertThat((x0 | x1) != ((x0 & x1) | (~x0 & x1)), Is().True()); });
       });
 
-      it("should check two derivations of different __bdd&&", [&]() {
-        AssertThat((x0 | x1) == ((x0 & x1) | (~x0 & x1)), Is().False());
-        AssertThat((x0 | x1) != ((x0 & x1) | (~x0 & x1)), Is().True());
+      describe("-", [&]() {
+        it("does nothing with '+(bdd&)' [x0]", [&]() { AssertThat(+x0 == x0, Is().True()); });
+
+        it("does nothing with '+(__bdd&) [x0 & x1]",
+           [&]() { AssertThat(+(x0 & x1) == x0_and_x1, Is().True()); });
+
+        it("computes 'x0 + x1'", [&]() {
+          const bdd f = x0 + x1;
+          AssertThat(f == (x0 | x1), Is().True());
+        });
+
+        it("accumulates with '+=(bdd&)' operator", [&]() {
+          bdd f = x0;
+          f += x1;
+          AssertThat(f == (x0 | x1), Is().True());
+
+          f += terminal_T;
+          AssertThat(f == terminal_T, Is().True());
+        });
+
+        it("accumulates with '+=(__bdd&&)' operator", [&]() {
+          bdd f = terminal_F;
+          f += x0 & x1;
+          AssertThat(f == (x0 & x1), Is().True());
+        });
+
+        it("computes 'x0 + x1'", [&]() {
+          const bdd f = x0 * x1;
+          AssertThat(f == (x0 & x1), Is().True());
+        });
+
+        it("accumulates with '+=(bdd&)' operator", [&]() {
+          bdd f = x0;
+          f *= x1;
+          AssertThat(f == (x0 & x1), Is().True());
+
+          f *= terminal_F;
+          AssertThat(f == terminal_F, Is().True());
+        });
+
+        it("accumulates with '+=(__bdd&&)' operator", [&]() {
+          bdd f = terminal_T;
+          f *= x0 & x1;
+          AssertThat(f == (x0 & x1), Is().True());
+        });
+
+        it("negates with '-(bdd&)' [x0]", [&]() { AssertThat(-x0 == ~x0, Is().True()); });
+
+        it("negates with '-(bdd&)' [x0 & x1]",
+           [&]() { AssertThat(-x0_and_x1 == ~x0_and_x1, Is().True()); });
+
+        it("negates with '-(__bdd&) [x0 & x1]",
+           [&]() { AssertThat(-(x0 & x1) == ~x0_and_x1, Is().True()); });
+
+        it("computes 'x0 - x1'", [&]() {
+          const bdd f = x0 - x1;
+          AssertThat(f == (x0 & ~x1), Is().True());
+        });
+
+        it("accumulates with '-=(bdd&)' operator", [&]() {
+          bdd f = x0;
+          f -= x1;
+          AssertThat(f == (x0 & ~x1), Is().True());
+
+          f -= x0;
+          AssertThat(f == terminal_F, Is().True());
+        });
+
+        it("accumulates with '-=(__bdd&&)' operator", [&]() {
+          bdd f = terminal_T;
+          f -= x0 & x1;
+          AssertThat(f == ~(x0 & x1), Is().True());
+        });
+
+        it("computes with '-(__bdd&&)' and '-(bdd&)' operators", [&]() {
+          const bdd f = x0_and_x1 - x0 - x1;
+          AssertThat(f == terminal_F, Is().True());
+          AssertThat(terminal_F == f, Is().True());
+        });
       });
     });
   });
diff --git a/test/adiar/zdd/test_zdd.cpp b/test/adiar/zdd/test_zdd.cpp
index 9934867a2..06b7bb25e 100644
--- a/test/adiar/zdd/test_zdd.cpp
+++ b/test/adiar/zdd/test_zdd.cpp
@@ -46,14 +46,14 @@ go_bandit([]() {
     zdd terminal_F(terminal_F_nf);
 
     describe("__zdd class", [&]() {
-      it("should copy-construct values from zdd", [&]() {
+      it("copy-constructs values from zdd", [&]() {
         __zdd t1 = x0_or_x1;
         AssertThat(t1.has<shared_levelized_file<zdd::node_type>>(), Is().True());
         AssertThat(t1.get<shared_levelized_file<zdd::node_type>>(), Is().EqualTo(x0_or_x1_nf));
         AssertThat(t1.negate, Is().False());
       });
 
-      it("should copy-construct values from __zdd", [&]() {
+      it("copy-constructs values from __zdd", [&]() {
         __zdd t1 = x0_or_x1;
         __zdd t2 = t1;
         AssertThat(t2.has<shared_levelized_file<zdd::node_type>>(), Is().True());
@@ -61,7 +61,7 @@ go_bandit([]() {
         AssertThat(t2.negate, Is().False());
       });
 
-      it("should copy-construct values from shared_levelized_file<zdd::node_type>", [&]() {
+      it("copy-constructs values from shared_levelized_file<zdd::node_type>", [&]() {
         __zdd t1 = x0_or_x1;
         AssertThat(t1.has<shared_levelized_file<zdd::node_type>>(), Is().True());
         AssertThat(t1.get<shared_levelized_file<zdd::node_type>>(), Is().EqualTo(x0_or_x1_nf));
@@ -84,7 +84,7 @@ go_bandit([]() {
 
       af->max_1level_cut = 1;
 
-      it("should copy-construct values from __zdd::shared_arc_file_type", [&]() {
+      it("copy-constructs values from __zdd::shared_arc_file_type", [&]() {
         __zdd t1 = __zdd(af, exec_policy::access::Random_Access);
         AssertThat(t1.has<__zdd::shared_arc_file_type>(), Is().True());
         AssertThat(t1.get<__zdd::shared_arc_file_type>(), Is().EqualTo(af));
@@ -92,96 +92,292 @@ go_bandit([]() {
         AssertThat(t1._policy, Is().EqualTo(exec_policy(exec_policy::access::Random_Access)));
       });
 
-      it("should reduce on copy construct to zdd with __zdd::shared_arc_file_type", [&]() {
+      it("reduces on copy construct to zdd with __zdd::shared_arc_file_type", [&]() {
         zdd out = __zdd(af, exec_policy());
         AssertThat(out, Is().EqualTo(x0_or_x1));
       });
     });
 
     describe("operators", [&]() {
-      it("should reject Ø == {Ø}",
-         [&]() { AssertThat(terminal_F, Is().Not().EqualTo(terminal_T)); });
+      describe("==, !=", [&]() {
+        it("rejects Ø == {Ø}", [&]() { AssertThat(terminal_F, Is().Not().EqualTo(terminal_T)); });
 
-      it("should accept {{0}} == {{0}} (different files)", [&]() {
-        shared_levelized_file<zdd::node_type> x0_nf_2;
+        it("accepts {{0}} == {{0}} (different files)", [&]() {
+          shared_levelized_file<zdd::node_type> other_nf;
+          {
+            node_writer nw(other_nf);
+            nw << node(0, node::max_id, ptr_uint64(false), ptr_uint64(true));
+          }
+          zdd other(other_nf);
 
-        {
-          node_writer nw_0(x0_nf_2);
-          nw_0 << node(0, node::max_id, ptr_uint64(false), ptr_uint64(true));
-        }
+          AssertThat(x0, Is().EqualTo(other));
+        });
 
-        zdd x0_2(x0_nf);
+        it("rejects {{0}} == {{1}}", [&]() { AssertThat(x0, Is().Not().EqualTo(x1)); });
 
-        AssertThat(x0, Is().EqualTo(x0_2));
+        it("rejects {{0}, {1}} == {{0}}", [&]() { AssertThat(x0_or_x1, Is().Not().EqualTo(x0)); });
       });
 
-      it("should compute {{0}} /\\ {{1}} == {{0}, {1}}",
-         [&]() { AssertThat((x0 | x1) == x0_or_x1, Is().True()); });
+      describe("~, &, |", [&]() {
+        it("computes ~{{0},{1}} == {Ø,{0,1}} with {0,1} domain", [&]() {
+          const std::vector<int> dom = { 0, 1 };
+          domain_set(dom.begin(), dom.end());
+
+          shared_levelized_file<zdd::node_type> expected;
+          {
+            node_writer nw(expected);
+            nw << node(1, node::max_id, ptr_uint64(false), ptr_uint64(true))
+               << node(0, node::max_id, ptr_uint64(true), ptr_uint64(1, ptr_uint64::max_id));
+          }
+          AssertThat(~x0_or_x1 == zdd(expected), Is().True());
+        });
+
+        it("computes {{0}} | {{1}} == {{0}, {1}}",
+           [&]() { AssertThat((x0 | x1) == x0_or_x1, Is().True()); });
+
+        it("accumulates with '|=(zdd&)' operator", [&]() {
+          zdd A = terminal_F;
+          A |= x0;
+          AssertThat(A, Is().EqualTo(x0));
+
+          A |= x1;
+          AssertThat(A, Is().EqualTo(x0_or_x1));
+        });
+
+        it("computes with __zdd&& operators [|]", [&]() {
+          const zdd A = (x0_or_x1 | (x0 | x1)) | x0;
+          AssertThat(A, Is().EqualTo(x0_or_x1));
+        });
+
+        it("computes {{0}} & {{0},{1}} == {{0}}",
+           [&]() { AssertThat((x0 & x0_or_x1) == x0, Is().True()); });
+
+        it("accumulates with '&=(zdd&)' operator", [&]() {
+          zdd A = x0_or_x1;
+          A &= x0;
+          AssertThat(A, Is().EqualTo(x0));
+
+          A &= x1;
+          AssertThat(A, Is().EqualTo(terminal_F));
+        });
+
+        it("computes with __zdd&& operators [&]", [&]() {
+          const zdd A = (x0 & (x0_or_x1 & x0)) & x1;
+          AssertThat(A, Is().EqualTo(terminal_F));
+        });
+
+        it("accumulates with '|=(__zdd&&)' and '&=(__zdd&&)'", [&]() {
+          zdd A = x0;
+
+          A |= x0_or_x1 & x1;
+          AssertThat(A, Is().EqualTo(x0_or_x1));
+
+          A &= x0_or_x1 & x1;
+          AssertThat(A, Is().EqualTo(x1));
+        });
+
+        it("computes with __zdd&& operators [|,&]", [&]() {
+          const zdd A = ((x0_or_x1 | x0) | ((x0 & x1) | x1)) & x0;
+          AssertThat(A, Is().EqualTo(x0));
+        });
+
+        it("computes with __zdd&& operators [~]", [&]() {
+          const std::vector<int> dom = { 0, 1 };
+          domain_set(dom.begin(), dom.end());
+
+          const zdd A = ~(x0 | x1);
+          AssertThat(~x0_or_x1 == A, Is().True());
+        });
+      });
 
-      it("should compute {{0}} \\/ {{0},{1}} == {{0}}",
-         [&]() { AssertThat((x0 & x0_or_x1) == x0, Is().True()); });
+      describe("-, +, *", [&]() {
+        it("computes -{{0},{1}} == {Ø,{0,1}} [zdd&] with {0,1} domain", [&]() {
+          const std::vector<int> dom = { 0, 1 };
+          domain_set(dom.begin(), dom.end());
 
-      it("should compute {{0},{1}} \\ {{0}} == {{1}}",
-         [&]() { AssertThat((x0_or_x1 - x0) == x1, Is().True()); });
+          shared_levelized_file<zdd::node_type> expected;
+          {
+            node_writer nw(expected);
+            nw << node(1, node::max_id, ptr_uint64(false), ptr_uint64(true))
+               << node(0, node::max_id, ptr_uint64(true), ptr_uint64(1, ptr_uint64::max_id));
+          }
+          AssertThat(-x0_or_x1 == zdd(expected), Is().True());
+        });
 
-      it("should compute {{0},{1}}' == {Ø,{0,1}} with dom {0,1}", [&]() {
-        shared_file<zdd::label_type> dom;
-        {
-          label_writer lw(dom);
-          lw << 0 << 1;
-        }
+        it("computes -{{0},{1}} == {Ø,{0,1}} [__zdd&&] with {0,1} domain", [&]() {
+          const std::vector<int> dom = { 0, 1 };
+          domain_set(dom.begin(), dom.end());
 
-        domain_set(dom);
+          shared_levelized_file<zdd::node_type> expected;
+          {
+            node_writer nw(expected);
+            nw << node(1, node::max_id, ptr_uint64(false), ptr_uint64(true))
+               << node(0, node::max_id, ptr_uint64(true), ptr_uint64(1, ptr_uint64::max_id));
+          }
+          AssertThat(-(x0 | x1) == zdd(expected), Is().True());
+        });
+
+        it("computes {{0},{1}} - {{0}} == {{1}}",
+           [&]() { AssertThat((x0_or_x1 - x0) == x1, Is().True()); });
+
+        it("accumulates with '-=(zdd&)'", [&]() {
+          zdd A = x0_or_x1;
+
+          A -= x0;
+          AssertThat(A == x1, Is().True());
+
+          A -= x1;
+          AssertThat(A == terminal_F, Is().True());
+        });
+
+        it("accumulates with '-=(__zdd&&)'", [&]() {
+          zdd A = x0_or_x1;
+
+          A -= x0 | x1;
+          AssertThat(A == terminal_F, Is().True());
+        });
+
+        it("computes +{{0}} == {{0}} [zdd&]", [&]() { AssertThat(+x0 == x0, Is().True()); });
+
+        it("computes +{{0}} == {{0}} [__zdd&&]",
+           [&]() { AssertThat(+(x0 & x0_or_x1) == x0, Is().True()); });
+
+        it("computes {{0}} + {{1}} == {{0}, {1}}",
+           [&]() { AssertThat((x0 + x1) == x0_or_x1, Is().True()); });
+
+        it("accumulates with '+=(zdd&)' operator", [&]() {
+          zdd A = terminal_F;
+          A += x0;
+          AssertThat(A, Is().EqualTo(x0));
+
+          A += x1;
+          AssertThat(A, Is().EqualTo(x0_or_x1));
+        });
+
+        it("computes with __zdd&& operators [+]", [&]() {
+          const zdd A = (x0_or_x1 + (x0 + x1)) + x0;
+          AssertThat(A, Is().EqualTo(x0_or_x1));
+        });
+
+        it("computes {{0}} * {{0},{1}} == {{0}}",
+           [&]() { AssertThat((x0 * x0_or_x1) == x0, Is().True()); });
+
+        it("accumulates with '*=(zdd&)' operator", [&]() {
+          zdd A = x0_or_x1;
+          A *= x0;
+          AssertThat(A, Is().EqualTo(x0));
+
+          A *= x1;
+          AssertThat(A, Is().EqualTo(terminal_F));
+        });
+
+        it("computes with __zdd&& operators [*]", [&]() {
+          const zdd A = (x0 * (x0_or_x1 & x0)) & x1;
+          AssertThat(A, Is().EqualTo(terminal_F));
+        });
+
+        it("accumulates with '+=(__zdd&&)' and '*=(__zdd&&)'", [&]() {
+          zdd A = x0;
+
+          A += x0_or_x1 & x1;
+          AssertThat(A, Is().EqualTo(x0_or_x1));
+
+          A *= x0_or_x1 & x1;
+          AssertThat(A, Is().EqualTo(x1));
+        });
+
+        it("computes with __zdd&& operators [+,*]", [&]() {
+          const zdd A = ((x0_or_x1 + x0) + ((x0 * x1) + x1)) * x0;
+          AssertThat(A, Is().EqualTo(x0));
+        });
+
+        it("computes with __zdd&& operators [-]", [&]() {
+          const std::vector<int> dom = { 0, 1 };
+          domain_set(dom.begin(), dom.end());
+
+          const zdd A = -(x0 | x1);
+          AssertThat(-x0_or_x1 == A, Is().True());
+        });
+
+        it("computes with __zdd&& operators [|,-,]", [&]() {
+          const std::vector<int> dom = { 0, 1 };
+          domain_set(dom.begin(), dom.end());
 
-        shared_levelized_file<zdd::node_type> expected;
-        {
-          node_writer nw(expected);
-          nw << node(1, node::max_id, ptr_uint64(false), ptr_uint64(true))
-             << node(0, node::max_id, ptr_uint64(true), ptr_uint64(1, ptr_uint64::max_id));
-        }
+          const zdd out      = -(-(x0 | x1) - terminal_T);
+          const zdd expected = x0 | x1 | terminal_T;
+          AssertThat(expected, Is().EqualTo(out));
+        });
 
-        AssertThat(~x0_or_x1 == zdd(expected), Is().True());
+        it("computes with __zdd&& operators [-,+,*]", [&]() {
+          const zdd A = ((x0_or_x1 - x0) + ((x0 + x1) * (x0_or_x1 + x1))) - (x0_or_x1 - x0);
+          AssertThat(x0, Is().EqualTo(A));
+        });
       });
 
-      it("should compute with __zdd&& operators [|,&,-]", [&]() {
-        zdd out = ((x0_or_x1 - x0) | ((x0 | x1) & (x0_or_x1 - x1))) - (x0_or_x1 - x0);
-        AssertThat(x0, Is().EqualTo(out));
-      });
+      describe("==, !=", [&]() {
+        it("checks two derivations of same __bdd&& [==]",
+           [&]() { AssertThat((x0 | x1) == ((x0_or_x1 - x1) | x1), Is().True()); });
 
-      it("should compute with __zdd&& operators [|,~,-,]", [&]() {
-        shared_file<zdd::label_type> dom;
-        {
-          label_writer lw(dom);
-          lw << 0 << 1;
-        }
+        it("checks two derivations of same __bdd&& [!=]",
+           [&]() { AssertThat((x0 | x1) != ((x0_or_x1 - x1) | x1), Is().False()); });
 
-        domain_set(dom);
+        it("checks two derivations of different __bdd&& [==]",
+           [&]() { AssertThat((x0 | x1) == (x0_or_x1 - x1), Is().False()); });
 
-        zdd out      = ~(~(x0 | x1) - terminal_T);
-        zdd expected = x0 | x1 | terminal_T;
-        AssertThat(expected, Is().EqualTo(out));
+        it("checks two derivations of different __bdd&& [!=]",
+           [&]() { AssertThat((x0 | x1) != (x0_or_x1 - x1), Is().True()); });
       });
 
-      it("should ?= __zdd&&", [&]() {
-        zdd out = x0_or_x1;
-        out -= x0_or_x1 & x1;
-        AssertThat(out, Is().EqualTo(x0));
+      describe("<, <=, >, >=", [&]() {
+        it("checks {{0}} < {{0}, {1}}", [&]() {
+          AssertThat(x0 < x0_or_x1, Is().True());
+          AssertThat(x0 < (x0 | x1), Is().True());
+        });
 
-        out |= x0_or_x1 & x1;
-        AssertThat(out, Is().EqualTo(x0_or_x1));
+        it("checks {{0}} < {{1}}", [&]() { AssertThat(x0 < x1, Is().False()); });
 
-        out &= x0_or_x1 & x1;
-        AssertThat(out, Is().EqualTo(x1));
-      });
+        it("checks {{0}, {1}} < {{0}, {1}}", [&]() {
+          AssertThat((x0 | x1) < x0_or_x1, Is().False());
+          AssertThat(x0_or_x1 < (x0 | x1), Is().False());
+          AssertThat((x0 | x1) < (x0 | x1), Is().False());
+        });
 
-      it("should check two derivations of same __bdd&&", [&]() {
-        AssertThat((x0 | x1) == ((x0_or_x1 - x1) | x1), Is().True());
-        AssertThat((x0 | x1) != ((x0_or_x1 - x1) | x1), Is().False());
-      });
+        it("checks {{0}} <= {{0}, {1}}", [&]() {
+          AssertThat(x0 <= x0_or_x1, Is().True());
+          AssertThat(x0 <= (x0 | x1), Is().True());
+        });
+
+        it("checks {{0}, {1}} <= {{0}, {1}}", [&]() {
+          AssertThat((x0 | x1) <= x0_or_x1, Is().True());
+          AssertThat((x0 | x1) <= (x0 | x1), Is().True());
+        });
+
+        it("checks {{0}} <= {{1}}", [&]() { AssertThat(x0 <= x1, Is().False()); });
+
+        it("checks {{0}, {1}} > {{0}}", [&]() { AssertThat(x0_or_x1 > x0, Is().True()); });
+
+        it("checks {{0}} > {{1}}", [&]() { AssertThat(x0 > x1, Is().False()); });
+
+        it("checks {{0}, {1}} > {{0}, {1}}", [&]() {
+          AssertThat((x0 | x1) > x0_or_x1, Is().False());
+          AssertThat(x0_or_x1 > (x0 | x1), Is().False());
+          AssertThat((x0 | x1) > (x0 | x1), Is().False());
+        });
+
+        it("checks {{0}, {1}} >= {{0}}", [&]() { AssertThat(x0_or_x1 >= x0, Is().True()); });
+
+        it("checks {{0}, {1}} >= {{0}, {1}}", [&]() {
+          AssertThat((x0 | x1) >= x0_or_x1, Is().True());
+          AssertThat(x0_or_x1 >= (x0 | x1), Is().True());
+          AssertThat((x0 | x1) >= (x0 | x1), Is().True());
+        });
 
-      it("should check two derivations of different __bdd&&", [&]() {
-        AssertThat((x0 | x1) == (x0_or_x1 - x1), Is().False());
-        AssertThat((x0 | x1) != (x0_or_x1 - x1), Is().True());
+        it("checks {{0}} >= {{1}}", [&]() {
+          AssertThat(x0 >= x1, Is().False());
+          AssertThat(x0 >= (x0_or_x1 & x1), Is().False());
+          AssertThat((x0_or_x1 & x0) >= x1, Is().False());
+          AssertThat((x0_or_x1 & x0) >= (x0_or_x1 & x1), Is().False());
+        });
       });
     });