/*
 * prop_alldiff.c -- bounds-consistent alldifferent propagator.
 *
 * Posts a single propagator that, for a set of integer variables
 * x_1..x_n, enforces that they take pairwise distinct values.
 *
 *
 *   THE HALL ARGUMENT
 *
 * For any value interval [a, b], let S(a, b) = { x_i : [lb_i, ub_i] ⊆ [a, b] }
 * be the set of variables whose domain is fully contained in [a, b]. Each
 * x_i in S(a, b) must take a value in [a, b], and all values must be
 * distinct, so we need |S(a, b)| <= b - a + 1.
 *
 *   (1) If |S(a, b)| >  b - a + 1: the constraint is infeasible (a Hall
 *       set with more variables than values is a "pigeonhole violation").
 *
 *   (2) If |S(a, b)| == b - a + 1: the interval [a, b] is *tight* --- the
 *       values are exhausted by S(a, b). Variables x_j NOT in S(a, b)
 *       must avoid [a, b]. With order-encoded bounds we can only enforce
 *       this when x_j's domain extends to one side of [a, b]:
 *
 *         - If ub_j is in [a, b] (and lb_j < a): tighten ub_j to a - 1.
 *         - If lb_j is in [a, b] (and ub_j > b): tighten lb_j to b + 1.
 *
 *       The case where lb_j < a AND ub_j > b (x_j straddles the Hall
 *       interval) cannot be expressed with bounds alone -- we would need
 *       to remove the *middle* of x_j's domain. This is the bounds-vs-
 *       domain consistency gap. Domain-consistent alldifferent requires
 *       per-value SAT atoms (an extension beyond Phase 3 scope).
 *
 *
 *   EXPLANATION
 *
 * When we tighten or conflict because of a Hall interval, the
 * explanation cites the bounds that put each x_i into [a, b]:
 *
 *     forall x_i in Hall set:  x_i >= a  AND  x_i <= b
 *
 * Plus, for a tightening of x_j, the bound on x_j that puts it into
 * range of [a, b]:
 *
 *     for tightening ub_j to a-1: cite  x_j <= b   (so x_j could overlap [a,b])
 *     for tightening lb_j to b+1: cite  x_j >= a   (so x_j could overlap [a,b])
 *
 * For a conflict, no x_j is involved --- only the Hall variables.
 *
 *
 *   ALGORITHM
 *
 * For each interval [a, b] in the union of variable domains, scan the
 * n variables and count those in S(a, b). The total cost is
 *   O(n * D * D)
 * where D is the spread of values. This is naive; the Lopez-Ortiz /
 * Quimper algorithm achieves O(n log n) with sorted lists. For the
 * tutorial scale we are targetting the naive version is correct and
 * readable.
 */

#include "lcg.h"

#include <limits.h>
#include <stdlib.h>
#include <string.h>

typedef struct {
    int *vars;
    int  n;
} AllDiffData;

static void alldiff_destroy(void *data) {
    AllDiffData *d = (AllDiffData *)data;
    free(d->vars);
    free(d);
}

/* Add the Hall-interval explanation literals to the explanation
 * buffer: for each Hall variable x_i, support x_i >= a AND x_i <= b. */
static void add_hall_supports(LcgCtx *ctx, const int *vars, int n,
                              int a, int b)
{
    for (int i = 0; i < n; i++) {
        int v = vars[i];
        if (lcg_lb(ctx, v) >= a && lcg_ub(ctx, v) <= b) {
            lcg_expl_lo(ctx, v, a);   /* support: x_v >= a */
            lcg_expl_hi(ctx, v, b);   /* support: x_v <= b */
        }
    }
}

static int alldiff_propagate(LcgCtx *ctx, void *data) {
    AllDiffData *d = (AllDiffData *)data;

    /* Compute the global value range. */
    int min_val = INT_MAX, max_val = INT_MIN;
    for (int i = 0; i < d->n; i++) {
        int lo = lcg_lb(ctx, d->vars[i]);
        int hi = lcg_ub(ctx, d->vars[i]);
        if (lo < min_val) min_val = lo;
        if (hi > max_val) max_val = hi;
    }
    if (min_val > max_val) return LCG_PROP_OK;

    int any_tight = 0;

    /* For each candidate Hall interval [a, b]. */
    for (int a = min_val; a <= max_val; a++) {
        for (int b = a; b <= max_val; b++) {
            int width = b - a + 1;

            /* Count variables fully inside [a, b]. */
            int count = 0;
            for (int i = 0; i < d->n; i++) {
                if (lcg_lb(ctx, d->vars[i]) >= a &&
                    lcg_ub(ctx, d->vars[i]) <= b) count++;
            }

            if (count > width) {
                /* Hall violation: more variables than values. */
                lcg_expl_clear(ctx);
                add_hall_supports(ctx, d->vars, d->n, a, b);
                return lcg_emit_conflict(ctx);
            }

            if (count != width) continue;   /* not a tight Hall interval */

            /* Tight Hall interval: values [a..b] are exhausted.
             * Tighten every non-Hall variable whose domain reaches
             * into [a..b] from one side. */
            for (int j = 0; j < d->n; j++) {
                int v   = d->vars[j];
                int lbj = lcg_lb(ctx, v);
                int ubj = lcg_ub(ctx, v);
                int in_hall = (lbj >= a && ubj <= b);
                if (in_hall) continue;

                /* Case 1: ubj in [a..b] AND lbj < a. Push ubj to a-1. */
                if (ubj >= a && ubj <= b && lbj < a) {
                    lcg_expl_clear(ctx);
                    add_hall_supports(ctx, d->vars, d->n, a, b);
                    lcg_expl_hi(ctx, v, b);   /* x_v <= b, so x_v could enter [a..b] */
                    int r = lcg_emit_le(ctx, v, a - 1);
                    if (r == LCG_PROP_CONFLICT) return LCG_PROP_CONFLICT;
                    if (r == LCG_PROP_TIGHTENED) any_tight = 1;
                }
                /* Case 2: lbj in [a..b] AND ubj > b. Push lbj to b+1. */
                if (lbj >= a && lbj <= b && ubj > b) {
                    lcg_expl_clear(ctx);
                    add_hall_supports(ctx, d->vars, d->n, a, b);
                    lcg_expl_lo(ctx, v, a);   /* x_v >= a, so x_v could enter [a..b] */
                    int r = lcg_emit_ge(ctx, v, b + 1);
                    if (r == LCG_PROP_CONFLICT) return LCG_PROP_CONFLICT;
                    if (r == LCG_PROP_TIGHTENED) any_tight = 1;
                }
                /* Case 3: lbj < a AND ubj > b ("straddling"). Cannot be
                 * tightened with order-encoded bounds. */
            }
        }
    }

    return any_tight ? LCG_PROP_TIGHTENED : LCG_PROP_OK;
}

void lcg_post_alldifferent(LcgCtx *ctx, const IntVar *vars, int n) {
    AllDiffData *d = malloc(sizeof(AllDiffData));
    d->n    = n;
    d->vars = malloc((size_t)n * sizeof(int));
    memcpy(d->vars, vars, (size_t)n * sizeof(int));
    LcgPropagator p = { .data = d,
                        .propagate = alldiff_propagate,
                        .destroy   = alldiff_destroy };
    lcg_register_propagator(ctx, p);
}
