Package com.microsoft.z3

Class FuncDecl<R extends Sort>

java.lang.Object

com.microsoft.z3.Z3Object

com.microsoft.z3.AST

com.microsoft.z3.FuncDecl<R>

All Implemented Interfaces:

Comparable<AST>

public class FuncDecl<R extends Sort>
extends AST

Function declarations.

Nested Class Summary

Nested Classes

Modifier and Type	Class	Description
static class	FuncDecl.Parameter	Function declarations can have Parameters associated with them.

Method Summary

Modifier and Type	Method	Description
Expr<R>	apply(Expr<?>... args)	Create expression that applies function to arguments.
boolean	equals(Object o)	Object comparison.
int	getArity()	The arity of the function declaration
Z3_decl_kind	getDeclKind()	The kind of the function declaration.
Sort[]	getDomain()	The domain of the function declaration
int	getDomainSize()	The size of the domain of the function declaration
int	getId()	Returns a unique identifier for the function declaration.
Symbol	getName()	The name of the function declaration
int	getNumParameters()	The number of parameters of the function declaration
FuncDecl.Parameter[]	getParameters()	The parameters of the function declaration
R	getRange()	The range of the function declaration
String	toString()	A string representation of the AST.
FuncDecl<R>	translate(Context ctx)	Translates (copies) the function declaration to the Context ctx.

Methods inherited from class com.microsoft.z3.AST

compareTo, getASTKind, getSExpr, hashCode, isApp, isExpr, isFuncDecl, isQuantifier, isSort, isVar

Methods inherited from class com.microsoft.z3.Z3Object

arrayLength, arrayToNative

Methods inherited from class java.lang.Object

clone, finalize, getClass, notify, notifyAll, wait, wait, wait

Method Details

equals

public boolean equals(Object o)

Object comparison.

Overrides:

equals in class AST

Parameters:

o - another AST

toString

public String toString()

Description copied from class: AST

A string representation of the AST.

Overrides:

toString in class AST

getId

public int getId()

Returns a unique identifier for the function declaration.

Overrides:

getId in class AST

translate

public FuncDecl<R> translate(Context ctx)

Translates (copies) the function declaration to the Context ctx.

Overrides:

translate in class AST

Parameters:

ctx - A context

Returns:

A copy of the function declaration which is associated with ctx

Throws:

Z3Exception - on error

getArity

public int getArity()

The arity of the function declaration

getDomainSize

public int getDomainSize()

The size of the domain of the function declaration

See Also:

• getArity()

getDomain

public Sort[] getDomain()

The domain of the function declaration

getRange

public R getRange()

The range of the function declaration

getDeclKind

public Z3_decl_kind getDeclKind()

The kind of the function declaration.

getName

public Symbol getName()

The name of the function declaration

getNumParameters

public int getNumParameters()

The number of parameters of the function declaration

getParameters

public FuncDecl.Parameter[] getParameters()

The parameters of the function declaration

apply

public Expr<R> apply(Expr<?>... args)

Create expression that applies function to arguments.