/*
 * euf.h -- the theory of equality and uninterpreted functions.
 *
 * Decides satisfiability of conjunctions of equalities and disequalities
 * over terms built from constants and uninterpreted function symbols, using
 * congruence closure.
 *
 * Usage from the SMT layer:
 *
 *   1. Construct terms via euf_mk_const / euf_mk_app.
 *   2. For each equality the SMT layer wants to assert under SAT control,
 *      assign it a propositional atom and call euf_register_eq(atom, t1, t2).
 *   3. Hand the SAT solver a TheoryHooks bundle pointing at euf_assign /
 *      euf_unassign / euf_check (with the EUF* as data).
 *   4. When the SAT solver asserts an atom A:
 *        +A means "t1 = t2"
 *        -A means "t1 != t2"
 *      The theory tracks both.
 */
#ifndef EUF_H
#define EUF_H

#ifdef __cplusplus
extern "C" {
#endif

typedef struct EUF EUF;

EUF *euf_new(void);
void euf_free(EUF *e);

/* Build / look up terms (hash-consed). Returns a term id >= 0. */
int  euf_mk_const(EUF *e, const char *name);
int  euf_mk_app  (EUF *e, const char *name, const int *args, int n_args);

/* Register the propositional atom `atom` (>= 1) as standing for the equality
 * t1 = t2. The same atom must not be registered twice. */
void euf_register_eq(EUF *e, int atom, int t1, int t2);

/* Theory callbacks. Signatures match TheoryHooks in sat.h. */
void euf_assign  (void *data, int lit);
void euf_unassign(void *data, int lit);
int  euf_check   (void *data, int **conflict_out, int *n_conflict_out);
int  euf_propagate(void *data, int *propagated_out,
                   int **reason_out, int *n_reason_out);

/* Statistics (Phase 2). */
long euf_n_propagations(const EUF *e);
long euf_n_explained   (const EUF *e);

/* Read-only queries -- mostly for tests and inspection. */
int  euf_find    (EUF *e, int term);
int  euf_n_terms (const EUF *e);

/* Pretty-printing of a term (for debugging / examples). buf must be writable. */
int  euf_term_print(const EUF *e, int term, char *buf, int buf_sz);

#ifdef __cplusplus
}
#endif

#endif
