/*
 * ex13_ui_toolbar.c -- A realistic small-toolbar layout.
 *
 * Three icon buttons (24 x 24) in a horizontal toolbar (240 x 40)
 * with the following design constraints:
 *
 *   1. Buttons fit inside the toolbar.
 *   2. Buttons don't overlap each other.
 *   3. Buttons are vertically centered in the toolbar
 *      (B.y == (40 - 24) / 2 == 8).
 *   4. Equal horizontal spacing -- the gap between B0 and B1 equals
 *      the gap between B1 and B2.
 *   5. The leftmost button starts at x >= 8 (left padding).
 *   6. The rightmost button ends at x + 24 <= 240 - 8 (right padding).
 *
 * This is the pattern any reasonable horizontal toolbar uses, and
 * it is what makes SMT pay over a plain CSP: the alignment (3) and
 * equal-spacing (4) constraints are linear equalities that LRA
 * handles directly. The non-overlap (2) and padding (1, 5, 6) are
 * inequalities, also linear. None of this involves arithmetic
 * outside what the simplex tableau can take in stride.
 *
 * Equal spacing as an equality:
 *
 *   B1.x - (B0.x + 24)  ==  B2.x - (B1.x + 24)
 *   <=>  2 * B1.x - B0.x - B2.x == 0
 *
 * Expected: SAT, very small search.
 */
#include "smt.h"
#include <stdio.h>

#define TOOLBAR_W  240
#define TOOLBAR_H   40
#define ICON       24
#define PADDING     8

int main(void) {
    SmtCtx *ctx = smt_new();
    int x0 = smt_mk_real_var(ctx, "B0.x");
    int y0 = smt_mk_real_var(ctx, "B0.y");
    int x1 = smt_mk_real_var(ctx, "B1.x");
    int y1 = smt_mk_real_var(ctx, "B1.y");
    int x2 = smt_mk_real_var(ctx, "B2.x");
    int y2 = smt_mk_real_var(ctx, "B2.y");

    /* Padding-aware horizontal bounds: PADDING <= x  AND  x + ICON <= W - PADDING. */
    int xs[3] = { x0, x1, x2 };
    int ys[3] = { y0, y1, y2 };
    for (int i = 0; i < 3; i++) {
        SmtLinTerm pos = { xs[i],  1, 1 }, neg = { xs[i], -1, 1 };
        smt_assert_lra_le(ctx, &pos, 1, TOOLBAR_W - ICON - PADDING, 1);
        smt_assert_lra_le(ctx, &neg, 1, -PADDING, 1);
    }

    /* Vertical centering: y == (TOOLBAR_H - ICON) / 2  for each button.
     * In our integer model, TOOLBAR_H - ICON = 16, so y = 8. */
    for (int i = 0; i < 3; i++) {
        SmtLinTerm yt = { ys[i], 1, 1 };
        smt_assert_lra_eq(ctx, &yt, 1, (TOOLBAR_H - ICON) / 2, 1);
    }

    /* Horizontal ordering and non-overlap: B0 left of B1 left of B2. */
    {
        SmtLinTerm chain01[2] = { { x0, 1, 1 }, { x1, -1, 1 } };
        SmtLinTerm chain12[2] = { { x1, 1, 1 }, { x2, -1, 1 } };
        smt_assert_lra_le(ctx, chain01, 2, -ICON, 1);  /* x0 + ICON <= x1 */
        smt_assert_lra_le(ctx, chain12, 2, -ICON, 1);  /* x1 + ICON <= x2 */
    }

    /* Equal horizontal spacing: 2*B1.x == B0.x + B2.x. */
    {
        SmtLinTerm spacing[3] = { { x1, 2, 1 }, { x0, -1, 1 }, { x2, -1, 1 } };
        smt_assert_lra_eq(ctx, spacing, 3, 0, 1);
    }

    int r = smt_check(ctx);

    printf("=== UI: toolbar with three centered, equally-spaced icons ===\n\n");
    printf("  toolbar        = %d x %d\n", TOOLBAR_W, TOOLBAR_H);
    printf("  icon           = %d x %d\n", ICON, ICON);
    printf("  padding        = %d\n", PADDING);
    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("  LRA pivots     = %ld\n", smt_lra_pivots(ctx));
    smt_free(ctx);
    return r == SMT_SAT ? 0 : 1;
}
