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

Member Function Documentation

AST getAST ( )
inline

The AST value of the parameter.

Definition at line 266 of file FuncDecl.java.

267  {
269  throw new Z3Exception("parameter is not an AST");
270  return ast;
271  }
Z3_parameter_kind getParameterKind()
Definition: FuncDecl.java:296
Z3_parameter_kind
The different kinds of parameters that can be associated with function symbols.
Definition: z3_api.h:171
double getDouble ( )
inline

The double value of the parameter.

Definition at line 236 of file FuncDecl.java.

237  {
239  throw new Z3Exception("parameter is not a double ");
240  return d;
241  }
Z3_parameter_kind getParameterKind()
Definition: FuncDecl.java:296
Z3_parameter_kind
The different kinds of parameters that can be associated with function symbols.
Definition: z3_api.h:171
FuncDecl getFuncDecl ( )
inline

The FunctionDeclaration value of the parameter.

Definition at line 276 of file FuncDecl.java.

277  {
279  throw new Z3Exception("parameter is not a function declaration");
280  return fd;
281  }
Z3_parameter_kind getParameterKind()
Definition: FuncDecl.java:296
Z3_parameter_kind
The different kinds of parameters that can be associated with function symbols.
Definition: z3_api.h:171
int getInt ( )
inline

The int value of the parameter.

Definition at line 226 of file FuncDecl.java.

227  {
229  throw new Z3Exception("parameter is not an int");
230  return i;
231  }
Z3_parameter_kind getParameterKind()
Definition: FuncDecl.java:296
Z3_parameter_kind
The different kinds of parameters that can be associated with function symbols.
Definition: z3_api.h:171
Z3_parameter_kind getParameterKind ( )
inline
String getRational ( )
inline

The rational string value of the parameter.

Definition at line 286 of file FuncDecl.java.

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

The Sort value of the parameter.

Definition at line 256 of file FuncDecl.java.

257  {
259  throw new Z3Exception("parameter is not a Sort");
260  return srt;
261  }
Z3_parameter_kind getParameterKind()
Definition: FuncDecl.java:296
Z3_parameter_kind
The different kinds of parameters that can be associated with function symbols.
Definition: z3_api.h:171
Symbol getSymbol ( )
inline

The Symbol value of the parameter.

Definition at line 246 of file FuncDecl.java.

247  {
249  throw new Z3Exception("parameter is not a Symbol");
250  return sym;
251  }
Z3_parameter_kind getParameterKind()
Definition: FuncDecl.java:296
Z3_parameter_kind
The different kinds of parameters that can be associated with function symbols.
Definition: z3_api.h:171