// Cuadrado latino de lado n: una tabla donde cada fila y cada columna tiene cada símbolo una vez.
// Una variable por cada (fila, columna, símbolo). Sirve para ver qué pasa con "al menos uno" y "a lo sumo uno".
#ifndef LATIN_H
#define LATIN_H

#include <vector>

#include "cnf.h"

struct LatinRules {
    bool cell_at_least_one = true;
    bool cell_at_most_one = true;
    bool line_at_least_one = true;   // cada símbolo sale en cada fila y en cada columna
    bool line_at_most_one = true;    // cada símbolo no se repite en una fila ni en una columna
};

inline int latin_variable(int n, int row, int column, int symbol) { return row * n * n + column * n + symbol + 1; }

struct Given {
    int row, column, symbol;
};

inline Cnf encode_latin(int n, const std::vector<Given>& givens, const LatinRules& rules) {
    Cnf formula;
    formula.variables = n * n * n;
    std::vector<int> vars(n);
    auto apply = [&](bool least, bool most) {
        if (least) add_at_least_one(formula, vars);
        if (most) add_at_most_one(formula, vars);
    };
    for (int a = 0; a < n; a++) {
        for (int b = 0; b < n; b++) {
            for (int x = 0; x < n; x++) vars[x] = latin_variable(n, a, b, x);
            apply(rules.cell_at_least_one, rules.cell_at_most_one);
            for (int x = 0; x < n; x++) vars[x] = latin_variable(n, a, x, b);
            apply(rules.line_at_least_one, rules.line_at_most_one);
            for (int x = 0; x < n; x++) vars[x] = latin_variable(n, x, a, b);
            apply(rules.line_at_least_one, rules.line_at_most_one);
        }
    }
    for (const Given& g : givens) formula.add({latin_variable(n, g.row, g.column, g.symbol)});
    return formula;
}

// Lee el primer símbolo verdadero de cada celda.
inline std::vector<std::vector<int>> decode_latin(int n, const Assignment& value) {
    std::vector<std::vector<int>> table(n, std::vector<int>(n, -1));
    for (int r = 0; r < n; r++) {
        for (int c = 0; c < n; c++) {
            for (int s = n - 1; s >= 0; s--) {
                if (value[latin_variable(n, r, c, s)]) table[r][c] = s;
            }
        }
    }
    return table;
}

inline bool is_latin(const std::vector<std::vector<int>>& table) {
    const int n = static_cast<int>(table.size());
    for (int a = 0; a < n; a++) {
        std::vector<int> in_row(n, 0), in_column(n, 0);
        for (int b = 0; b < n; b++) {
            if (table[a][b] < 0 || table[b][a] < 0) return false;
            if (in_row[table[a][b]]++ || in_column[table[b][a]]++) return false;
        }
    }
    return true;
}

// Una sola fila de n celdas: al menos un símbolo por celda, y cada símbolo a lo sumo una vez en la fila.
// Es la situación del argumento del palomar.
inline Cnf one_row_formula(int n) {
    Cnf formula;
    formula.variables = n * n;
    auto var = [&](int cell, int symbol) { return cell * n + symbol + 1; };
    std::vector<int> vars(n);
    for (int a = 0; a < n; a++) {
        for (int x = 0; x < n; x++) vars[x] = var(a, x);
        add_at_least_one(formula, vars);
        for (int x = 0; x < n; x++) vars[x] = var(x, a);
        add_at_most_one(formula, vars);
    }
    return formula;
}

#endif