sig
  val mk_sort : Z3.context -> Z3.Symbol.symbol -> int64 -> Z3.Sort.sort
  val mk_sort_s : Z3.context -> string -> int64 -> Z3.Sort.sort
  val is_finite_domain : Z3.Expr.expr -> bool
  val is_lt : Z3.Expr.expr -> bool
  val get_size : Z3.Sort.sort -> int64
end