Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines
Public Member Functions | Package Functions
FuncDecl.Parameter Class Reference

Public Member Functions

int getInt () throws Z3Exception
double getDouble () throws Z3Exception
Symbol getSymbol () throws Z3Exception
Sort getSort () throws Z3Exception
AST getAST () throws Z3Exception
FuncDecl getFuncDecl () throws Z3Exception
String getRational () throws Z3Exception
Z3_parameter_kind getParameterKind () throws Z3Exception

Package Functions

 Parameter (Z3_parameter_kind k, int i)
 Parameter (Z3_parameter_kind k, double d)
 Parameter (Z3_parameter_kind k, Symbol s)
 Parameter (Z3_parameter_kind k, Sort s)
 Parameter (Z3_parameter_kind k, AST a)
 Parameter (Z3_parameter_kind k, FuncDecl fd)
 Parameter (Z3_parameter_kind k, String r)

Detailed Description

Function declarations can have Parameters associated with them.

Definition at line 212 of file FuncDecl.java.


Constructor & Destructor Documentation

Parameter ( Z3_parameter_kind  k,
int  i 
) [inline, package]

Definition at line 301 of file FuncDecl.java.

        {
            this.kind = k;
            this.i = i;
        }
Parameter ( Z3_parameter_kind  k,
double  d 
) [inline, package]

Definition at line 307 of file FuncDecl.java.

        {
            this.kind = k;
            this.d = d;
        }
Parameter ( Z3_parameter_kind  k,
Symbol  s 
) [inline, package]

Definition at line 313 of file FuncDecl.java.

        {
            this.kind = k;
            this.sym = s;
        }
Parameter ( Z3_parameter_kind  k,
Sort  s 
) [inline, package]

Definition at line 319 of file FuncDecl.java.

        {
            this.kind = k;
            this.srt = s;
        }
Parameter ( Z3_parameter_kind  k,
AST  a 
) [inline, package]

Definition at line 325 of file FuncDecl.java.

        {
            this.kind = k;
            this.ast = a;
        }
Parameter ( Z3_parameter_kind  k,
FuncDecl  fd 
) [inline, package]

Definition at line 331 of file FuncDecl.java.

        {
            this.kind = k;
            this.fd = fd;
        }
Parameter ( Z3_parameter_kind  k,
String  r 
) [inline, package]

Definition at line 337 of file FuncDecl.java.

        {
            this.kind = k;
            this.r = r;
        }

Member Function Documentation

AST getAST ( ) throws Z3Exception [inline]

The AST value of the parameter.

Definition at line 266 of file FuncDecl.java.

        {
            if (getParameterKind() != Z3_parameter_kind.Z3_PARAMETER_AST)
                throw new Z3Exception("parameter is not an AST");
            return ast;
        }
double getDouble ( ) throws Z3Exception [inline]

The double value of the parameter.

Definition at line 236 of file FuncDecl.java.

        {
            if (getParameterKind() != Z3_parameter_kind.Z3_PARAMETER_DOUBLE)
                throw new Z3Exception("parameter is not a double ");
            return d;
        }
FuncDecl getFuncDecl ( ) throws Z3Exception [inline]

The FunctionDeclaration value of the parameter.

Definition at line 276 of file FuncDecl.java.

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

The int value of the parameter.

Definition at line 226 of file FuncDecl.java.

        {
            if (getParameterKind() != Z3_parameter_kind.Z3_PARAMETER_INT)
                throw new Z3Exception("parameter is not an int");
            return i;
        }
String getRational ( ) throws Z3Exception [inline]

The rational string value of the parameter.

Definition at line 286 of file FuncDecl.java.

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

The Sort value of the parameter.

Definition at line 256 of file FuncDecl.java.

        {
            if (getParameterKind() != Z3_parameter_kind.Z3_PARAMETER_SORT)
                throw new Z3Exception("parameter is not a Sort");
            return srt;
        }
Symbol getSymbol ( ) throws Z3Exception [inline]

The Symbol value of the parameter.

Definition at line 246 of file FuncDecl.java.

        {
            if (getParameterKind() != Z3_parameter_kind.Z3_PARAMETER_SYMBOL)
                throw new Z3Exception("parameter is not a Symbol");
            return sym;
        }
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines