/*
 * ex2_custom_prop.c -- Phase 2 demo: a user-defined propagator.
 *
 * Phase 2 made the propagator interface a first-class part of the
 * public API. To prove the abstraction is general, this example
 * implements a small propagator OUTSIDE lcg.c and registers it
 * through `lcg_register_propagator`.
 *
 * The propagator is `not_equal(x, k)`: it removes a single value k
 * from x's domain. It is the simplest non-trivial propagator that is
 * not already covered by the bounds API.
 *
 * Logic: if x has been narrowed to exactly k (cur_lo == cur_hi == k),
 * we have a conflict. If cur_lo == k, we tighten cur_lo to k+1 (with
 * the explanation "x >= k AND x <= k", so the negation x != k forces
 * x >= k+1). Symmetrically if cur_hi == k.
 *
 * We use the propagator to express "x in {0, 1, 2, 3, 4, 5, 6, 7, 8, 9} \ {5}"
 * and combine it with a linear constraint to find a feasible value.
 */
#include "lcg.h"
#include <stdio.h>
#include <stdlib.h>

typedef struct {
    IntVar v;
    int    k;
} NotEqData;

static int not_equal_propagate(LcgCtx *ctx, void *data) {
    NotEqData *d = (NotEqData *)data;
    int lo = lcg_lb(ctx, d->v);
    int hi = lcg_ub(ctx, d->v);

    /* Domain wiped out at value k: conflict. Explanation: x >= k AND x <= k. */
    if (lo == d->k && hi == d->k) {
        lcg_expl_clear(ctx);
        lcg_expl_lo(ctx, d->v, d->k);
        lcg_expl_hi(ctx, d->v, d->k);
        return lcg_emit_conflict(ctx);
    }
    /* x is pinned to k from below: push lo up. */
    if (lo == d->k) {
        lcg_expl_clear(ctx);
        lcg_expl_hi(ctx, d->v, d->k);   /* x <= k */
        /* x >= k is the consequence of x not being any of 0..k-1, but
         * the propagator's *current* bound also says x >= k. We cite
         * that. */
        lcg_expl_lo(ctx, d->v, d->k);
        return lcg_emit_ge(ctx, d->v, d->k + 1);
    }
    /* x is pinned to k from above: push hi down. */
    if (hi == d->k) {
        lcg_expl_clear(ctx);
        lcg_expl_lo(ctx, d->v, d->k);
        lcg_expl_hi(ctx, d->v, d->k);
        return lcg_emit_le(ctx, d->v, d->k - 1);
    }
    return LCG_PROP_OK;
}

static void not_equal_destroy(void *data) {
    free(data);
}

static void post_not_equal(LcgCtx *ctx, IntVar v, int k) {
    NotEqData *d = malloc(sizeof(NotEqData));
    d->v = v; d->k = k;
    LcgPropagator p = { .data = d,
                        .propagate = not_equal_propagate,
                        .destroy = not_equal_destroy };
    lcg_register_propagator(ctx, p);
}

static void post_unit(LcgCtx *ctx, int lit) {
    lcg_post_clause(ctx, &lit, 1);
}

int main(void) {
    /* Find x in [0..9] such that:
     *   x + y == 10  (encoded as two linear inequalities)
     *   x != 5
     *   y != 5
     *   y >= 3
     */
    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 <= 10  AND  x + y >= 10 */
    int     c[2] = { 1, 1 };
    IntVar  v[2] = { x, y };
    lcg_post_linear_le(ctx,  c, v, 2,  10);
    int     cn[2] = { -1, -1 };
    lcg_post_linear_le(ctx, cn, v, 2, -10);

    post_not_equal(ctx, x, 5);
    post_not_equal(ctx, y, 5);
    post_unit(ctx, lcg_lit_ge(ctx, y, 3));

    int r = lcg_solve(ctx);

    printf("=== Phase 2: custom propagator (not_equal) ===\n\n");
    printf("  x + y == 10\n");
    printf("  x != 5,  y != 5\n");
    printf("  y >= 3\n\n");
    printf("  status         = %s\n",
        r == LCG_SAT   ? "SAT" :
        r == LCG_UNSAT ? "UNSAT" : "unknown");
    if (r == LCG_SAT) {
        int vx = lcg_value(ctx, x), vy = lcg_value(ctx, y);
        printf("  x              = %d\n", vx);
        printf("  y              = %d\n", vy);
        printf("  x + y          = %d  (== 10)\n", vx + vy);
    }
    printf("\n  decisions      = %ld\n", lcg_decisions   (ctx));
    printf("  conflicts      = %ld\n",   lcg_conflicts   (ctx));
    printf("  explanations   = %ld\n",   lcg_explanations(ctx));

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