// Copyright 2025 Oliver Theimer
#pragma once

#include <cstdint>
#include <cstdio>
#include <iostream>

#include "./bbdd_node.hpp"
#include "./bbdd_types.hpp"
#include "./chain_variable_ordering.hpp"
#include "./unique_table.hpp"

/**
 * @brief decrement external reference count for a given bbdd node
 *
 * @param table hash table in which the node is stored
 * @param node for which the external reference count is supposed to be
 * decremented
 * @return the same node with the new external reference value
 */
inline bbdd_node_t *del_ref(Unique_table *table, bbdd_node_t *node) {
  if (node->ref > 0) {
    node->ref--;
  }
  return node;
}

/**
 * @brief increment external reference value for given node
 *
 * @param node whose external reference count is supposed to be incremented
 * @return the same node with the new external reference value
 */
inline bbdd_node_t *add_ref(bbdd_node_t *node) {
  node->ref++;
  return node;
}

/**
 * @brief revursively negate the bbdd given by a bbdd node
 *
 * @param table in which the bbdd nodes are stored
 * @param f root node for which the subtree should be negated
 * @return new bbdd node that is the root for the resulting diagram
 */
inline bbdd_node_t *negate_recursive(Unique_table *table, bbdd_node_t *f) {
  if (IS_TERM(f->index)) {
    if (f->index == 0) {
      return table->get_node_p(1);
    } else {
      return table->get_node_p(0);
    }
  }
  bbdd_node_t *neq, *eq, *new_root;
  neq = negate_recursive(table, table->get_node_p(f->neq_child));
  eq = negate_recursive(table, table->get_node_p(f->eq_child));
  assert(f->cvo_lvl.sv == INT_MAX ||
         POS(f->cvo_lvl.pv, table->cvo) < POS(f->cvo_lvl.sv, table->cvo));
  new_root = table->insert_node({f->cvo_lvl, neq->index, eq->index});
  return new_root;
}

/**
 * @brief returns bbdd for two given inputs and a Boolean operation
 *
 * @param table table in which the result should be stored
 * @param c1_i first input
 * @param c2_i second input
 * @param op boolean operation which combines the two inputs
 * @return bbdd node that is the root to the resulting bbdd
 */
inline bbdd_node_t *base_case_two_inputs(Unique_table *table, node_index_t c1_i,
                                         node_index_t c2_i,
                                         const bbdd_op_t op) {
#ifdef DEBUG_BBDD
  std::cout << "[INFO] TWO INPUT BASE CASE: " << c1_i << " " << bbdd_op_s[op]
            << " " << c2_i << "\n";
#endif
  assert(c1_i != c2_i);
  uint32_t pv, sv;
  // define pv and sv based on position in ordering
  if (POS(c1_i, table->cvo) < POS(c2_i, table->cvo)) {
    pv = c1_i;
    sv = c2_i;
  } else {
    pv = c2_i;
    sv = c1_i;
  }
  assert(POS(pv, table->cvo) < POS(sv, table->cvo));
  bbdd_node_t *root, *child;
  switch (op) {
  case bbdd_and:
    child = table->insert_node({{sv, INT_MAX}, 0, 1});
    root = table->insert_node({{pv, sv}, 0, child->index});
    break;
  case bbdd_or:
    child = table->insert_node({{sv, INT_MAX}, 0, 1});
    root = table->insert_node({{pv, sv}, 1, child->index});
    break;
  case bbdd_xor:
    // cvo, eq, neq
    root = table->insert_node({{pv, sv}, 1, 0});
    break;
  case bbdd_xnor:
    root = table->insert_node({{pv, sv}, 0, 1});
    break;
  case bbdd_nand:
    child = table->insert_node({{sv, INT_MAX}, 1, 0});
    root = table->insert_node({{pv, sv}, 1, child->index});
    break;
  case bbdd_nor:
    child = table->insert_node({{sv, INT_MAX}, 1, 0});
    root = table->insert_node({{pv, sv}, 0, child->index});
    break;
  case bbdd_andnot:
    child = table->insert_node({{sv, INT_MAX}, 1, 0});
    root = table->insert_node({{pv, sv}, child->index, 0});
    break;
  case bbdd_notand:
    child = table->insert_node({{sv, INT_MAX}, 0, 1});
    root = table->insert_node({{pv, sv}, child->index, 0});
    break;
  default:
    std::cout << "[ERROR] MERGE: base case " << bbdd_op_s[op].c_str()
              << " not implemented \n";
    assert(false && "base case not implemented yet :");
  }
  return root;
}

/**
 * @brief returns bbdd that is the result of combining a bbdd with a primary
 * input and a given Boolean operation
 *
 * @param table in whicht the result should be stored and the given bbdd is
 * stored
 * @param f bbdd root node
 * @param g_i primary input index
 * @param op Boolean operation which should be used for the calculation
 * @return root node to the calculated bbdd
 */
inline bbdd_node_t *merge_one_terminal_base_case(Unique_table *table,
                                                 bbdd_node_t *f,
                                                 node_index_t g_i,
                                                 bbdd_op_t op) {
  assert(g_i == 0 || g_i == 1);
#ifdef DEBUG_BBDD
  std::cout << "[INFO] MERGE: one terminal " << f->index << " and " << g_i
            << " = " << bbdd_op_s[op].c_str() << "\n";
#endif
  bbdd_node_t *neg_f;
  if (g_i == 1) {
    switch (op) {
    case bbdd_and:
    case bbdd_xnor:
      return f;
    case bbdd_or:
      return table->get_node_p(1);
    case bbdd_xor:
    case bbdd_nand:
      return negate_recursive(table, f);
    case bbdd_nor:
      return table->get_node_p(0);
    case bbdd_notand:
      return negate_recursive(table, f);
      break;
    default:
      std::cout << "[ERROR] MERGE: one terminal " << bbdd_op_s[op].c_str()
                << " not implemented \n";
      assert(false && "one terminal base case not implemented");
      return 0;
    }
  } else {
    switch (op) {
    case bbdd_and:
    case bbdd_notand:
      return table->get_node_p(0);
    case bbdd_or:
    case bbdd_xor:
    case bbdd_nand:
      return f;
    case bbdd_xnor:
    case bbdd_nor:
      return negate_recursive(table, f);
    default:
      std::cout << "[ERROR] MERGE: one terminal " << bbdd_op_s[op].c_str()
                << " not implemented \n";
      assert(false);
      return 0;
    }
  }
}

/**
 * @brief merge two terminal bbdd nodes
 *
 * @param c1 first terminal node
 * @param c2 second terminal node
 * @param op Boolean operation which is used to combine the terminal node
 * @return terminal bbdd node (either 0 or 1)
 */
inline node_index_t
merge_two_terminal_base_case(node_index_t c1, node_index_t c2, bbdd_op_t op) {
  assert((c1 == 0 || c1 == 1) && (c2 == 0 || c2 == 1));
#ifdef DEBUG_BBDD
  std::cout << "[INFO] MERGE: two terminal " << c1 << " and " << c2 << " = "
            << bbdd_op_s[op].c_str() << "\n";
#endif
  switch (op) {
  case bbdd_and:
    return c1 && c2;
  case bbdd_nand:
    if (c1 && c2) {
      return 0;
    } else {
      return 1;
    }
  case bbdd_or:
    return c1 || c2;
  case bbdd_nor:
    if (c1 || c2) {
      return 0;
    } else {
      return 1;
    }
  case bbdd_xor:
    return c1 != c2;
  case bbdd_xnor:
    return c1 == c2;
  case bbdd_notand:
    if (c1 == 1) {
      return 0;
    } else {
      return c2;
    }
  default:
    std::cout << "[ERROR] MERGE: two terminal " << bbdd_op_s[op].c_str()
              << " not implemented \n";
    assert(false);
    return 0;
  }
  return 0;
}

/**
 * @brief merge two bbdd nodes that are identical with the fiven Boolean
 * operation
 *
 * @param table
 * @param f
 * @param op
 * @return
 */
inline bbdd_node_t *merge_equal_base_case(Unique_table *table, bbdd_node_t *f,
                                          bbdd_op_t op) {
#ifdef DEBUG_BBDD
  std::cout << "[INFO] MERGE: equal base case " << f->index << " with "
            << bbdd_op_s[op].c_str() << "\n";
#endif
  switch (op) {
  case bbdd_and:
  case bbdd_or:
    return f;
  case bbdd_xor:
  case bbdd_notand:
    return table->get_node_p(0);
  case bbdd_xnor:
    return table->get_node_p(1);
  case bbdd_nand:
  case bbdd_nor:
    return negate_recursive(table, f);
  default:
    std::cout << "[ERROR] MERGE: equal case " << bbdd_op_s[op].c_str()
              << " not implemented \n";
    assert(false);
    return 0;
  }
}

/**
 * @brief extend bbdd node based on a second bbdd and an extend case
 *
 * @param table hash table in which the two bbdd must be stored and the result
 * will be inserted
 * @param f bbdd node to be extended
 * @param g bbdd node to be used for case
 * @param extend_case case in which the two bbdd cvo intervals intersect
 * @return root node of newly created bbdd
 */
static bbdd_node_t *extend_node(Unique_table *table, bbdd_node_t *f,
                                bbdd_node_t *g, bbdd_cases_t extend_case) {
  bbdd_node_t *new_root, *neq, *eq, *c_neq_eq, *c_eq_neq, *c_neq_neq, *c_eq_eq;
  bool update_neq, update_eq;
#ifdef DEBUG_BBDD
  printf("[INFO] EXTEND: extending %d and %d with %s\n", f->index, g->index,
         bbdd_cases_s[extend_case].c_str());
#endif
  assert(g->cvo_lvl.sv == INT_MAX ||
         POS(g->cvo_lvl.pv, table->cvo) < POS(g->cvo_lvl.sv, table->cvo));
  assert(f->cvo_lvl.sv == INT_MAX ||
         POS(f->cvo_lvl.pv, table->cvo) < POS(f->cvo_lvl.sv, table->cvo));
  switch (extend_case) {
  case case_2f:
    assert(POS(g->cvo_lvl.pv, table->cvo) < POS(f->cvo_lvl.sv, table->cvo) ||
           f->cvo_lvl.sv == INT_MAX);
    c_eq_neq = table->insert_node(
        {{g->cvo_lvl.pv, f->cvo_lvl.sv}, f->eq_child, f->neq_child});
    c_neq_eq = table->insert_node(
        {{g->cvo_lvl.pv, f->cvo_lvl.sv}, f->neq_child, f->eq_child});
    assert(POS(f->cvo_lvl.pv, table->cvo) < POS(g->cvo_lvl.pv, table->cvo));
    return table->insert_node(
        {{f->cvo_lvl.pv, g->cvo_lvl.pv}, c_eq_neq->index, c_neq_eq->index});
  case case_2g:
    assert(POS(g->cvo_lvl.sv, table->cvo) < POS(f->cvo_lvl.sv, table->cvo) ||
           f->cvo_lvl.sv == INT_MAX);
    c_eq_neq = table->insert_node(
        {{g->cvo_lvl.sv, f->cvo_lvl.sv}, f->eq_child, f->neq_child});
    c_neq_eq = table->insert_node(
        {{g->cvo_lvl.sv, f->cvo_lvl.sv}, f->neq_child, f->eq_child});
    assert(POS(f->cvo_lvl.pv, table->cvo) < POS(g->cvo_lvl.sv, table->cvo));
    return table->insert_node(
        {{f->cvo_lvl.pv, g->cvo_lvl.sv}, c_eq_neq->index, c_neq_eq->index});
  case case_3f:
    c_eq_neq = table->insert_node({g->cvo_lvl, f->eq_child, f->neq_child});
    c_neq_eq = table->insert_node({g->cvo_lvl, f->neq_child, f->eq_child});
    assert(POS(f->cvo_lvl.pv, table->cvo) < POS(g->cvo_lvl.pv, table->cvo));
    return table->insert_node(
        {{f->cvo_lvl.pv, g->cvo_lvl.pv}, c_eq_neq->index, c_neq_eq->index});
  case case_4f:
    assert(POS(g->cvo_lvl.pv, table->cvo) < POS(f->cvo_lvl.sv, table->cvo) ||
           f->cvo_lvl.sv == INT_MAX);
    neq = table->insert_node(
        {{g->cvo_lvl.pv, f->cvo_lvl.sv}, f->eq_child, f->neq_child});
    eq = table->insert_node(
        {{g->cvo_lvl.pv, f->cvo_lvl.sv}, f->neq_child, f->eq_child});
    assert(POS(f->cvo_lvl.pv, table->cvo) < POS(g->cvo_lvl.pv, table->cvo));
    return table->insert_node(
        {{f->cvo_lvl.pv, g->cvo_lvl.pv}, neq->index, eq->index});
  case case_5f:
    assert(POS(g->cvo_lvl.sv, table->cvo) < POS(f->cvo_lvl.sv, table->cvo) ||
           f->cvo_lvl.sv == INT_MAX);
    neq = table->insert_node(
        {{g->cvo_lvl.sv, f->cvo_lvl.sv}, f->eq_child, f->neq_child});
    eq = table->insert_node(
        {{g->cvo_lvl.sv, f->cvo_lvl.sv}, f->neq_child, f->eq_child});
    assert(POS(f->cvo_lvl.pv, table->cvo) < POS(g->cvo_lvl.sv, table->cvo));
    return table->insert_node(
        {{f->cvo_lvl.pv, g->cvo_lvl.sv}, neq->index, eq->index});
  default:
    std::cout << "[ERROR] EXTEND " << bbdd_cases_s[extend_case].c_str()
              << " not implemented \n";
    assert(false);
  }
  return NULL;
}

/**
 * @brief extend two bbdds in order that they have the same levels of nodes
 *
 * @param table in which the two bbdds are stored and the result should be
 * inserted
 * @param f first bbdd node
 * @param g second bbdd node
 * @return pair of newly created root nodes after the extension
 */
inline bbdd_node_ppair_t extend_bbdds(Unique_table *table, bbdd_node_t *f,
                                      bbdd_node_t *g) {
  extend_key key = {f->index, g->index};
  auto res = table->extend_table.find(key);
#ifdef CACHE_STATS
  table->cache_stats.extend_lookups++;
#endif
  if (res != table->extend_table.end()) {
#ifdef CACHE_STATS
    table->cache_stats.extend_hits++;
#endif
    return res->second;
  }
  assert(g->cvo_lvl.sv == INT_MAX ||
         POS(g->cvo_lvl.pv, table->cvo) < POS(g->cvo_lvl.sv, table->cvo));
  assert(f->cvo_lvl.sv == INT_MAX ||
         POS(f->cvo_lvl.pv, table->cvo) < POS(f->cvo_lvl.sv, table->cvo));
  if (g->index == f->index) {
    return {f, g};
  }
  if (IS_TERM(g->index) || IS_TERM(f->index)) {
    return {f, g};
  }
  bbdd_cases_t extend_case = compare_nodes(f, g, table->cvo);
  bbdd_node_t *f_neq = table->get_node_p(f->neq_child),
              *f_eq = table->get_node_p(f->eq_child),
              *g_neq = table->get_node_p(g->neq_child),
              *g_eq = table->get_node_p(g->eq_child);
  bbdd_node_t *new_f, *new_g, *extended_f, *extended_g;
  bbdd_node_ppair_t new_neq, new_eq;
  switch (extend_case) {
  case case_0:
    new_neq = extend_bbdds(table, f_neq, g_neq);
    new_eq = extend_bbdds(table, f_eq, g_eq);
    new_f = table->insert_node({f->cvo_lvl, new_neq.f->index, new_eq.f->index});
    new_g = table->insert_node({g->cvo_lvl, new_neq.g->index, new_eq.g->index});
    table->extend_table[key] = {new_f, new_g};
    return {new_f, new_g};
  case case_1f:
    new_neq = extend_bbdds(table, f_neq, g);
    new_eq = extend_bbdds(table, f_eq, g);
    new_f = table->insert_node({f->cvo_lvl, new_neq.f->index, new_eq.f->index});
    new_g = table->insert_node({f->cvo_lvl, new_neq.g->index, new_eq.g->index});
    table->extend_table[key] = {new_f, new_g};
    return {new_f, new_g};
  case case_1g:
    new_neq = extend_bbdds(table, f, g_neq);
    new_eq = extend_bbdds(table, f, g_eq);
    new_f = table->insert_node({g->cvo_lvl, new_neq.f->index, new_eq.f->index});
    new_g = table->insert_node({g->cvo_lvl, new_neq.g->index, new_eq.g->index});
    table->extend_table[key] = {new_f, new_g};
    return {new_f, new_g};
  case case_2f:
    extended_f = extend_node(table, f, g, case_2f);
    extended_g = extend_node(table, g, f, case_2g);
    new_neq = extend_bbdds(table, table->get_node_p(extended_f->neq_child),
                           extended_g);
    new_eq = extend_bbdds(table, table->get_node_p(extended_f->eq_child),
                          extended_g);
    new_f = table->insert_node(
        {extended_f->cvo_lvl, new_neq.f->index, new_eq.f->index});
    new_g = table->insert_node(
        {extended_f->cvo_lvl, new_neq.g->index, new_eq.g->index});
    table->extend_table[key] = {new_f, new_g};
    return {new_f, new_g};
  case case_2g:
    extended_f = extend_node(table, f, g, case_2g);
    extended_g = extend_node(table, g, f, case_2f);
    new_neq = extend_bbdds(table, extended_f,
                           table->get_node_p(extended_g->neq_child));
    new_eq = extend_bbdds(table, extended_f,
                          table->get_node_p(extended_g->eq_child));
    new_f = table->insert_node(
        {extended_g->cvo_lvl, new_neq.f->index, new_eq.f->index});
    new_g = table->insert_node(
        {extended_g->cvo_lvl, new_neq.g->index, new_eq.g->index});
    table->extend_table[key] = {new_f, new_g};
    return {new_f, new_g};
  case case_3f:
    extended_f = extend_node(table, f, g, case_3f);
    new_neq = extend_bbdds(table, table->get_node_p(extended_f->neq_child), g);
    new_eq = extend_bbdds(table, table->get_node_p(extended_f->eq_child), g);
    new_f = table->insert_node(
        {extended_f->cvo_lvl, new_neq.f->index, new_eq.f->index});
    new_g = table->insert_node(
        {extended_f->cvo_lvl, new_neq.g->index, new_eq.g->index});
    table->extend_table[key] = {new_f, new_g};
    return {new_f, new_g};
  case case_3g:
    extended_g = extend_node(table, g, f, case_3f);
    new_neq = extend_bbdds(table, f, table->get_node_p(extended_g->neq_child));
    new_eq = extend_bbdds(table, f, table->get_node_p(extended_g->eq_child));
    new_f = table->insert_node(
        {extended_g->cvo_lvl, new_neq.f->index, new_eq.f->index});
    new_g = table->insert_node(
        {extended_g->cvo_lvl, new_neq.g->index, new_eq.g->index});
    table->extend_table[key] = {new_f, new_g};
    return {new_f, new_g};
  case case_4f:
    extended_f = extend_node(table, f, g, case_4f);
    new_neq = extend_bbdds(table, table->get_node_p(extended_f->neq_child), g);
    new_eq = extend_bbdds(table, table->get_node_p(extended_f->eq_child), g);
    new_f = table->insert_node(
        {extended_f->cvo_lvl, new_neq.f->index, new_eq.f->index});
    new_g = table->insert_node(
        {extended_f->cvo_lvl, new_neq.g->index, new_eq.g->index});
    table->extend_table[key] = {new_f, new_g};
    return {new_f, new_g};
  case case_4g:
    extended_g = extend_node(table, g, f, case_4f);
    new_neq = extend_bbdds(table, f, table->get_node_p(extended_g->neq_child));
    new_eq = extend_bbdds(table, f, table->get_node_p(extended_g->eq_child));
    new_f = table->insert_node(
        {extended_g->cvo_lvl, new_neq.f->index, new_eq.f->index});
    new_g = table->insert_node(
        {extended_g->cvo_lvl, new_neq.g->index, new_eq.g->index});
    table->extend_table[key] = {new_f, new_g};
    return {new_f, new_g};
  case case_5f:
    extended_f = extend_node(table, f, g, case_5f);
    new_neq =
        extend_bbdds(table, table->get_node_p(extended_f->neq_child), g_neq);
    new_eq = extend_bbdds(table, table->get_node_p(extended_f->eq_child), g_eq);
    new_f = table->insert_node(
        {extended_f->cvo_lvl, new_neq.f->index, new_eq.f->index});
    new_g = table->insert_node(
        {extended_f->cvo_lvl, new_neq.g->index, new_eq.g->index});
    table->extend_table[key] = {new_f, new_g};
    return {new_f, new_g};
  case case_5g:
    extended_g = extend_node(table, g, f, case_5f);
    new_neq =
        extend_bbdds(table, f_neq, table->get_node_p(extended_g->neq_child));
    new_eq = extend_bbdds(table, f_eq, table->get_node_p(extended_g->eq_child));
    new_f = table->insert_node(
        {extended_g->cvo_lvl, new_neq.f->index, new_eq.f->index});
    new_g = table->insert_node(
        {extended_g->cvo_lvl, new_neq.g->index, new_eq.g->index});
    table->extend_table[key] = {new_f, new_g};
    return {new_f, new_g};
  default:
    assert(false && "not implemented");
  }
}

/**
 * @brief recursive helper function to merge two bbdds
 *
 * @param table in which the two bbdds are stored and in which the result should
 * be inserted
 * @param f first bbdd root node
 * @param g second bbdd root node
 * @param op Boolean operation that should be used to merge the two bbdds
 * @return root node to subgraph that is the result of the merge
 */
static bbdd_node_t *merge_recursive(Unique_table *table, bbdd_node_t *f,
                                    bbdd_node_t *g, bbdd_op_t op) {
  bbdd_node_t *new_root, *new_neq, *new_eq, *insert_neq, *insert_eq;
  if (IS_TERM(g->index)) {
    if (IS_TERM(f->index)) {
      return table->get_node_p(
          merge_two_terminal_base_case(f->index, g->index, op));
    } else {
      return merge_one_terminal_base_case(table, f, g->index, op);
    }
  } else if (IS_TERM(f->index)) {
    return merge_one_terminal_base_case(table, g, f->index, op);
  }
  if (f == g) {
    return merge_equal_base_case(table, f, op);
  }
  bbdd_cases_t bbdd_case = compare_nodes(f, g, table->cvo);
  if (bbdd_case != case_0) {
    printf("[ERROR] MERGE: error case %s should not happen with %d and %d\n",
           bbdd_cases_s[bbdd_case].c_str(), f->index, g->index);
    dump_node(f);
    std::cout << "\n";
    dump_node(g);
    std::cout << "\n";
    table->dump_table();
  }
  assert(bbdd_case == case_0);
  assert(f->cvo_lvl.pv == g->cvo_lvl.pv && f->cvo_lvl.sv == g->cvo_lvl.sv);
  assert(f->cvo_lvl.sv == INT_MAX ||
         POS(f->cvo_lvl.pv, table->cvo) < POS(f->cvo_lvl.sv, table->cvo));
  new_neq = merge_recursive(table, table->get_node_p(f->neq_child),
                            table->get_node_p(g->neq_child), op);
  new_eq = merge_recursive(table, table->get_node_p(f->eq_child),
                           table->get_node_p(g->eq_child), op);
  new_root = table->insert_node({f->cvo_lvl, new_neq->index, new_eq->index});
  return new_root;
}

/**
 * @brief delete the bbdd from the table if it does not have any other external
 * references
 *
 * @param table in which the bbdd is stored
 * @param f root node of a bbdd that should be deleted
 */
inline void delete_bbdd(Unique_table *table, bbdd_node_t *f) {
  if (IS_TERM(f->index)) {
    return;
  }
  if (f->ref == 0) {
    table->delete_node(f);
    del_ref(table, table->get_node_p(f->neq_child));
    delete_bbdd(table, table->get_node_p(f->neq_child));
    del_ref(table, table->get_node_p(f->eq_child));
    delete_bbdd(table, table->get_node_p(f->eq_child));
  }
}

/**
 * @brief merge two existing bbdds into a single one based on a given Boolean
 * operation
 *
 * @param table hash table in which both bbdds are stored
 * @param f first bbdd
 * @param g second bbdd
 * @param op Boolean operation that is used for the merge
 * @return root node of the resulting bbdd
 */
inline bbdd_node_t *merge_bbdds(Unique_table *table, bbdd_node_t *f,
                                bbdd_node_t *g, bbdd_op_t op) {
#ifdef DEBUG_BBDD
  printf("[INFO]-----------------------------------------------\n");
  printf("[INFO] Extending %d\n", f->index);
  dump_node(f);
  printf("\n");
  printf("[INFO]-----------------------------------------------\n");
  printf("[INFO] Extending %d \n", g->index);
  dump_node(g);
  printf("\n");
#endif
  merge_key key = {f, g, op};
  auto res = table->computed_table.find(key);
#ifdef CACHE_STATS
  table->cache_stats.merge_lookups++;
#endif
  if (res != table->computed_table.end()) {
#ifdef CACHE_STATS
    table->cache_stats.merge_hits++;
#endif
#ifdef DEBUG
    printf("[INFO] UNIQUE TABLE: %d %s %d\n", f->index, bbdd_op_s[op].c_str(),
           g->index);
#endif
    bbdd_node_t *node = table->get_node_p(res->second);
    assert(node->cvo_lvl.sv == INT_MAX ||
           POS(node->cvo_lvl.pv, table->cvo) <
               POS(node->cvo_lvl.sv, table->cvo));
    return node;
  }
  bbdd_node_ppair_t extended_nodes = extend_bbdds(table, f, g);
  bbdd_node_t *new_root =
      merge_recursive(table, extended_nodes.f, extended_nodes.g, op);
  table->computed_table[key] = new_root->index;
  return table->reduce_bbdd(new_root);
}

/**
 * @brief merge bbdd with a primary input based on a given Boolean operation
 *
 * @param table in which the provided bbdd is stored and the newly created is
 * inserted
 * @param f root node to the bbdd that should be merged
 * @param g_i primary input to be used for the merge
 * @param op Boolean operation for the merge operation
 * @return root node to the resulting bbdd
 */
inline bbdd_node_t *merge_bbdds(Unique_table *table, bbdd_node_t *f,
                                node_index_t g_i, bbdd_op_t op) {
  bbdd_node_t *g = table->insert_node({{g_i, INT_MAX}, 0, 1});
  return merge_bbdds(table, f, g, op);
}

/**
 * @brief sifting algorithm based on a given target function. Implementation is
 * based on the original paper by Bryant
 *
 * @param table hash table in which the bbdd nodes should be sifted
 * @param obj target function which should be minimized
 */
inline void sift(Unique_table *table, uint32_t (Unique_table::*f)(),
                 Unique_table *obj) {
  table->clear_computed_table();
  table->clear_extend_table();
  for (int variable = 0; variable < table->cvo->size(); variable++) {
    int original_pos = POS(variable, table->cvo);
    int best_pos = original_pos;
    uint32_t initial_height = (obj->*f)();
    uint32_t best_height = (obj->*f)();
#ifdef DEBUG_SIFT
    printf("initial best height for variable %d: %d at %d\n", variable,
           best_height, best_pos);
    table->dump_outputs();
#endif

    // Move variable up step by step
    int current_pos = original_pos;
    while (current_pos > 0) {
      table->swap_all_positions(current_pos - 1, current_pos);
      uint32_t current_height = (obj->*f)();
#ifdef DEBUG_SIFT
      printf("height: %d at pos: %d\n", current_height, current_pos - 1);
#endif
      if (current_height < best_height) {
        best_height = current_height;
        best_pos = current_pos - 1;
      }
      current_pos--;
    }
    assert(current_pos == 0);

    // Move variable down step by step
    while (current_pos < table->cvo->size() - 1) {
      table->swap_all_positions(current_pos, current_pos + 1);
      uint32_t current_height = (obj->*f)();
#ifdef DEBUG_SIFT
      printf("height: %d at pos: %d\n", current_height, current_pos + 1);
#endif
      if (current_height < best_height) {
        best_height = current_height;
        best_pos = current_pos + 1;
      }
      current_pos++;
    }
    assert(current_pos == table->cvo->size() - 1);

    // Restore best position
    while (current_pos > best_pos) {
      table->swap_all_positions(current_pos - 1, current_pos);
      current_pos--;
    }
#ifdef DEBUG_SIFT
    printf("best pos of variable %d: %d with height: %d\n", variable, best_pos,
           table->get_total_height());
    dump_ordering(table->cvo);
    table->dump_outputs();
#endif
  }
}

/**
 * @brief sift algorithm that uses the bbdd height as a target function.
 * Implementation is based on the work by Bryant
 *
 * @param table in which the bbdd nodes should be sifted
 */
inline void sift(Unique_table *table) {
  for (int variable = 0; variable < table->cvo->size(); variable++) {
    int original_pos = POS(variable, table->cvo);
    int best_pos = original_pos;
    uint32_t initial_height = table->get_total_height();
    uint32_t best_height = table->get_total_height();
#ifdef DEBUG_SIFT
    printf("initial best height for variable %d: %d at %d\n", variable,
           best_height, best_pos);
    table->dump_outputs();
#endif

    // Move variable up step by step
    int current_pos = original_pos;
    while (current_pos > 0) {
      table->swap_all_positions(current_pos - 1, current_pos);
      uint32_t current_height = table->get_total_height();
#ifdef DEBUG_SIFT
      printf("height: %d at pos: %d\n", current_height, current_pos - 1);
#endif
      if (current_height < best_height) {
        best_height = current_height;
        best_pos = current_pos - 1;
      }
      current_pos--;
    }
    assert(current_pos == 0);

    // Move variable down step by step
    while (current_pos < table->cvo->size() - 1) {
      table->swap_all_positions(current_pos, current_pos + 1);
      uint32_t current_height = table->get_total_height();
#ifdef DEBUG_SIFT
      printf("height: %d at pos: %d\n", current_height, current_pos + 1);
#endif
      if (current_height < best_height) {
        best_height = current_height;
        best_pos = current_pos + 1;
      }
      current_pos++;
    }
    assert(current_pos == table->cvo->size() - 1);

    // Restore best position
    /*while (current_pos < best_pos) {
      table->swap_all_positions(current_pos, current_pos + 1);
      current_pos++;
    }*/
    while (current_pos > best_pos) {
      table->swap_all_positions(current_pos - 1, current_pos);
      current_pos--;
    }
#ifdef DEBUG_SIFT
    printf("best pos of variable %d: %d with height: %d\n", variable, best_pos,
           table->get_total_height());
    dump_ordering(table->cvo);
    table->dump_outputs();
#endif
  }
}

/**
 * @brief sift a single bbdd
 *
 * @param table hash table in which the bbdd is stored and the result will be inserted
 * @param node root node of the input bbdd
 * @return  root node of the resulting bbdd
 */
inline bbdd_node_t *sift_bbdd(Unique_table *table, bbdd_node_t *node) {
  bbdd_node_t *new_root = node;
  for (int variable = 0; variable < table->cvo->size(); variable++) {
    int original_pos = POS(variable, table->cvo);
    int best_pos = original_pos;
    uint32_t best_height = table->get_tree_height(new_root);
    printf("initial best height: %d\n", best_height);

    // Move variable up step by step
    int current_pos = original_pos;
    while (current_pos > 0) {
      new_root = table->reduce_bbdd(
          table->swap_positions(new_root, current_pos - 1, current_pos));

      uint32_t current_height = table->get_tree_height(node);
      if (current_height < best_height) {
        best_height = current_height;
        best_pos = current_pos - 1;
      }
      current_pos--;
    }

    // Restore variable to original position
    while (current_pos < original_pos) {
      new_root = table->reduce_bbdd(
          table->swap_positions(new_root, current_pos, current_pos + 1));
      current_pos++;
    }

    // Move variable down step by step
    current_pos = original_pos;
    while (current_pos < table->cvo->size() - 1) {
      new_root = table->reduce_bbdd(
          table->swap_positions(new_root, current_pos, current_pos + 1));

      uint32_t current_height = table->get_tree_height(new_root);
      if (current_height < best_height) {
        best_height = current_height;
        best_pos = current_pos + 1;
      }
      current_pos++;
    }

    // Restore variable to original position
    while (current_pos > original_pos) {
      new_root = table->reduce_bbdd(
          table->swap_positions(new_root, current_pos - 1, current_pos));
      current_pos--;
    }

    // Finally move variable to best position
    while (original_pos < best_pos) {
      new_root = table->reduce_bbdd(
          table->swap_positions(new_root, original_pos, original_pos + 1));
      original_pos++;
    }
    while (original_pos > best_pos) {
      new_root = table->reduce_bbdd(
          table->swap_positions(new_root, original_pos - 1, original_pos));
      original_pos--;
    }
    // printf("best pos of variable %d: %d with height: %d\n", variable,
    // best_pos, table->get_tree_height(new_root)); dump_ordering(table->cvo);
  }
  return new_root;
}