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

Detailed Description

Function declarations can have Parameters associated with them.

Definition at line 212 of file FuncDecl.java.

Member Function Documentation

AST getAST ( ) throws Z3Exception
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 ( ) throws Z3Exception
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 ( ) throws Z3Exception
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 ( ) throws Z3Exception
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 ( ) throws Z3Exception
inline
String getRational ( ) throws Z3Exception
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 ( ) throws Z3Exception
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 ( ) throws Z3Exception
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