// Copyright 2025 Oliver Theimer
#pragma once
#include <climits>
#include <cstdint>

#include "../bbdd/include/bbdd.hpp"
#include "../bbdd/include/bbdd_node.hpp"
#include "../bbdd/include/unique_table.hpp"
#include "mockturtle/traits.hpp"
#include "util.hpp"

#define LEFT_CHILD(node) node.children[0].index
#define RIGHT_CHILD(node) node.children[1].index

#define CUBE(node) ntk._storage->data.covers[node.data[1].h1]

int nodes_visited;

using namespace mockturtle;

/**
 * @brief recursively creates a bbdd based on the given network
 *
 * @tparam Ntk template for which network type is used
 * @param table unique table in which the bbdd should be stored in
 * @param ntk input network data structure that should be converted
 * @param node_i starting node from which onwards the bbdd should be created,
 * will be used for the recursion
 * @param output_completed statistics that are used in the recursion to properly
 * show the progress bar
 * @return root node of the created bbdd
 */
template <typename Ntk>
static bbdd_node_t *create_bbdd(Unique_table *table, Ntk &ntk,
                                const auto &node_i, int output_completed) {
  static_assert(has_is_ci_v<Ntk>, "Ntk does not implement the is_ci method");
  const auto &node = ntk._storage->nodes[node_i];
  bbdd_node_t *f, *g, *result;
  bbdd_op_t op = Util::cube_to_bbdd_op(CUBE(node));
  if (ntk.visited(node_i)) {
    return table->get_node_p(ntk.visited(node_i));
  }
#ifdef DEBUG_COVER
  printf("[INFO] CREATE: node %d with op %s\n", node_i, bbdd_op_s[op].c_str());
#endif
  if (node.children.size() != 2 && node.children.size() != 1) {
    if (node_i == 1 || node_i == 0) {
      return table->get_node_p(node_i);
    }
#ifdef DEBUG_COVER
    std::cout << node_i << ": " << node.children.size() << " with "
              << bbdd_op_s[op].c_str() << "\n";
#endif
    assert(ntk.is_ci(node_i));
    assert(node_i < pow(2, 31));
    assert(node_i - 2 < ntk._storage->inputs.size());
    return table->insert_node({{(node_index_t)node_i, INT_MAX}, 0, 1});
  }
  assert(node.children.size() == 2 || node.children.size() == 1);
  // all the logic gates except buf and inv
  if (node.children.size() == 2) {
    node_index_t f_i = LEFT_CHILD(node), g_i = RIGHT_CHILD(node);
    if (ntk.is_ci(LEFT_CHILD(node)) && ntk.is_ci(RIGHT_CHILD(node))) {
      result = base_case_two_inputs(table, f_i, g_i, op);
#ifdef DEBUG_COVER
      printf("[INFO] CREATE: two input case %d: %d %s %d\n", result->index, f_i,
             bbdd_op_s[op].c_str(), g_i);
#endif
      return result;
    }
    f = create_bbdd(table, ntk, LEFT_CHILD(node), output_completed);
    g = create_bbdd(table, ntk, RIGHT_CHILD(node), output_completed);
    result = merge_bbdds(table, f, g, op);
#ifdef DEBUG_COVER
    std::cout << "[INFO] CREATE: merging " << result->index << ": " << f->index
              << " " << bbdd_op_s[op] << " " << g->index << "\n";
    dump_node(g);
#endif
    ntk.set_visited(node_i, result->index);
    Util::show_progress_bar(
        {{"Output", {output_completed, ntk._storage->outputs.size()}},
         {"Nodes", {++nodes_visited, ntk._storage->nodes.size()}}},
        50);
    return result;
  } else {
    // buf and inverter nodes
    f = create_bbdd(table, ntk, LEFT_CHILD(node), output_completed);
    if (op == bbdd_inv) {
      result = negate_recursive(table, f);
      ntk.set_visited(node_i, result->index);
      Util::show_progress_bar(
          {{"Output", {output_completed, ntk._storage->outputs.size()}},
           {"Nodes", {++nodes_visited, ntk._storage->nodes.size()}}},
          50);
      return result;
    }
    ntk.set_visited(node_i, f->index);
    Util::show_progress_bar(
        {{"Output", {output_completed, ntk._storage->outputs.size()}},
         {"Nodes", {++nodes_visited, ntk._storage->nodes.size()}}},
        50);
    return f;
  }
}

/**
 * @brief main conversion function that should be used as an interface, it
 * interact with the recursive function, instantiates the progress bar and
 * registers output in the unique table
 *
 * @tparam Ntk template of network type that should be used
 * @param table unique table in which the data structure should be stores
 * @param ntk data strucutre that stores the input network type which should be
 * converted
 * @param use_height if true the height of the bbdd is used as the target
 * function for the sifting algorithm, otherwise the number of nodes i used
 * @param sifting_repetitions indicates how often the sifting algorithm should be repeated at the end of the conversion
 */
template <typename Ntk>
void cover_to_bbdd(Unique_table *table, Ntk &ntk, bool use_height,
                   int sifting_repetitions) {

  static_assert(has_foreach_co_v<Ntk>,
                "Ntk does not implement the foreach_pi method");
  static_assert(has_get_node_v<Ntk>,
                "Ntk does not implement the get_node method");
  static_assert(has_set_visited_v<Ntk>,
                "Ntk does not implement the set_visited method");
  static_assert(has_visited_v<Ntk>,
                "Ntk does not implement the set_visited method");
  int index = ntk._storage->inputs.size() + 2;
  int output_completed = 0;
  nodes_visited = 0;
  Util::show_progress_bar(
      {{"Output", {output_completed, ntk._storage->outputs.size()}},
       {"Nodes", {++nodes_visited, ntk._storage->nodes.size()}}},
      50);
  ntk.foreach_co([ntk, &table, &index, &output_completed,
                  sifting_repetitions](const auto &node_i) {
    const auto &node = ntk.get_node(node_i);
    auto &n = ntk._storage->nodes[node_i];
#ifdef DEBUG_COVER
    std::cout << "output with node_i: " << node_i << " and n->index: " << " : "
              << n.children.size() << "\n";
#endif
    bbdd_node_t *output =
        add_ref(create_bbdd(table, ntk, node, output_completed));
    Util::show_progress_bar(
        {{"Output", {++output_completed, ntk._storage->outputs.size()}},
         {"Nodes", {++nodes_visited, ntk._storage->nodes.size()}}},
        50);
    table->add_output(ntk.get_signal_name(index), output);
    index++;
  });
  for (int i = 0; i < sifting_repetitions; i++) {
    if (table->get_total_height() < 30) {
      if (use_height) {
        sift(table, &Unique_table::get_total_height, table);
      } else {
        sift(table, &Unique_table::get_total_number_nodes, table);
      }
    }
  }
}