/*
 * ex10_ui_two_boxes.c -- The smallest possible UI-placement problem.
 *
 * Two rectangles A and B, each 40 wide, must fit in a 100-wide canvas
 * without overlapping. Modelled as four real-valued variables:
 *
 *   A.x, A.y   top-left of A
 *   B.x, B.y   top-left of B
 *
 * (Heights and widths are constants -- we model only the free
 * coordinates.)
 *
 * Constraints:
 *
 *   0 <= A.x,            A.x + 40 <= 100      (A fits horizontally)
 *   0 <= B.x,            B.x + 40 <= 100      (B fits horizontally)
 *
 *   non-overlap on x:    A.x + 40 <= B.x  OR  B.x + 40 <= A.x
 *
 * The non-overlap is a disjunction over two LRA atoms -- exactly the
 * sort of thing pure simplex can't handle but SMT eats natively. SAT
 * branches on the disjunction; for each branch LRA either finds a
 * model or sends back a Farkas conflict. The combination is small
 * enough here that SAT picks the right branch with no backtracking.
 *
 * Expected: SAT, 0-1 decisions.
 */
#include "smt.h"
#include <stdio.h>

#define CANVAS_W 100
#define BOX_W     40

int main(void) {
    SmtCtx *ctx = smt_new();
    int ax = smt_mk_real_var(ctx, "A.x");
    int bx = smt_mk_real_var(ctx, "B.x");

    SmtLinTerm a = { ax, 1, 1 };
    SmtLinTerm b = { bx, 1, 1 };

    /* A on canvas: 0 <= A.x  AND  A.x + BOX_W <= CANVAS_W
     *              i.e.  A.x <= CANVAS_W - BOX_W  AND  -A.x <= 0 */
    smt_assert_lra_le(ctx, &a, 1, CANVAS_W - BOX_W, 1);
    SmtLinTerm neg_a = { ax, -1, 1 };
    smt_assert_lra_le(ctx, &neg_a, 1, 0, 1);

    smt_assert_lra_le(ctx, &b, 1, CANVAS_W - BOX_W, 1);
    SmtLinTerm neg_b = { bx, -1, 1 };
    smt_assert_lra_le(ctx, &neg_b, 1, 0, 1);

    /* Non-overlap: A.x + 40 <= B.x  OR  B.x + 40 <= A.x.
     * Encoded as two atoms in one disjunctive clause. */
    SmtLinTerm a_minus_b[2] = { { ax, 1, 1 }, { bx, -1, 1 } };
    SmtLinTerm b_minus_a[2] = { { bx, 1, 1 }, { ax, -1, 1 } };
    int a_left  = smt_mk_lra_le_atom(ctx, a_minus_b, 2, -BOX_W, 1);  /* A.x - B.x <= -40 */
    int b_left  = smt_mk_lra_le_atom(ctx, b_minus_a, 2, -BOX_W, 1);  /* B.x - A.x <= -40 */
    int cl[2] = { a_left, b_left };
    smt_assert_clause(ctx, cl, 2);

    int r = smt_check(ctx);

    printf("=== UI: two non-overlapping boxes in a row ===\n\n");
    printf("  canvas width   = %d\n", CANVAS_W);
    printf("  box width      = %d\n", BOX_W);
    printf("  result         = %s\n",
           r == SMT_SAT   ? "SAT (valid layout exists)" :
           r == SMT_UNSAT ? "UNSAT (infeasible)" : "unknown");
    printf("  decisions      = %ld\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;
}
