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

Member Function Documentation

§ getAST()

AST getAST ( )
inline

The AST value of the parameter.

Definition at line 242 of file FuncDecl.java.

243  {
245  throw new Z3Exception("parameter is not an AST");
246  return ast;
247  }
Z3_parameter_kind getParameterKind()
Definition: FuncDecl.java:272
Z3_parameter_kind
The different kinds of parameters that can be associated with function symbols.
Definition: z3_api.h:139

§ getDouble()

double getDouble ( )
inline

The double value of the parameter.

Definition at line 212 of file FuncDecl.java.

213  {
215  throw new Z3Exception("parameter is not a double ");
216  return d;
217  }
Z3_parameter_kind getParameterKind()
Definition: FuncDecl.java:272
Z3_parameter_kind
The different kinds of parameters that can be associated with function symbols.
Definition: z3_api.h:139

§ getFuncDecl()

FuncDecl getFuncDecl ( )
inline

The FunctionDeclaration value of the parameter.

Definition at line 252 of file FuncDecl.java.

253  {
255  throw new Z3Exception("parameter is not a function declaration");
256  return fd;
257  }
Z3_parameter_kind getParameterKind()
Definition: FuncDecl.java:272
Z3_parameter_kind
The different kinds of parameters that can be associated with function symbols.
Definition: z3_api.h:139

§ getInt()

int getInt ( )
inline

The int value of the parameter.

Definition at line 202 of file FuncDecl.java.

203  {
205  throw new Z3Exception("parameter is not an int");
206  return i;
207  }
Z3_parameter_kind getParameterKind()
Definition: FuncDecl.java:272
Z3_parameter_kind
The different kinds of parameters that can be associated with function symbols.
Definition: z3_api.h:139

§ getParameterKind()

Z3_parameter_kind getParameterKind ( )
inline

§ getRational()

String getRational ( )
inline

The rational string value of the parameter.

Definition at line 262 of file FuncDecl.java.

263  {
265  throw new Z3Exception("parameter is not a rational String");
266  return r;
267  }
Z3_parameter_kind getParameterKind()
Definition: FuncDecl.java:272
Z3_parameter_kind
The different kinds of parameters that can be associated with function symbols.
Definition: z3_api.h:139

§ getSort()

Sort getSort ( )
inline

The Sort value of the parameter.

Definition at line 232 of file FuncDecl.java.

233  {
235  throw new Z3Exception("parameter is not a Sort");
236  return srt;
237  }
Z3_parameter_kind getParameterKind()
Definition: FuncDecl.java:272
Z3_parameter_kind
The different kinds of parameters that can be associated with function symbols.
Definition: z3_api.h:139

§ getSymbol()

Symbol getSymbol ( )
inline

The Symbol value of the parameter.

Definition at line 222 of file FuncDecl.java.

223  {
225  throw new Z3Exception("parameter is not a Symbol");
226  return sym;
227  }
Z3_parameter_kind getParameterKind()
Definition: FuncDecl.java:272
Z3_parameter_kind
The different kinds of parameters that can be associated with function symbols.
Definition: z3_api.h:139