/*
 * ex4_cumulative.c -- Phase 4 demonstration: cumulative scheduling.
 *
 * Five tasks must each run for some duration, sharing a renewable
 * resource with capacity 3. Each task has a release window: it may
 * start no earlier than its release time and no later than its
 * deadline minus duration.
 *
 *     task   duration   release  deadline   demand
 *      T0       3          0        8        2
 *      T1       2          0        6        1
 *      T2       3          2        9        2
 *      T3       2          1        5        1
 *      T4       4          0        10       1
 *
 * Capacity = 3.
 *
 * The cumulative propagator's time-table reasoning prunes the search
 * space by computing each task's mandatory part (when ub(start) <
 * lb(start) + duration) and propagating bound tightenings whenever
 * scheduling a task at a particular start would push some time-point
 * over capacity. The clauses learned along the way prevent the SAT
 * engine from re-exploring the same dead ends.
 */
#include "lcg.h"

#include <stdio.h>

int main(void) {
    LcgCtx *ctx = lcg_new();

    /* Task parameters (release, deadline, duration, demand). */
    int rel[5]  = { 0, 0, 2, 1, 0 };
    int dl [5]  = { 8, 6, 9, 5, 10 };
    int du [5]  = { 3, 2, 3, 2, 4  };
    int de [5]  = { 2, 1, 2, 1, 1  };

    /* Start-time variables. */
    IntVar s[5];
    char name[8];
    for (int i = 0; i < 5; i++) {
        snprintf(name, sizeof name, "T%d", i);
        /* latest start = deadline - duration */
        s[i] = lcg_new_int_var(ctx, rel[i], dl[i] - du[i], name);
    }

    lcg_post_cumulative(ctx, s, du, de, 5, /*capacity=*/3);

    int r = lcg_solve(ctx);

    printf("=== Phase 4: cumulative scheduling ===\n\n");
    printf("  status         = %s\n",
        r == LCG_SAT   ? "SAT" :
        r == LCG_UNSAT ? "UNSAT" : "unknown");

    if (r == LCG_SAT) {
        printf("\n  schedule:\n");
        for (int i = 0; i < 5; i++) {
            int st = lcg_value(ctx, s[i]);
            printf("    T%d  start=%2d  end=%2d  demand=%d\n",
                   i, st, st + du[i], de[i]);
        }
        /* Print a Gantt-style timeline. */
        int max_end = 0;
        for (int i = 0; i < 5; i++) {
            int e = lcg_value(ctx, s[i]) + du[i];
            if (e > max_end) max_end = e;
        }
        printf("\n  timeline (0..%d):\n", max_end - 1);
        printf("    t :  ");
        for (int t = 0; t < max_end; t++) printf("%2d ", t);
        printf("\n");
        for (int i = 0; i < 5; i++) {
            printf("    T%d:  ", i);
            int st = lcg_value(ctx, s[i]);
            for (int t = 0; t < max_end; t++) {
                if (t >= st && t < st + du[i]) printf(" # ");
                else                            printf(" . ");
            }
            printf("\n");
        }
        /* Per-time-point demand */
        printf("    Σ :  ");
        for (int t = 0; t < max_end; t++) {
            int load = 0;
            for (int i = 0; i < 5; i++) {
                int st = lcg_value(ctx, s[i]);
                if (t >= st && t < st + du[i]) load += de[i];
            }
            printf("%2d ", load);
        }
        printf("    (capacity = 3)\n");
    }

    printf("\n  decisions      = %ld\n", lcg_decisions   (ctx));
    printf("  conflicts      = %ld\n",   lcg_conflicts   (ctx));
    printf("  propagations   = %ld\n",   lcg_propagations(ctx));
    printf("  explanations   = %ld\n",   lcg_explanations(ctx));

    lcg_free(ctx);
    return r == LCG_SAT ? 0 : 1;
}
