/*
 * ex6_lra_basic.c -- the canonical Farkas-style LRA UNSAT.
 *
 *   x + y <= 5,   x > 3,   y > 3
 *
 * Adding the lower bounds: x + y > 6, which contradicts the upper
 * bound x + y <= 5. The SMT solver discovers this contradiction
 * inside the LRA theory and emits a single-clause learned conflict
 * naming exactly the three bounds at fault -- no SAT decisions
 * required.
 */
#include "smt.h"
#include <stdio.h>

int main(void) {
    SmtCtx *ctx = smt_new();
    int x = smt_mk_real_var(ctx, "x");
    int y = smt_mk_real_var(ctx, "y");

    /* x + y <= 5 */
    SmtLinTerm xy[2] = { {x, 1, 1}, {y, 1, 1} };
    smt_assert_lra_le(ctx, xy, 2, 5, 1);

    /* x > 3  (asserted as the negation of (x <= 3)) */
    SmtLinTerm xt = {x, 1, 1};
    int a_xle3 = smt_mk_lra_le_atom(ctx, &xt, 1, 3, 1);
    int u1 = -a_xle3;
    smt_assert_clause(ctx, &u1, 1);

    /* y > 3 */
    SmtLinTerm yt = {y, 1, 1};
    int a_yle3 = smt_mk_lra_le_atom(ctx, &yt, 1, 3, 1);
    int u2 = -a_yle3;
    smt_assert_clause(ctx, &u2, 1);

    int r = smt_check(ctx);

    printf("=== Phase 3: Farkas UNSAT (linear arithmetic) ===\n");
    printf("\nConstraints:\n"
           "    x + y <= 5\n"
           "    x > 3\n"
           "    y > 3\n");
    printf("\nFarkas witness: take the constraints as written, with\n"
           "multipliers (1, 1, 1) on (x>3, y>3, x+y<=5 negated). The\n"
           "sum is  6 < x + y <= 5, immediate contradiction.\n");

    printf("\n  result        : %s\n",
           r == SMT_UNSAT ? "UNSAT" :
           r == SMT_SAT   ? "SAT (BUG)" : "unknown");
    printf("  decisions     = %ld    (expect 0: theory alone refutes)\n",
           smt_decisions(ctx));
    printf("  theory conf.  = %ld    (expect 1: the Farkas certificate)\n",
           smt_theory_conflicts(ctx));
    printf("  LRA pivots    = %ld\n", smt_lra_pivots(ctx));
    smt_free(ctx);
    return r == SMT_UNSAT ? 0 : 1;
}
