/*
 * prop_cumulative.c -- cumulative resource constraint via time-table
 *                       reasoning, with explanations.
 *
 *
 *   THE CUMULATIVE CONSTRAINT
 *
 * Given n tasks, each with a start-time variable s_i, fixed duration p_i,
 * and fixed resource demand h_i, and a global resource capacity C:
 *
 *     for all t,  sum_{i : s_i <= t < s_i + p_i}  h_i  <=  C.
 *
 * Task i occupies the half-open interval [s_i, s_i + p_i).
 *
 *
 *   TIME-TABLE REASONING
 *
 * Each task has a "mandatory part" --- the time interval where it
 * definitely runs across all currently valid starts. For task i:
 *
 *     mandatory_i = [ub(s_i), lb(s_i) + p_i)      (non-empty when
 *                                                  ub(s_i) < lb(s_i) + p_i)
 *
 * (For lb=2, ub=4, p=3: starts in {2,3,4} cover [2,5), [3,6), [4,7).
 *  The mandatory part is [4, 5) = {4}: the only time all three intervals
 *  share.)
 *
 * Propagation algorithm:
 *   1. Compute the per-time-point demand from each task's mandatory part.
 *   2. If any time point has demand > C, that is a conflict; the
 *      explanation cites every task whose mandatory part covers that
 *      time.
 *   3. For each task j, scan candidate starts. If starting j at s would
 *      put j's demand into a time t where other-task mandatory demand
 *      already exceeds C - h_j, then s is forbidden. Tighten lb(s_j) or
 *      ub(s_j) accordingly. The explanation cites j's current
 *      neighbouring bound and the contributing tasks' mandatory bounds
 *      at the witness time t.
 *
 * Phase 4 implements naive O(n * D) per-call propagation where D is the
 * time horizon. Faster algorithms (Aggoun-Beldiceanu sweep, edge-finding,
 * energetic reasoning) are out of scope for the tutorial.
 *
 *
 *   EXPLANATIONS
 *
 * The supports for "task i is mandatorily running at time t" are:
 *     s_i  <=  t                cited as  lcg_expl_hi(s_i, t)
 *     s_i  >=  t - p_i + 1      cited as  lcg_expl_lo(s_i, t - p_i + 1)
 *
 * From which any propagator can derive:
 *     ub(s_i) <= t   AND   lb(s_i) >= t - p_i + 1
 *  -> for all valid s_i in [lb, ub], s_i <= t < s_i + p_i
 *  -> t is in [s_i, s_i + p_i) regardless of choice
 *  -> task i demands h_i at time t.
 */

#include "lcg.h"

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

typedef struct {
    int     n;
    IntVar *start;
    int    *dur;
    int    *demand;
    int     capacity;
} CumData;

static void cum_destroy(void *data) {
    CumData *d = (CumData *)data;
    free(d->start);
    free(d->dur);
    free(d->demand);
    free(d);
}

/* Add the "task i is mandatorily running at time t" supports to the
 * current explanation buffer. */
static void cum_explain_mandatory(LcgCtx *ctx, IntVar s, int p, int t) {
    lcg_expl_hi(ctx, s, t);
    lcg_expl_lo(ctx, s, t - p + 1);
}

/* Cite every task (other than `skip`) whose mandatory part covers
 * time `t`, contributing to the demand at t. */
static void cum_explain_demand_at(LcgCtx *ctx, CumData *d, int t, int skip) {
    for (int i = 0; i < d->n; i++) {
        if (i == skip) continue;
        int mand_start = lcg_ub(ctx, d->start[i]);
        int mand_end   = lcg_lb(ctx, d->start[i]) + d->dur[i];
        if (mand_start <= t && t < mand_end) {
            cum_explain_mandatory(ctx, d->start[i], d->dur[i], t);
        }
    }
}

/* Check whether starting task j at `s` is feasible against the demand
 * profile (where j's own mandatory contribution has been subtracted).
 * If infeasible, return the offending time t through *witness; else
 * leave *witness untouched and return 1. */
static int cum_start_feasible(CumData *d, int *demand_at, int min_t, int max_t,
                              int j, int s, int *witness)
{
    int p = d->dur[j], h = d->demand[j];
    for (int t = s; t < s + p; t++) {
        if (t < min_t || t >= max_t) continue;
        if (demand_at[t - min_t] + h > d->capacity) {
            *witness = t;
            return 0;
        }
    }
    return 1;
}

static int cum_propagate(LcgCtx *ctx, void *data) {
    CumData *d = (CumData *)data;
    if (d->n == 0) return LCG_PROP_OK;

    /* 1. Time horizon: cover from the earliest possible start to the
     *    latest possible end. */
    int min_t = INT_MAX, max_t = INT_MIN;
    for (int i = 0; i < d->n; i++) {
        int est = lcg_lb(ctx, d->start[i]);
        int lct = lcg_ub(ctx, d->start[i]) + d->dur[i];   /* latest completion */
        if (est < min_t) min_t = est;
        if (lct > max_t) max_t = lct;
    }
    if (min_t >= max_t) return LCG_PROP_OK;
    int horizon = max_t - min_t;

    /* 2. Demand profile from all mandatory parts. */
    int *demand_at = calloc((size_t)horizon, sizeof(int));
    if (!demand_at) return LCG_PROP_OK;
    for (int i = 0; i < d->n; i++) {
        int mand_start = lcg_ub(ctx, d->start[i]);
        int mand_end   = lcg_lb(ctx, d->start[i]) + d->dur[i];
        for (int t = mand_start; t < mand_end; t++) {
            demand_at[t - min_t] += d->demand[i];
        }
    }

    /* 3. Conflict: any time point exceeds capacity. */
    for (int t = 0; t < horizon; t++) {
        if (demand_at[t] > d->capacity) {
            int real_t = t + min_t;
            lcg_expl_clear(ctx);
            cum_explain_demand_at(ctx, d, real_t, /*skip=*/-1);
            free(demand_at);
            return lcg_emit_conflict(ctx);
        }
    }

    /* 4. Bound tightening. For each task j, see whether the current est
     * or lst is infeasible against the (other tasks') demand profile.
     * Emit one tightening per direction per task per call --- SAT drives
     * the rest via repeated invocation. */
    int any_tight = 0;
    for (int j = 0; j < d->n; j++) {
        int est = lcg_lb(ctx, d->start[j]);
        int lst = lcg_ub(ctx, d->start[j]);
        if (est == lst) continue;             /* already fixed */
        int p = d->dur[j];
        int h = d->demand[j];

        /* Temporarily remove j's own mandatory contribution. */
        int mand_start_j = lst;
        int mand_end_j   = est + p;
        for (int t = mand_start_j; t < mand_end_j; t++) {
            if (t < min_t || t >= max_t) continue;
            demand_at[t - min_t] -= h;
        }

        /* Check est: would starting j at est overflow some t? */
        int witness;
        if (!cum_start_feasible(d, demand_at, min_t, max_t, j, est, &witness)) {
            lcg_expl_clear(ctx);
            /* Cite j's current lower bound, so the clause is asserting
             * that est+1 follows from "s_j was previously at est". */
            lcg_expl_lo(ctx, d->start[j], est);
            cum_explain_demand_at(ctx, d, witness, j);
            int r = lcg_emit_ge(ctx, d->start[j], est + 1);
            /* Restore j's mandatory before any early return. */
            for (int t = mand_start_j; t < mand_end_j; t++) {
                if (t < min_t || t >= max_t) continue;
                demand_at[t - min_t] += h;
            }
            if (r == LCG_PROP_CONFLICT) { free(demand_at); return LCG_PROP_CONFLICT; }
            if (r == LCG_PROP_TIGHTENED) any_tight = 1;
            continue;   /* skip lst check; will revisit on next call */
        }

        /* Check lst: would starting j at lst overflow? */
        if (!cum_start_feasible(d, demand_at, min_t, max_t, j, lst, &witness)) {
            lcg_expl_clear(ctx);
            lcg_expl_hi(ctx, d->start[j], lst);
            cum_explain_demand_at(ctx, d, witness, j);
            int r = lcg_emit_le(ctx, d->start[j], lst - 1);
            for (int t = mand_start_j; t < mand_end_j; t++) {
                if (t < min_t || t >= max_t) continue;
                demand_at[t - min_t] += h;
            }
            if (r == LCG_PROP_CONFLICT) { free(demand_at); return LCG_PROP_CONFLICT; }
            if (r == LCG_PROP_TIGHTENED) any_tight = 1;
            continue;
        }

        /* Restore j's mandatory for subsequent tasks. */
        for (int t = mand_start_j; t < mand_end_j; t++) {
            if (t < min_t || t >= max_t) continue;
            demand_at[t - min_t] += h;
        }
    }

    free(demand_at);
    return any_tight ? LCG_PROP_TIGHTENED : LCG_PROP_OK;
}

void lcg_post_cumulative(LcgCtx *ctx,
                         const IntVar *starts,
                         const int    *dur,
                         const int    *demand,
                         int n_tasks,
                         int capacity)
{
    CumData *d = malloc(sizeof(CumData));
    d->n        = n_tasks;
    d->start    = malloc((size_t)n_tasks * sizeof(IntVar));
    d->dur      = malloc((size_t)n_tasks * sizeof(int));
    d->demand   = malloc((size_t)n_tasks * sizeof(int));
    d->capacity = capacity;
    memcpy(d->start,  starts, (size_t)n_tasks * sizeof(IntVar));
    memcpy(d->dur,    dur,    (size_t)n_tasks * sizeof(int));
    memcpy(d->demand, demand, (size_t)n_tasks * sizeof(int));
    LcgPropagator p = { .data = d,
                        .propagate = cum_propagate,
                        .destroy   = cum_destroy };
    lcg_register_propagator(ctx, p);
}

void lcg_post_no_overlap(LcgCtx *ctx,
                         const IntVar *starts,
                         const int    *dur,
                         int n_tasks)
{
    int *unit = malloc((size_t)n_tasks * sizeof(int));
    for (int i = 0; i < n_tasks; i++) unit[i] = 1;
    lcg_post_cumulative(ctx, starts, dur, unit, n_tasks, 1);
    free(unit);
}
