// Copyright 2025 Oliver Theimer
#pragma once

#include <cassert>
#include <climits>
#include <cstdint>
#include <cstdio>
#include <iostream>

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

#define IS_TERM(n) n == 0 || n == 1

#define MARK_ON 0x80000000
#define MARK_OFF 0x7FFFFFFF
#define MARKED(n) n->index &MARK_ON
#define GET_INDEX(n) n->index &MARK_OFF
#define SET_MARKED(n) n->index |= MARK_ON
#define CLEAR_MARKED(n) n->index &= MARK_OFF

/**
 * @class bbdd_node_t
 * @brief main bbdd storage element
 *
 */
struct bbdd_node_t {
  uint32_t ref;
  node_index_t index;
  cvo_pair_t cvo_lvl;
  bbdd_halfword_t neq_child;
  bbdd_halfword_t eq_child;
};

/**
 * @class bbdd_node_template_t
 * @brief minimal storage element with information that is needed to insert a
 * bbdd node into the hash table
 *
 */
struct bbdd_node_template_t {
  cvo_pair_t cvo_lvl;
  node_index_t neq_child;
  node_index_t eq_child;
};

/**
 * @class bbdd_node_ppair_t
 * @brief combination of two pointers to bbdd_nodes. Only used for the extension
 * of the bbdds
 *
 */
struct bbdd_node_ppair_t {
  bbdd_node_t *f;
  bbdd_node_t *g;
};

/**
 * @brief comparison of a bbdd_node_t and a bbdd_node_template_t that wants to
 * be inserted into the hash table
 *
 * @param lhs bbdd node
 * @param rhs bbdd node template
 * @return boolean whether or not the two equal
 */
bool inline node_eq(bbdd_node_t lhs, bbdd_node_template_t rhs) {
  return lhs.cvo_lvl.pv == rhs.cvo_lvl.pv && lhs.cvo_lvl.sv == rhs.cvo_lvl.sv &&
         lhs.eq_child == rhs.eq_child && lhs.neq_child == rhs.neq_child;
}

/**
 * @brief checks the equivalence of two bbdd nodes
 *
 * @param lhs bbdd node
 * @param rhs bbdd node
 * @return boolean whether or not the two equal
 */
bool inline node_eq(bbdd_node_t lhs, bbdd_node_t rhs) {
  return lhs.cvo_lvl.pv == rhs.cvo_lvl.pv && lhs.cvo_lvl.sv == rhs.cvo_lvl.sv &&
         lhs.eq_child == rhs.eq_child && lhs.neq_child == rhs.neq_child;
}

/**
 * @brief cantor pairing implementation based on the original paper on bbdd by
 * Amaru et al.
 *
 * @param i value for calculation
 * @param j value for calculation
 * @return result of the cantor_pairing function
 */
static bbdd_halfword_t inline cantor_pairing(uint32_t i, uint32_t j) {
  return (bbdd_halfword_t)(0.5f * (i + j) * (i + j + 1)) + i;
}

/**
 * @brief hashing function a bbdd node template
 *
 * @param node_t bbdd node template information
 * @param capacity capacity of the hash table
 * @return hashing value for the given node and capacity
 */
uint32_t inline hash_node(bbdd_node_template_t node_t, uint64_t capacity) {
  return cantor_pairing(node_t.neq_child,
                        cantor_pairing(node_t.cvo_lvl.pv,
                                       cantor_pairing(node_t.cvo_lvl.sv,
                                                      node_t.eq_child))) %
         capacity;
}

/**
 * @brief hashing function for a bbdd node
 *
 * @param node bbdd node to be hashed
 * @param capacity capacity of the hash table
 * @return
 */
uint32_t inline hash_node(bbdd_node_t node, uint64_t capacity) {
  return hash_node({node.cvo_lvl, node.neq_child, node.eq_child}, capacity);
}

/**
 * @brief dump formatted node information to stdout
 *
 * @param node to be printed
 */
void inline dump_node(bbdd_node_t *node) {
  fprintf(stdout, "%3d: (%3d, (%3d, %3d), %3d, %3d)", GET_INDEX(node),
          node->ref, node->cvo_lvl.pv == INT_MAX ? 1 : node->cvo_lvl.pv,
          node->cvo_lvl.sv == INT_MAX ? 1 : node->cvo_lvl.sv, node->neq_child,
          node->eq_child);
}

/**
 * @brief compare two nodes based on there primary and secondary variable and
 * return the information how these intervals intersect
 *
 * @param f first bbdd node
 * @param g second bbdd node
 * @param cvo chain variable ordering for which the two bbdds should be assessed
 * @return case in which way the two intervals intersect
 */
inline bbdd_cases_t compare_nodes(bbdd_node_t *f, bbdd_node_t *g, cvo_t *cvo) {
#ifdef DEBUG
  printf("[INFO] COMPARE: ");
  dump_node(f);
  std::cout << " and ";
  dump_node(g);
  std::cout << "\n";
#endif
  // f.pv = i, f.sv = j
  // g.pv = k, g.sv = l
  uint32_t i = POS(f->cvo_lvl.pv, cvo), k = POS(g->cvo_lvl.pv, cvo);
  uint32_t j, l;
  if (f->cvo_lvl.sv != INT_MAX) {
    j = POS(f->cvo_lvl.sv, cvo);
  } else {
    j = INT_MAX;
  }
  if (g->cvo_lvl.sv != INT_MAX) {
    l = POS(g->cvo_lvl.sv, cvo);
  } else {
    l = INT_MAX;
  }
  if (!((i < j) && (k < l))) {
    dump_ordering(cvo);
    printf("i:%d, j:%d, k:%d, l:%d\n", i, j, k, l);
    dump_node(f);
    printf("\n");
    dump_node(g);
    printf("\n");
  }
  assert((i < j) && (k < l));
  // assumption i < j and k < j
  if ((i == k) && (j == l)) {
    return case_0;
    // Case 1
  } else if (j <= k) {
    return case_1f;
  } else if (l <= i) {
    return case_1g;
    // Case 2
  } else if ((i < k) && (k < j) && (j < l)) {
    return case_2f;
  } else if ((k < i) && (i < l) && (l < j)) {
    return case_2g;
    // Case 3
  } else if ((i < k) && (j == l)) {
    return case_3f;
  } else if ((k < i) && (j == l)) {
    return case_3g;
    // Case 4
  } else if ((i < k) && (k < l) && (l < j)) {
    return case_4f;
  } else if ((k < i) && (i < j) && (j < l)) {
    return case_4g;
    // Case 5
  } else if ((i == k) && (l < j)) {
    return case_5f;
  } else if ((i == k) && (j < l)) {
    return case_5g;
  }
  return case_not_implemented;
}