builder.h

#ifndef ADIAR_BUILDER_H
#define ADIAR_BUILDER_H
 
#include <adiar/bdd/bdd_policy.h>
#include <adiar/exception.h>
#include <adiar/zdd/zdd_policy.h>
 
#include <adiar/internal/assert.h>
#include <adiar/internal/data_types/node.h>
#include <adiar/internal/data_types/uid.h>
#include <adiar/internal/io/node_file.h>
#include <adiar/internal/io/node_writer.h>
#include <adiar/internal/memory.h>
 
 
namespace adiar
{
 
  struct builder_shared
  {};
 
  template <typename dd_policy>
  class builder;
 
  template <typename Policy>
  class builder_ptr
  {
  public:
    friend class builder<Policy>;
 
  private:
    // TODO: rename to 'ptr ptr' when using complement edges
    /*const*/ internal::node::uid_type uid;
 
    /*const*/ shared_ptr<const builder_shared> builder_ref;
 
    /*const*/ shared_ptr<bool> unreferenced = make_shared<bool>(true);
 
  public:
    builder_ptr() = default;
 
    builder_ptr(const builder_ptr& bp) = default;
 
    builder_ptr(builder_ptr&& bp) = default;
 
  public:
    builder_ptr&
    operator=(const builder_ptr& bp) = default;
 
    builder_ptr&
    operator=(builder_ptr&& bp) = default;
 
  private:
    builder_ptr(const internal::node::uid_type& p, const shared_ptr<const builder_shared>& sp)
      : uid(p)
      , builder_ref(sp)
    {}
  };
 
  using bdd_ptr = builder_ptr<bdd_policy>;
 
  using zdd_ptr = builder_ptr<zdd_policy>;
 
  template <typename Policy>
  class builder
  {
  private:
    // See 'attach_if_needed()' for default values of most values below.
 
    using node_type = typename Policy::node_type;
 
    shared_ptr<internal::levelized_file<node_type>> nf;
 
    internal::node_writer nw;
 
    bool created_terminal;
 
    bool terminal_val;
 
    typename Policy::label_type current_label;
 
    typename Policy::id_type current_id;
 
    size_t unref_nodes;
 
    shared_ptr<builder_shared> builder_ref;
 
  public:
    builder() noexcept
    {}
 
    ~builder() noexcept
    {}
 
  public:
    builder_ptr<Policy>
    add_node(typename Policy::label_type label,
             const builder_ptr<Policy>& low,
             const builder_ptr<Policy>& high)
    {
      attach_if_needed();
 
      // Check validity of input
      if (low.builder_ref != builder_ref || high.builder_ref != builder_ref) {
        throw invalid_argument("Cannot use pointers from a different builder");
      }
      if (label > Policy::max_label) { throw invalid_argument("Nodes must have a valid label"); }
      if (label > current_label) { throw invalid_argument("Nodes must be added bottom-up"); }
      if (low.uid.is_node() && low.uid.label() <= label) {
        throw invalid_argument("Low child must point to a node with higher label");
      }
      if (high.uid.is_node() && high.uid.label() <= label) {
        throw invalid_argument("High child must point to a node with higher label");
      }
 
      // Update label and ID if necessary
      if (label < current_label) {
        current_label = label;
        current_id    = Policy::max_id;
      }
 
      // Create potential node
      const node_type n(label, current_id, low.uid, high.uid);
 
      // Check whether this node is 'redundant'
      const typename node_type::uid_type res_uid = Policy::reduction_rule(n);
 
      if (res_uid.is_terminal()) {
        created_terminal = true;
        terminal_val     = res_uid.value();
      }
 
      if (res_uid == low.uid) { return low; }
      if (res_uid == high.uid) { return high; }
 
      // Push node to file
      nw.push(n);
      unref_nodes++;
      current_id--;
 
      // Update count of unreferenced nodes
      bool& low_unref = *low.unreferenced;
      if (low_unref && !low.uid.is_terminal()) {
        low_unref = false;
        unref_nodes--;
      }
 
      bool& high_unref = *high.unreferenced;
      if (high_unref && !high.uid.is_terminal()) {
        high_unref = false;
        unref_nodes--;
      }
 
      return make_ptr(res_uid);
    }
 
    builder_ptr<Policy>
    add_node(const typename Policy::label_type label,
             const bool low,
             const builder_ptr<Policy>& high)
    {
      attach_if_needed();
 
      builder_ptr<Policy> low_ptr = make_ptr(typename node_type::pointer_type(low));
      return add_node(label, low_ptr, high);
    }
 
    builder_ptr<Policy>
    add_node(const typename Policy::label_type label,
             const builder_ptr<Policy>& low,
             const bool high)
    {
      attach_if_needed();
 
      builder_ptr<Policy> high_ptr = make_ptr(typename node_type::pointer_type(high));
      return add_node(label, low, high_ptr);
    }
 
    builder_ptr<Policy>
    add_node(const typename Policy::label_type label, const bool low, const bool high)
    {
      attach_if_needed();
 
      builder_ptr<Policy> low_ptr  = make_ptr(typename node_type::pointer_type(low));
      builder_ptr<Policy> high_ptr = make_ptr(typename node_type::pointer_type(high));
      return add_node(label, low_ptr, high_ptr);
    }
 
    builder_ptr<Policy>
    add_node(bool terminal_value)
    {
      attach_if_needed();
 
      created_terminal = true;
      terminal_val     = terminal_value;
 
      return make_ptr(typename node_type::pointer_type(terminal_value));
    }
 
    typename Policy::dd_type
    build()
    {
      attach_if_needed();
 
      if (!nw.has_pushed()) {
        if (created_terminal) {
          nw.push(node_type(terminal_val));
        } else {
          throw domain_error("There must be at least one node or terminal in the decision diagram");
        }
      }
      nw.detach();
 
      if (unref_nodes > 1) { throw domain_error("Decision diagram has more than one root"); }
 
      const typename Policy::dd_type res(nf);
      detach();
      return res;
    }
 
    void
    clear() noexcept
    {
      detach();
    }
 
  private:
    inline void
    attach_if_needed() noexcept
    {
      if (!nf) {
        adiar_assert(!nw.attached(),
                     "`nw`'s attachment should be consistent with existence of `nf`");
 
        // Initialise file
        nf = internal::make_shared_levelized_file<node_type>();
        nw.attach(nf);
 
        // Initialise state variables
        current_label    = Policy::max_label;
        current_id       = Policy::max_id;
        created_terminal = false;
        terminal_val     = false;
        unref_nodes      = 0;
 
        // Initialise shared builder reference.
        builder_ref = make_shared<builder_shared>();
      }
    }
 
    inline void
    detach() noexcept
    {
      nw.detach();
      nf.reset();
    }
 
    builder_ptr<Policy>
    make_ptr(const typename node_type::pointer_type& p) noexcept
    {
      return builder_ptr<Policy>(p, builder_ref);
    }
  };
 
  using bdd_builder = builder<bdd_policy>;
 
  using zdd_builder = builder<zdd_policy>;
 
}
 
#endif // ADIAR_BUILDER_H