/*
 * ex12_ui_grid_placement.c -- 2D non-overlap of free boxes.
 *
 * Place four boxes (B0..B3) anywhere in a 100 x 100 canvas so that
 * no two overlap. Each box is 40 wide x 30 tall.
 *
 * The key constraint is rectangle non-overlap, which is not a linear
 * inequality on its own -- two rectangles fail to overlap iff *at
 * least one* of four conditions holds:
 *
 *   A.right <= B.left   (A is to the left of B)
 *   B.right <= A.left   (A is to the right of B)
 *   A.bottom <= B.top   (A is above B)        [y grows downward]
 *   B.bottom <= A.top   (A is below B)
 *
 * In SMT this is a four-literal clause per pair of boxes. With N
 * boxes you get N*(N-1)/2 such clauses. SAT enumerates the cases;
 * LRA refutes the infeasible ones. With N = 4 the solver does a
 * few decisions and finds a model.
 *
 * Expected: SAT, a small number of decisions, no learned conflicts
 * needed in the best case.
 */
#include "smt.h"
#include <stdio.h>

#define N         4
#define CANVAS_W 100
#define CANVAS_H 100
#define BOX_W     40
#define BOX_H     30

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

    int x[N], y[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);
        snprintf(name, sizeof name, "B%d.y", i); y[i] = smt_mk_real_var(ctx, name);
    }

    /* Canvas bounds for each box: 0 <= x, x + BOX_W <= W, same for y. */
    for (int i = 0; i < N; i++) {
        SmtLinTerm pos_x = { x[i],  1, 1 }, neg_x = { x[i], -1, 1 };
        SmtLinTerm pos_y = { y[i],  1, 1 }, neg_y = { y[i], -1, 1 };
        smt_assert_lra_le(ctx, &pos_x, 1, CANVAS_W - BOX_W, 1);
        smt_assert_lra_le(ctx, &neg_x, 1, 0, 1);
        smt_assert_lra_le(ctx, &pos_y, 1, CANVAS_H - BOX_H, 1);
        smt_assert_lra_le(ctx, &neg_y, 1, 0, 1);
    }

    /* Non-overlap on each pair (i, j) with i < j. */
    for (int i = 0; i < N; i++) {
        for (int j = i + 1; j < N; j++) {
            /* i.x + BOX_W <= j.x   <=>   i.x - j.x <= -BOX_W */
            SmtLinTerm ix_minus_jx[2] = { { x[i], 1, 1 }, { x[j], -1, 1 } };
            SmtLinTerm jx_minus_ix[2] = { { x[j], 1, 1 }, { x[i], -1, 1 } };
            SmtLinTerm iy_minus_jy[2] = { { y[i], 1, 1 }, { y[j], -1, 1 } };
            SmtLinTerm jy_minus_iy[2] = { { y[j], 1, 1 }, { y[i], -1, 1 } };

            int left  = smt_mk_lra_le_atom(ctx, ix_minus_jx, 2, -BOX_W, 1);
            int right = smt_mk_lra_le_atom(ctx, jx_minus_ix, 2, -BOX_W, 1);
            int above = smt_mk_lra_le_atom(ctx, iy_minus_jy, 2, -BOX_H, 1);
            int below = smt_mk_lra_le_atom(ctx, jy_minus_iy, 2, -BOX_H, 1);

            int cl[4] = { left, right, above, below };
            smt_assert_clause(ctx, cl, 4);
        }
    }

    int r = smt_check(ctx);

    printf("=== UI: 2D non-overlap of %d boxes ===\n\n", N);
    printf("  canvas         = %d x %d\n", CANVAS_W, CANVAS_H);
    printf("  box            = %d x %d\n", BOX_W, BOX_H);
    printf("  pairs          = %d (each: 4-literal non-overlap clause)\n",
           N * (N - 1) / 2);
    printf("  result         = %s\n",
           r == SMT_SAT   ? "SAT (valid layout)" :
           r == SMT_UNSAT ? "UNSAT (infeasible)" : "unknown");
    printf("  atoms          = %d\n",   smt_n_atoms(ctx));
    printf("  decisions      = %ld\n",  smt_decisions(ctx));
    printf("  theory conf.   = %ld\n",  smt_theory_conflicts(ctx));
    printf("  conflicts      = %ld\n",  smt_conflicts(ctx));
    printf("  LRA pivots     = %ld\n",  smt_lra_pivots(ctx));
    smt_free(ctx);
    return r == SMT_SAT ? 0 : 1;
}
