/*
 * lra.h -- linear real arithmetic theory solver.
 *
 * Implements the Dutertre / de Moura "General Simplex for SMT":
 *
 *   - Variables x_1, ..., x_n with rational lower and upper bounds.
 *     Initially unbounded; bounds are tightened on SAT assertions.
 *
 *   - A tableau of rows  x_i = sum_j a_ij x_j  partitioning variables
 *     into "basic" (LHS) and "non-basic" (RHS). Non-basic variables
 *     are free within their bounds; basic variables are determined.
 *
 *   - Each external constraint  sum_k c_k x_k  OP  rhs   is rewritten
 *     by introducing a slack variable  s = sum_k c_k x_k. The atom
 *     becomes a bound on s, and the new row enters the tableau.
 *
 *   - check() runs the simplex pivoting loop. If some basic variable
 *     violates its bound and no non-basic on its row can absorb the
 *     deficit, the row gives a Farkas-style infeasibility certificate.
 *
 *   - propagate() derives implied bounds: a row whose non-basics are
 *     tightly bounded implies a bound on the basic variable; if the
 *     atom for that bound is unassigned, queue it.
 *
 * Strict inequalities (x < c, x > c) are handled by delta-augmentation:
 * the bound is x <= c - eps for some symbolic infinitesimal eps. All
 * variable values and bounds are delta-rationals (q + d * eps).
 */
#ifndef LRA_H
#define LRA_H

#include "rat.h"
#include <stdint.h>

#ifdef __cplusplus
extern "C" {
#endif

typedef struct LRA LRA;

LRA *lra_new (void);
void lra_free(LRA *lra);

/* Allocate a fresh real-valued variable; returns its id (>= 0). */
int lra_mk_var(LRA *lra, const char *name);

/* A term in a linear combination. */
typedef struct { int var; Rat coeff; } LraTerm;

/*
 * Register an atom of the form  (sum_k coeff_k * var_k)  OP  rhs.
 *
 *   op = 0:  expr <= rhs    (weak)
 *   op = 1:  expr <  rhs    (strict)
 *
 * Returns SAT-layer atom (caller-assigned).
 *
 * Internally, allocates a slack variable s with row s = sum_k coeff_k x_k
 * and stores the atom as a bound on s:
 *
 *   pos LE: s <= rhs            (upper bound, weak)
 *   neg LE: s >  rhs            (lower bound, strict)
 *   pos LT: s <  rhs            (upper bound, strict)
 *   neg LT: s >= rhs            (lower bound, weak)
 */
void lra_register_atom(LRA *lra, int atom, int op,
                       const LraTerm *terms, int n_terms,
                       Rat rhs);

#define LRA_OP_LE 0
#define LRA_OP_LT 1

/* Theory hooks (callable as TheoryHooks methods via the combined theory). */
void lra_assign  (void *data, int lit);
void lra_unassign(void *data, int lit);
int  lra_check   (void *data, int **conflict_out, int *n_conflict_out);
int  lra_propagate(void *data, int *prop_out,
                   int **reason_out, int *n_reason_out);

/* Has this atom been registered with the LRA solver? */
int  lra_owns_atom(const LRA *lra, int atom);

/* Stats. */
long lra_n_pivots(const LRA *lra);
long lra_n_propagations(const LRA *lra);

#ifdef __cplusplus
}
#endif

#endif
