/*
 * ex8_no_basic.c -- Nelson-Oppen: EUF tells LRA.
 *
 *   f(x) != f(y)  AND  shared_eq(x, y).
 *
 * The shared_eq asserts the EUF equality atom for the (x, y) pair.
 * EUF receives it, merges x.euf and y.euf in its union-find, and
 * congruence on f gives f(x) = f(y), which conflicts with the
 * inequality. UNSAT in 0 decisions, 1 theory conflict.
 *
 * The EUF -> LRA bridge clauses (eq -> le, eq -> ge) also fire here,
 * propagating x.lra - y.lra <= 0 and y.lra - x.lra <= 0 into LRA,
 * but LRA has nothing else to constrain, so they have no consequence.
 * The arrow is "live" but inert.
 */
#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);
    smt_assert_shared_eq(ctx, x, y);

    int r = smt_check(ctx);

    printf("=== Phase 4: Nelson-Oppen, EUF -> LRA arrow ===\n");
    printf("\n  Constraints:\n"
           "    f(x) != f(y)\n"
           "    shared_eq(x, 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  (0: SAT never has to guess)\n",
           smt_decisions(ctx));
    printf("  theory conf.  = %ld  (1: EUF congruence on f closes it)\n",
           smt_theory_conflicts(ctx));
    printf("  theory props  = %ld\n", smt_theory_props(ctx));
    smt_free(ctx);
    return r == SMT_UNSAT ? 0 : 1;
}
