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;
        }

Z3_parameter_kind getParameterKind

(

)

throws Z3Exception [inline]

The kind of the parameter.

Definition at line 296 of file FuncDecl.java.

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

        {
            return kind;
        }

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;
        }