/*
 * ex5_propagation.c -- visible theory propagation.
 *
 * Phase 2 added a theory-to-SAT communication channel: whenever the
 * theory state implies the value of an unassigned literal, the theory
 * pushes that literal onto the SAT trail with a reason clause built
 * from the proof-forest path. This example shows it working.
 *
 * SETUP. Build a chain a_0 = a_1 = ... = a_n via unit assertions, and
 * register the equality atoms (a_0 = a_n), (a_0 = a_{n/2}), and
 * (a_{n/2} = a_n) without putting any of them in a clause. Then run.
 *
 * EXPECTED. UNSAT only if we also assert a contradiction; here we
 * just want satisfiability. Result is SAT with zero SAT decisions:
 *   * The n unit clauses propagate at SAT level (one per chain link).
 *   * The theory processes them in order, merging the chain.
 *   * compute_propagations scans every registered equality atom; the
 *     three derived equalities all hold and none is assigned, so all
 *     three are pushed onto the trail with proof-forest reasons. The
 *     reason for (a_0 = a_n) is the n unit literals (negated) plus
 *     the conclusion -- a clause linear in n, not in n^2 or the
 *     total number of asserted lits.
 *
 * "theory props" counts those three pushes. Without theory
 * propagation the SAT layer would have no information about the
 * derived equalities and would happily branch on them (here, decision
 * count would be at least one).
 */
#include "smt.h"
#include <stdio.h>
#include <stdlib.h>

int main(int argc, char **argv) {
    int N = (argc > 1) ? atoi(argv[1]) : 8;
    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 unit-clause equalities. */
    for (int i = 0; i < N; i++) smt_assert_eq(ctx, a[i], a[i + 1]);

    /* Register three derived-equality atoms (not asserted). */
    (void)smt_mk_eq_atom(ctx, a[0],     a[N]);
    (void)smt_mk_eq_atom(ctx, a[0],     a[N/2]);
    (void)smt_mk_eq_atom(ctx, a[N/2],   a[N]);

    printf("=== Theory propagation visible ===\n");
    printf("  chain length    : %d\n", N);
    printf("  asserted        : a_0 = a_1, ..., a_%d = a_%d  (%d unit clauses)\n",
        N - 1, N, N);
    printf("  registered only : (a_0 = a_%d), (a_0 = a_%d), (a_%d = a_%d)\n",
        N, N/2, N/2, N);
    printf("  atoms total     : %d  (chain + 3 derived)\n", smt_n_atoms(ctx));

    int r = smt_check(ctx);
    printf("  result          : %s\n",
        r == SMT_SAT   ? "SAT (as expected)" :
        r == SMT_UNSAT ? "UNSAT (BUG!)" : "unknown");
    printf("  decisions       = %ld    (expect 0 -- theory determines everything)\n",
        smt_decisions(ctx));
    printf("  theory props    = %ld    (expect 3 -- the registered derived atoms)\n",
        smt_theory_props(ctx));
    printf("  theory conf.    = %ld\n", smt_theory_conflicts(ctx));
    printf("  propagations    = %ld    (BCP-level)\n", smt_propagations(ctx));

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