// Programa principal del laboratorio. No hace falta cambiar este archivo: ustedes escriben encode y
// decode en solution.cpp, y este archivo los conecta con minisat.
//
//   build/solution                  lee el sudoku de stdin, llama a encode, corre minisat, llama a decode
//   build/solution --encode         lee el sudoku de stdin y escribe la fórmula en stdout
//   build/solution --decode G R     lee el sudoku del archivo G y la respuesta de minisat del archivo R
//
// Antes de pasarle la fórmula a minisat, se revisa que sea DIMACS correcto. minisat solo avisa cuando
// el encabezado no coincide, y aquí eso es un error: el programa termina con código 2.
#ifndef DRIVER_H
#define DRIVER_H

#include <cstdio>
#include <cstdlib>
#include <filesystem>
#include <fstream>
#include <iostream>
#include <sstream>
#include <string>
#include <vector>

#include <sys/wait.h>
#include <unistd.h>

struct Sudoku {
    int k = 0;                            // lado de una caja
    int n = 0;                            // lado del tablero: n = k · k
    std::vector<std::vector<int>> cells;  // n filas de n valores; 0 es una celda vacía
};

using Encoder = void (*)(const Sudoku&, std::ostream&);
using Decoder = void (*)(const Sudoku&, std::istream&, std::ostream&);

inline Sudoku read_sudoku(std::istream& in) {
    Sudoku s;
    if (!(in >> s.k) || s.k < 1) {
        std::cerr << "entrada: falta k\n";
        std::exit(2);
    }
    s.n = s.k * s.k;
    s.cells.assign(s.n, std::vector<int>(s.n, 0));
    for (auto& row : s.cells) {
        for (int& value : row) {
            if (!(in >> value) || value < 0 || value > s.n) {
                std::cerr << "entrada: valor fuera de rango\n";
                std::exit(2);
            }
        }
    }
    return s;
}

// Devuelve "" si el texto es una fórmula DIMACS con exactamente n³ variables y con tantas cláusulas
// como dice su encabezado. Si no, devuelve qué está mal.
inline std::string dimacs_error(const std::string& text, long long variables) {
    std::size_t i = 0;
    const std::size_t size = text.size();
    auto next_line = [&] {
        while (i < size && text[i] != '\n') i++;
        if (i < size) i++;
    };
    auto skip_space = [&] {
        while (i < size && (text[i] == ' ' || text[i] == '\t' || text[i] == '\n' || text[i] == '\r')) i++;
    };
    skip_space();
    while (i < size && text[i] == 'c') {
        next_line();
        skip_space();
    }
    std::size_t end = text.find('\n', i);
    std::istringstream header(text.substr(i, end == std::string::npos ? end : end - i));
    std::string p, cnf;
    long long declared_vars = 0, declared_clauses = 0;
    if (!(header >> p >> cnf >> declared_vars >> declared_clauses) || p != "p" || cnf != "cnf") {
        return "falta el encabezado: p cnf <variables> <cláusulas>";
    }
    if (declared_vars != variables) {
        return "el encabezado declara " + std::to_string(declared_vars) + " variables, y deben ser n³ = " +
               std::to_string(variables);
    }
    i = end == std::string::npos ? size : end;

    long long clauses = 0;
    bool open_clause = false;
    while (true) {
        skip_space();
        if (i >= size) break;
        bool negative = text[i] == '-';
        if (negative) i++;
        if (i >= size || text[i] < '0' || text[i] > '9') return "se esperaba un literal, y hay otra cosa";
        long long value = 0;
        while (i < size && text[i] >= '0' && text[i] <= '9') {
            value = value * 10 + (text[i] - '0');
            if (value > variables) return "un literal usa una variable mayor que " + std::to_string(variables);
            i++;
        }
        if (value == 0) {
            clauses++;
            open_clause = false;
        } else {
            open_clause = true;
        }
    }
    if (open_clause) return "la última cláusula no termina en 0";
    if (clauses != declared_clauses) {
        return "el encabezado declara " + std::to_string(declared_clauses) + " cláusulas, y hay " +
               std::to_string(clauses);
    }
    return "";
}

inline std::string encode_checked(const Sudoku& s, Encoder encode) {
    std::ostringstream formula;
    encode(s, formula);
    std::string text = formula.str();
    std::string error = dimacs_error(text, 1LL * s.n * s.n * s.n);
    if (!error.empty()) {
        std::cerr << "encode: " << error << "\n";
        std::exit(2);
    }
    return text;
}

inline int run_pipeline(Encoder encode, Decoder decode) {
    Sudoku s = read_sudoku(std::cin);
    std::string text = encode_checked(s, encode);

    // Archivos temporales propios: pueden correr varios programas a la vez.
    std::string pattern = (std::filesystem::temp_directory_path() / "sudoku_sat_XXXXXX").string();
    if (mkdtemp(pattern.data()) == nullptr) {
        std::cerr << "no se pudo crear la carpeta temporal\n";
        return 3;
    }
    const std::filesystem::path folder = pattern;
    const std::filesystem::path cnf_path = folder / "formula.cnf";
    const std::filesystem::path result_path = folder / "result.txt";
    {
        std::ofstream cnf(cnf_path);
        cnf << text;
    }
    std::string command = "minisat -verb=0 '" + cnf_path.string() + "' '" + result_path.string() + "' > /dev/null 2>&1";
    int status = std::system(command.c_str());
    // minisat termina con 10 si la fórmula es satisfacible y con 20 si no lo es.
    int code = WIFEXITED(status) ? WEXITSTATUS(status) : -1;
    if (code != 10 && code != 20) {
        std::cerr << "minisat terminó con el código " << code << "\n";
        std::filesystem::remove_all(folder);
        return 3;
    }
    {
        std::ifstream result(result_path);
        decode(s, result, std::cout);
    }
    std::filesystem::remove_all(folder);
    return 0;
}

inline int run_sudoku(int argc, char** argv, Encoder encode, Decoder decode) {
    const std::string mode = argc > 1 ? argv[1] : "";
    if (argc == 1) return run_pipeline(encode, decode);
    if (mode == "--encode" && argc == 2) {
        std::cout << encode_checked(read_sudoku(std::cin), encode);
        return 0;
    }
    if (mode == "--decode" && argc == 4) {
        std::ifstream grid(argv[2]), result(argv[3]);
        if (!grid || !result) {
            std::cerr << "no se pudo abrir un archivo\n";
            return 2;
        }
        decode(read_sudoku(grid), result, std::cout);
        return 0;
    }
    std::cerr << "uso: solution | solution --encode | solution --decode <sudoku> <respuesta>\n";
    return 2;
}

#endif