/*
 * sanity.c -- Phase 1 smoke tests.
 *
 * Coverage:
 *   1. Variable creation: order encoding, bounds queries, sentinels.
 *   2. Bounds enforcement via the order-encoding atoms (no propagator).
 *   3. Linear propagator: feasible problem.
 *   4. Linear propagator: forced narrowing through propagation.
 *   5. Linear propagator: unsatisfiable problem.
 *   6. Multiple linear constraints interacting through shared variables.
 */
#include "lcg.h"

#include <stdio.h>
#include <stdlib.h>
#include <string.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)

/* -------- helpers -------- */
static int post_unit(LcgCtx *ctx, int lit) {
    int cl[1] = { lit };
    lcg_post_clause(ctx, cl, 1);
    return lit;
}

/* -------- 1. variable creation and literal queries -------- */
static void test_create(void) {
    TEST("create");
    LcgCtx *ctx = lcg_new();
    IntVar x = lcg_new_int_var(ctx, 0, 5, "x");

    /* domain queries via literal sentinels */
    CHECK(lcg_lit_le(ctx, x,  5) == LCG_LIT_TRUE);    /* x <= 5  trivially true */
    CHECK(lcg_lit_le(ctx, x, -1) == LCG_LIT_FALSE);   /* x <= -1 trivially false */
    CHECK(lcg_lit_ge(ctx, x,  0) == LCG_LIT_TRUE);    /* x >=  0 trivially true */
    CHECK(lcg_lit_ge(ctx, x,  6) == LCG_LIT_FALSE);   /* x >=  6 trivially false */

    /* middle literals are real (positive) atoms */
    int l = lcg_lit_le(ctx, x, 2);
    CHECK(l > 0 && l != LCG_LIT_TRUE);
    CHECK(lcg_lit_ge(ctx, x, 3) == -l);   /* x >= 3 iff !(x <= 2) */

    lcg_free(ctx);
}

/* -------- 2. unit-clause bounds without a propagator -------- */
static void test_unit_bounds(void) {
    TEST("unit_bounds");
    LcgCtx *ctx = lcg_new();
    IntVar x = lcg_new_int_var(ctx, 0, 9, "x");
    /* Force x <= 3 and x >= 2 via unit clauses; expect a value in {2, 3}. */
    post_unit(ctx, lcg_lit_le(ctx, x, 3));
    post_unit(ctx, lcg_lit_ge(ctx, x, 2));
    int r = lcg_solve(ctx);
    CHECK(r == LCG_SAT);
    int v = lcg_value(ctx, x);
    CHECK(v >= 2 && v <= 3);
    lcg_free(ctx);
}

/* -------- 3. linear feasibility -------- */
static void test_linear_feasible(void) {
    TEST("linear_feasible");
    LcgCtx *ctx = lcg_new();
    IntVar x = lcg_new_int_var(ctx, 0, 9, "x");
    IntVar y = lcg_new_int_var(ctx, 0, 9, "y");
    /* x + y <= 5 ; force x >= 2, y >= 1.  Feasible. */
    int     coeffs[2] = { 1, 1 };
    IntVar  vars  [2] = { x, y };
    lcg_post_linear_le(ctx, coeffs, vars, 2, 5);
    post_unit(ctx, lcg_lit_ge(ctx, x, 2));
    post_unit(ctx, lcg_lit_ge(ctx, y, 1));
    int r = lcg_solve(ctx);
    CHECK(r == LCG_SAT);
    int vx = lcg_value(ctx, x), vy = lcg_value(ctx, y);
    CHECK(vx + vy <= 5);
    CHECK(vx >= 2);
    CHECK(vy >= 1);
    lcg_free(ctx);
}

/* -------- 4. linear propagator narrows another variable -------- */
static void test_linear_propagate(void) {
    TEST("linear_propagate");
    LcgCtx *ctx = lcg_new();
    IntVar x = lcg_new_int_var(ctx, 0, 9, "x");
    IntVar y = lcg_new_int_var(ctx, 0, 9, "y");
    /* x + y <= 5, x = 4 -> y must be <= 1. */
    int     coeffs[2] = { 1, 1 };
    IntVar  vars  [2] = { x, y };
    lcg_post_linear_le(ctx, coeffs, vars, 2, 5);
    /* x == 4: x <= 4 AND x >= 4 */
    post_unit(ctx, lcg_lit_le(ctx, x, 4));
    post_unit(ctx, lcg_lit_ge(ctx, x, 4));
    int r = lcg_solve(ctx);
    CHECK(r == LCG_SAT);
    CHECK(lcg_value(ctx, x) == 4);
    CHECK(lcg_value(ctx, y) <= 1);
    lcg_free(ctx);
}

/* -------- 5. linear infeasibility -------- */
static void test_linear_infeasible(void) {
    TEST("linear_infeasible");
    LcgCtx *ctx = lcg_new();
    IntVar x = lcg_new_int_var(ctx, 0, 9, "x");
    IntVar y = lcg_new_int_var(ctx, 0, 9, "y");
    /* x + y <= 5, x >= 3, y >= 4 ; sum_min = 7 > 5 -> UNSAT. */
    int     coeffs[2] = { 1, 1 };
    IntVar  vars  [2] = { x, y };
    lcg_post_linear_le(ctx, coeffs, vars, 2, 5);
    post_unit(ctx, lcg_lit_ge(ctx, x, 3));
    post_unit(ctx, lcg_lit_ge(ctx, y, 4));
    int r = lcg_solve(ctx);
    CHECK(r == LCG_UNSAT);
    lcg_free(ctx);
}

/* -------- 6. multiple constraints sharing variables -------- */
static void test_multi_constraint(void) {
    TEST("multi_constraint");
    LcgCtx *ctx = lcg_new();
    IntVar x = lcg_new_int_var(ctx, 0, 9, "x");
    IntVar y = lcg_new_int_var(ctx, 0, 9, "y");
    IntVar z = lcg_new_int_var(ctx, 0, 9, "z");
    /* x + y <= 7
       y + z <= 6
       x + z >= 8  (encoded as -x - z <= -8)
       x >= 3 */
    {
        int c[2] = { 1, 1 }; IntVar v[2] = { x, y };
        lcg_post_linear_le(ctx, c, v, 2, 7);
    }
    {
        int c[2] = { 1, 1 }; IntVar v[2] = { y, z };
        lcg_post_linear_le(ctx, c, v, 2, 6);
    }
    {
        int c[2] = { -1, -1 }; IntVar v[2] = { x, z };
        lcg_post_linear_le(ctx, c, v, 2, -8);
    }
    post_unit(ctx, lcg_lit_ge(ctx, x, 3));
    int r = lcg_solve(ctx);
    CHECK(r == LCG_SAT);
    int vx = lcg_value(ctx, x), vy = lcg_value(ctx, y), vz = lcg_value(ctx, z);
    CHECK(vx + vy <= 7);
    CHECK(vy + vz <= 6);
    CHECK(vx + vz >= 8);
    CHECK(vx >= 3);
    lcg_free(ctx);
}

/* -------- 7. Phase 2: register a custom propagator --------
 *
 * Posts a propagator that forbids the value 0 for a variable, and
 * checks that the solver returns a non-zero model.
 */
typedef struct { IntVar v; } NeqZeroData;

static int neq_zero_propagate(LcgCtx *ctx, void *data) {
    NeqZeroData *d = (NeqZeroData *)data;
    int lo = lcg_lb(ctx, d->v);
    int hi = lcg_ub(ctx, d->v);
    if (lo == 0 && hi == 0) {
        lcg_expl_clear(ctx);
        lcg_expl_lo(ctx, d->v, 0);
        lcg_expl_hi(ctx, d->v, 0);
        return lcg_emit_conflict(ctx);
    }
    if (lo == 0) {
        lcg_expl_clear(ctx);
        lcg_expl_hi(ctx, d->v, 0);
        return lcg_emit_ge(ctx, d->v, 1);
    }
    return LCG_PROP_OK;
}
static void neq_zero_destroy(void *data) { free(data); }

static void test_custom_propagator(void) {
    TEST("custom_propagator");
    LcgCtx *ctx = lcg_new();
    IntVar x = lcg_new_int_var(ctx, 0, 3, "x");

    NeqZeroData *d = malloc(sizeof(NeqZeroData));
    d->v = x;
    LcgPropagator p = { .data = d, .propagate = neq_zero_propagate,
                        .destroy = neq_zero_destroy };
    lcg_register_propagator(ctx, p);

    /* Force x <= 1 so the only allowed value is 1 (since 0 is forbidden). */
    int cl = lcg_lit_le(ctx, x, 1);
    lcg_post_clause(ctx, &cl, 1);

    int r = lcg_solve(ctx);
    CHECK(r == LCG_SAT);
    CHECK(lcg_value(ctx, x) == 1);
    lcg_free(ctx);
}

/* -------- 8. Phase 2: lcg_lb / lcg_ub agree with explicit bounds --------
 *
 * The new bounds accessors must reflect cached bounds even before
 * lcg_solve runs (they start at dom_lo / dom_hi).
 */
static void test_bounds_api(void) {
    TEST("bounds_api");
    LcgCtx *ctx = lcg_new();
    IntVar x = lcg_new_int_var(ctx, 3, 9, "x");
    CHECK(lcg_lb(ctx, x) == 3);
    CHECK(lcg_ub(ctx, x) == 9);
    lcg_free(ctx);
}

/* -------- 9. Phase 3: alldifferent --- feasible case -------- */
static void test_alldiff_feasible(void) {
    TEST("alldiff_feasible");
    LcgCtx *ctx = lcg_new();
    IntVar x = lcg_new_int_var(ctx, 1, 3, "x");
    IntVar y = lcg_new_int_var(ctx, 1, 3, "y");
    IntVar z = lcg_new_int_var(ctx, 1, 3, "z");
    IntVar vars[3] = { x, y, z };
    lcg_post_alldifferent(ctx, vars, 3);
    int r = lcg_solve(ctx);
    CHECK(r == LCG_SAT);
    int vx = lcg_value(ctx, x), vy = lcg_value(ctx, y), vz = lcg_value(ctx, z);
    CHECK(vx >= 1 && vx <= 3);
    CHECK(vy >= 1 && vy <= 3);
    CHECK(vz >= 1 && vz <= 3);
    CHECK(vx != vy);
    CHECK(vy != vz);
    CHECK(vx != vz);
    lcg_free(ctx);
}

/* -------- 10. Phase 3: alldifferent --- pigeonhole UNSAT --------
 *
 * 4 variables in [1..3]. The whole-range Hall set (a=1, b=3) has size
 * 3 < 4 variables. Conflict immediately on the first propagator call,
 * before any decisions.
 */
static void test_alldiff_pigeonhole(void) {
    TEST("alldiff_pigeonhole");
    LcgCtx *ctx = lcg_new();
    IntVar v[4];
    char name[8];
    for (int i = 0; i < 4; i++) {
        snprintf(name, sizeof name, "x%d", i);
        v[i] = lcg_new_int_var(ctx, 1, 3, name);
    }
    lcg_post_alldifferent(ctx, v, 4);
    int r = lcg_solve(ctx);
    CHECK(r == LCG_UNSAT);
    /* Expect: no decisions needed; the Hall violation is at the root. */
    CHECK(lcg_decisions(ctx) == 0);
    lcg_free(ctx);
}

/* -------- 11. Phase 3: alldifferent --- Hall tightening --------
 *
 * Three variables: x, y in [1..2]; z in [1..3]. The Hall set {x, y}
 * exhausts [1..2], so z must take value 3.
 */
static void test_alldiff_tighten(void) {
    TEST("alldiff_tighten");
    LcgCtx *ctx = lcg_new();
    IntVar x = lcg_new_int_var(ctx, 1, 2, "x");
    IntVar y = lcg_new_int_var(ctx, 1, 2, "y");
    IntVar z = lcg_new_int_var(ctx, 1, 3, "z");
    IntVar v[3] = { x, y, z };
    lcg_post_alldifferent(ctx, v, 3);
    int r = lcg_solve(ctx);
    CHECK(r == LCG_SAT);
    CHECK(lcg_value(ctx, z) == 3);
    /* x and y must be a permutation of 1, 2 */
    int vx = lcg_value(ctx, x), vy = lcg_value(ctx, y);
    CHECK((vx == 1 && vy == 2) || (vx == 2 && vy == 1));
    lcg_free(ctx);
}

/* -------- 12. Phase 4: cumulative --- feasible schedule --------
 *
 * Two tasks of duration 3, capacity 2 (so they can run in parallel),
 * each window [0..3]. Should find a feasible schedule. */
static void test_cumulative_feasible(void) {
    TEST("cumulative_feasible");
    LcgCtx *ctx = lcg_new();
    IntVar s0 = lcg_new_int_var(ctx, 0, 3, "s0");
    IntVar s1 = lcg_new_int_var(ctx, 0, 3, "s1");
    IntVar st[2] = { s0, s1 };
    int    du[2] = { 3, 3 };
    int    de[2] = { 1, 1 };
    lcg_post_cumulative(ctx, st, du, de, 2, 2);
    int r = lcg_solve(ctx);
    CHECK(r == LCG_SAT);
    /* Both tasks scheduled, no further constraint --- any starts work. */
    int v0 = lcg_value(ctx, s0), v1 = lcg_value(ctx, s1);
    CHECK(v0 >= 0 && v0 <= 3);
    CHECK(v1 >= 0 && v1 <= 3);
    lcg_free(ctx);
}

/* -------- 13. Phase 4: cumulative --- capacity forces sequencing --------
 *
 * Two tasks of duration 3, capacity 1 (unary resource). Both must fit
 * in a window of 7 time slots: one starts at 0..3, the other at 3..6
 * (or vice versa). One must start <= 0 if other starts >= 3, etc. */
static void test_cumulative_sequence(void) {
    TEST("cumulative_sequence");
    LcgCtx *ctx = lcg_new();
    IntVar s0 = lcg_new_int_var(ctx, 0, 6, "s0");
    IntVar s1 = lcg_new_int_var(ctx, 0, 6, "s1");
    IntVar st[2] = { s0, s1 };
    int    du[2] = { 3, 3 };
    int    de[2] = { 1, 1 };
    lcg_post_cumulative(ctx, st, du, de, 2, 1);   /* unary */
    int r = lcg_solve(ctx);
    CHECK(r == LCG_SAT);
    int v0 = lcg_value(ctx, s0), v1 = lcg_value(ctx, s1);
    /* Either v0 + 3 <= v1, or v1 + 3 <= v0. */
    CHECK((v0 + 3 <= v1) || (v1 + 3 <= v0));
    lcg_free(ctx);
}

/* -------- 14. Phase 4: cumulative --- overflow UNSAT --------
 *
 * Three duration-2 tasks all pinned to start at time 0, capacity 2.
 * Three tasks demanding 1 each at t=0 totals 3 > 2: conflict. */
static void test_cumulative_overflow(void) {
    TEST("cumulative_overflow");
    LcgCtx *ctx = lcg_new();
    IntVar s[3];
    for (int i = 0; i < 3; i++) s[i] = lcg_new_int_var(ctx, 0, 0, "s");
    int du[3] = { 2, 2, 2 };
    int de[3] = { 1, 1, 1 };
    lcg_post_cumulative(ctx, s, du, de, 3, 2);
    int r = lcg_solve(ctx);
    CHECK(r == LCG_UNSAT);
    lcg_free(ctx);
}

/* -------- 15. Phase 4: no_overlap convenience wrapper --------
 *
 * Two unit-time tasks, both must start at the same time slot 0:
 * with no_overlap that's UNSAT. */
static void test_no_overlap_basic(void) {
    TEST("no_overlap_basic");
    LcgCtx *ctx = lcg_new();
    IntVar s0 = lcg_new_int_var(ctx, 0, 0, "s0");
    IntVar s1 = lcg_new_int_var(ctx, 0, 0, "s1");
    IntVar st[2] = { s0, s1 };
    int    du[2] = { 1, 1 };
    lcg_post_no_overlap(ctx, st, du, 2);
    int r = lcg_solve(ctx);
    CHECK(r == LCG_UNSAT);
    lcg_free(ctx);
}

int main(void) {
    test_create();
    test_unit_bounds();
    test_linear_feasible();
    test_linear_propagate();
    test_linear_infeasible();
    test_multi_constraint();
    test_custom_propagator();
    test_bounds_api();
    test_alldiff_feasible();
    test_alldiff_pigeonhole();
    test_alldiff_tighten();
    test_cumulative_feasible();
    test_cumulative_sequence();
    test_cumulative_overflow();
    test_no_overlap_basic();

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