/*
 * sanity.c -- Phase 1 smoke tests.
 *
 * Coverage:
 *   1. Empty problem.
 *   2. Hard-only feasibility.
 *   3. Hard-only infeasibility (MAXSAT_HARD_UNSAT).
 *   4. All soft satisfiable -> cost 0.
 *   5. One soft made infeasible by hard -> cost 1.
 *   6. Pigeonhole: three soft clauses (x_i) plus at-most-one(x_1..x_3) -> cost 2.
 *   7. Small WTA: 3 weapons, 5 targets -> cost 2.
 *   8. Compatibility: maxsat_value on unsolved problem returns 0.
 */
#include "maxsat.h"

#include <stdio.h>

static int g_pass = 0, g_fail = 0;
static const char *g_name = "";

#define TEST(name)  do { g_name = name; } while (0)
#define CHECK(cond) do {                                              \
    if (cond) g_pass++;                                                \
    else { g_fail++;                                                   \
        fprintf(stderr, "  FAIL %s : %s  (%s:%d)\n",                   \
                g_name, #cond, __FILE__, __LINE__);                    \
    }                                                                  \
} while (0)

/* -------- 1. empty problem -------- */
static void test_empty(void) {
    TEST("empty");
    MaxSatCtx *m = maxsat_new();
    long r = maxsat_solve(m);
    CHECK(r == 0);
    maxsat_free(m);
}

/* -------- 2. hard-only feasibility -------- */
static void test_hard_feasible(void) {
    TEST("hard_feasible");
    MaxSatCtx *m = maxsat_new();
    int x = maxsat_new_var(m);
    int y = maxsat_new_var(m);
    int cl[2];
    cl[0] = x;        maxsat_add_hard_clause(m, cl, 1);
    cl[0] = -x;
    cl[1] =  y;       maxsat_add_hard_clause(m, cl, 2);
    long r = maxsat_solve(m);
    CHECK(r == 0);
    CHECK(maxsat_value(m, x) == 1);
    CHECK(maxsat_value(m, y) == 1);
    maxsat_free(m);
}

/* -------- 3. hard-only infeasibility -------- */
static void test_hard_unsat(void) {
    TEST("hard_unsat");
    MaxSatCtx *m = maxsat_new();
    int x = maxsat_new_var(m);
    int cl[1];
    cl[0] =  x; maxsat_add_hard_clause(m, cl, 1);
    cl[0] = -x; maxsat_add_hard_clause(m, cl, 1);
    long r = maxsat_solve(m);
    CHECK(r == MAXSAT_HARD_UNSAT);
    maxsat_free(m);
}

/* -------- 4. soft satisfiable -------- */
static void test_soft_satisfiable(void) {
    TEST("soft_satisfiable");
    MaxSatCtx *m = maxsat_new();
    int x = maxsat_new_var(m);
    int cl[1] = { x };
    maxsat_add_soft_clause(m, cl, 1);
    long r = maxsat_solve(m);
    CHECK(r == 0);
    CHECK(maxsat_value(m, x) == 1);
    maxsat_free(m);
}

/* -------- 5. soft made infeasible by hard -------- */
static void test_soft_forced_unsat(void) {
    TEST("soft_forced_unsat");
    MaxSatCtx *m = maxsat_new();
    int x = maxsat_new_var(m);
    int cl[1];
    cl[0] = -x; maxsat_add_hard_clause(m, cl, 1);
    cl[0] =  x; maxsat_add_soft_clause(m, cl, 1);
    long r = maxsat_solve(m);
    CHECK(r == 1);
    CHECK(maxsat_value(m, x) == 0);
    maxsat_free(m);
}

/* -------- 6. pigeonhole: cardinality kicks in --------
 *
 * Three soft clauses (x_1), (x_2), (x_3) plus at-most-one(x_1..x_3) hard.
 * At most one x_i is true; the other two soft clauses are unsatisfied.
 * Cost = 2.
 */
static void test_pigeonhole(void) {
    TEST("pigeonhole");
    MaxSatCtx *m = maxsat_new();
    int x[3];
    for (int i = 0; i < 3; i++) x[i] = maxsat_new_var(m);
    maxsat_add_at_most_one(m, x, 3);
    for (int i = 0; i < 3; i++) {
        int cl = x[i];
        maxsat_add_soft_clause(m, &cl, 1);
    }
    long r = maxsat_solve(m);
    CHECK(r == 2);
    /* Exactly one x_i true. */
    int n_true = 0;
    for (int i = 0; i < 3; i++) n_true += maxsat_value(m, x[i]);
    CHECK(n_true == 1);
    /* And the solver did make use of the iterations. */
    CHECK(maxsat_iterations(m) >= 2);
    maxsat_free(m);
}

/* -------- 7. small WTA --------
 *
 * 3 weapons w_1, w_2, w_3 and 5 targets t_1..t_5. Compatibility:
 *     w_1 can engage t_1, t_2, t_3
 *     w_2 can engage t_2, t_3, t_4
 *     w_3 can engage t_3, t_4, t_5
 *
 * Variables x_{i,j} = "weapon i engages target j" for compatible pairs.
 * Hard: each weapon engages at most one target.
 * Hard: each target is engaged by at most one weapon.
 * Soft: each target is engaged by at least one weapon.
 *
 * With 3 weapons and 5 targets we engage at most 3, so at least 2 soft
 * clauses are unsatisfied. The optimal cost is 2.
 */
static void test_small_wta(void) {
    TEST("small_wta");
    MaxSatCtx *m = maxsat_new();

    /* Build variable table x[w][t], or -1 if (w, t) is incompatible. */
    int compat[3][5] = {
        { 1, 1, 1, 0, 0 },
        { 0, 1, 1, 1, 0 },
        { 0, 0, 1, 1, 1 },
    };
    int x[3][5];
    for (int w = 0; w < 3; w++) {
        for (int t = 0; t < 5; t++) {
            x[w][t] = compat[w][t] ? maxsat_new_var(m) : -1;
        }
    }

    /* Each weapon: at most one engagement. */
    for (int w = 0; w < 3; w++) {
        int row[5], n = 0;
        for (int t = 0; t < 5; t++) if (x[w][t] > 0) row[n++] = x[w][t];
        maxsat_add_at_most_one(m, row, n);
    }
    /* Each target: at most one weapon. */
    for (int t = 0; t < 5; t++) {
        int col[3], n = 0;
        for (int w = 0; w < 3; w++) if (x[w][t] > 0) col[n++] = x[w][t];
        if (n > 0) maxsat_add_at_most_one(m, col, n);
    }
    /* Each target: soft "at least one weapon engages it". */
    for (int t = 0; t < 5; t++) {
        int col[3], n = 0;
        for (int w = 0; w < 3; w++) if (x[w][t] > 0) col[n++] = x[w][t];
        if (n > 0) maxsat_add_soft_clause(m, col, n);
    }

    long r = maxsat_solve(m);
    CHECK(r == 2);

    /* Verify the model: at-most-one per row, at-most-one per col, and
     * exactly 3 engagements (since 3 weapons each used). */
    int engaged_targets = 0;
    for (int t = 0; t < 5; t++) {
        int n = 0;
        for (int w = 0; w < 3; w++)
            if (x[w][t] > 0 && maxsat_value(m, x[w][t])) n++;
        CHECK(n <= 1);
        if (n) engaged_targets++;
    }
    for (int w = 0; w < 3; w++) {
        int n = 0;
        for (int t = 0; t < 5; t++)
            if (x[w][t] > 0 && maxsat_value(m, x[w][t])) n++;
        CHECK(n <= 1);
    }
    CHECK(engaged_targets == 3);

    maxsat_free(m);
}

/* -------- 8. maxsat_value before solve returns 0 -------- */
static void test_value_before_solve(void) {
    TEST("value_before_solve");
    MaxSatCtx *m = maxsat_new();
    int x = maxsat_new_var(m);
    CHECK(maxsat_value(m, x) == 0);
    maxsat_free(m);
}

/* -------- 9. Phase 2: both algorithms agree on the pigeonhole --------
 *
 * 4 soft clauses (x_1..x_4) plus at-most-1 hard. Expected cost: 3
 * (only one x_i true; three soft clauses unsatisfied).
 */
static void test_algorithm_agreement(void) {
    TEST("algorithm_agreement_linear");
    MaxSatCtx *m = maxsat_new();
    maxsat_set_algorithm(m, MAXSAT_ALG_LINEAR);
    int x[4];
    for (int i = 0; i < 4; i++) x[i] = maxsat_new_var(m);
    maxsat_add_at_most_one(m, x, 4);
    for (int i = 0; i < 4; i++) { int cl = x[i]; maxsat_add_soft_clause(m, &cl, 1); }
    long r1 = maxsat_solve(m);
    CHECK(r1 == 3);
    CHECK(maxsat_get_algorithm(m) == MAXSAT_ALG_LINEAR);
    maxsat_free(m);

    TEST("algorithm_agreement_core_guided");
    m = maxsat_new();
    maxsat_set_algorithm(m, MAXSAT_ALG_CORE_GUIDED);
    int y[4];
    for (int i = 0; i < 4; i++) y[i] = maxsat_new_var(m);
    maxsat_add_at_most_one(m, y, 4);
    for (int i = 0; i < 4; i++) { int cl = y[i]; maxsat_add_soft_clause(m, &cl, 1); }
    long r2 = maxsat_solve(m);
    CHECK(r2 == 3);
    /* Core-guided should have found exactly one core per increment of cost. */
    CHECK(maxsat_cores_found(m) == 3);
    maxsat_free(m);
}

/* -------- 10. Phase 2: cores_found is zero for the linear algorithm -------- */
static void test_cores_found_zero_for_linear(void) {
    TEST("cores_found_zero_for_linear");
    MaxSatCtx *m = maxsat_new();
    maxsat_set_algorithm(m, MAXSAT_ALG_LINEAR);
    int x[3];
    for (int i = 0; i < 3; i++) x[i] = maxsat_new_var(m);
    maxsat_add_at_most_one(m, x, 3);
    for (int i = 0; i < 3; i++) { int cl = x[i]; maxsat_add_soft_clause(m, &cl, 1); }
    maxsat_solve(m);
    CHECK(maxsat_cores_found(m) == 0);
    maxsat_free(m);
}

/* -------- 11. Phase 3: weighted soft, satisfied -------- */
static void test_weighted_satisfied(void) {
    TEST("weighted_satisfied");
    MaxSatCtx *m = maxsat_new();
    int x = maxsat_new_var(m);
    int cl = x;
    maxsat_add_soft_clause_weighted(m, &cl, 1, 5);
    long r = maxsat_solve(m);
    CHECK(r == 0);
    CHECK(maxsat_value(m, x) == 1);
    maxsat_free(m);
}

/* -------- 12. Phase 3: weighted soft, forced unsat -------- */
static void test_weighted_forced_unsat(void) {
    TEST("weighted_forced_unsat");
    MaxSatCtx *m = maxsat_new();
    int x = maxsat_new_var(m);
    int cl[1];
    cl[0] = -x; maxsat_add_hard_clause(m, cl, 1);
    cl[0] =  x; maxsat_add_soft_clause_weighted(m, cl, 1, 5);
    long r = maxsat_solve(m);
    CHECK(r == 5);
    CHECK(maxsat_value(m, x) == 0);
    maxsat_free(m);
}

/* -------- 13. Phase 3: pick the heavier of two mutually exclusive softs --------
 *
 * Two soft clauses (x_1), (x_2) with weights 7 and 3, and a hard
 * constraint saying x_1 AND x_2 cannot both be true. The solver should
 * keep the weight-7 soft satisfied and pay 3 for falsifying the lighter.
 */
static void test_weighted_pick_heavier(void) {
    TEST("weighted_pick_heavier");
    MaxSatCtx *m = maxsat_new();
    int a = maxsat_new_var(m);
    int b = maxsat_new_var(m);
    int conflict[2] = { -a, -b };
    maxsat_add_hard_clause(m, conflict, 2);   /* not both */
    int la = a; maxsat_add_soft_clause_weighted(m, &la, 1, 7);
    int lb = b; maxsat_add_soft_clause_weighted(m, &lb, 1, 3);
    long r = maxsat_solve(m);
    CHECK(r == 3);
    CHECK(maxsat_value(m, a) == 1);
    CHECK(maxsat_value(m, b) == 0);
    maxsat_free(m);
}

/* -------- 14. Phase 3: weighted pigeonhole --------
 *
 * Three soft clauses (x_1), (x_2), (x_3) with weights [10, 5, 1] and a
 * hard at-most-one over x_1..x_3. The solver should satisfy x_1
 * (weight 10) and pay 5 + 1 = 6 for the others.
 */
static void test_weighted_pigeonhole(void) {
    TEST("weighted_pigeonhole");
    MaxSatCtx *m = maxsat_new();
    int x[3];
    for (int i = 0; i < 3; i++) x[i] = maxsat_new_var(m);
    maxsat_add_at_most_one(m, x, 3);
    long w[3] = { 10, 5, 1 };
    for (int i = 0; i < 3; i++) {
        int cl = x[i];
        maxsat_add_soft_clause_weighted(m, &cl, 1, w[i]);
    }
    long r = maxsat_solve(m);
    CHECK(r == 6);
    CHECK(maxsat_value(m, x[0]) == 1);
    CHECK(maxsat_value(m, x[1]) == 0);
    CHECK(maxsat_value(m, x[2]) == 0);
    maxsat_free(m);
}

/* -------- 15. Phase 3: weight 0 is a no-op -------- */
static void test_weight_zero_noop(void) {
    TEST("weight_zero_noop");
    MaxSatCtx *m = maxsat_new();
    int x = maxsat_new_var(m);
    int cl[1];
    cl[0] = -x; maxsat_add_hard_clause(m, cl, 1);
    cl[0] =  x; maxsat_add_soft_clause_weighted(m, cl, 1, 0);
    long r = maxsat_solve(m);
    CHECK(r == 0);     /* nothing to be unsatisfied */
    CHECK(maxsat_value(m, x) == 0);
    maxsat_free(m);
}

int main(void) {
    test_empty();
    test_hard_feasible();
    test_hard_unsat();
    test_soft_satisfiable();
    test_soft_forced_unsat();
    test_pigeonhole();
    test_small_wta();
    test_value_before_solve();
    test_algorithm_agreement();
    test_cores_found_zero_for_linear();
    test_weighted_satisfied();
    test_weighted_forced_unsat();
    test_weighted_pick_heavier();
    test_weighted_pigeonhole();
    test_weight_zero_noop();

    printf("%d / %d passed\n", g_pass, g_pass + g_fail);
    return g_fail ? 1 : 0;
}
