sig
  val mk_sort :
    Z3.context -> Z3.Symbol.symbol -> Z3.Symbol.symbol list -> Z3.Sort.sort
  val mk_sort_s : Z3.context -> string -> string list -> Z3.Sort.sort
  val get_const_decls : Z3.Sort.sort -> Z3.FuncDecl.func_decl list
  val get_const_decl : Z3.Sort.sort -> int -> Z3.FuncDecl.func_decl
  val get_consts : Z3.Sort.sort -> Z3.Expr.expr list
  val get_const : Z3.Sort.sort -> int -> Z3.Expr.expr
  val get_tester_decls : Z3.Sort.sort -> Z3.FuncDecl.func_decl list
  val get_tester_decl : Z3.Sort.sort -> int -> Z3.FuncDecl.func_decl
end