sig
  val mk_sort : Z3.context -> Z3.Sort.sort
  val get_numerator : Z3.Expr.expr -> Z3.Expr.expr
  val get_denominator : Z3.Expr.expr -> Z3.Expr.expr
  val get_ratio : Z3.Expr.expr -> Q.t
  val to_decimal_string : Z3.Expr.expr -> int -> string
  val numeral_to_string : Z3.Expr.expr -> string
  val mk_const : Z3.context -> Z3.Symbol.symbol -> Z3.Expr.expr
  val mk_const_s : Z3.context -> string -> Z3.Expr.expr
  val mk_numeral_nd : Z3.context -> int -> int -> Z3.Expr.expr
  val mk_numeral_s : Z3.context -> string -> Z3.Expr.expr
  val mk_numeral_i : Z3.context -> int -> Z3.Expr.expr
  val mk_is_integer : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr
  val mk_real2int : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr
  module AlgebraicNumber :
    sig
      val to_upper : Z3.Expr.expr -> int -> Z3.Expr.expr
      val to_lower : Z3.Expr.expr -> int -> Z3.Expr.expr
      val to_decimal_string : Z3.Expr.expr -> int -> string
      val numeral_to_string : Z3.Expr.expr -> string
    end
end