Module Z3.FuncDecl

type func_decl
module Parameter : sig ... end
val mk_func_decl : context -> Symbol.symbol -> Sort.sort list -> Sort.sort -> func_decl
val mk_func_decl_s : context -> string -> Sort.sort list -> Sort.sort -> func_decl
val mk_rec_func_decl : context -> Symbol.symbol -> Sort.sort list -> Sort.sort -> func_decl
val mk_rec_func_decl_s : context -> string -> Sort.sort list -> Sort.sort -> func_decl
val add_rec_def : context -> func_decl -> Expr.expr list -> Expr.expr -> unit
val mk_fresh_func_decl : context -> string -> Sort.sort list -> Sort.sort -> func_decl
val mk_const_decl : context -> Symbol.symbol -> Sort.sort -> func_decl
val mk_const_decl_s : context -> string -> Sort.sort -> func_decl
val mk_fresh_const_decl : context -> string -> Sort.sort -> func_decl
val equal : func_decl -> func_decl -> bool
val to_string : func_decl -> string
val get_id : func_decl -> int
val get_arity : func_decl -> int
val get_domain_size : func_decl -> int
val get_domain : func_decl -> Sort.sort list
val get_range : func_decl -> Sort.sort
val get_decl_kind : func_decl -> Z3enums.decl_kind
val get_name : func_decl -> Symbol.symbol
val get_num_parameters : func_decl -> int
val get_parameters : func_decl -> Parameter.parameter list
val apply : func_decl -> Expr.expr list -> Expr.expr