// Correr minisat desde C++: se escribe la fórmula en un archivo, se llama al programa y se lee su respuesta.
// mkdtemp y WEXITSTATUS no son C++ estándar: son de POSIX, y el entorno del curso los tiene.
#ifndef MINISAT_H
#define MINISAT_H

#include <cstdlib>
#include <filesystem>
#include <fstream>
#include <stdexcept>
#include <string>
#include <vector>

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

#include "cnf.h"

struct SatResult {
    bool satisfiable = false;
    int exit_code = 0;
    Assignment value;       // si satisfiable; una variable que no sale en la respuesta queda falsa
    std::string raw;        // el archivo de respuesta, tal cual
    std::string statistics; // lo que minisat escribe en la terminal
};

inline SatResult run_minisat(const Cnf& formula, const std::string& options = "-verb=0") {
    std::string pattern = (std::filesystem::temp_directory_path() / "week13_XXXXXX").string();
    if (mkdtemp(pattern.data()) == nullptr) throw std::runtime_error("no se pudo crear la carpeta temporal");
    const std::filesystem::path folder = pattern;
    {
        std::ofstream cnf(folder / "formula.cnf");
        cnf << formula.to_dimacs();
    }
    const std::string command = "minisat " + options + " '" + (folder / "formula.cnf").string() + "' '" +
                                (folder / "result.txt").string() + "' > '" + (folder / "log.txt").string() + "' 2>&1";
    int status = std::system(command.c_str());

    SatResult result;
    result.exit_code = WIFEXITED(status) ? WEXITSTATUS(status) : -1;
    auto slurp = [](const std::filesystem::path& path) {
        std::ifstream in(path);
        std::ostringstream all;
        all << in.rdbuf();
        return all.str();
    };
    result.raw = slurp(folder / "result.txt");
    result.statistics = slurp(folder / "log.txt");
    std::filesystem::remove_all(folder);
    if (result.exit_code != 10 && result.exit_code != 20) {
        throw std::runtime_error("minisat terminó con el código " + std::to_string(result.exit_code));
    }

    result.satisfiable = result.exit_code == 10;
    result.value.assign(formula.variables + 1, false);
    if (result.satisfiable) {
        std::istringstream in(result.raw);
        std::string verdict;
        in >> verdict;
        int literal;
        while (in >> literal && literal != 0) {
            if (literal > 0) result.value[literal] = true;
        }
    }
    return result;
}

#endif