sig
  type func_decl
  module Parameter :
    sig
      type parameter =
          P_Int of int
        | P_Dbl of float
        | P_Sym of Z3.Symbol.symbol
        | P_Srt of Z3.Sort.sort
        | P_Ast of Z3.AST.ast
        | P_Fdl of Z3.FuncDecl.func_decl
        | P_Rat of string
      val get_kind :
        Z3.FuncDecl.Parameter.parameter -> Z3enums.parameter_kind
      val get_int : Z3.FuncDecl.Parameter.parameter -> int
      val get_float : Z3.FuncDecl.Parameter.parameter -> float
      val get_symbol : Z3.FuncDecl.Parameter.parameter -> Z3.Symbol.symbol
      val get_sort : Z3.FuncDecl.Parameter.parameter -> Z3.Sort.sort
      val get_ast : Z3.FuncDecl.Parameter.parameter -> Z3.AST.ast
      val get_func_decl :
        Z3.FuncDecl.Parameter.parameter -> Z3.FuncDecl.func_decl
      val get_rational : Z3.FuncDecl.Parameter.parameter -> string
    end
  val mk_func_decl :
    Z3.context ->
    Z3.Symbol.symbol ->
    Z3.Sort.sort list -> Z3.Sort.sort -> Z3.FuncDecl.func_decl
  val mk_func_decl_s :
    Z3.context ->
    string -> Z3.Sort.sort list -> Z3.Sort.sort -> Z3.FuncDecl.func_decl
  val mk_rec_func_decl :
    Z3.context ->
    Z3.Symbol.symbol ->
    Z3.Sort.sort list -> Z3.Sort.sort -> Z3.FuncDecl.func_decl
  val mk_rec_func_decl_s :
    Z3.context ->
    string -> Z3.Sort.sort list -> Z3.Sort.sort -> Z3.FuncDecl.func_decl
  val add_rec_def :
    Z3.context ->
    Z3.FuncDecl.func_decl -> Z3.Expr.expr list -> Z3.Expr.expr -> unit
  val mk_fresh_func_decl :
    Z3.context ->
    string -> Z3.Sort.sort list -> Z3.Sort.sort -> Z3.FuncDecl.func_decl
  val mk_const_decl :
    Z3.context -> Z3.Symbol.symbol -> Z3.Sort.sort -> Z3.FuncDecl.func_decl
  val mk_const_decl_s :
    Z3.context -> string -> Z3.Sort.sort -> Z3.FuncDecl.func_decl
  val mk_fresh_const_decl :
    Z3.context -> string -> Z3.Sort.sort -> Z3.FuncDecl.func_decl
  val equal : Z3.FuncDecl.func_decl -> Z3.FuncDecl.func_decl -> bool
  val to_string : Z3.FuncDecl.func_decl -> string
  val get_id : Z3.FuncDecl.func_decl -> int
  val get_arity : Z3.FuncDecl.func_decl -> int
  val get_domain_size : Z3.FuncDecl.func_decl -> int
  val get_domain : Z3.FuncDecl.func_decl -> Z3.Sort.sort list
  val get_range : Z3.FuncDecl.func_decl -> Z3.Sort.sort
  val get_decl_kind : Z3.FuncDecl.func_decl -> Z3enums.decl_kind
  val get_name : Z3.FuncDecl.func_decl -> Z3.Symbol.symbol
  val get_num_parameters : Z3.FuncDecl.func_decl -> int
  val get_parameters :
    Z3.FuncDecl.func_decl -> Z3.FuncDecl.Parameter.parameter list
  val apply : Z3.FuncDecl.func_decl -> Z3.Expr.expr list -> Z3.Expr.expr
end