S.SMT
type sym
type exp
val logic : Smtml.Logic.t
val eval : Smtml.Model.t -> sym -> t
val exp_of_t : t -> exp
val exp_of_s : sym -> exp
val mk : Base.string -> sym * Smtml.Expr.t Base.list
val add : exp -> exp -> exp
val mul : exp -> exp -> exp
val ge : exp -> exp -> Smtml.Expr.t
val eq : exp -> exp -> Smtml.Expr.t