Module Algebra.Rat

Rational-number semiring: (ℚ, +, ×, 0, 1).

Rationals are represented as arbitrary-precision Q.t values (from the zarith library). The semiring is unbounded and infinite, so elements is not supported.

SMT encoding represents each rational as a pair of integer symbols (numerator, denominator) with constraint den > 0, then lifts addition and multiplication via cross-multiplication. Equality and ordering become cross-multiplication comparisons, keeping the SMT fragment to QF_NIA (non-linear integer arithmetic).

module Log : sig ... end
module T : sig ... end
include module type of struct include T end
type t = Q.t
val compare : t -> t -> Base.int
val equal : t -> t -> Base.bool
val hash : Q.t -> int
val hash_fold_t : Base.Hash.state -> Q.t -> Base.Hash.state
val sexp_of_t : Q.t -> Sexplib0__.Sexp.t
include sig ... end
type comparator_witness = Base__Comparator.Make(T).comparator_witness
val comparator : (T.t, comparator_witness) Base__Comparator.comparator
val zero : Q.t
val one : Q.t
val rand : ?non_zero:Base__Float.t -> ?max:Base__Int.t -> unit -> Q.t
val add : Q.t -> Q.t -> Q.t
val mul : Q.t -> Q.t -> Q.t
val elements : unit -> 'a
val to_string : Q.t -> string
module SMT : sig ... end