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) |
Function declarations can have Parameters associated with them.
Definition at line 212 of file FuncDecl.java.
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; }
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; }