/*
 * sat.h -- CDCL SAT solver tailored as a DPLL(T) driver.
 *
 * Same family as the SAT solver in Predictive Algorithms (two watched
 * literals, first-UIP conflict analysis, VSIDS, Luby restarts), with
 * additional hooks so that a theory solver can stay in lockstep with
 * the trail and ingest theory conflicts as learned clauses.
 *
 * Lits are signed integers in DIMACS form: +k for atom k, -k for its
 * negation. Atoms are numbered 1..N.
 */

#ifndef SAT_H
#define SAT_H

#ifdef __cplusplus
extern "C" {
#endif

typedef struct Sat Sat;

/* Solver result. */
#define SAT_SATISFIABLE   10
#define SAT_UNSATISFIABLE 20
#define SAT_UNKNOWN        0

/* Atom values. */
#define SAT_FALSE  0
#define SAT_TRUE   1
#define SAT_UNDEF -1

/*
 * Theory interface. The DPLL(T) layer registers a callback bundle. After
 * each round of SAT-level unit propagation, the solver alternates between
 * `check` (consistency) and `propagate` (deriving implied literals) until
 * a fixpoint is reached.
 *
 *   - `check` returns 0 (OK) or 1 (CONFLICT) and on conflict fills
 *     *conflict_out / *n_conflict_out with a clause currently falsified
 *     by the trail. This clause is treated as a learned clause -- it
 *     enters the solver's clause database and conflict analysis runs as
 *     usual.
 *
 *   - `propagate` returns 1 if the theory has derived an implied literal,
 *     filling *propagated_out with the literal and *reason_out /
 *     *n_reason_out with a clause that has the propagated literal at
 *     position 0 and whose other literals are the negations of literals
 *     currently asserted true. The clause is added to the database and
 *     becomes the reason for the propagated literal -- if it later
 *     participates in a conflict, analysis can follow back through it.
 *     `propagate` returns 0 if no propagation is available.
 *
 * `assign` and `unassign` are called whenever the trail grows or shrinks,
 * so the theory can mirror the SAT trail in its own data structures.
 *
 * Buffers returned by callbacks are owned by the theory and must remain
 * valid until the next theory callback.
 *
 * The `propagate` field may be NULL: the SAT solver treats absent
 * propagation as ``no further propagation available'' on every call.
 */
typedef struct {
    void *data;
    void  (*assign)  (void *data, int lit);
    void  (*unassign)(void *data, int lit);
    int   (*check)   (void *data, int **conflict_out, int *n_conflict_out);
    int   (*propagate)(void *data, int *propagated_out,
                       int **reason_out, int *n_reason_out);
} TheoryHooks;

Sat *sat_new(int n_atoms);
void sat_free(Sat *s);

void sat_set_theory(Sat *s, const TheoryHooks *t);

int  sat_add_clause(Sat *s, const int *lits, int n_lits);
int  sat_solve(Sat *s);
int  sat_value(const Sat *s, int atom);

void sat_set_conflict_limit(Sat *s, long limit);
void sat_set_verbose       (Sat *s, int level);

long sat_decisions        (const Sat *s);
long sat_conflicts        (const Sat *s);   /* propositional + theory */
long sat_theory_conflicts (const Sat *s);
long sat_theory_props     (const Sat *s);   /* theory-propagated literals */
long sat_propagations     (const Sat *s);
long sat_restarts         (const Sat *s);
long sat_learned_clauses  (const Sat *s);

#ifdef __cplusplus
}
#endif

#endif
