// Copyright 2025 Oliver Theimer
#include <algorithm>
#include <cstdlib>
#include <filesystem>
#include <iostream>
#include <string>
#include <vector>
#include <cstdio>

#include <lorina/diagnostics.hpp>
#include <lorina/lorina.hpp>
#include <mockturtle/algorithms/cover_to_graph.hpp>
#include <mockturtle/mockturtle.hpp>

#include "bdd.h"
#include "mockturtle/io/write_blif.hpp"
#include "mockturtle/networks/cover.hpp"
#include "util/cover_to_bdd.hpp"

int write_blif_recursive(std::ofstream &blif_file, cover_network cover,
                         const BDD &node, int next_index, bool output) {
  if (node < 2) {
    return node;
  }
  int low_out =
      write_blif_recursive(blif_file, cover, bdd_low(node), next_index, false);
  int high_out = write_blif_recursive(blif_file, cover, bdd_high(node),
                                      next_index++, false);
  blif_file << ".names " << cover.signal_map[bdd_var(node)] << " ";
  if (IS_TERM(low_out)) {
    if (low_out == 0) {
      blif_file << "$false ";
    } else {
      blif_file << "$true ";
    }
  } else {
    blif_file << std::to_string(low_out);
  }
  blif_file << " ";
  if (IS_TERM(high_out)) {
    if (high_out == 0) {
      blif_file << "$false ";
    } else {
      blif_file << "$true ";
    }
  } else {
    blif_file << std::to_string(high_out) << " ";
  }
  /*blif_file << std::format(
      ".names {} {} {} {}", cover.signal_map[bdd_var(node)],
      IS_TERM(low_out) ? (low_out == 0 ? "$false" : "$true")
                       : std::to_string(low_out),
      IS_TERM(high_out) ? (high_out == 0 ? "$false" : "$true")
                        : std::to_string(high_out),
      !output ? std::to_string(node) : "");*/
  if (!output) {
    blif_file << std::to_string(node);
    blif_file << "\n0-1 1\n11- 1\n";
  }
  return node;
}

void write_blif(std::string filename, mockturtle::cover_network cover,
                std::vector<std::pair<bdd, std::string>> output_map) {
  std::ofstream blif_file(filename);
  blif_file << ".model " + cover.get_module_name() + "\n";
  blif_file << ".inputs";
  for (unsigned int i = 0; i < cover.signal_map.size(); i++) {
    blif_file << " " << cover.signal_map[i];
    if (i + 1 == cover._storage->inputs.size()) {
      blif_file << "\n.outputs";
    }
  }
  blif_file << "\n.names $true\n1\n";
  blif_file << ".names $false\n";
  int next_index = cover._storage->inputs.size() + 1;
  for (std::pair<bdd, std::string> out_map : output_map) {
    if (out_map.first == bdd_true()) {
      blif_file << ".names " << out_map.second << "\n1\n";
    } else if (out_map.first == bdd_false()) {
      blif_file << ".names " << out_map.second << "\n0\n";
    } else {
      write_blif_recursive(blif_file, cover, out_map.first.id(), next_index,
                           true);
      blif_file << out_map.second << "\n0-1 1\n11- 1\n";
    }
  }
  blif_file << ".end\n";
}

int get_bdd_height(BDD node) {
  if (node < 2) {
    return 0;
  }
  int low_height = get_bdd_height(bdd_low(node));
  int high_height = get_bdd_height(bdd_high(node));
  return std::max(low_height, high_height) + 1;
}

int get_total_height(std::vector<std::pair<bdd, std::string>> output_map) {
  int max_height = -1;
  for (std::pair<bdd, std::string> out_map : output_map) {
    int current_height = get_bdd_height(out_map.first.id());
    if (current_height > max_height) {
      max_height = current_height;
    }
  }
  return max_height;
}

int main(int argc, char *argv[]) {
  if (optind >= argc) {
    std::cout << "[ERROR] input file in blif format is missing\n";
    std::cerr << "[INFO] Usage: " << argv[0] << " <blif-file>" << std::endl;
    return EXIT_FAILURE;
  }

  std::string benchmark(argv[optind]);
  if (!std::filesystem::exists(benchmark)) {
    std::cout << "[ERROR] File does not exist\n";
    return EXIT_FAILURE;
  }

  std::filesystem::path path(benchmark);
  std::string base_name = path.stem().string();

  mockturtle::cover_network cover;
  // lorina::diagnostic_engine diag;

  if (lorina::read_blif(benchmark, mockturtle::blif_reader(cover)) !=
      lorina::return_code::success) {
    std::cout << "[ERROR] While Lorina tried to read in file\n";
    return EXIT_FAILURE;
  }

  std::vector<std::pair<bdd, std::string>> output_map;

  bdd_init(300000, 10000);
  bdd_setvarnum(cover._storage->inputs.size());
  bdd_autoreorder(BDD_REORDER_SIFT);
  printf("[INFO] init with %zu variables\n", cover._storage->inputs.size());
  cover_to_bdd(cover, output_map);
  // bdd_reorder_siftite is the same but repeats until no more progress is done
  bdd_reorder(BDD_REORDER_SIFT);
  printf("height after: %d\n", get_total_height(output_map));
  write_blif("temp/" + base_name + "_bdd.blif", cover, output_map);
  bdd_done();
  return EXIT_SUCCESS;
}