Module Z3.FuncDecl

module FuncDecl: sig .. end
Function declarations

type func_decl 
module Parameter: sig .. end
Parameters of Func_Decls
val mk_func_decl : context ->
Symbol.symbol ->
Sort.sort list -> Sort.sort -> func_decl
Creates a new function declaration.
val mk_func_decl_s : context ->
string -> Sort.sort list -> Sort.sort -> func_decl
Creates a new function declaration.

Creates a fresh function declaration with a name prefixed with a prefix string.

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
Creates a new constant function declaration.
val mk_const_decl_s : context -> string -> Sort.sort -> func_decl
Creates a new constant function declaration.
val mk_fresh_const_decl : context -> string -> Sort.sort -> func_decl
Creates a fresh constant function declaration with a name prefixed with a prefix string. FuncDecl.mk_func_decl FuncDecl.mk_func_decl
val equal : func_decl -> func_decl -> bool
Comparison operator.
Returns True if a and b are from the same context and represent the same func_decl; false otherwise.
val to_string : func_decl -> string
A string representations of the function declaration.
val get_id : func_decl -> int
Returns a unique identifier for the function declaration.
val get_arity : func_decl -> int
The arity of the function declaration
val get_domain_size : func_decl -> int
The size of the domain of the function declaration FuncDecl.get_arity
val get_domain : func_decl -> Sort.sort list
The domain of the function declaration
val get_range : func_decl -> Sort.sort
The range of the function declaration
val get_decl_kind : func_decl -> Z3enums.decl_kind
The kind of the function declaration.
val get_name : func_decl -> Symbol.symbol
The name of the function declaration
val get_num_parameters : func_decl -> int
The number of parameters of the function declaration
val get_parameters : func_decl -> Parameter.parameter list
The parameters of the function declaration
val apply : func_decl -> Expr.expr list -> Expr.expr
Create expression that applies function to arguments.