sig
  module Integer :
    sig
      val mk_sort : Z3.context -> Z3.Sort.sort
      val get_big_int : Z3.Expr.expr -> Z.t
      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_mod : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
      val mk_rem : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> 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_int2real : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr
      val mk_int2bv : Z3.context -> int -> Z3.Expr.expr -> Z3.Expr.expr
    end
  module Real :
    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
  val is_int : Z3.Expr.expr -> bool
  val is_arithmetic_numeral : Z3.Expr.expr -> bool
  val is_le : Z3.Expr.expr -> bool
  val is_ge : Z3.Expr.expr -> bool
  val is_lt : Z3.Expr.expr -> bool
  val is_gt : Z3.Expr.expr -> bool
  val is_add : Z3.Expr.expr -> bool
  val is_sub : Z3.Expr.expr -> bool
  val is_uminus : Z3.Expr.expr -> bool
  val is_mul : Z3.Expr.expr -> bool
  val is_div : Z3.Expr.expr -> bool
  val is_idiv : Z3.Expr.expr -> bool
  val is_remainder : Z3.Expr.expr -> bool
  val is_modulus : Z3.Expr.expr -> bool
  val is_int2real : Z3.Expr.expr -> bool
  val is_real2int : Z3.Expr.expr -> bool
  val is_real_is_int : Z3.Expr.expr -> bool
  val is_real : Z3.Expr.expr -> bool
  val is_int_numeral : Z3.Expr.expr -> bool
  val is_rat_numeral : Z3.Expr.expr -> bool
  val is_algebraic_number : Z3.Expr.expr -> bool
  val mk_add : Z3.context -> Z3.Expr.expr list -> Z3.Expr.expr
  val mk_mul : Z3.context -> Z3.Expr.expr list -> Z3.Expr.expr
  val mk_sub : Z3.context -> Z3.Expr.expr list -> Z3.Expr.expr
  val mk_unary_minus : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr
  val mk_div : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
  val mk_power : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
  val mk_lt : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
  val mk_le : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
  val mk_gt : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
  val mk_ge : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
end