/*
 * smt.h -- SMT solver: SAT + EUF (the theory of equality and
 *          uninterpreted functions). Phase 1 of the SMT book.
 *
 * Builds an unsigned-int term DAG over uninterpreted constants and
 * function applications, lets the user attach propositional atoms to
 * equalities, accept clauses over those atoms, and dispatches to the
 * underlying DPLL(T) solver.
 *
 * Typical use:
 *
 *     SmtCtx *ctx = smt_new();
 *     int a = smt_mk_const(ctx, "a");
 *     int b = smt_mk_const(ctx, "b");
 *     int c = smt_mk_const(ctx, "c");
 *
 *     // a = b
 *     smt_assert_eq(ctx, a, b);
 *     // b = c
 *     smt_assert_eq(ctx, b, c);
 *     // a != c
 *     smt_assert_neq(ctx, a, c);
 *
 *     int r = smt_check(ctx);   // -> SMT_UNSAT
 *     smt_free(ctx);
 *
 * For Boolean structure beyond unit clauses, the user explicitly works
 * at the level of atoms: `smt_mk_eq_atom` returns an atom id that can be
 * placed in clauses via `smt_assert_clause`.
 */
#ifndef SMT_H
#define SMT_H

#include <stdint.h>

#ifdef __cplusplus
extern "C" {
#endif

typedef struct SmtCtx SmtCtx;
typedef int SmtTerm;
typedef int SmtAtom;

#define SMT_SAT     10
#define SMT_UNSAT   20
#define SMT_UNKNOWN  0

SmtCtx *smt_new(void);
void    smt_free(SmtCtx *ctx);

/* ====== EUF: term construction (hash-consed) ====== */
SmtTerm smt_mk_const(SmtCtx *ctx, const char *name);
SmtTerm smt_mk_app  (SmtCtx *ctx, const char *fname,
                     const SmtTerm *args, int n_args);

/* Atom construction for an equality. Atoms are 1..N. The same equality
 * (regardless of argument order) gets the same atom. */
SmtAtom smt_mk_eq_atom(SmtCtx *ctx, SmtTerm a, SmtTerm b);

/* Convenience assertions over equalities (unit clauses). */
void smt_assert_eq (SmtCtx *ctx, SmtTerm a, SmtTerm b);
void smt_assert_neq(SmtCtx *ctx, SmtTerm a, SmtTerm b);

/* ====== LRA: real-valued variables and linear constraints ======
 *
 * Variables are integers in a disjoint namespace from EUF terms; they
 * are not interchangeable. (Combining the two -- "the EUF function
 * applied to a real number" -- is what Nelson--Oppen will deliver in
 * Phase 4.)
 *
 * Coefficients and right-hand sides are exact rationals, passed as
 * (numerator, denominator) pairs. den must be non-zero; the API
 * normalizes internally.
 *
 * Atoms are constructed as a linear combination compared to a constant:
 *
 *     sum_k coeff_k * var_k   <=    rhs   (weak)
 *     sum_k coeff_k * var_k   <     rhs   (strict)
 *
 * Each returns an SMT atom id usable in clauses. Negation gives the
 * other side: ~atom of "<=" is ">", ~atom of "<" is ">=".
 */
typedef int SmtVar;

SmtVar smt_mk_real_var(SmtCtx *ctx, const char *name);

typedef struct {
    SmtVar  var;
    int64_t num;     /* coefficient: num/den, den > 0 in normalized form. */
    int64_t den;
} SmtLinTerm;

SmtAtom smt_mk_lra_le_atom(SmtCtx *ctx,
                           const SmtLinTerm *terms, int n_terms,
                           int64_t rhs_num, int64_t rhs_den);
SmtAtom smt_mk_lra_lt_atom(SmtCtx *ctx,
                           const SmtLinTerm *terms, int n_terms,
                           int64_t rhs_num, int64_t rhs_den);

/* Unit-clause shortcuts. */
void smt_assert_lra_le(SmtCtx *ctx,
                       const SmtLinTerm *terms, int n_terms,
                       int64_t rhs_num, int64_t rhs_den);
void smt_assert_lra_lt(SmtCtx *ctx,
                       const SmtLinTerm *terms, int n_terms,
                       int64_t rhs_num, int64_t rhs_den);
/* Equality is two unit assertions: <= rhs AND >= rhs. */
void smt_assert_lra_eq(SmtCtx *ctx,
                       const SmtLinTerm *terms, int n_terms,
                       int64_t rhs_num, int64_t rhs_den);

/* ====== Clauses and solve ====== */
/* Assert a clause as a disjunction of signed atoms.
 * +atom means "atom is true", -atom means negation. */
void smt_assert_clause(SmtCtx *ctx, const int *signed_atoms, int n);

/* ====== Phase 4: shared variables across EUF and LRA ======
 *
 * A SmtShared is a single logical variable that exists in both
 * theories: as an EUF constant (so it can be the argument of an
 * uninterpreted function) and as an LRA real-valued variable (so it
 * can appear in linear constraints). The two views are kept in sync
 * by the Nelson-Oppen machinery: whenever either theory derives an
 * equality between two shareds, the other is informed.
 *
 * Creating a SmtShared also eagerly creates the cross-theory
 * "bridge" atoms with every previously-allocated shared. Concretely,
 * for each pair (s_i, s_j) we register:
 *
 *   eq_ij  : (s_i.euf == s_j.euf)           -- EUF atom
 *   le_ij  : (s_i.lra - s_j.lra <= 0)       -- LRA atom
 *   ge_ij  : (s_i.lra - s_j.lra >= 0)       -- LRA atom
 *
 * with three linking clauses:
 *
 *   eq_ij -> le_ij
 *   eq_ij -> ge_ij
 *   (le_ij & ge_ij) -> eq_ij
 *
 * That, plus LRA bound propagation, plus the existing EUF theory
 * propagation, is the entire NO machinery: SAT's BCP carries the
 * cross-theory implications.
 */
typedef struct { SmtTerm euf; SmtVar lra; } SmtShared;

SmtShared smt_mk_shared(SmtCtx *ctx, const char *name);

/* Convenience: assert s1.euf = s2.euf (which by bridge clauses also
 * tightens s1.lra = s2.lra). */
void smt_assert_shared_eq (SmtCtx *ctx, SmtShared s1, SmtShared s2);
void smt_assert_shared_neq(SmtCtx *ctx, SmtShared s1, SmtShared s2);

int smt_check(SmtCtx *ctx);

/* Inspect the model after a SAT result. */
int smt_model_eq(SmtCtx *ctx, SmtTerm a, SmtTerm b);

int smt_term_print(const SmtCtx *ctx, SmtTerm t, char *buf, int buf_sz);

/* Numbers. */
int  smt_n_atoms(const SmtCtx *ctx);
int  smt_n_terms(const SmtCtx *ctx);
long smt_decisions       (const SmtCtx *ctx);
long smt_conflicts       (const SmtCtx *ctx);
long smt_theory_conflicts(const SmtCtx *ctx);
long smt_theory_props    (const SmtCtx *ctx);
long smt_propagations    (const SmtCtx *ctx);
long smt_lra_pivots      (const SmtCtx *ctx);

void smt_set_verbose(SmtCtx *ctx, int v);

#ifdef __cplusplus
}
#endif

#endif
