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.

val mk_rec_func_decl : context ->
       Symbol.symbol ->
       Sort.sort list -> Sort.sort -> func_decl

Creates a function declaration that can be used in a recursive function definition. FuncDecl.add_rec_def

val mk_rec_func_decl_s : context ->
       string -> Sort.sort list -> Sort.sort -> func_decl

Creates a function declaration that can be used in a recursive function definition. FuncDecl.add_rec_def

val add_rec_def : context ->
       func_decl -> Expr.expr list -> Expr.expr -> unit

Registers a recursive function definition

val mk_fresh_func_decl : context ->
       string -> Sort.sort list -> Sort.sort -> func_decl

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

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.