/*
 * lcg.h -- Lazy Clause Generation: a CP solver with CDCL-style nogood
 *          learning, built on top of the SAT engine from the SMT book.
 *
 * Architecture (Phase 1):
 *
 *   LCG is a "theory" attached to the SAT engine via TheoryHooks. The
 *   theory's universe is finite-domain integer variables. Each integer
 *   variable's domain is reified into a chain of order-encoding Boolean
 *   literals:
 *
 *       For variable x with domain [lo .. hi], we allocate (hi - lo)
 *       SAT Booleans  b[lo], b[lo+1], ..., b[hi-1]  where
 *
 *           b[k]  means  "x <= k".
 *
 *       Monotonicity is enforced by binary clauses  b[k] -> b[k+1]
 *       posted at variable-creation time. The SAT engine's BCP then
 *       maintains the chain "for free".
 *
 *   When the SAT layer assigns a literal corresponding to b[k], the
 *   theory updates the relevant variable's cached upper or lower
 *   bound. Propagators inspect those bounds, derive new bounds for
 *   other variables, and emit explanation clauses through the
 *   theory_propagate channel.
 *
 *   A conflict (empty domain) becomes a SAT-level conflict clause
 *   whose literals are exactly the bound atoms that caused the
 *   wipeout.
 *
 * What Phase 1 contains:
 *   - Integer variable manager.
 *   - One propagator: `linear_le`, enforcing sum(a_i x_i) <= K.
 *   - The plumbing to plug LCG into the SAT engine via TheoryHooks.
 *   - One worked example showing the full loop.
 *
 * What is left for later phases (see book/book.tex for the plan):
 *   - First-class explanation pipeline (Phase 2).
 *   - alldifferent with matching (Phase 3).
 *   - cumulative / no_overlap for scheduling (Phase 4), with DWTA
 *     as the worked example.
 */
#ifndef LCG_H
#define LCG_H

#ifdef __cplusplus
extern "C" {
#endif

typedef struct LcgCtx LcgCtx;

/* An integer variable, identified by an opaque int handle. */
typedef int IntVar;

/* Solver result codes (same as SAT). */
#define LCG_SAT     10
#define LCG_UNSAT   20
#define LCG_UNKNOWN  0

/* Construct / destroy. */
LcgCtx *lcg_new(void);
void    lcg_free(LcgCtx *ctx);

/* Create a finite-domain integer variable in [lo..hi].
 * The order-encoding Booleans and monotonicity clauses are posted
 * immediately. Returns the variable's id (>= 0). */
IntVar lcg_new_int_var(LcgCtx *ctx, int lo, int hi, const char *name);

/* Return the SAT literal encoding "x <= k".
 *   If k >= hi, the relation is trivially true.
 *   If k <  lo, it is trivially false.
 * For the trivial cases we return a sentinel; the caller decides
 * what to do.
 *
 * Sentinels: LCG_LIT_TRUE and LCG_LIT_FALSE. Most users will use the
 * convenience constraint posters below instead of going through the
 * literal level directly. */
#define LCG_LIT_TRUE   ( 0x7fffffff)
#define LCG_LIT_FALSE  (-0x7fffffff)
int lcg_lit_le(LcgCtx *ctx, IntVar x, int k);
int lcg_lit_ge(LcgCtx *ctx, IntVar x, int k);

/* Post a constraint  sum(coeff[i] * vars[i])  <=  k. */
void lcg_post_linear_le(LcgCtx *ctx,
                        const int *coeff, const IntVar *vars, int n_terms,
                        int k);

/* Post a constraint enforcing that the values of `vars` are pairwise
 * distinct. The propagator is bounds-consistent: it detects Hall-set
 * conflicts and propagates bound tightenings, but does not (yet)
 * remove non-extreme values from the middle of a domain. */
void lcg_post_alldifferent(LcgCtx *ctx, const IntVar *vars, int n);

/* Post a cumulative resource constraint:
 *     for all t,  sum over tasks running at t of demand[i]  <=  capacity.
 *
 * Each task i has a start-time variable `starts[i]`, a fixed integer
 * duration `dur[i]`, and a fixed integer resource demand `demand[i]`.
 * The task occupies the interval  [starts[i], starts[i] + dur[i]).
 *
 * The propagator is time-table reasoning, bounds-consistent: it
 * computes each task's mandatory part (when the task definitely runs,
 * for all currently valid starts), checks the per-time-point demand
 * profile against `capacity`, and tightens task bounds when scheduling
 * a task at certain starts would push total demand over capacity. */
void lcg_post_cumulative(LcgCtx *ctx,
                         const IntVar *starts,
                         const int    *dur,
                         const int    *demand,
                         int n_tasks,
                         int capacity);

/* Post a unary-resource (disjunctive / no-overlap) constraint: each
 * task occupies the resource exclusively, so no two tasks may run at
 * the same time. Equivalent to `cumulative` with all demands = 1 and
 * capacity = 1. */
void lcg_post_no_overlap(LcgCtx *ctx,
                         const IntVar *starts,
                         const int    *dur,
                         int n_tasks);

/* Post a SAT-level clause. The clause literals must be obtained from
 * lcg_lit_le / lcg_lit_ge; trivial-true or trivial-false sentinels are
 * handled gracefully (true literal removes the clause, false literal
 * is dropped from it). */
void lcg_post_clause(LcgCtx *ctx, const int *lits, int n);

/* Solve. */
int lcg_solve(LcgCtx *ctx);

/* After lcg_solve == LCG_SAT, query the value of an integer variable. */
int lcg_value(const LcgCtx *ctx, IntVar x);

/* Read the current cached bounds (live during search; the propagator
 * uses these to make decisions). */
int lcg_lb(const LcgCtx *ctx, IntVar x);
int lcg_ub(const LcgCtx *ctx, IntVar x);

/* ====== Propagator interface (Phase 2) ======
 *
 * A propagator is a black-box function the solver calls during search.
 * Its job: look at the current bounds of integer variables and derive
 * either (a) new bounds, each with an explanation of which other
 * bounds entailed it, or (b) a conflict explanation showing that the
 * current bounds together are infeasible.
 *
 * The propagator does not directly modify bounds. It calls the emit_*
 * functions below, which build the right SAT-clause shape and hand the
 * derivation to the SAT engine. The engine then propagates the literal
 * (which feeds back through theory_assign to update the cached bound)
 * or backtracks on a conflict.
 *
 * Return values:
 *   LCG_PROP_OK          --- nothing derived; bounds untouched.
 *   LCG_PROP_TIGHTENED   --- at least one emit_* call succeeded.
 *   LCG_PROP_CONFLICT    --- emit_conflict was called, or an emit_*
 *                            call returned conflict; LCG core will
 *                            pick up ctx's explanation buffer as the
 *                            conflict clause.
 */
#define LCG_PROP_OK         0
#define LCG_PROP_TIGHTENED  1
#define LCG_PROP_CONFLICT   2

typedef struct {
    void *data;
    int  (*propagate)(LcgCtx *ctx, void *data);
    void (*destroy)(void *data);
} LcgPropagator;

/* Register a propagator. The LCG core takes ownership of `p.data` and
 * will free it via p.destroy() during lcg_free. */
void lcg_register_propagator(LcgCtx *ctx, LcgPropagator p);

/* ----- explanation builder (called from inside a propagator) -----
 *
 * A propagator builds an explanation by listing the bound literals that
 * support its inference. The LCG core converts them to the right
 * clause shape (negated supports + the derived literal).
 *
 * Typical usage inside a propagator:
 *
 *     lcg_expl_clear(ctx);
 *     lcg_expl_lo(ctx, x, lcg_lb(ctx, x));   // because x >= lb(x)
 *     lcg_expl_hi(ctx, y, lcg_ub(ctx, y));   // because y <= ub(y)
 *     return lcg_emit_le(ctx, z, 5);         // therefore z <= 5
 */
void lcg_expl_clear(LcgCtx *ctx);
void lcg_expl_lo   (LcgCtx *ctx, IntVar v, int lo);
void lcg_expl_hi   (LcgCtx *ctx, IntVar v, int hi);

/* Emit a derived bound on v with the current explanation buffer as
 * justification. Returns one of LCG_PROP_OK / TIGHTENED / CONFLICT. */
int  lcg_emit_le(LcgCtx *ctx, IntVar v, int k);
int  lcg_emit_ge(LcgCtx *ctx, IntVar v, int k);

/* Emit a conflict: the current explanation buffer is infeasible. */
int  lcg_emit_conflict(LcgCtx *ctx);

/* Stats. */
long lcg_decisions    (const LcgCtx *ctx);
long lcg_conflicts    (const LcgCtx *ctx);
long lcg_propagations (const LcgCtx *ctx);
long lcg_explanations (const LcgCtx *ctx);  /* nogoods generated by propagators */

void lcg_set_verbose(LcgCtx *ctx, int level);

#ifdef __cplusplus
}
#endif

#endif
