zdd.h

#ifndef ADIAR_ZDD_ZDD_H
#define ADIAR_ZDD_ZDD_H
 
#include <string_view>
 
#include <adiar/internal/cut.h>
#include <adiar/internal/dd.h>
 
namespace adiar
{
  // Class declarations to be able to reference it
  class zdd;
 
  class __zdd : public internal::__dd
  {
  public:
    __zdd();
 
    __zdd(const shared_node_file_type& f);
 
    __zdd(const shared_arc_file_type& f, const exec_policy& ep);
 
    __zdd(const zdd& zdd);
 
    // NOTE:
    //   '__dd' class includes 'max_1level_cut' and 'max_2level_cut' operations. This does not take
    //   the potential extra 'false' arc into account.
    //
    //   For now, we do not care to add this, since we are not using `__zdd` in a context where it
    //   is necessary such as 'zdd_union'.
 
    explicit operator bool() &&;
  };
 
  class zdd : public internal::dd
  {
    // Friends
    // |- classes
    friend __zdd;
 
    // |- functions
    friend size_t
    zdd_nodecount(const zdd&);
    friend label_type
    zdd_varcount(const zdd&);
 
    friend bool
    zdd_subseteq(const exec_policy& ep, const zdd&, const zdd&);
    friend bool
    zdd_disjoint(const exec_policy& ep, const zdd&, const zdd&);
 
  public:
    static constexpr std::string_view false_print = "Ø";
 
    static constexpr std::string_view true_print = "{Ø}";
 
    // Constructors
  public:
    zdd();
 
    zdd(terminal_type t);
 
    zdd(const shared_node_file_type& A, bool negate = false, signed_label_type shift = 0);
 
    zdd(const zdd& oA);
 
    zdd(zdd&& A);
 
    zdd(__zdd&& A);
 
    // Accessors overwrite
  public:
    internal::cut::size_type
    max_1level_cut(const internal::cut ct) const
    {
      return add_false_cofactor(ct, this->_file->max_1level_cut);
    }
 
    internal::cut::size_type
    max_2level_cut(const internal::cut ct) const
    {
      return add_false_cofactor(ct, this->_file->max_2level_cut);
    }
 
 
  private:
    internal::cut::size_type
    add_false_cofactor(const internal::cut ct, const internal::cuts_t& ilevel_cuts) const
    {
      const internal::safe_size_t cut_size = ilevel_cuts[ct];
 
      // Bit-mask (allowing implicit conversion to size_t with bit-operators) to get the cut-type
      // WITHOUT the false arcs.
      constexpr size_t bit_mask         = internal::cut::Internal_True;
      const internal::cut ct_excl_false = static_cast<internal::cut>(ct & bit_mask);
 
      // In product construction algorithms we need to take into account the (single) suppressed
      // false arc, which may suddenly become visible (e.g. 'zdd_union'). Here, the DAG gets stuck
      // inside of a copy of only one of the input ZDDs. To get there, one followed an arc of the
      // input but afterwards one pairs with an invisible false arc that spans all levels.
      //
      // We do not need to account for this invisible false arc in the following two cases
      //
      // - If the requested cut does not include false arcs.
      //
      // - If the cut size is strictly larger than the corresponding cut excluding false. In this
      //   case, we already have a false arc to pair with.
      const size_t add_suppressed = !ct.includes(false) && cut_size == ilevel_cuts[ct_excl_false];
 
      return internal::to_size(cut_size + add_suppressed);
    }
 
 
    // Operator overloading for use in conditionals
  public:
 
    explicit operator bool() const;
 
    // Assignment operator overloadings
  public:
    zdd&
    operator=(const zdd& other);
 
    zdd&
    operator=(__zdd&& other);
 
    zdd&
    operator&=(const zdd& other);
 
    zdd&
    operator&=(zdd&& other);
 
    zdd&
    operator*=(const zdd& other);
 
    zdd&
    operator*=(zdd&& other);
 
    zdd&
    operator|=(const zdd& other);
 
    zdd&
    operator|=(zdd&& other);
 
    zdd&
    operator+=(const zdd& other);
 
    zdd&
    operator+=(zdd&& other);
 
    zdd&
    operator-=(const zdd& other);
 
    zdd&
    operator-=(zdd&& other);
  };
}
 
#endif // ADIAR_ZDD_ZDD_H