/*
 * ex11_ui_row_layout.c -- A row of four buttons with spacing.
 *
 * Four buttons B0..B3, each 30 wide, laid out left-to-right with at
 * least 5px between adjacent buttons. The row must fit in 200 pixels.
 *
 * Layout constraints:
 *   B0.x >= 0
 *   B[i].x + 30 + 5 <= B[i+1].x        for i in 0..2
 *   B3.x + 30 <= 200
 *
 * Modelled as an ordering chain rather than a quadratic non-overlap
 * disjunction. The chain is much tighter for SAT to reason about --
 * there are no disjunctions at all, so the solver finds a model in 0
 * decisions and 0 conflicts.
 *
 * This is the "happy path" SMT layout: when the visual structure
 * imposes a total order (a row, a column, a list), you can encode it
 * as a chain of inequalities and the solver runs in time linear in
 * the chain length.
 *
 * Expected: SAT, 0 decisions, 0 conflicts.
 */
#include "smt.h"
#include <stdio.h>

#define N         4
#define BOX_W    30
#define GAP       5
#define CANVAS_W 200

int main(void) {
    SmtCtx *ctx = smt_new();

    int x[N];
    char name[8];
    for (int i = 0; i < N; i++) {
        snprintf(name, sizeof name, "B%d.x", i);
        x[i] = smt_mk_real_var(ctx, name);
    }

    /* B0.x >= 0 (encoded as -B0.x <= 0) */
    SmtLinTerm neg0 = { x[0], -1, 1 };
    smt_assert_lra_le(ctx, &neg0, 1, 0, 1);

    /* For each adjacent pair: B[i].x - B[i+1].x <= -(BOX_W + GAP) */
    for (int i = 0; i + 1 < N; i++) {
        SmtLinTerm gap[2] = { { x[i], 1, 1 }, { x[i+1], -1, 1 } };
        smt_assert_lra_le(ctx, gap, 2, -(BOX_W + GAP), 1);
    }

    /* B[N-1].x + BOX_W <= CANVAS_W, i.e. B[N-1].x <= CANVAS_W - BOX_W */
    SmtLinTerm last = { x[N-1], 1, 1 };
    smt_assert_lra_le(ctx, &last, 1, CANVAS_W - BOX_W, 1);

    int r = smt_check(ctx);

    printf("=== UI: four buttons in a row ===\n\n");
    printf("  buttons        = %d\n", N);
    printf("  box width      = %d\n", BOX_W);
    printf("  gap            = %d\n", GAP);
    printf("  canvas width   = %d\n", CANVAS_W);
    printf("  result         = %s\n",
           r == SMT_SAT   ? "SAT (valid layout)" :
           r == SMT_UNSAT ? "UNSAT (infeasible)" : "unknown");
    printf("  decisions      = %ld (expect 0: pure chain, no disjunction)\n",
           smt_decisions(ctx));
    printf("  theory conf.   = %ld\n", smt_theory_conflicts(ctx));
    printf("  LRA pivots     = %ld\n", smt_lra_pivots(ctx));
    smt_free(ctx);
    return r == SMT_SAT ? 0 : 1;
}
