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:140

§ 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  }
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:140

§ 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  }
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:140

§ 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  }
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:140

§ 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  }
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:140

§ 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  }
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:140

§ 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  }
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:140