/*
 * ex9_no_arithmetic.c -- Nelson-Oppen: LRA tells EUF.
 *
 *   x = 5,  y = 5,  f(x) != f(y).
 *
 * This is the other direction of the NO information exchange. LRA
 * pins x and y to the same value (5). The bridge slacks x - y and
 * y - x both have implied upper bound 0 from the tableau, so LRA
 * theory-propagates the two bridge atoms le_xy and ge_xy.
 *
 * BCP on the bridge clause (le_xy & ge_xy) -> eq_xy then fires:
 * eq_xy is forced true. EUF receives it, merges x.euf and y.euf,
 * congruence on f forces f(x) = f(y), conflict with f(x) != f(y).
 * UNSAT.
 *
 * Read the stats: 0 SAT decisions, >= 2 theory propagations from
 * LRA (the two bridge atoms), 1 theory conflict from the final EUF
 * congruence step.
 */
#include "smt.h"
#include <stdio.h>

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

    int fx = smt_mk_app(ctx, "f", &x.euf, 1);
    int fy = smt_mk_app(ctx, "f", &y.euf, 1);
    smt_assert_neq(ctx, fx, fy);

    SmtLinTerm xt = {x.lra, 1, 1};
    SmtLinTerm yt = {y.lra, 1, 1};
    smt_assert_lra_eq(ctx, &xt, 1, 5, 1);
    smt_assert_lra_eq(ctx, &yt, 1, 5, 1);

    int r = smt_check(ctx);

    printf("=== Phase 4: Nelson-Oppen, LRA -> EUF arrow ===\n");
    printf("\n  Constraints:\n"
           "    x = 5\n"
           "    y = 5\n"
           "    f(x) != f(y)\n\n");
    printf("  result        : %s\n",
           r == SMT_UNSAT ? "UNSAT" :
           r == SMT_SAT   ? "SAT (BUG)" : "unknown");
    printf("  atoms         = %d\n",  smt_n_atoms(ctx));
    printf("  decisions     = %ld\n", smt_decisions(ctx));
    printf("  theory conf.  = %ld  (1: final EUF closure on f)\n",
           smt_theory_conflicts(ctx));
    printf("  theory props  = %ld  (>= 2: bridge atoms from LRA)\n",
           smt_theory_props(ctx));
    printf("  LRA pivots    = %ld\n", smt_lra_pivots(ctx));
    smt_free(ctx);
    return r == SMT_UNSAT ? 0 : 1;
}
