/*
 * ex5_dwta.c -- Dynamic Weapon-Target Assignment as a cumulative
 *               scheduling problem.
 *
 *
 *   SCENARIO
 *
 * A naval combatant has a fire-control radar with K = 2 illumination
 * channels. Each engagement requires one channel for the full duration
 * from launch through intercept. Six threats are inbound, each with:
 *
 *   - an "arrival" time     (time the threat enters engagement envelope)
 *   - a "deadline" time     (time the threat impacts; engagement must
 *                            complete strictly before this)
 *   - an engagement duration (interceptor flight time + safety margin)
 *
 * The doctrine: every threat must be engaged at least once, completely
 * within its [arrival, deadline) window, and the K = 2 channel capacity
 * must never be exceeded.
 *
 *
 *   MODEL
 *
 * One integer variable per threat: start_i = time the engagement begins.
 *
 *   start_i  in  [arrival_i,  deadline_i - duration_i]
 *
 * with one global cumulative constraint:
 *
 *   for all t:  count of i such that start_i <= t < start_i + duration_i
 *               must be at most K.
 *
 * If a feasible schedule exists, the solver finds one. If the threat
 * picture is over-saturated relative to channel capacity, the cumulative
 * propagator's time-table reasoning detects the conflict and the solver
 * returns UNSAT (typically after some search; sometimes at the root).
 *
 *
 *   WHY THIS IS A GOOD FIT FOR LCG
 *
 * Pure SAT would have to encode the cumulative constraint as a sea of
 * pseudo-Boolean inequalities, one per time point. The propagator does
 * the same reasoning lazily, generating CDCL-shaped explanations only
 * for the dead ends actually visited. The clauses learnt during search
 * cut off similar dead ends elsewhere in the tree, even though they
 * were never enumerated explicitly.
 */
#include "lcg.h"

#include <stdio.h>
#include <stdlib.h>

typedef struct {
    const char *id;            /* short id, e.g. "T0"                       */
    const char *kind;          /* descriptive kind, e.g. "drone-A"          */
    int   arrival;
    int   deadline;
    int   duration;
} Threat;

int main(void) {
    Threat threats[] = {
        { "T0", "drone-A",         0,  4,  2 },
        { "T1", "cruise-missile",  0,  5,  3 },
        { "T2", "drone-B",         2,  6,  2 },
        { "T3", "anti-ship",       3,  8,  3 },
        { "T4", "drone-C",         4,  8,  2 },
        { "T5", "cruise-missile",  5, 10,  3 },
    };
    int N = (int)(sizeof threats / sizeof threats[0]);
    int K = 2;       /* fire-control channels */

    LcgCtx *ctx = lcg_new();

    IntVar *start = malloc((size_t)N * sizeof(IntVar));
    int    *du    = malloc((size_t)N * sizeof(int));
    int    *de    = malloc((size_t)N * sizeof(int));

    for (int i = 0; i < N; i++) {
        Threat *t = &threats[i];
        int latest_start = t->deadline - t->duration;
        start[i] = lcg_new_int_var(ctx, t->arrival, latest_start, t->id);
        du[i]    = t->duration;
        de[i]    = 1;      /* each engagement uses one channel */
    }
    lcg_post_cumulative(ctx, start, du, de, N, K);

    int r = lcg_solve(ctx);

    printf("=== DWTA: naval air-defense channel scheduling ===\n\n");
    printf("  channels K   = %d\n", K);
    printf("  threats      = %d\n\n", N);
    printf("  status       = %s\n",
        r == LCG_SAT   ? "FEASIBLE engagement schedule found" :
        r == LCG_UNSAT ? "INFEASIBLE  (defence over-saturated)" :
                         "unknown");

    if (r == LCG_SAT) {
        printf("\n  schedule:\n");
        printf("    threat               arr  ddl  dur   start  end\n");
        for (int i = 0; i < N; i++) {
            int st = lcg_value(ctx, start[i]);
            char label[32];
            snprintf(label, sizeof label, "%s %s", threats[i].id, threats[i].kind);
            printf("    %-18s %4d %4d %4d    %4d %4d\n",
                   label,
                   threats[i].arrival, threats[i].deadline, threats[i].duration,
                   st, st + threats[i].duration);
        }

        /* Find time extent. */
        int max_end = 0;
        for (int i = 0; i < N; i++) {
            int e = lcg_value(ctx, start[i]) + threats[i].duration;
            if (e > max_end) max_end = e;
        }

        /* Gantt chart. */
        printf("\n  timeline:\n    t :  ");
        for (int t = 0; t < max_end; t++) printf("%2d ", t);
        printf("\n");
        for (int i = 0; i < N; i++) {
            int st = lcg_value(ctx, start[i]);
            printf("    %-3s  ", threats[i].id);
            for (int t = 0; t < max_end; t++) {
                if (t >= st && t < st + threats[i].duration) printf(" # ");
                else                                          printf(" . ");
            }
            putchar('\n');
        }
        printf("    Σ    ");
        for (int t = 0; t < max_end; t++) {
            int load = 0;
            for (int i = 0; i < N; i++) {
                int st = lcg_value(ctx, start[i]);
                if (t >= st && t < st + threats[i].duration) load++;
            }
            printf("%2d ", load);
        }
        printf("    (cap = %d)\n", K);
    }

    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));

    free(start); free(du); free(de);
    lcg_free(ctx);
    return r == LCG_SAT ? 0 : 1;
}
