// Pruebas de lo que afirman los apuntes.
#include <cassert>
#include <iostream>
#include <random>

#include "coloring.h"
#include "graphs.h"
#include "latin.h"
#include "minisat.h"

namespace {

Graph graph_from_mask(int n, unsigned mask) {
    Graph g{n, {}};
    int bit = 0;
    for (int u = 0; u < n; u++) {
        for (int v = u + 1; v < n; v++) {
            if ((mask >> bit++) & 1u) g.edges.emplace_back(u, v);
        }
    }
    return g;
}

Graph random_graph(int n, std::mt19937& rng) {
    const int pairs = n * (n - 1) / 2;
    unsigned mask = pairs == 0 ? 0 : static_cast<unsigned>(rng()) & ((1u << pairs) - 1);
    return graph_from_mask(n, mask);
}

// S es independiente si y solo si V − S es cobertura, para cada subconjunto.
void test_complement_lemma(const Graph& g) {
    const unsigned all = (1u << g.n) - 1;
    for (unsigned set = 0; set <= all; set++) {
        assert(is_independent_set(g, set) == is_vertex_cover(g, all & ~set));
        assert(is_independent_set(g, set) == is_clique(complement(g), set));
    }
}

// Las reducciones conservan la respuesta, también con k fuera de rango.
void test_reductions(const Graph& g) {
    for (int k = -1; k <= g.n + 2; k++) {
        Instance independent{g, k};
        bool answer = has_independent_set(independent);
        assert(answer == has_vertex_cover(independent_set_to_vertex_cover(independent)));
        assert(answer == has_clique(independent_set_to_clique(independent)));
        Instance cover{g, k};
        assert(has_vertex_cover(cover) == has_clique(vertex_cover_to_clique(cover)));
    }
}

void test_graph_reductions() {
    for (int n = 0; n <= 5; n++) {
        for (unsigned mask = 0; mask < (1u << (n * (n - 1) / 2)); mask++) {
            Graph g = graph_from_mask(n, mask);
            test_complement_lemma(g);
            test_reductions(g);
            // 2-coloreo se reduce a 3-coloreo con el nodo nuevo, y BFS coincide con fuerza bruta.
            assert(two_colorable(g) == colorable_brute_force(g, 2));
            assert(two_colorable(g) == colorable_brute_force(add_apex(g), 3));
        }
    }
    std::mt19937 rng(13);
    for (int i = 0; i < 300; i++) {
        Graph g = random_graph(6 + i % 3, rng);
        test_reductions(g);
    }
}

// El contraejemplo de los apuntes para la reducción que conserva k: una sola arista, con k = 2.
void test_wrong_reduction() {
    const Graph edge{2, {{0, 1}}};
    assert(!has_independent_set({edge, 2}));
    assert(has_vertex_cover({edge, 2}));
}

void test_exactly_one() {
    Cnf formula;
    formula.variables = 3;
    add_exactly_one(formula, {1, 2, 3});
    assert(formula.clauses.size() == 4);
    for (int mask = 0; mask < 8; mask++) {
        Assignment value{false, (mask & 1) != 0, (mask & 2) != 0, (mask & 4) != 0};
        assert(satisfies(formula, value) == (value[1] + value[2] + value[3] == 1));
    }
}

// DPLL contra la fuerza bruta, y minisat contra los dos.
void test_solvers() {
    std::mt19937 rng(7);
    int disagreements = 0;
    for (int round = 0; round < 400; round++) {
        Cnf formula;
        formula.variables = 3 + static_cast<int>(rng() % 6);
        const int clauses = 1 + static_cast<int>(rng() % 24);
        for (int c = 0; c < clauses; c++) {
            Clause clause;
            const int size = 1 + static_cast<int>(rng() % 3);
            for (int i = 0; i < size; i++) {
                int v = 1 + static_cast<int>(rng() % static_cast<unsigned>(formula.variables));
                clause.push_back(rng() % 2 == 0 ? v : -v);
            }
            formula.add(clause);
        }
        const bool truth = count_models(formula) > 0;
        Dpll solver(formula);
        const bool answer = solver.solve();
        assert(answer == truth);
        if (answer) {
            Assignment value(formula.variables + 1, false);
            for (int v = 1; v <= formula.variables; v++) value[v] = solver.value(v);
            assert(satisfies(formula, value));
        }
        if (round % 4 == 0) {
            SatResult result = run_minisat(formula);
            if (result.satisfiable != truth) disagreements++;
            if (result.satisfiable) assert(satisfies(formula, result.value));
        }
    }
    assert(disagreements == 0);
}

void test_minisat_format() {
    Cnf sat;
    sat.variables = 2;
    sat.add({1});
    sat.add({-1, 2});
    SatResult yes = run_minisat(sat);
    assert(yes.exit_code == 10);
    assert(yes.raw.rfind("SAT\n", 0) == 0);
    assert(yes.value[1] && yes.value[2]);

    Cnf unsat;
    unsat.variables = 1;
    unsat.add({1});
    unsat.add({-1});
    SatResult no = run_minisat(unsat);
    assert(no.exit_code == 20);
    assert(no.raw.rfind("UNSAT", 0) == 0);
}

// El coloreo con minisat contra la fuerza bruta. Sin "a lo sumo uno", cualquier color verdadero sirve.
void test_coloring() {
    std::mt19937 rng(21);
    for (int round = 0; round < 150; round++) {
        Graph g = random_graph(1 + round % 7, rng);
        for (int colors = 1; colors <= 3; colors++) {
            const bool truth = colorable_brute_force(g, colors);
            for (bool at_most_one : {true, false}) {
                SatResult result = run_minisat(encode_coloring(g, colors, at_most_one));
                assert(result.satisfiable == truth);
                if (truth) assert(is_proper_coloring(g, decode_coloring(g, colors, result.value)));
            }
        }
    }
    // Exhaustivo: en todo modelo sin la regla, dos vecinos no comparten ningún color verdadero.
    for (int n = 1; n <= 4; n++) {
        for (unsigned mask = 0; mask < (1u << (n * (n - 1) / 2)); mask++) {
            Graph g = graph_from_mask(n, mask);
            for (int colors = 1; colors <= 3; colors++) {
                if (n * colors > 12) continue;
                Cnf loose = encode_coloring(g, colors, false);
                Cnf strict = encode_coloring(g, colors, true);
                assert((count_models(loose) > 0) == (count_models(strict) > 0));
                for_each_model(loose, [&](const Assignment& value) {
                    for (auto [u, v] : g.edges) {
                        for (int c = 0; c < colors; c++) {
                            assert(!(value[color_variable(u, c, colors)] && value[color_variable(v, c, colors)]));
                        }
                    }
                });
            }
        }
    }
    // Las cuentas de los apuntes.
    const Graph triangle{3, {{0, 1}, {1, 2}, {0, 2}}};
    assert(encode_coloring(triangle, 3, true).variables == 9);
    assert(encode_coloring(triangle, 3, true).clauses.size() == 21);
    assert(encode_coloring(triangle, 3, false).clauses.size() == 12);
}

// Palomar: en una fila, "al menos un símbolo por celda" y "a lo sumo una vez cada símbolo" obligan a uno por celda.
void test_pigeonhole() {
    for (int n = 2; n <= 4; n++) {
        for_each_model(one_row_formula(n), [&](const Assignment& value) {
            for (int cell = 0; cell < n; cell++) {
                int count = 0;
                for (int s = 0; s < n; s++) count += value[cell * n + s + 1] ? 1 : 0;
                assert(count == 1);
            }
        });
    }
}

void test_latin_rules() {
    const LatinRules complete;
    LatinRules at_least_only;
    at_least_only.cell_at_most_one = false;
    at_least_only.line_at_most_one = false;
    LatinRules no_cell_rule;
    no_cell_rule.cell_at_most_one = false;
    no_cell_rule.line_at_least_one = false;

    assert(count_models(encode_latin(2, {}, complete)) == 2);
    assert(count_models(encode_latin(2, {}, no_cell_rule)) == 2);
    assert(count_models(encode_latin(2, {}, at_least_only)) > 2);

    // Dos veces el mismo símbolo en una fila: con reglas de "a lo sumo", no hay solución; sin ellas, sí.
    const std::vector<Given> clash{{0, 0, 0}, {0, 1, 0}};
    assert(!run_minisat(encode_latin(3, clash, complete)).satisfiable);
    assert(!run_minisat(encode_latin(3, clash, no_cell_rule)).satisfiable);
    assert(run_minisat(encode_latin(3, clash, at_least_only)).satisfiable);
    auto wrong = decode_latin(3, run_minisat(encode_latin(3, clash, at_least_only)).value);
    assert(!is_latin(wrong));

    const std::vector<Given> fine{{0, 0, 0}, {1, 1, 1}};
    assert(is_latin(decode_latin(3, run_minisat(encode_latin(3, fine, complete)).value)));
    assert(is_latin(decode_latin(3, run_minisat(encode_latin(3, fine, no_cell_rule)).value)));
}

}  // namespace

int main() {
    test_graph_reductions();
    test_wrong_reduction();
    test_exactly_one();
    test_minisat_format();
    test_solvers();
    test_coloring();
    test_pigeonhole();
    test_latin_rules();
    std::cout << "todas las pruebas pasaron\n";
}