/*
 * euf.c -- congruence closure with proof-forest explanations,
 *          theory propagation, and use lists.
 *
 * Phase 2 upgrade to Phase 1's basic congruence closure:
 *
 *   - Proof forest. Each term carries a `proof_parent` pointer and a
 *     `proof_label`; the chains within an equivalence class form a tree
 *     whose edges record either the input literal that asserted a merge
 *     or "congruence", meaning the two endpoints are function
 *     applications whose arguments are pairwise equivalent. Explanations
 *     for conflicts and propagations are computed by walking these
 *     proof chains to a lowest common ancestor.
 *
 *   - Theory propagation. After each batch of assertions, scan the
 *     registered equality atoms; any unassigned atom whose terms have
 *     become equivalent is queued for propagation (with reason = the
 *     proof-forest explanation), and any unassigned atom whose terms
 *     belong to classes with an asserted disequality between them is
 *     queued for NEGATIVE propagation.
 *
 *   - Use lists. Each term holds a list of function applications that
 *     mention it directly as an argument; we use them to bound the
 *     congruence-candidate search rather than re-scanning all terms.
 */
#include "euf.h"

#include <stdio.h>
#include <stdlib.h>
#include <string.h>
#include <assert.h>

/* ====== terms ====== */
typedef struct {
    char *name;
    int   n_args;
    int  *args;
} Term;

typedef struct {
    int *buf;
    int  n, cap;
} UseList;

/* Proof-forest label kinds. */
enum { PL_NONE = 0, PL_LIT = 1, PL_CONG = 2 };

typedef struct {
    int term;
    int old_parent;
    int old_kind;
    int old_atom;
} ProofUndo;

typedef struct {
    int  lit;            /* DIMACS lit: +atom or -atom */
    int *reason;         /* clause; reason[0] == lit */
    int  n_reason;
    int  reason_cap;
} Prop;

struct EUF {
    /* terms */
    Term *terms;
    int   n_terms, cap_terms;

    /* union-find */
    int *parent;
    int *size;

    /* union-find merge trail */
    int *merge_trail;
    int  n_merges, cap_merges;

    /* For each merge i: pre-merge size of uses[surviving root].
     * On merge we append the demoted class's use list onto the
     * surviving root's list so uses[r] reflects the whole class
     * when r is the class root; on undo we truncate back. */
    int *merge_use_size;
    int  cap_merge_use;

    /* proof forest */
    int *proof_parent;
    int *proof_kind;
    int *proof_atom;
    ProofUndo *proof_trail;
    int        n_proof_trail, cap_proof_trail;

    /* use lists, indexed by term id */
    UseList *uses;

    /* registered equality atoms */
    struct { int atom, t1, t2; } *eq;
    int n_eq, cap_eq;

    int *atom_idx;
    int  cap_atom_idx;

    /* atom assignment state: 1=true, 0=false, -1=unassigned */
    int *atom_state;
    int  cap_atom_state;

    /* SAT-asserted lits, in order */
    int *asserts;
    int  n_asserts, cap_asserts;

    /* check_pos: position up to which check() has processed.
     * pre_*[i]: trail sizes captured at assign-time for assert i. */
    int  check_pos;
    int *pre_merge, *pre_proof, *pre_propq;
    int  cap_pre;

    /* asserted disequalities */
    int *diseq_atoms;
    int  n_diseq, cap_diseq;

    /* propagation queue */
    Prop *propq;
    int   n_propq, cap_propq;
    int   propq_head;

    /* conflict buffer */
    int *conf_buf;
    int  conf_n, cap_conf;

    /* explain() scratch */
    int *explain_seen_atom;
    int  cap_explain_seen_atom;
    int *path_mark;
    int *path_mark_stack;
    int  path_mark_top, cap_path_mark;
    int *pending_a, *pending_b;
    int  n_pending, cap_pending;

    /* stats */
    long n_propagations;
    long n_explained;
};

/* ====== dynamic array helpers ====== */
static void grow_int(int **buf, int *cap, int want) {
    if (want <= *cap) return;
    int nc = *cap ? *cap * 2 : 8;
    while (nc < want) nc *= 2;
    *buf = realloc(*buf, (size_t)nc * sizeof(int));
    *cap = nc;
}
static void use_push(UseList *u, int t) {
    if (u->n == u->cap) {
        u->cap = u->cap ? u->cap * 2 : 4;
        u->buf = realloc(u->buf, (size_t)u->cap * sizeof(int));
    }
    u->buf[u->n++] = t;
}

/* ====== terms / hash-cons ====== */
static int term_equal(const Term *a, const Term *b) {
    if (strcmp(a->name, b->name) != 0) return 0;
    if (a->n_args != b->n_args) return 0;
    for (int i = 0; i < a->n_args; i++)
        if (a->args[i] != b->args[i]) return 0;
    return 1;
}
static int term_lookup(const EUF *e, const char *name, const int *args, int n_args) {
    Term probe = {(char*)name, n_args, (int*)args};
    for (int i = 0; i < e->n_terms; i++)
        if (term_equal(&e->terms[i], &probe)) return i;
    return -1;
}

static int term_new(EUF *e, const char *name, const int *args, int n_args) {
    if (e->n_terms == e->cap_terms) {
        int old_cap = e->cap_terms;
        e->cap_terms = e->cap_terms ? e->cap_terms * 2 : 16;
        e->terms        = realloc(e->terms,        (size_t)e->cap_terms * sizeof(Term));
        e->parent       = realloc(e->parent,       (size_t)e->cap_terms * sizeof(int));
        e->size         = realloc(e->size,         (size_t)e->cap_terms * sizeof(int));
        e->proof_parent = realloc(e->proof_parent, (size_t)e->cap_terms * sizeof(int));
        e->proof_kind   = realloc(e->proof_kind,   (size_t)e->cap_terms * sizeof(int));
        e->proof_atom   = realloc(e->proof_atom,   (size_t)e->cap_terms * sizeof(int));
        e->uses         = realloc(e->uses,         (size_t)e->cap_terms * sizeof(UseList));
        e->path_mark    = realloc(e->path_mark,    (size_t)e->cap_terms * sizeof(int));
        for (int i = old_cap; i < e->cap_terms; i++) {
            e->path_mark[i] = 0;
            e->uses[i].buf = NULL; e->uses[i].n = e->uses[i].cap = 0;
        }
    }
    int id = e->n_terms;
    Term *t = &e->terms[id];
    size_t nlen = strlen(name);
    t->name = malloc(nlen + 1);
    memcpy(t->name, name, nlen + 1);
    t->n_args = n_args;
    if (n_args > 0) {
        t->args = malloc((size_t)n_args * sizeof(int));
        memcpy(t->args, args, (size_t)n_args * sizeof(int));
    } else t->args = NULL;

    e->parent[id]       = id;
    e->size[id]         = 1;
    e->proof_parent[id] = -1;
    e->proof_kind[id]   = PL_NONE;
    e->proof_atom[id]   = 0;

    /* Register this term in the use lists of its arguments. */
    for (int i = 0; i < n_args; i++) use_push(&e->uses[args[i]], id);

    e->n_terms++;
    return id;
}

int euf_mk_const(EUF *e, const char *name) {
    int t = term_lookup(e, name, NULL, 0);
    return t >= 0 ? t : term_new(e, name, NULL, 0);
}
int euf_mk_app(EUF *e, const char *name, const int *args, int n_args) {
    int t = term_lookup(e, name, args, n_args);
    return t >= 0 ? t : term_new(e, name, args, n_args);
}

/* ====== union-find ====== */
static int find_root(const EUF *e, int t) {
    while (e->parent[t] != t) t = e->parent[t];
    return t;
}
int euf_find(EUF *e, int term) { return find_root(e, term); }
int euf_n_terms(const EUF *e)  { return e->n_terms; }

/* ====== proof-forest reorientation ====== */
static void proof_undo_push(EUF *e, int term, int old_parent, int old_kind, int old_atom) {
    if (e->n_proof_trail == e->cap_proof_trail) {
        e->cap_proof_trail = e->cap_proof_trail ? e->cap_proof_trail * 2 : 16;
        e->proof_trail = realloc(e->proof_trail,
                                 (size_t)e->cap_proof_trail * sizeof(ProofUndo));
    }
    ProofUndo u = {term, old_parent, old_kind, old_atom};
    e->proof_trail[e->n_proof_trail++] = u;
}

/* Walk x up the proof forest, reversing each edge; on return, x is
 * the root of its proof tree (proof_parent[x] = -1). Every touched
 * term has its old (parent, kind, atom) saved on the proof_trail. */
static void reorient(EUF *e, int x) {
    int prev = -1, prev_kind = PL_NONE, prev_atom = 0;
    int cur = x;
    while (cur != -1) {
        int next_cur  = e->proof_parent[cur];
        int next_kind = e->proof_kind[cur];
        int next_atom = e->proof_atom[cur];
        proof_undo_push(e, cur, next_cur, next_kind, next_atom);
        e->proof_parent[cur] = prev;
        e->proof_kind[cur]   = prev_kind;
        e->proof_atom[cur]   = prev_atom;
        prev      = cur;
        prev_kind = next_kind;
        prev_atom = next_atom;
        cur       = next_cur;
    }
}

/* Attach a (already a proof-tree root) to b's proof tree with a labeled edge. */
static void attach_proof(EUF *e, int a, int b, int kind, int atom) {
    proof_undo_push(e, a, -1, PL_NONE, 0);
    e->proof_parent[a] = b;
    e->proof_kind[a]   = kind;
    e->proof_atom[a]   = atom;
}

static int do_union_labeled(EUF *e, int a, int b, int kind, int atom) {
    int ra = find_root(e, a), rb = find_root(e, b);
    if (ra == rb) return 0;
    int merge_a = a, merge_b = b;
    if (e->size[ra] >= e->size[rb]) {
        int t = ra; ra = rb; rb = t;
        int u = merge_a; merge_a = merge_b; merge_b = u;
    }
    /* ra is the smaller-class root; demote it under rb. */
    e->parent[ra]  = rb;
    e->size[rb]   += e->size[ra];
    grow_int(&e->merge_trail,    &e->cap_merges,    e->n_merges + 1);
    grow_int(&e->merge_use_size, &e->cap_merge_use, e->n_merges + 1);
    e->merge_use_size[e->n_merges] = e->uses[rb].n;
    e->merge_trail[e->n_merges++]  = ra;

    /* Aggregate use list under the surviving root. uses[ra] is left
     * intact so it can be restored as ra's own list on undo. */
    UseList *ua = &e->uses[ra];
    for (int i = 0; i < ua->n; i++) use_push(&e->uses[rb], ua->buf[i]);

    reorient(e, merge_a);
    attach_proof(e, merge_a, merge_b, kind, atom);
    return 1;
}

static void undo_one_union(EUF *e) {
    assert(e->n_merges > 0);
    int ra = e->merge_trail[--e->n_merges];
    int rb = e->parent[ra];
    e->size[rb] -= e->size[ra];
    e->uses[rb].n = e->merge_use_size[e->n_merges];
    e->parent[ra] = ra;
}

static void undo_proof_to(EUF *e, int target) {
    while (e->n_proof_trail > target) {
        ProofUndo u = e->proof_trail[--e->n_proof_trail];
        e->proof_parent[u.term] = u.old_parent;
        e->proof_kind[u.term]   = u.old_kind;
        e->proof_atom[u.term]   = u.old_atom;
    }
}

/* ====== use-list based congruence closure ======
 * After a merge, candidates for new congruences are exactly the
 * function applications that mention some term in the just-changed
 * class. We find them via the use list of the demoted root.
 */
static int try_congruence(EUF *e, int i, int j) {
    if (i == j) return 0;
    Term *ti = &e->terms[i];
    Term *tj = &e->terms[j];
    if (ti->n_args == 0 || tj->n_args == 0) return 0;
    if (ti->n_args != tj->n_args) return 0;
    if (strcmp(ti->name, tj->name) != 0) return 0;
    if (find_root(e, i) == find_root(e, j)) return 0;
    for (int k = 0; k < ti->n_args; k++) {
        if (find_root(e, ti->args[k]) != find_root(e, tj->args[k])) return 0;
    }
    do_union_labeled(e, i, j, PL_CONG, 0);
    return 1;
}

/* Scan the use list of `demoted_root` (which just became part of a
 * larger class) for new congruence candidates. For each app f(...)
 * in the use list, look at every arg's use list for other apps
 * with the same name/arity. */
static void scan_congruence_pairs(EUF *e, int demoted_root) {
    UseList *u = &e->uses[demoted_root];
    for (int k = 0; k < u->n; k++) {
        int app = u->buf[k];
        Term *ta = &e->terms[app];
        for (int aidx = 0; aidx < ta->n_args; aidx++) {
            int arg_root = find_root(e, ta->args[aidx]);
            UseList *u2 = &e->uses[arg_root];
            for (int j = 0; j < u2->n; j++) {
                int app2 = u2->buf[j];
                try_congruence(e, app, app2);
            }
        }
    }
}

/* Drive congruence to fixpoint via newly-demoted roots. */
static void close_congruence_from(EUF *e, int demoted_root) {
    int processed = e->n_merges - 1;
    scan_congruence_pairs(e, demoted_root);
    while (processed + 1 < e->n_merges) {
        processed++;
        int dr = e->merge_trail[processed];
        scan_congruence_pairs(e, dr);
    }
}

/* ====== equality registration ====== */
static void grow_atom_idx(EUF *e, int needed) {
    if (needed <= e->cap_atom_idx) return;
    int nc = e->cap_atom_idx ? e->cap_atom_idx * 2 : 16;
    while (nc < needed) nc *= 2;
    e->atom_idx = realloc(e->atom_idx, (size_t)nc * sizeof(int));
    for (int i = e->cap_atom_idx; i < nc; i++) e->atom_idx[i] = -1;
    e->cap_atom_idx = nc;
}
static void grow_atom_state(EUF *e, int needed) {
    if (needed <= e->cap_atom_state) return;
    int nc = e->cap_atom_state ? e->cap_atom_state * 2 : 16;
    while (nc < needed) nc *= 2;
    e->atom_state = realloc(e->atom_state, (size_t)nc * sizeof(int));
    for (int i = e->cap_atom_state; i < nc; i++) e->atom_state[i] = -1;
    e->cap_atom_state = nc;
}

void euf_register_eq(EUF *e, int atom, int t1, int t2) {
    if (atom <= 0) return;
    grow_atom_idx  (e, atom);
    grow_atom_state(e, atom);
    if (e->n_eq == e->cap_eq) {
        e->cap_eq = e->cap_eq ? e->cap_eq * 2 : 8;
        e->eq = realloc(e->eq, (size_t)e->cap_eq * sizeof(*e->eq));
    }
    e->atom_idx[atom - 1] = e->n_eq;
    e->eq[e->n_eq].atom = atom;
    e->eq[e->n_eq].t1   = t1;
    e->eq[e->n_eq].t2   = t2;
    e->n_eq++;
}

/* ====== explain() ====== */
static void explain_push_pair(EUF *e, int a, int b) {
    if (a == b) return;
    if (e->n_pending == e->cap_pending) {
        e->cap_pending = e->cap_pending ? e->cap_pending * 2 : 8;
        e->pending_a = realloc(e->pending_a, (size_t)e->cap_pending * sizeof(int));
        e->pending_b = realloc(e->pending_b, (size_t)e->cap_pending * sizeof(int));
    }
    e->pending_a[e->n_pending] = a;
    e->pending_b[e->n_pending] = b;
    e->n_pending++;
}

static void explain_clear_marks(EUF *e) {
    while (e->path_mark_top > 0) {
        int t = e->path_mark_stack[--e->path_mark_top];
        e->path_mark[t] = 0;
    }
}
static void explain_mark(EUF *e, int t) {
    if (e->path_mark[t]) return;
    e->path_mark[t] = 1;
    if (e->path_mark_top >= e->cap_path_mark) {
        e->cap_path_mark = e->cap_path_mark ? e->cap_path_mark * 2 : 16;
        e->path_mark_stack = realloc(e->path_mark_stack,
                                     (size_t)e->cap_path_mark * sizeof(int));
    }
    e->path_mark_stack[e->path_mark_top++] = t;
}

static void explain_record_lit(EUF *e, int atom, int *out, int *n_out, int out_cap) {
    if (atom <= 0) return;
    if (atom > e->cap_explain_seen_atom) {
        int nc = e->cap_explain_seen_atom ? e->cap_explain_seen_atom * 2 : 16;
        while (nc < atom) nc *= 2;
        e->explain_seen_atom = realloc(e->explain_seen_atom, (size_t)nc * sizeof(int));
        for (int i = e->cap_explain_seen_atom; i < nc; i++) e->explain_seen_atom[i] = 0;
        e->cap_explain_seen_atom = nc;
    }
    if (e->explain_seen_atom[atom - 1]) return;
    e->explain_seen_atom[atom - 1] = 1;
    if (*n_out < out_cap) out[*n_out] = atom;
    (*n_out)++;
}

static void explain_clear_seen_atoms(EUF *e, int *out, int n_out) {
    for (int i = 0; i < n_out; i++) {
        int a = out[i];
        if (a > 0 && a <= e->cap_explain_seen_atom) e->explain_seen_atom[a - 1] = 0;
    }
}

static void process_label(EUF *e, int from, int to, int *out, int *n_out, int out_cap) {
    int kind = e->proof_kind[from];
    if (kind == PL_LIT) {
        explain_record_lit(e, e->proof_atom[from], out, n_out, out_cap);
    } else if (kind == PL_CONG) {
        Term *ta = &e->terms[from];
        Term *tb = &e->terms[to];
        assert(ta->n_args == tb->n_args);
        for (int k = 0; k < ta->n_args; k++) {
            explain_push_pair(e, ta->args[k], tb->args[k]);
        }
    }
}

static int explain(EUF *e, int x, int y, int *out, int out_cap) {
    e->n_explained++;
    int n_out = 0;
    e->n_pending = 0;
    explain_push_pair(e, x, y);

    while (e->n_pending > 0) {
        e->n_pending--;
        int a = e->pending_a[e->n_pending];
        int b = e->pending_b[e->n_pending];
        if (a == b) continue;

        explain_clear_marks(e);
        int cur = a;
        while (cur != -1) { explain_mark(e, cur); cur = e->proof_parent[cur]; }

        int lca = -1;
        cur = b;
        while (cur != -1) {
            if (e->path_mark[cur]) { lca = cur; break; }
            cur = e->proof_parent[cur];
        }
        assert(lca != -1);

        cur = a;
        while (cur != lca) {
            int next = e->proof_parent[cur];
            process_label(e, cur, next, out, &n_out, out_cap);
            cur = next;
        }
        cur = b;
        while (cur != lca) {
            int next = e->proof_parent[cur];
            process_label(e, cur, next, out, &n_out, out_cap);
            cur = next;
        }
    }
    explain_clear_marks(e);
    return n_out;
}

/* ====== conflict detection ====== */
static int detect_conflict(EUF *e) {
    for (int i = 0; i < e->n_diseq; i++) {
        int atom = e->diseq_atoms[i];
        int idx  = e->atom_idx[atom - 1];
        if (idx < 0) continue;
        int t1 = e->eq[idx].t1, t2 = e->eq[idx].t2;
        if (find_root(e, t1) != find_root(e, t2)) continue;

        int cap = e->n_eq > 0 ? e->n_eq : 1;
        int *expl = malloc((size_t)cap * sizeof(int));
        int n_expl = explain(e, t1, t2, expl, cap);

        grow_int(&e->conf_buf, &e->cap_conf, n_expl + 1);
        e->conf_n = 0;
        for (int k = 0; k < n_expl; k++) e->conf_buf[e->conf_n++] = -expl[k];
        e->conf_buf[e->conf_n++] = atom;
        explain_clear_seen_atoms(e, expl, n_expl);
        free(expl);
        return 1;
    }
    return 0;
}

/* ====== assignment hooks ====== */
static void grow_pre(EUF *e, int needed) {
    if (needed <= e->cap_pre) return;
    int nc = e->cap_pre ? e->cap_pre * 2 : 16;
    while (nc < needed) nc *= 2;
    e->pre_merge = realloc(e->pre_merge, (size_t)nc * sizeof(int));
    e->pre_proof = realloc(e->pre_proof, (size_t)nc * sizeof(int));
    e->pre_propq = realloc(e->pre_propq, (size_t)nc * sizeof(int));
    e->cap_pre = nc;
}

void euf_assign(void *data, int lit) {
    EUF *e = (EUF*)data;
    grow_int(&e->asserts, &e->cap_asserts, e->n_asserts + 1);
    grow_pre(e, e->n_asserts + 1);

    int atom = lit > 0 ? lit : -lit;
    grow_atom_state(e, atom);
    e->atom_state[atom - 1] = (lit > 0) ? 1 : 0;

    e->pre_merge[e->n_asserts] = e->n_merges;
    e->pre_proof[e->n_asserts] = e->n_proof_trail;
    e->pre_propq[e->n_asserts] = e->n_propq;
    e->asserts[e->n_asserts++] = lit;
}

static void prop_free(Prop *p) {
    free(p->reason);
    p->reason = NULL;
    p->reason_cap = 0;
    p->n_reason = 0;
    p->lit = 0;
}

void euf_unassign(void *data, int lit) {
    EUF *e = (EUF*)data;
    assert(e->n_asserts > 0);
    e->n_asserts--;
    assert(e->asserts[e->n_asserts] == lit);

    int atom = lit > 0 ? lit : -lit;
    if (atom <= e->cap_atom_state) e->atom_state[atom - 1] = -1;

    if (e->check_pos > e->n_asserts) {
        e->check_pos = e->n_asserts;

        int target_m = e->pre_merge[e->n_asserts];
        while (e->n_merges > target_m) undo_one_union(e);

        int target_p = e->pre_proof[e->n_asserts];
        undo_proof_to(e, target_p);

        if (lit < 0) {
            if (e->n_diseq > 0 && e->diseq_atoms[e->n_diseq - 1] == atom)
                e->n_diseq--;
        }

        int target_q = e->pre_propq[e->n_asserts];
        while (e->n_propq > target_q) prop_free(&e->propq[--e->n_propq]);
        if (e->propq_head > e->n_propq) e->propq_head = e->n_propq;
    }
}

/* ====== propagation queue ====== */
static void prop_enqueue(EUF *e, int lit, const int *reason, int n_reason) {
    if (e->n_propq == e->cap_propq) {
        int old_cap = e->cap_propq;
        e->cap_propq = e->cap_propq ? e->cap_propq * 2 : 8;
        e->propq = realloc(e->propq, (size_t)e->cap_propq * sizeof(Prop));
        for (int i = old_cap; i < e->cap_propq; i++) {
            e->propq[i].lit = 0;
            e->propq[i].reason = NULL;
            e->propq[i].n_reason = 0;
            e->propq[i].reason_cap = 0;
        }
    }
    Prop *p = &e->propq[e->n_propq];
    p->lit = lit;
    if (p->reason_cap < n_reason) {
        p->reason_cap = n_reason;
        p->reason = realloc(p->reason, (size_t)p->reason_cap * sizeof(int));
    }
    memcpy(p->reason, reason, (size_t)n_reason * sizeof(int));
    p->n_reason = n_reason;
    e->n_propq++;
    e->n_propagations++;
}

static int atom_is_unassigned(const EUF *e, int atom) {
    if (atom <= 0 || atom > e->cap_atom_state) return 1;
    return e->atom_state[atom - 1] == -1;
}

static void compute_propagations(EUF *e) {
    int *expl = NULL;
    int  expl_cap = 0;

    for (int i = 0; i < e->n_eq; i++) {
        int atom = e->eq[i].atom;
        if (!atom_is_unassigned(e, atom)) continue;
        int t1 = e->eq[i].t1, t2 = e->eq[i].t2;
        int r1 = find_root(e, t1), r2 = find_root(e, t2);

        if (r1 == r2) {
            grow_int(&expl, &expl_cap, e->n_eq > 0 ? e->n_eq : 1);
            int n_expl = explain(e, t1, t2, expl, expl_cap);
            int n_reason = 1 + n_expl;
            int *reason = malloc((size_t)n_reason * sizeof(int));
            reason[0] = atom;
            for (int k = 0; k < n_expl; k++) reason[1 + k] = -expl[k];
            explain_clear_seen_atoms(e, expl, n_expl);
            prop_enqueue(e, atom, reason, n_reason);
            free(reason);
        } else {
            for (int j = 0; j < e->n_diseq; j++) {
                int datom = e->diseq_atoms[j];
                int didx  = e->atom_idx[datom - 1];
                if (didx < 0) continue;
                int dt1 = e->eq[didx].t1, dt2 = e->eq[didx].t2;
                int dr1 = find_root(e, dt1), dr2 = find_root(e, dt2);
                int match_direct = (dr1 == r1 && dr2 == r2);
                int match_swap   = (dr1 == r2 && dr2 == r1);
                if (!match_direct && !match_swap) continue;

                int ta1 = match_direct ? dt1 : dt2;
                int ta2 = match_direct ? dt2 : dt1;

                grow_int(&expl, &expl_cap, 2 * (e->n_eq > 0 ? e->n_eq : 1));
                int n_expl  = explain(e, t1, ta1, expl, expl_cap);
                n_expl     += explain(e, t2, ta2, expl + n_expl, expl_cap - n_expl);

                int n_reason = 1 + n_expl + 1;
                int *reason = malloc((size_t)n_reason * sizeof(int));
                int p = 0;
                reason[p++] = -atom;
                for (int k = 0; k < n_expl; k++) reason[p++] = -expl[k];
                reason[p++] = datom;
                explain_clear_seen_atoms(e, expl, n_expl);
                prop_enqueue(e, -atom, reason, n_reason);
                free(reason);
                break;
            }
        }
    }
    free(expl);
}

/* ====== check entry point ====== */
int euf_check(void *data, int **conflict_out, int *n_conflict_out) {
    EUF *e = (EUF*)data;

    while (e->check_pos < e->n_asserts) {
        int lit  = e->asserts[e->check_pos];
        int atom = lit > 0 ? lit : -lit;

        if (atom > e->cap_atom_idx || e->atom_idx[atom - 1] < 0) {
            e->check_pos++;
            continue;
        }

        int idx = e->atom_idx[atom - 1];
        int t1 = e->eq[idx].t1, t2 = e->eq[idx].t2;

        if (lit > 0) {
            if (do_union_labeled(e, t1, t2, PL_LIT, atom)) {
                int demoted = e->merge_trail[e->n_merges - 1];
                close_congruence_from(e, demoted);
            }
        } else {
            grow_int(&e->diseq_atoms, &e->cap_diseq, e->n_diseq + 1);
            e->diseq_atoms[e->n_diseq++] = atom;
        }
        e->check_pos++;

        if (detect_conflict(e)) {
            *conflict_out   = e->conf_buf;
            *n_conflict_out = e->conf_n;
            return 1;
        }
    }

    compute_propagations(e);
    return 0;
}

/* ====== propagate entry point ====== */
int euf_propagate(void *data, int *propagated_out,
                  int **reason_out, int *n_reason_out)
{
    EUF *e = (EUF*)data;
    while (e->propq_head < e->n_propq) {
        Prop *p = &e->propq[e->propq_head];
        int atom = p->lit > 0 ? p->lit : -p->lit;
        if (!atom_is_unassigned(e, atom)) {
            e->propq_head++;
            continue;
        }
        *propagated_out = p->lit;
        *reason_out     = p->reason;
        *n_reason_out   = p->n_reason;
        e->propq_head++;
        return 1;
    }
    return 0;
}

/* ====== lifecycle ====== */
EUF *euf_new(void) {
    EUF *e = calloc(1, sizeof(EUF));
    return e;
}

void euf_free(EUF *e) {
    if (!e) return;
    for (int i = 0; i < e->n_terms; i++) {
        free(e->terms[i].name);
        free(e->terms[i].args);
    }
    for (int i = 0; i < e->cap_terms; i++) free(e->uses[i].buf);
    free(e->terms);
    free(e->parent); free(e->size);
    free(e->merge_trail);
    free(e->merge_use_size);
    free(e->proof_parent); free(e->proof_kind); free(e->proof_atom);
    free(e->proof_trail);
    free(e->uses);
    free(e->eq); free(e->atom_idx); free(e->atom_state);
    free(e->asserts);
    free(e->pre_merge); free(e->pre_proof); free(e->pre_propq);
    free(e->diseq_atoms);
    for (int i = 0; i < e->cap_propq; i++) free(e->propq[i].reason);
    free(e->propq);
    free(e->conf_buf);
    free(e->explain_seen_atom);
    free(e->path_mark); free(e->path_mark_stack);
    free(e->pending_a); free(e->pending_b);
    free(e);
}

/* ====== stats ====== */
long euf_n_propagations(const EUF *e) { return e->n_propagations; }
long euf_n_explained   (const EUF *e) { return e->n_explained; }

/* ====== pretty-printing ====== */
int euf_term_print(const EUF *e, int t, char *buf, int sz) {
    if (t < 0 || t >= e->n_terms) return snprintf(buf, (size_t)sz, "<bad>");
    const Term *tm = &e->terms[t];
    if (tm->n_args == 0) return snprintf(buf, (size_t)sz, "%s", tm->name);
    int w = snprintf(buf, (size_t)sz, "%s(", tm->name);
    for (int i = 0; i < tm->n_args; i++) {
        if (w < sz) w += euf_term_print(e, tm->args[i], buf + w, sz - w);
        if (i + 1 < tm->n_args && w < sz)
            w += snprintf(buf + w, (size_t)(sz - w), ", ");
    }
    if (w < sz) w += snprintf(buf + w, (size_t)(sz - w), ")");
    return w;
}
