/*
 * ex1_linear.c -- Phase 1 demonstration: linear feasibility.
 *
 * Three integer variables in [0, 9], a handful of linear constraints,
 * and we ask LCG for a satisfying assignment. The output prints both
 * the witness and the solver's statistics.
 *
 *   x + y      <=  10
 *   y + z      <=   8
 *   2x - z     >=   3       (encoded as -2x + z <= -3)
 *   x          >=   2
 *   z          <=   5
 *
 * This is just enough to exercise:
 *   - order-encoded variable creation
 *   - mixed bound assertions via unit clauses
 *   - the linear_le propagator producing both upper and lower-bound
 *     tightenings from positive and negative coefficients
 *   - the SAT layer driving the search
 *
 * Expected output: a satisfying assignment of (x, y, z) and small
 * statistics (a few decisions, a handful of explanations).
 */
#include "lcg.h"
#include <stdio.h>

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

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

    IntVar x = lcg_new_int_var(ctx, 0, 9, "x");
    IntVar y = lcg_new_int_var(ctx, 0, 9, "y");
    IntVar z = lcg_new_int_var(ctx, 0, 9, "z");

    /* x + y <= 10 */
    { int c[2] = { 1, 1 }; IntVar v[2] = { x, y };
      lcg_post_linear_le(ctx, c, v, 2, 10); }

    /* y + z <= 8 */
    { int c[2] = { 1, 1 }; IntVar v[2] = { y, z };
      lcg_post_linear_le(ctx, c, v, 2, 8); }

    /* 2x - z >= 3   <=>  -2x + z <= -3 */
    { int c[2] = { -2, 1 }; IntVar v[2] = { x, z };
      lcg_post_linear_le(ctx, c, v, 2, -3); }

    /* x >= 2 ; z <= 5 (as unit clauses on the order-encoding atoms) */
    post_unit(ctx, lcg_lit_ge(ctx, x, 2));
    post_unit(ctx, lcg_lit_le(ctx, z, 5));

    int r = lcg_solve(ctx);

    printf("=== Phase 1: linear feasibility ===\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);
        int vy = lcg_value(ctx, y);
        int vz = lcg_value(ctx, z);
        printf("  x              = %d\n", vx);
        printf("  y              = %d\n", vy);
        printf("  z              = %d\n", vz);
        printf("  x + y          = %d  (<= 10)\n", vx + vy);
        printf("  y + z          = %d  (<=  8)\n", vy + vz);
        printf("  2x - z         = %d  (>=  3)\n", 2*vx - vz);
    }
    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;
}
