/*
 * rat.h -- exact rational arithmetic on int64 numerator / denominator.
 *
 * Used by the LRA theory solver, where Farkas-style explanations
 * depend on exact arithmetic (any rounding in the simplex tableau
 * can make a learned clause unsound).
 *
 * Two types:
 *
 *   Rat  = int64 numerator / int64 denominator, denominator > 0.
 *          Always kept in lowest terms (gcd(num, den) = 1, sign in num).
 *
 *   Drat = (q, d) pair of Rats representing the value q + d * eps,
 *          where eps is a symbolic infinitesimal. Used to handle
 *          strict inequalities via the standard delta-augmentation
 *          trick (Dutertre / de Moura): the strict bound x < c becomes
 *          the weak bound x <= (c, -1), and all comparisons happen
 *          lexicographically on (q, d).
 *
 * Numerator overflow on int64 is possible for adversarial inputs;
 * the routines assert in debug builds. For tutorial-scale problems
 * (coefficients single- or double-digit, a few dozen pivots) this is
 * fine. A production solver would use bigint or GMP rationals.
 */
#ifndef RAT_H
#define RAT_H

#include <stdint.h>

#ifdef __cplusplus
extern "C" {
#endif

typedef struct { int64_t n, d; } Rat;
typedef struct { Rat q, d;     } Drat;

/* --- Rat --- */
Rat rat_int  (int64_t k);                   /* k / 1 */
Rat rat_make (int64_t n, int64_t d);        /* normalizes; d > 0 */
Rat rat_neg  (Rat a);
Rat rat_add  (Rat a, Rat b);
Rat rat_sub  (Rat a, Rat b);
Rat rat_mul  (Rat a, Rat b);
Rat rat_div  (Rat a, Rat b);                /* b != 0 */
int rat_cmp  (Rat a, Rat b);                /* -1 / 0 / +1 */
int rat_sgn  (Rat a);                       /* -1 / 0 / +1 */
int rat_is_zero(Rat a);
int rat_eq(Rat a, Rat b);

/* Pretty-printer, returns characters written (snprintf-style). */
int rat_print(char *buf, int sz, Rat a);

/* --- Drat --- */
Drat drat_rat  (Rat q);                     /* q + 0*eps */
Drat drat_int  (int64_t k);                 /* k + 0*eps */
Drat drat_make (Rat q, Rat d);
Drat drat_neg  (Drat a);
Drat drat_add  (Drat a, Drat b);
Drat drat_sub  (Drat a, Drat b);
Drat drat_mul_rat(Drat a, Rat k);
int  drat_cmp  (Drat a, Drat b);            /* lex on (q, d) */
int  drat_is_zero(Drat a);

extern const Drat DRAT_ZERO;

int drat_print(char *buf, int sz, Drat a);

#ifdef __cplusplus
}
#endif

#endif
