Z3
Public Member Functions
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.

255 {
257 throw new Z3Exception("parameter is not an AST");
258 return ast;
259 }
Z3_parameter_kind getParameterKind()
Definition: FuncDecl.java:284
Z3_parameter_kind
The different kinds of parameters that can be associated with function symbols.
Definition: z3_api.h:134

◆ getDouble()

double getDouble ( )
inline

The double value of the parameter.

Definition at line 224 of file FuncDecl.java.

225 {
227 throw new Z3Exception("parameter is not a double ");
228 return d;
229 }

◆ getFuncDecl()

FuncDecl getFuncDecl ( )
inline

The FunctionDeclaration value of the parameter.

Definition at line 264 of file FuncDecl.java.

265 {
267 throw new Z3Exception("parameter is not a function declaration");
268 return fd;
269 }

◆ getInt()

int getInt ( )
inline

The int value of the parameter.

Definition at line 214 of file FuncDecl.java.

215 {
217 throw new Z3Exception("parameter is not an int");
218 return i;
219 }

◆ getParameterKind()

Z3_parameter_kind getParameterKind ( )
inline

◆ getRational()

String getRational ( )
inline

The rational string value of the parameter.

Definition at line 274 of file FuncDecl.java.

275 {
277 throw new Z3Exception("parameter is not a rational String");
278 return r;
279 }

◆ getSort()

Sort getSort ( )
inline

The Sort value of the parameter.

Definition at line 244 of file FuncDecl.java.

245 {
247 throw new Z3Exception("parameter is not a Sort");
248 return srt;
249 }

◆ getSymbol()

Symbol getSymbol ( )
inline

The Symbol value of the parameter.

Definition at line 234 of file FuncDecl.java.

235 {
237 throw new Z3Exception("parameter is not a Symbol");
238 return sym;
239 }