Module Rat.SMT

module Log : sig ... end
type sym = Smtml.Symbol.t * Smtml.Symbol.t

A rational symbol is a pair of integer SMT symbols (num, den).

type exp = Smtml.Expr.t * Smtml.Expr.t
val logic : Smtml.Logic.t
val exp_of_t : Q.t -> Smtml.Expr.t * Smtml.Expr.t
val exp_of_s : (Smtml.Symbol.t * Smtml.Symbol.t) -> Smtml.Expr.t * Smtml.Expr.t
val eval : Smtml.Model.t -> (Smtml.Symbol.t * Smtml.Symbol.t) -> Q.t
val add : (Smtml.Expr.t * Smtml.Expr.t) -> (Smtml.Expr.t * Smtml.Expr.t) -> Smtml.Expr.t * Smtml.Expr.t

add (n1/d1) (n2/d2) = (n1·d2 + n2·d1) / (d1·d2) at the SMT level.

val mul : (Smtml.Expr.t * Smtml.Expr.t) -> (Smtml.Expr.t * Smtml.Expr.t) -> Smtml.Expr.t * Smtml.Expr.t

mul (n1/d1) (n2/d2) = (n1·n2) / (d1·d2) at the SMT level.

val ge : (Smtml.Expr.t * Smtml.Expr.t) -> (Smtml.Expr.t * Smtml.Expr.t) -> Smtml.Expr.t

ge (n1/d1) (n2/d2) ↔ n1·d2 ≥ n2·d1 (cross-multiply, positive denoms).

val eq : (Smtml.Expr.t * Smtml.Expr.t) -> (Smtml.Expr.t * Smtml.Expr.t) -> Smtml.Expr.t

eq (n1/d1) (n2/d2) ↔ n1·d2 = n2·d1.

val mk : Base.String.t -> (Smtml.Symbol.t * Smtml.Symbol.t) * Smtml.Expr.t list

Domain constraint: den > 0 ensures the pair encodes a valid rational.