/*
 * ex1_transitivity.c -- the classical transitivity refutation.
 *
 * Build a chain a_0 = a_1, a_1 = a_2, ..., a_{n-1} = a_n, then assert
 * a_0 != a_n. The theory must close the chain transitively and detect
 * the contradiction.
 *
 * What this exercises:
 *
 *   - The core EUF union-find: every assertion unions two terms, and
 *     by the end of the chain a_0 and a_n are in the same equivalence
 *     class.
 *   - Theory conflict detection: the asserted disequality clashes with
 *     the discovered equality.
 *   - The DPLL(T) integration: with no Boolean structure beyond unit
 *     clauses, the SAT layer just hands every assertion to the theory.
 *     Theory does the entire decision; the SAT solver acts as a passive
 *     orchestrator.
 */
#include "smt.h"
#include <stdio.h>
#include <stdlib.h>

int main(int argc, char **argv) {
    int N = (argc > 1) ? atoi(argv[1]) : 12;
    if (N < 2 || N > 1000) { fprintf(stderr, "N out of range\n"); return 1; }

    SmtCtx *ctx = smt_new();

    int *a = malloc((size_t)(N + 1) * sizeof(int));
    char name[32];
    for (int i = 0; i <= N; i++) {
        snprintf(name, sizeof(name), "a%d", i);
        a[i] = smt_mk_const(ctx, name);
    }

    /* Chain of equalities. */
    for (int i = 0; i < N; i++) smt_assert_eq(ctx, a[i], a[i + 1]);

    /* The fatal disequality. */
    smt_assert_neq(ctx, a[0], a[N]);

    printf("=== Transitivity chain ===\n");
    printf("  length     : %d (a_0 = a_1 = ... = a_%d, a_0 != a_%d)\n", N, N, N);
    printf("  terms      : %d\n", smt_n_terms(ctx));
    printf("  atoms      : %d\n", smt_n_atoms(ctx));

    int r = smt_check(ctx);
    printf("  result     : %s\n",
        r == SMT_UNSAT ? "UNSAT (as expected)" :
        r == SMT_SAT   ? "SAT (BUG!)" : "unknown");
    printf("  decisions     = %ld\n", smt_decisions(ctx));
    printf("  conflicts     = %ld\n", smt_conflicts(ctx));
    printf("  theory conf.  = %ld\n", smt_theory_conflicts(ctx));
    printf("  theory props  = %ld\n", smt_theory_props(ctx));
    printf("  propagations  = %ld\n", smt_propagations(ctx));

    free(a);
    smt_free(ctx);
    return r == SMT_UNSAT ? 0 : 1;
}
