FuncDecl.Parameter Class Reference

Public Member Functions
int	getInt ()
double	getDouble ()
Symbol	getSymbol ()
Sort	getSort ()
AST	getAST ()
FuncDecl	getFuncDecl ()
String	getRational ()
Z3_parameter_kind	getParameterKind ()

Detailed Description

Function declarations can have Parameters associated with them.

Definition at line 200 of file FuncDecl.java.

Member Function Documentation

getAST()

AST getAST ( )

inline

The AST value of the parameter.

Definition at line 254 of file FuncDecl.java.

        {
            if (getParameterKind() != Z3_parameter_kind.Z3_PARAMETER_AST)
                throw new Z3Exception("parameter is not an AST");
            return ast;
        }

getDouble()

double getDouble ( )

inline

The double value of the parameter.

Definition at line 224 of file FuncDecl.java.

        {
            if (getParameterKind() != Z3_parameter_kind.Z3_PARAMETER_DOUBLE)
                throw new Z3Exception("parameter is not a double ");
            return d;
        }

getFuncDecl()

FuncDecl getFuncDecl ( )

inline

The FunctionDeclaration value of the parameter.

Definition at line 264 of file FuncDecl.java.

        {
            if (getParameterKind() != Z3_parameter_kind.Z3_PARAMETER_FUNC_DECL)
                throw new Z3Exception("parameter is not a function declaration");
            return fd;
        }

getInt()

int getInt ( )

inline

The int value of the parameter.

Definition at line 214 of file FuncDecl.java.

        {
            if (getParameterKind() != Z3_parameter_kind.Z3_PARAMETER_INT)
                throw new Z3Exception("parameter is not an int");
            return i;
        }

getParameterKind()

Z3_parameter_kind getParameterKind ( )

inline

The kind of the parameter.

Definition at line 284 of file FuncDecl.java.

        {
            return kind;
        }

Referenced by FuncDecl.Parameter.getAST(), FuncDecl.Parameter.getDouble(), FuncDecl.Parameter.getFuncDecl(), FuncDecl.Parameter.getInt(), FuncDecl.Parameter.getRational(), FuncDecl.Parameter.getSort(), and FuncDecl.Parameter.getSymbol().

getRational()

String getRational ( )

inline

The rational string value of the parameter.

Definition at line 274 of file FuncDecl.java.

        {
            if (getParameterKind() != Z3_parameter_kind.Z3_PARAMETER_RATIONAL)
                throw new Z3Exception("parameter is not a rational String");
            return r;
        }

getSort()

Sort getSort ( )

inline

The Sort value of the parameter.

Definition at line 244 of file FuncDecl.java.

        {
            if (getParameterKind() != Z3_parameter_kind.Z3_PARAMETER_SORT)
                throw new Z3Exception("parameter is not a Sort");
            return srt;
        }

getSymbol()

Symbol getSymbol ( )

inline

The Symbol value of the parameter.

Definition at line 234 of file FuncDecl.java.

        {
            if (getParameterKind() != Z3_parameter_kind.Z3_PARAMETER_SYMBOL)
                throw new Z3Exception("parameter is not a Symbol");
            return sym;
        }