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 206 of file FuncDecl.java.

Member Function Documentation

AST getAST ( )
inline

The AST value of the parameter.

Definition at line 260 of file FuncDecl.java.

261  {
263  throw new Z3Exception("parameter is not an AST");
264  return ast;
265  }
Z3_parameter_kind getParameterKind()
Definition: FuncDecl.java:290
Z3_parameter_kind
The different kinds of parameters that can be associated with function symbols.
Definition: z3_api.h:179
double getDouble ( )
inline

The double value of the parameter.

Definition at line 230 of file FuncDecl.java.

231  {
233  throw new Z3Exception("parameter is not a double ");
234  return d;
235  }
Z3_parameter_kind getParameterKind()
Definition: FuncDecl.java:290
Z3_parameter_kind
The different kinds of parameters that can be associated with function symbols.
Definition: z3_api.h:179
FuncDecl getFuncDecl ( )
inline

The FunctionDeclaration value of the parameter.

Definition at line 270 of file FuncDecl.java.

271  {
273  throw new Z3Exception("parameter is not a function declaration");
274  return fd;
275  }
Z3_parameter_kind getParameterKind()
Definition: FuncDecl.java:290
Z3_parameter_kind
The different kinds of parameters that can be associated with function symbols.
Definition: z3_api.h:179
int getInt ( )
inline

The int value of the parameter.

Definition at line 220 of file FuncDecl.java.

221  {
223  throw new Z3Exception("parameter is not an int");
224  return i;
225  }
Z3_parameter_kind getParameterKind()
Definition: FuncDecl.java:290
Z3_parameter_kind
The different kinds of parameters that can be associated with function symbols.
Definition: z3_api.h:179
Z3_parameter_kind getParameterKind ( )
inline
String getRational ( )
inline

The rational string value of the parameter.

Definition at line 280 of file FuncDecl.java.

281  {
283  throw new Z3Exception("parameter is not a rational String");
284  return r;
285  }
Z3_parameter_kind getParameterKind()
Definition: FuncDecl.java:290
Z3_parameter_kind
The different kinds of parameters that can be associated with function symbols.
Definition: z3_api.h:179
Sort getSort ( )
inline

The Sort value of the parameter.

Definition at line 250 of file FuncDecl.java.

251  {
253  throw new Z3Exception("parameter is not a Sort");
254  return srt;
255  }
Z3_parameter_kind getParameterKind()
Definition: FuncDecl.java:290
Z3_parameter_kind
The different kinds of parameters that can be associated with function symbols.
Definition: z3_api.h:179
Symbol getSymbol ( )
inline

The Symbol value of the parameter.

Definition at line 240 of file FuncDecl.java.

241  {
243  throw new Z3Exception("parameter is not a Symbol");
244  return sym;
245  }
Z3_parameter_kind getParameterKind()
Definition: FuncDecl.java:290
Z3_parameter_kind
The different kinds of parameters that can be associated with function symbols.
Definition: z3_api.h:179