// Copyright 2025 Oliver Theimer
#pragma once

#include "../bbdd/include/bbdd_node.hpp"
#include "bdd.h"
#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]

using namespace mockturtle;

/**
 * @brief recursively creates a bdd based on the given network
 *
 * @tparam Ntk which network type is used as an input to the function
 * @param ntk input network which should be converted to bdd
 * @param node_i current network node which is currently converted is used for
 * the recursion
 * @return return root bdd node of the created binary decision diagram
 */
template <typename Ntk> static bdd create_bdd(Ntk &ntk, const auto &node_i) {
  static_assert(has_is_ci_v<Ntk>, "Ntk does not implement the is_ci method");
  const auto &node = ntk._storage->nodes[node_i];
  bdd f, g, result;
  bbdd_op_t op = Util::cube_to_bbdd_op(CUBE(node));
  if (node.children.size() != 2 && node.children.size() != 1) {
    if (node_i == 1) {
#ifdef DEBUG_BDD
      printf("[INFO] cover to bdd: constant 1 node\n");
#endif
      return bdd_true();
    }
    if (node_i == 0) {
#ifdef DEBUG_BDD
      printf("[INFO] cover to bdd: constant 0 node\n");
#endif
      return bdd_false();
    }
    assert(ntk.is_ci(node_i));
    assert(node_i < pow(2, 31));
    assert(node_i - 2 < ntk._storage->inputs.size());
#ifdef DEBUG_BDD
    printf("[INFO] cover to bdd: base case input: %d\n", node_i);
#endif
    return bdd_ithvar(node_i - 2);
  }
  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);
    f = create_bdd(ntk, LEFT_CHILD(node));
#ifdef DEBUG_BDD
    printf("[INFO] cover to bdd: return from f\n");
#endif
    g = create_bdd(ntk, RIGHT_CHILD(node));
#ifdef DEBUG_BDD
    printf("[INFO] cover to bdd: merge %d %s %d\n", f, bbdd_op_s[op].c_str(),
           g);
#endif
    switch (op) {
    case bbdd_and:
      result = bdd_apply(f, g, bddop_and);
      break;
    case bbdd_xor:
      result = bdd_apply(f, g, bddop_xor);
      break;
    case bbdd_xnor:
      result = bdd_not(bdd_apply(f, g, bddop_xor));
      break;
    case bbdd_or:
      result = bdd_apply(f, g, bddop_or);
      break;
    case bbdd_nand:
      result = bdd_apply(f, g, bddop_nand);
      break;
    case bbdd_nor:
      result = bdd_apply(f, g, bddop_nor);
      break;
    default:
      printf("%s\n", bbdd_op_s[op].c_str());
      assert(false && "not implemented yet");
      break;
    }
    return result;
  } else {
    // buf and inverter nodes
    f = create_bdd(ntk, LEFT_CHILD(node));
    // TODO how to invert
    if (op == bbdd_inv) {
#ifdef DEBUG_BDD
      printf("[INFO] cover to bdd: negate\n");
#endif
      result = bdd_not(f);
      return result;
    }
#ifdef DEBUG_BDD
    printf("[INFO] cover to bdd: buffer\n");
#endif
    return f;
  }
}

/**
 * @brief main interface function that handles the conversion to a bdd from a given input network type
 *
 * @tparam Ntk network type that is used as an input to the conversion
 * @param ntk network that should be converted to a bdd
 * @param output_map outputmap that stores the pointers to the root nodes of each output in the network
 */
template <typename Ntk>
void cover_to_bdd(Ntk &ntk,
                  std::vector<std::pair<bdd, std::string>> &output_map) {

  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;
  ntk.foreach_co([ntk, &index, &output_map](const auto &node_i) {
    const auto &node = ntk.get_node(node_i);
    auto &n = ntk._storage->nodes[node_i];
    bdd output = create_bdd(ntk, node);
    output_map.emplace_back(output, ntk.get_signal_name(index));
    bdd_printtable(output);
    index++;
  });
}