// Copyright 2025 Oliver Theimer
#pragma once
#include <algorithm>
#include <cassert>
#include <climits>
#include <cmath>
#include <cstdint>
#include <cstdio>
#include <fstream>
#include <iostream>
#include <string>
#include <unordered_map>
#include <vector>

#include "./bbdd_node.hpp"
#include "./bbdd_types.hpp"
#include "./chain_variable_ordering.hpp"
#include "./computed_table.hpp"
#include "./extend_table.hpp"

// idea from CUDD package
#define SIZEOF_VOID_P 8
#define SIZEOF_INT 4
#if SIZEOF_VOID_P == 8 && SIZEOF_INT == 4
typedef uint32_t bbdd_halfword_t;
#else
typedef uint16_t bbdd_halfword_t;
#endif

#define REF(n) entries[n].ref
#define LEVEL(n) entries[n].node.cvo_lvl
#define EQ(n) entries[n].node.eq_child
#define NEQ(n) entries[n].node.neq_child
#define INDEX(n) entries[n].node.index
#define NEXT(n) entries[n].next
#define NEXT_ENTRY(n) entries[n->next]

typedef uint32_t node_index_t;

/**
 * @class variable_relation_t
 * @brief struct used to store information about a bbdd to generate its truth
 * table
 *
 */
struct variable_relation_t {
  node_index_t pv;
  node_index_t sv;
  bool eq;
};

/**
 * @class table_entry_t
 * @brief struct that stored a single entry of the hash table
 *
 */
struct table_entry_t {
  bbdd_node_t node;
  bbdd_halfword_t next;
  bbdd_halfword_t ref;
};

/**
 * @class output_map_t
 * @brief struct that maps a bbdd root node to a human readable string
 *
 */
struct output_map_t {
  std::string output;
  bbdd_node_t *bbdd;
};

class Unique_table {
  enum return_codes { SUCCESS, OUT_OF_MEMORY, TABLE_FULL };

#define NODE(n) entries[n].node
#define ENTRY(n) entries[n]

private:
  table_entry_t *entries;
  node_index_t free_pos;
  uint32_t capacity;
  std::string module_name;
  std::vector<node_index_t> free_slots;

  /**
   * @brief swap two adhacent variables in variable ordering
   *
   * @param pos_b position of the first variable
   * @param pos_c position of the second variable
   */
  void swap_variable_order(node_index_t pos_b, node_index_t pos_c) {
    assert(pos_b + 1 == pos_c);
    node_index_t temp = (*cvo)[pos_b].in;
    (*cvo)[pos_b].in = (*cvo)[pos_c].in;
    (*cvo)[pos_c].in = temp;
    (*cvo)[(*cvo)[pos_b].in % num_inputs].pos = pos_b;
    (*cvo)[(*cvo)[pos_c].in % num_inputs].pos = pos_c;
  }

  /**
   * @brief recursive helper function to count the number of nodes in bbdd
   *
   * @param node bbdd root node whose size should be evaluated
   * @return number of nodes in subgraph denoted by root node
   */
  uint32_t get_number_nodes_recursive(bbdd_node_t *node) {
    if (IS_TERM(node->index) || MARKED(node)) {
      return 0;
    }
    SET_MARKED(node);
    uint32_t neq_size = get_number_nodes_recursive(get_node_p(node->neq_child));
    uint32_t eq_size = get_number_nodes_recursive(get_node_p(node->eq_child));
    return (neq_size + eq_size) + 1;
  }

  /**
   * @brief recursive helper function to dump a bbdd into a dot file format
   *
   * @param file dot file in which the output should be written to
   * @param node root node whose subgraph should be printed into dot file format
   * @return node index used for recursive print
   */
  node_index_t recursive_dump_dot(std::ofstream &file, bbdd_node_t *node) {
    if (IS_TERM(node->index) || MARKED(node)) {
      return node->index;
    }
    if (node->cvo_lvl.sv != INT_MAX) {
      file << "\n\t" << (GET_INDEX(node)) << " [label=\"" << node->ref << ""
           << (GET_INDEX(node)) << ": " << node->cvo_lvl.pv << ","
           << node->cvo_lvl.sv << "\"]\n";
    } else {
      file << "\n\t" << (GET_INDEX(node)) << " [label=\"" << node->ref << ""
           << (GET_INDEX(node)) << ": " << node->cvo_lvl.pv << "," << 1
           << "\"]\n";
    }
    SET_MARKED(node);
    recursive_dump_dot(file, get_node_p(node->neq_child));
    recursive_dump_dot(file, get_node_p(node->eq_child));
    file << "\t" << (GET_INDEX(node)) << " -- " << node->neq_child
         << "[style=\"dashed\"]\n";
    //<< "[style=\"dashed\", label=<<FONT POINT-SIZE=\"14\">&ne;</FONT>>]\n";
    file << "\t" << (GET_INDEX(node)) << " -- " << node->eq_child << "\n";
    return (GET_INDEX(node));
  }

  /**
   * @brief return the ith bit of an integer
   *
   * @param integer integer from which the bit should be retrieved
   * @param bits number of bits in the integer
   * @param index position of bit that should be retrieved
   * @return boolean rather the bit is high (true) or low (false)
   */
  bool get_ith_bit(node_index_t integer, node_index_t bits, uint8_t index) {
    return integer & (1 << ((bits - 1) - index));
  }

  /**
   * @brief helper function that is used to collect truth table entries based on
   * a variable relation list
   *
   * @param var_rel vector of variable relation entries retrieved from
   * traversing the bbdd
   * @param inputs number of inputs to the truth table
   * @param tt vector of truth table values that should be filled by this
   * function
   * @param value that should be inserted into the truth table
   */
  void insert_tt_value(std::vector<variable_relation_t> var_rel,
                       node_index_t inputs, std::vector<bool> &tt, bool value) {
    if (!value) {
      return;
    }
    for (variable_relation_t rel : var_rel) {
#ifdef DEBUG_TABLE
      printf("%d %s %d\n", rel.pv, rel.eq ? "=" : "!=", rel.sv);
#endif
    }
    for (uint32_t i = 0; i < tt.size(); i++) {
      bool insert = true;
      for (variable_relation_t rel : var_rel) {
        if (rel.eq) {
          if (rel.sv == INT_MAX) {
            if (!get_ith_bit(i, inputs, rel.pv - 2)) {
              insert = false;
            }
          } else if (get_ith_bit(i, inputs, rel.pv - 2) !=
                     get_ith_bit(i, inputs, rel.sv - 2)) {
            insert = false;
          }
        } else {
          if (rel.sv == INT_MAX) {
            if (get_ith_bit(i, inputs, rel.pv - 2)) {
              insert = false;
            }
          } else if (get_ith_bit(i, inputs, rel.pv - 2) ==
                     get_ith_bit(i, inputs, rel.sv - 2)) {
            insert = false;
          }
        }
      }
      if (insert && value) {
#ifdef DEBUG_TABLE
        printf("INSERTED %d at : %d %d%d%d%d\n", value, i,
               get_ith_bit(i, inputs, 3), get_ith_bit(i, inputs, 2),
               get_ith_bit(i, inputs, 1), get_ith_bit(i, inputs, 0));
#endif
        tt[i] = value;
      }
    }
  }

  /**
   * @brief helper function that is used to recursively fill the truth table of
   * the target bbdd
   *
   * @param node bbdd root node for which the truth table should be created
   * @param var_rel helper data structure that stores the relation between the
   * inputs
   * @param inputs number of inputs to be considered for the truth table
   * @param tt truth table data structure that should be filled by this function
   */
  void recursive_dump_tt(bbdd_node_t *node,
                         std::vector<variable_relation_t> var_rel,
                         node_index_t inputs, std::vector<bool> &tt) {
    std::vector<variable_relation_t> neq_rel = var_rel;
    std::vector<variable_relation_t> eq_rel = var_rel;
    if (IS_TERM(node->index)) {
      return;
    }
    neq_rel.push_back({node->cvo_lvl.pv, node->cvo_lvl.sv, false});
    eq_rel.push_back({node->cvo_lvl.pv, node->cvo_lvl.sv, true});
    if (node->neq_child == 1) {
      insert_tt_value(neq_rel, inputs, tt, true);
    }
    if (node->eq_child == 1) {
      insert_tt_value(eq_rel, inputs, tt, true);
    }
    recursive_dump_tt(get_node_p(node->neq_child), neq_rel, inputs, tt);
    recursive_dump_tt(get_node_p(node->eq_child), eq_rel, inputs, tt);
  }

  /**
   * @brief recursive helper function that recursively writes the bbdd into a
   * blif file format uses only multiplexer and xor nodes
   *
   * @param blif_file output filestream in which the bbdd should be written to
   * @param node root node to the bbdd that should be converted
   * @param signal_map signal mal between internal indices and human readable
   * strings
   * @param output helper variable rather the current node is a output node or
   * internal node
   * @return index of the current bbdd node
   */
  uint32_t write_blif_recursive(std::ofstream &blif_file, bbdd_node_t *node,
                                std::vector<std::string> signal_map,
                                bool output) {
    if (IS_TERM(node->index) || MARKED(node)) {
      return GET_INDEX(node);
    }
    SET_MARKED(node);
    uint32_t left_child = write_blif_recursive(
        blif_file, get_node_p(node->neq_child), signal_map, false);
    uint32_t right_child = write_blif_recursive(
        blif_file, get_node_p(node->eq_child), signal_map, false);
    if (node->cvo_lvl.sv != INT_MAX) {
      blif_file << ".names " << signal_map[node->cvo_lvl.pv - 2].c_str() << " "
                << signal_map[node->cvo_lvl.sv - 2].c_str() << " "
                << std::to_string(GET_INDEX(node)) << "s\n";
    } else {
      blif_file << ".names " << signal_map[node->cvo_lvl.pv - 2].c_str()
                << " $true " << std::to_string(GET_INDEX(node)) << "s\n";
    }
    blif_file << "00 1\n11 1\n";
    blif_file << ".names " << std::to_string(GET_INDEX(node)) << "s ";
    if (IS_TERM(right_child)) {
      if (right_child == 0) {
        blif_file << "$false ";
      } else {
        blif_file << "$true ";
      }
    } else {
      blif_file << std::to_string(right_child);
    }
    blif_file << " ";
    if (IS_TERM(left_child)) {
      if (left_child == 0) {
        blif_file << "$false ";
      } else {
        blif_file << "$true ";
      }
    } else {
      blif_file << std::to_string(left_child);
    }
    blif_file << " ";
    if (!output) {
      blif_file << std::to_string(GET_INDEX(node)) << "\n";
    }
    if (!output) {
      blif_file << "0-1 1\n11- 1\n";
    }
    return GET_INDEX(node);
  }

  /**
   * @brief recursive helper function that dumps the bbdd node into a blif file
   * format and only uses NEMS specific muxxor nodes
   *
   * @param blif_file output file in which should the design by written to
   * @param node root node of the bbdd that should be dumped
   * @param signal_map map between the internal indices and human readable
   * string used for the design inputs
   * @param output boolean that represents if the current bbdd node is an output
   * or not
   * @return bbdd node index of the current bbdd node only used during recursion
   */
  uint32_t write_blif_recursive_muxxor(std::ofstream &blif_file,
                                       bbdd_node_t *node,
                                       std::vector<std::string> signal_map,
                                       bool output) {
    if (IS_TERM(node->index) || MARKED(node)) {
      return GET_INDEX(node);
    }
    SET_MARKED(node);
    // format a, b, in0, in1, out
    // 00-1 1
    // 011- 1
    // 101- 1
    // 11-1 1
    uint32_t left_child = write_blif_recursive_muxxor(
        blif_file, get_node_p(node->neq_child), signal_map, false);
    uint32_t right_child = write_blif_recursive_muxxor(
        blif_file, get_node_p(node->eq_child), signal_map, false);
    //  MUXXOR part
    std::string a, b, in0, in1, out;
    a = signal_map[node->cvo_lvl.pv - 2].c_str();
    if (node->cvo_lvl.sv != INT_MAX) {
      b = signal_map[node->cvo_lvl.sv - 2].c_str();
    } else {
      b = "$true";
    }
    if (IS_TERM(right_child)) {
      in1 = right_child == 0 ? "$false" : "$true";
    } else {
      in1 = std::to_string(right_child);
    }
    if (IS_TERM(left_child)) {
      in0 = left_child == 0 ? "$false" : "$true";
    } else {
      in0 = std::to_string(left_child);
    }
    blif_file << ".names " << a << " " << b << " " << in0 << " " << in1 << " ";
    if (!output) {
      blif_file << std::to_string(GET_INDEX(node)) << "\n";
      // blif_file << "0-1 1\n11- 1\n";
      blif_file << "00-1 1\n011- 1\n101- 1\n11-1 1\n";
    }
    return GET_INDEX(node);
  }

public:
#ifdef CACHE_STATS
  struct cache_stats_t {
    uint32_t hits;
    uint32_t inserts;
    uint32_t misses;
    uint32_t chain;
    uint32_t current_chain;
    uint32_t extend_hits;
    uint32_t extend_lookups;
    uint32_t merge_hits;
    uint32_t merge_lookups;
  };
  cache_stats_t cache_stats;
#endif

  std::vector<output_map_t> output_map;
  std::vector<std::string> signal_map;
  cvo_t *cvo;
  uint32_t num_inputs;
  std::unordered_map<merge_key, node_index_t, merge_hash> computed_table;
  std::unordered_map<extend_key, bbdd_node_ppair_t, extend_hash> extend_table;
  Unique_table() {}

  /**
   * @brief return bbdd node based on given index
   *
   * @param index for which the bbdd node should be retrieved
   * @return bbdd node at index
   */
  bbdd_node_t get_node(node_index_t index) { return entries[index].node; }
  /**
   * @brief return pointer to node at given index
   *
   * @param index for which the pointer to the bbdd node should be retrieved
   * @return pointer to bbdd node at index
   */
  bbdd_node_t *get_node_p(node_index_t index) { return &entries[index].node; }

  /**
   * @brief initialize cvo based on input list, cvo initial ordering strategy
   * and optional ordering that should be used
   *
   * @param inputs list of inputs that should are going to be used in design
   * @param cvo_opt chain variable ordering initial ordering strategy. Currently
   * strategies available: cvo_none, cvo_even, cvo_even_reversed, cvo_random,
   * cvo_input
   * @param input_cvo list of initial ordering only considered when cvo_opt is
   * cvo_input
   */
  void
  init_cvo(std::vector<uint64_t> inputs, cvo_init_t cvo_opt,
           std::vector<node_index_t> input_cvo = std::vector<node_index_t>()) {
    cvo = reinterpret_cast<cvo_t *>(malloc(sizeof(cvo_t)));
    num_inputs = inputs.size();
    init_ordering(inputs, cvo, cvo_opt, input_cvo);
  }

  /**
   * @brief initial signal map with a list of input name strings. Only required
   * if output should be written to blif file
   *
   * @param input_names list of input name strings
   */
  void init_signal_map(std::vector<std::string> input_names) {
    for (std::string input : input_names) {
      this->signal_map.emplace_back(input);
    }
  }

  /**
   * @brief Clear cache that is used during merge operations
   */
  void clear_computed_table() { computed_table.clear(); }

  /**
   * @brief Clear cache that is used during extend operations
   */
  void clear_extend_table() { extend_table.clear(); }

  /**
   * @brief Get next free position in the hash table
   *
   * @return index of next free position
   */
  uint32_t get_free_pos() { return free_pos; }

  /**
   * @brief initialise has table that stores the node information
   *
   * @param init_node_count capacity of the hash table
   * @param module_name name of the module that is represented by the bbdds,
   * only required for writing the design into blif file format
   * @return status code depending if the operations was succesful
   */
  int8_t init_table(uint64_t init_node_count, std::string module_name) {
    if (init_node_count > pow(2, 31)) {
      std::cerr << "[ERROR] init table: node count is too large\n";
      return -1;
    }
    this->module_name = module_name;
    entries = reinterpret_cast<table_entry_t *>(
        malloc(sizeof(table_entry_t) * init_node_count));
    if (entries == NULL) {
      std::cerr << "[ERROR] init failed, because out of memeory\n";
      return OUT_OF_MEMORY;
    }
    capacity = init_node_count;
    for (node_index_t i = 0; i < init_node_count; i++) {
      // init with zero
      LEVEL(i).pv = 0;
      LEVEL(i).sv = 0;
      EQ(i) = 0;
      NEQ(i) = 0;
      NEXT(i) = 0;
      REF(i) = 0;
      INDEX(i) = 0;
    }
    LEVEL(0).pv = INT_MAX;
    LEVEL(0).sv = INT_MAX;
    INDEX(0) = 0;
    // Constant 1
    LEVEL(1).pv = INT_MAX;
    LEVEL(1).sv = INT_MAX;
    INDEX(1) = 1;
    REF(1) = 1;
    // first empty space after constants
    free_pos = 2;
#ifdef CACHE_STATS
    cache_stats.hits = 0;
    cache_stats.inserts = 0;
    cache_stats.misses = 0;
    cache_stats.chain = 0;
    cache_stats.current_chain = 0;
    cache_stats.extend_lookups = 0;
    cache_stats.extend_hits = 0;
    cache_stats.merge_lookups = 0;
    cache_stats.merge_hits = 0;
#endif
    return SUCCESS;
  }

  /**
   * @brief free hash table
   */
  void free_table() { free(entries); }

  /**
   * @brief insert bbdd node into the hash table
   *
   * @param node_t bbdd node template that should be inserted
   * @return pointer to bbdd node in the hash table
   */
  bbdd_node_t *insert_node(bbdd_node_template_t node_t) {
#ifdef CACHE_STATS
    cache_stats.inserts++;
#endif
    assert(node_t.cvo_lvl.sv == INT_MAX ||
           POS(node_t.cvo_lvl.pv, cvo) < POS(node_t.cvo_lvl.sv, cvo));
    node_index_t hash = hash_node(node_t, capacity);
#ifdef DEBUG_TABLE
    printf("[INFO] INSERT: trying (%d, %d) %d %d hash: %d\n", node_t.cvo_lvl.pv,
           node_t.cvo_lvl.sv, node_t.neq_child, node_t.eq_child, hash);
#endif
    if (free_pos >= capacity && free_slots.empty()) {
      // resize not implemented yet
      std::cerr << "[ERROR] Unique Table is full resize not implemented yet";
      int count = 0;
      for (int i = 0; i < capacity; i++) {
        if (entries[i].ref == 0) {
          count++;
        }
      }
      assert(false);
      return 0;
    }
    table_entry_t *entry = &entries[hash];
    node_index_t chain_i = -1;
    if (entry->ref != 0) {
      // there is already a node with this hash
      chain_i = entry->ref;
#ifdef CACHE_STATS
      cache_stats.current_chain = 0;
#endif
      while (true) {
        // see if that is the node we currently want to insert
        if (node_eq(entries[chain_i].node, node_t)) {
#ifdef DEBUG_TABLE
          std::cout << "[INFO] INSERT: node hit ";
          dump_node(&entries[chain_i].node);
          std::cout << "\n";
#endif
#ifdef CACHE_STATS
          cache_stats.hits++;
#endif
          return &entries[chain_i].node;
        }
        // if there is no more node in the chain break and insert at that
        // position
        if (NEXT(chain_i) == 0) {
#ifdef CACHE_STATS
          if (cache_stats.current_chain > cache_stats.chain) {
            cache_stats.chain = cache_stats.current_chain;
          }
#endif
          break;
        }
        chain_i = NEXT(chain_i);
#ifdef CACHE_STATS
        cache_stats.current_chain++;
#endif
      }
    }
    node_index_t insert_pos;
    if (free_slots.empty()) {
      insert_pos = free_pos;
      free_pos++;
    } else {
      insert_pos = free_slots.back();
      free_slots.pop_back();
    }
    // insert node
    bbdd_node_t node = {0, insert_pos, node_t.cvo_lvl, node_t.neq_child,
                        node_t.eq_child};
    get_node_p(node_t.eq_child)->ref++;
    get_node_p(node_t.neq_child)->ref++;
    NODE(insert_pos) = node;
    // extend chain
    if (chain_i != -1) {
#ifdef DEBUG_TABLE
      std::cout << "[INFO] INSERT: extending chain at " << chain_i << " ";
      dump_node(&NODE(insert_pos));
      std::cout << "\n";
#endif
      entries[chain_i].next = insert_pos;
    } else {
      entry->ref = insert_pos;
#ifdef DEBUG_TABLE
      printf("[INFO] INSERT: no chain ");
      dump_node(&NODE(insert_pos));
      std::cout << "\n";
#endif
    }
#ifdef CACHE_STATS
    cache_stats.misses++;
#endif
    return &NODE(insert_pos);
  }

  /**
   * @brief delte bbdd node from the hash table
   *
   * @param node pointer to bbdd node that should be deleted from the hash table
   */
  void delete_node(bbdd_node_t *node) {
    node_index_t hash = hash_node(*node, capacity);
    // assert(entries[hash].ref != 0);
    node_index_t ref = entries[hash].ref;
    if (ref == node->index) {
      // not part of a chain
#ifdef DEBUG_TABLE
      printf("[INFO] DELETE: no chain replacing %d with %d\n", node->index,
             entries[ref].next);
#endif
      entries[hash].ref = entries[ref].next;
      free_slots.emplace_back(node->index);
    } else {
      // part of a chain get first element
      table_entry_t *chain_entry = &entries[entries[hash].ref];
      for (int i = 0; i < capacity; i++) {
        if (node_eq(entries[chain_entry->next].node, *node)) {
          // remove node from chain
#ifdef DEBUG_TABLE
          printf("[INFO] DELETE: chain replacing at %d with %d\n",
                 chain_entry->node.index, entries[node->index].next);
#endif
          chain_entry->next = entries[node->index].next;
          entries[node->index].next = 0;
          entries[node->index].node = {0, 0, {0, 0}, 0, 0};
          free_slots.emplace_back(node->index);
          return;
        }
        chain_entry = &entries[chain_entry->next];
      }
      dump_table();
      std::cout << "[ERROR] Node Node found: " << node->index << "\n";
      dump_node(node);
      std::cout << " with hash " << hash << "\n";
      fflush(stdout);
      assert(false && "node not found");
    }
  }

  /**
   * @brief add output map from bbdd node pointer to a string, used for
   * displaying and blif file purposes
   *
   * @param output string to human readable output
   * @param bbdd root bbdd node that represents output function
   */
  void add_output(std::string output, bbdd_node_t *bbdd) {
    output_map_t map = {output, bbdd};
    bbdd->ref++;
    output_map.emplace_back(map);
  }

  /**
   * @brief recursively clears marks from bbdd
   *
   * @param bbdd root bbdd node for which all marks should be cleared
   */
  void clear_marks(bbdd_node_t *bbdd) {
    if (IS_TERM(bbdd->index)) {
      return;
    }
    CLEAR_MARKED(bbdd);
    clear_marks(get_node_p(bbdd->neq_child));
    clear_marks(get_node_p(bbdd->eq_child));
  }

  /**
   * @brief dump hash table entries, only entries with data are printed
   */
  void dump_table() {
    for (uint64_t i = 0; i < free_pos; i++) {
      printf("Hash: %6d Ref: %3d Next: %4d Node: ",
             hash_node(entries[i].node, capacity), entries[i].ref,
             entries[i].next);
      dump_node(&entries[i].node);
      std::cout << "\n";
    }
    for (uint64_t i = free_pos; i < capacity; i++) {
      if (entries[i].ref != 0) {
        printf("i: %3lu Ref: %2d Next: %4d Node: \n", i, entries[i].ref,
               entries[i].next);
      }
    }
  }

  /**
   * @brief dump the truth table of given bbdd
   *
   * @param output pointer to the root of a bbdd for which the truth table
   * should be printed
   * @return string of the output tt
   */
  std::string dump_tt(bbdd_node_t *output) {
    std::vector<bool> tt(std::pow(2, this->num_inputs), false);
    std::vector<variable_relation_t> var_rel;
    recursive_dump_tt(output, var_rel, this->num_inputs, tt);
    for (int i = 0; i < tt.size(); i++) {
      for (int j = 0; j < this->num_inputs; j++) {
        printf("%d", get_ith_bit(i, this->num_inputs, j));
      }
      printf(" | %s\n", tt[i] ? "1" : "0");
    }
    std::string out_string = "";
    for (int i = 0; i < tt.size(); i++) {
      out_string += tt[i] ? "1" : "0";
    }
    return out_string;
  }

  /**
   * @brief dump truth table for output string name
   *
   * @param output name of the output in the output map
   * @return string of the tt, empty if output name does not exist in output map
   */
  std::string dump_tt(std::string output) {
    std::printf("Truth table of output %s\n", output.c_str());
    for (output_map_t out_map : this->output_map) {
      if (out_map.output == output) {
        return dump_tt(out_map.bbdd);
      }
    }
    return "";
  }

  /**
   * @brief dump bbdd of given output into a dot file format
   *
   * @param filename name of the file in which the output will be dumped
   * @param output name of the output which should be dumped, dot file only
   * consists of terminal node if output name is not in the output map
   */
  void dump_dot(std::string filename, std::string output) {
    std::ofstream dot_file(filename);
    dot_file << "graph bbdd {\n";
    // terminal nodes
    dot_file << "\t0 [shape=square]\n";
    dot_file << "\t1 [shape=square]";
    bbdd_node_t *root_node;
    for (output_map_t map : output_map) {
      if (map.output == output) {
        root_node = map.bbdd;
        break;
      }
    }
    node_index_t root = recursive_dump_dot(dot_file, root_node);
    clear_marks(root_node);
    dot_file << "\n\t" << free_pos + 1 << " [shape=plaintext, label=\""
             << output << "\"]\n";
    dot_file << "\t" << free_pos + 1 << " -- " << root_node->index << "\n";
    dot_file << "}\n";
  }

  /**
   * @brief dump all bbdd nodes that have a defined output of the module into a
   * dot file format
   *
   * @param filename name in which the design should be printed to
   */
  void dump_dot(std::string filename) {
    std::ofstream dot_file(filename);
    dot_file << "graph bbdd {\n";
    // terminal nodes
    dot_file << "\t0 [shape=square]\n";
    dot_file << "\t1 [shape=square]\n";
    // insert nodes
    for (uint64_t i = 2; i < free_pos; i++) {
      table_entry_t entry = entries[i];
      if (entry.node.cvo_lvl.sv != INT_MAX) {
        dot_file << "\n"
                 << i << " [label=\"" << entry.node.ref << "\n"
                 << i << ": " << entry.node.cvo_lvl.pv << ","
                 << entry.node.cvo_lvl.sv << "\"]";
      } else {
        dot_file << "\n"
                 << i << " [label=\"" << entry.node.ref << "\n"
                 << i << ": " << entry.node.cvo_lvl.pv << ",1" << "\"]";
      }
      dot_file << "\t" << i << " -- " << entry.node.neq_child
               << "[label=<<FONT POINT-SIZE=\"14\">&ne;</FONT>>, "
                  "style=\"dashed\"]\n";
      dot_file << "\t" << i << " -- " << entry.node.eq_child
               << "[label=\"=\"]\n";
    }
    for (output_map_t map : output_map) {
      dot_file << "\n"
               << map.output << " [shape=plaintext, label=\"" << map.output
               << "\"]";
      dot_file << "\t" << map.output << " -- " << map.bbdd->index << "\n";
    }
    dot_file << "}\n";
  }

  /**
   * @brief same as previous dump_dot function but it uses a signal map that
   * maps primary and secondary variables to human readable strings
   *
   * @param filename in which the design should be written to
   * @param signal_map maps indices of primary and secondary variables to human
   * readable strings
   */
  void dump_dot(std::string filename, std::vector<std::string> signal_map) {
    std::ofstream dot_file(filename);
    dot_file << "graph bbdd {\n";
    // terminal nodes
    dot_file << "\t0 [shape=square]";
    dot_file << "\t1 [shape=square]";
    // insert nodes
    for (uint64_t i = 2; i < free_pos; i++) {
      table_entry_t entry = entries[i];
      if (entry.node.ref == 0) {
        continue;
      }
      if (entry.node.cvo_lvl.sv != INT_MAX) {
        dot_file << "\n"
                 << i << " [label=\"" << entry.node.ref << "\n"
                 << i << ": " << signal_map[entry.node.cvo_lvl.pv - 2] << ","
                 << signal_map[entry.node.cvo_lvl.sv - 2] << "\"]";
      } else {
        dot_file << "\n"
                 << i << " [label=\"" << entry.node.ref << "\n"
                 << i << ": " << signal_map[entry.node.cvo_lvl.pv - 2] << ",1"
                 << "\"]";
      }
      dot_file << "\t" << i << " -- " << entry.node.neq_child
               << "[label=<<FONT POINT-SIZE=\"14\">&ne;</FONT>>, "
                  "style=\"dashed\"]\n";
      dot_file << "\t" << i << " -- " << entry.node.eq_child
               << "[label=\"=\"]\n";
    }
    for (output_map_t map : output_map) {
      dot_file << "\n"
               << map.output << " [shape=plaintext, label=\"" << map.output
               << "\"]";
      dot_file << "\t" << map.output << " -- " << map.bbdd->index << "\n";
    }
    dot_file << "}\n";
  }

  /**
   * @brief dump the current module into blif file format
   *
   * @param filename name of the file in which the diagrams should be dumped
   * into, only outputs are considered that are present in the output map
   */
  void write_blif(std::string filename) {
    std::ofstream blif_file(filename);
    blif_file << ".model " + this->module_name + "\n";
    blif_file << ".inputs";
    for (int i = 0; i < this->signal_map.size(); i++) {
      blif_file << " " << this->signal_map[i];
    }
    blif_file << "\n.outputs";
    for (output_map_t output : this->output_map) {
      blif_file << " " << output.output;
    }
    blif_file << "\n.names $true\n1\n";
    blif_file << ".names $false\n";
    for (output_map_t map : this->output_map) {
      if (IS_TERM(map.bbdd->index)) {
        if (map.bbdd->index == 0) {
          blif_file << ".names " << map.output << "\n";
        } else {
          blif_file << ".names " << map.output << "\n1\n";
        }
      } else if (MARKED(map.bbdd)) {
        blif_file << ".names " << (GET_INDEX(map.bbdd)) << " " << map.output
                  << "\n1 1\n";
      } else {
        // write_blif_recursive(blif_file, map.bbdd, cover.signal_map, true);
        // blif_file << map.output << "\n0-1 1\n11- 1\n";
        write_blif_recursive_muxxor(blif_file, map.bbdd, signal_map, true);
        blif_file << map.output << "\n00-1 1\n011- 1\n101- 1\n11-1 1\n";
      }
    }
    blif_file << ".end\n";
  }

#ifdef CACHE_STATS
  void print_cache_stats() {
    printf(
        "[INFO] CACHE STATS: inserts: %d, hits: %d, misses %d, max chain: %d\n",
        cache_stats.inserts, cache_stats.hits, cache_stats.misses,
        cache_stats.chain);
  }

  void dump_cache_stats(std::string path) {
    std::ofstream csv_file(path);
    csv_file << "inserts;hits;misses;max_chain;extend_lookups;extend_hits;"
                "merge_lookups;merge_hits\n";
    csv_file << std::to_string(cache_stats.inserts) << ";"
             << std::to_string(cache_stats.hits) << ";"
             << std::to_string(cache_stats.misses) << ";"
             << std::to_string(cache_stats.chain) << ";"
             << std::to_string(cache_stats.extend_lookups) << ";"
             << std::to_string(cache_stats.extend_hits) << ";"
             << std::to_string(cache_stats.merge_lookups) << ";"
             << std::to_string(cache_stats.merge_hits) << "\n";
    csv_file.close();
  }
#endif

  /**
   * @brief get maximum tree height of a bbdd
   *
   * @param root root node of bbdd node for which the height should be
   * calculated
   * @param height intermediate values used for the recursion
   * @return maximum height of the current bbdd node to any terminal node
   */
  uint32_t get_tree_height(bbdd_node_t *root, uint32_t height) {
    if (IS_TERM(root->index)) {
      return 0;
    }
    bbdd_node_t *neq = get_node_p(root->neq_child);
    bbdd_node_t *eq = get_node_p(root->eq_child);
    return std::max(get_tree_height(neq, height) + 1,
                    get_tree_height(eq, height) + 1);
  }

  /**
   * @brief gets maximum tree height of a bbdd
   *
   * @param node root node of bbdd node for which the height should be
   * calculated
   * @return maximum height of the current bbdd node to any terminal node
   */
  uint32_t get_tree_height(bbdd_node_t *node) {
    return get_tree_height(node, 0);
  }

  /**
   * @brief return the maximum tree height of all bbdds registered in the output
   * map
   *
   * @return maximum tree height of all bbdds in the design
   */
  uint32_t get_max_height() {
    uint32_t max_height = -1;
    uint32_t current_height;
    for (output_map_t out_map : output_map) {
      current_height = get_tree_height(out_map.bbdd);
      if (current_height > max_height) {
        max_height = current_height;
      }
    }
    return max_height;
  }

  /**
   * @brief return the sum of all maximum tree heights of all bbdd nodes that
   * have registered an output in the output map
   *
   * @return sum of all maximum tree heights
   */
  uint32_t get_total_height() {
    uint32_t sum = 0;
    for (output_map_t out_map : output_map) {
      sum += get_tree_height(out_map.bbdd);
    }
    return sum;
  }

  /**
   * @brief reorders a bbdd based on two variables that are swapped
   *
   * @param node root node to the bbdd which should be reordered
   * @param b first variable
   * @param c second variable
   * @return newly created bbdd based on the swapped varaibles inserted into the
   * hash table
   */
  bbdd_node_t *reorder_bbdd(bbdd_node_t *node, node_index_t b, node_index_t c) {
#ifdef DEBUG_REORDER
    printf("reorder: ");
    dump_node(node);
    printf("\n");
#endif
    if (IS_TERM(node->index)) {
      return node;
    }
    bbdd_node_t *neq_child = get_node_p(node->neq_child);
    bbdd_node_t *eq_child = get_node_p(node->eq_child);
    bbdd_node_t *new_neq, *new_eq, *new_neq_neq, *new_neq_eq, *new_eq_neq,
        *new_eq_eq;
    bbdd_node_t *neq_neq_child, *neq_eq_child, *eq_neq_child, *eq_eq_child;
    node_index_t nnn, nne, nen, nee, enn, ene, een, eee;
    uint32_t nn_sv, ne_sv, en_sv, ee_sv;
    // b no SV
    if (node->cvo_lvl.pv == b) {
      // c not present in this bbdd
      if (node->cvo_lvl.sv != c) {
        return node;
      }
      // NEQ-Child
      if (neq_child->cvo_lvl.pv != c) {
        new_neq = neq_child;
      } else {
        new_neq = insert_node({{b, neq_child->cvo_lvl.sv},
                               neq_child->eq_child,
                               neq_child->neq_child});
      }
      // EQ-Child
      if (eq_child->cvo_lvl.pv != c) {
        new_eq = eq_child;
      } else {
        new_eq = insert_node({{b, eq_child->cvo_lvl.sv},
                              eq_child->neq_child,
                              eq_child->eq_child});
      }
      assert(new_neq->cvo_lvl.sv == INT_MAX ||
             POS(new_neq->cvo_lvl.pv, cvo) < POS(new_neq->cvo_lvl.sv, cvo));
      assert(new_eq->cvo_lvl.sv == INT_MAX ||
             POS(new_eq->cvo_lvl.pv, cvo) < POS(new_eq->cvo_lvl.sv, cvo));
      assert(POS(c, cvo) < POS(b, cvo));
      return insert_node({{c, b}, new_neq->index, new_eq->index});
    }
    // b SV
    if (node->cvo_lvl.sv == b) {
      // NEQ-Child
      if (neq_child->cvo_lvl.pv == b) {
        if (neq_child->cvo_lvl.sv != c) {
          nnn = nee = neq_child->eq_child;
          nne = nen = neq_child->neq_child;
          nn_sv = ne_sv = neq_child->cvo_lvl.sv;
        } else {
          // c SV in neq_child
          neq_neq_child = get_node_p(neq_child->neq_child);
          neq_eq_child = get_node_p(neq_child->eq_child);
          // full neq neq
          if (neq_neq_child->cvo_lvl.pv == c) {
            nnn = neq_neq_child->neq_child;
            nne = neq_neq_child->eq_child;
            nn_sv = neq_neq_child->cvo_lvl.sv;
            // c no neq neq PV
          } else {
            nnn = nne = neq_neq_child->index;
            nn_sv = neq_neq_child->cvo_lvl.pv;
          }
          // full neq eq
          if (neq_eq_child->cvo_lvl.pv == c) {
            nen = neq_eq_child->neq_child;
            nee = neq_eq_child->eq_child;
            ne_sv = neq_eq_child->cvo_lvl.sv;
            // c no neq eq PV
          } else {
            nen = nee = neq_eq_child->index;
            ne_sv = neq_eq_child->cvo_lvl.pv;
          }
        }
      } else {
        // b no PV in neq_child
        if (neq_child->cvo_lvl.pv == c) {
          // c PV in neq_child
          nnn = nen = neq_child->neq_child;
          nne = nee = neq_child->eq_child;
          nn_sv = ne_sv = neq_child->cvo_lvl.sv;
        } else {
          nnn = nne = nen = nee = neq_child->index;
          nn_sv = ne_sv = neq_child->cvo_lvl.pv;
        }
      }
      // EQ-Child
      if (eq_child->cvo_lvl.pv == b) {
        if (eq_child->cvo_lvl.sv != c) {
          ene = een = eq_child->neq_child;
          enn = eee = eq_child->eq_child;
          en_sv = ee_sv = eq_child->cvo_lvl.sv;
        } else {
          // c is sv in eq_child
          eq_neq_child = get_node_p(eq_child->neq_child);
          eq_eq_child = get_node_p(eq_child->eq_child);
          if (eq_neq_child->cvo_lvl.pv == c) {
            enn = eq_neq_child->neq_child;
            ene = eq_neq_child->eq_child;
            en_sv = eq_neq_child->cvo_lvl.sv;
          } else {
            enn = ene = eq_neq_child->index;
            en_sv = eq_neq_child->cvo_lvl.pv;
          }
          if (eq_eq_child->cvo_lvl.pv == c) {
            een = eq_eq_child->neq_child;
            eee = eq_eq_child->eq_child;
            ee_sv = eq_eq_child->cvo_lvl.sv;
          } else {
            een = eee = eq_eq_child->index;
            ee_sv = eq_eq_child->cvo_lvl.pv;
          }
        }
      } else {
        // b is not pv in eq_child
        if (eq_child->cvo_lvl.pv == c) {
          enn = een = eq_child->neq_child;
          ene = eee = eq_child->eq_child;
          en_sv = ee_sv = eq_child->cvo_lvl.sv;
        } else {
          enn = ene = een = eee = eq_child->index;
          en_sv = ee_sv = eq_child->cvo_lvl.pv;
        }
      }
      // create new bbdd
      // new neq
      assert(en_sv == INT_MAX || ene == enn || POS(b, cvo) < POS(en_sv, cvo));
      assert(ne_sv == INT_MAX || nen == nee || POS(b, cvo) < POS(ne_sv, cvo));
      assert(POS(c, cvo) < POS(b, cvo));
      new_neq_neq = insert_node({{b, en_sv}, ene, enn});
      new_neq_eq = insert_node({{b, ne_sv}, nen, nee});
      new_neq = insert_node({{c, b}, new_neq_neq->index, new_neq_eq->index});
      // new eq
      assert(nn_sv == INT_MAX || nne == nnn || POS(b, cvo) < POS(nn_sv, cvo));
      assert(ee_sv == INT_MAX || een == eee || POS(b, cvo) < POS(ee_sv, cvo));
      assert(POS(c, cvo) < POS(b, cvo));
      new_eq_neq = insert_node({{b, nn_sv}, nne, nnn});
      new_eq_eq = insert_node({{b, ee_sv}, een, eee});
      new_eq = insert_node({{c, b}, new_eq_neq->index, new_eq_eq->index});
      // new root
      assert(POS(node->cvo_lvl.pv, cvo) < POS(c, cvo));
      return insert_node(
          {{node->cvo_lvl.pv, c}, new_neq->index, new_eq->index});
    }
    new_neq = reorder_bbdd(get_node_p(node->neq_child), b, c);
    new_eq = reorder_bbdd(get_node_p(node->eq_child), b, c);
    if (!(node->cvo_lvl.sv == INT_MAX ||
          POS(node->cvo_lvl.pv, cvo) < POS(node->cvo_lvl.sv, cvo))) {
      dump_node(node);
      std::cout << "\n";
    }
    assert(node->cvo_lvl.sv == INT_MAX ||
           POS(node->cvo_lvl.pv, cvo) < POS(node->cvo_lvl.sv, cvo));
    return insert_node({{node->cvo_lvl}, new_neq->index, new_eq->index});
  }

  /**
   * @brief return the total number of nodes in a bbdd
   *
   * @return total number od nodes in a bbdd
   */
  uint32_t get_total_number_nodes() {
    uint32_t count = 0;
    for (output_map_t out_map : output_map) {
      count += get_number_nodes_recursive(out_map.bbdd);
    }
    for (output_map_t out_map : output_map) {
      clear_marks(out_map.bbdd);
    }
    return count;
  }

  /**
   * @brief dump information stored in the output map: name of the output and
   * the index of the bbdd node that is the root noddump information stored in
   * the output map: name of the output and the index of the bbdd node that is
   * the root node for that output
   */
  void dump_outputs() {
    for (output_map_t out_map : output_map) {
      printf("Output: %s: ", out_map.output.c_str());
      dump_node(out_map.bbdd);
      printf("\n");
    }
  }

  /**
   * @brief swap two inputs in the variable ordering and reorder bbdd based on the new ordering
   *
   * @param root root bbdd node that should be reordered after variable swap
   * @param b first variable
   * @param c second variable
   * @return newly created bbdd node based on new variable order
   */
  bbdd_node_t *swap_positions(bbdd_node_t *root, node_index_t b,
                              node_index_t c) {
    // assert(POS(b, cvo) + 1 == POS(c, cvo));
    assert(b + 1 == c);
    node_index_t temp = (*cvo)[b].in;
    (*cvo)[b].in = (*cvo)[c].in;
    (*cvo)[c].in = temp;
    (*cvo)[(*cvo)[b].in % num_inputs].pos = b;
    (*cvo)[(*cvo)[c].in % num_inputs].pos = c;
    return reorder_bbdd(root, VAR(c, cvo), VAR(b, cvo));
  }

  /**
   * @brief reduce size of the bbdd node based on reduction rules
   *
   * @param f root node to bbdd that should be reduced
   * @return pointer to reduced bbdd
   */
  bbdd_node_t *reduce_bbdd(bbdd_node_t *f) {
    if (IS_TERM(f->index)) {
      return f;
    }
    bbdd_node_t *child_neq = get_node_p(f->neq_child),
                *child_eq = get_node_p(f->eq_child);
    bbdd_node_t *new_neq, *new_eq, new_root;
    new_neq = reduce_bbdd(child_neq);
    new_eq = reduce_bbdd(child_eq);
    if (new_neq->index == new_eq->index) {
#ifdef DEBUG_BBDD
      printf("[INFO] REDUCE: node %d\n", f->index);
#endif
      return new_neq;
    }
    if (!(IS_TERM(new_neq->index)) && !(IS_TERM(new_eq->index)) &&
        new_neq->cvo_lvl.pv == new_eq->cvo_lvl.pv &&
        new_neq->cvo_lvl.sv == new_eq->cvo_lvl.sv &&
        f->cvo_lvl.sv == new_neq->cvo_lvl.pv &&
        new_neq->neq_child == new_eq->eq_child &&
        new_neq->eq_child == new_eq->neq_child) {
      return insert_node({{f->cvo_lvl.pv, new_neq->cvo_lvl.sv},
                          new_neq->eq_child,
                          new_neq->neq_child});
    }
    assert(f->cvo_lvl.sv == INT_MAX ||
           POS(f->cvo_lvl.pv, cvo) < POS(f->cvo_lvl.sv, cvo));
    return insert_node({f->cvo_lvl, new_neq->index, new_eq->index});
  }

  /**
   * @brief swap two adjacent variables in ordering and reorder all bbdd that have a registered output
   *
   * @param pos_b position of first variable
   * @param pos_c position of second variable
   */
  void swap_all_positions(node_index_t pos_b, node_index_t pos_c) {
    node_index_t var_b = (*cvo)[pos_b].in;
    node_index_t var_c = (*cvo)[pos_c].in;
    swap_variable_order(pos_b, pos_c);
    for (uint32_t i = 0; i < output_map.size(); i++) {
      output_map[i].bbdd =
          reduce_bbdd(reorder_bbdd(output_map[i].bbdd, var_b, var_c));
    }
  }
};