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  }

◆ 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  }

◆ 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  }

◆ 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  }

◆ 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  }

◆ 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  }

◆ 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  }
com.microsoft.z3.enumerations.Z3_parameter_kind.Z3_PARAMETER_DOUBLE
Z3_PARAMETER_DOUBLE
Definition: Z3_parameter_kind.java:15
com.microsoft.z3.enumerations.Z3_parameter_kind.Z3_PARAMETER_AST
Z3_PARAMETER_AST
Definition: Z3_parameter_kind.java:19
com.microsoft.z3.enumerations.Z3_parameter_kind.Z3_PARAMETER_SYMBOL
Z3_PARAMETER_SYMBOL
Definition: Z3_parameter_kind.java:17
com.microsoft.z3.FuncDecl.Parameter.getParameterKind
Z3_parameter_kind getParameterKind()
Definition: FuncDecl.java:284
com.microsoft.z3.enumerations.Z3_parameter_kind.Z3_PARAMETER_FUNC_DECL
Z3_PARAMETER_FUNC_DECL
Definition: Z3_parameter_kind.java:20
com.microsoft.z3.enumerations.Z3_parameter_kind.Z3_PARAMETER_SORT
Z3_PARAMETER_SORT
Definition: Z3_parameter_kind.java:18
com.microsoft.z3.enumerations.Z3_parameter_kind.Z3_PARAMETER_INT
Z3_PARAMETER_INT
Definition: Z3_parameter_kind.java:14
com.microsoft.z3.enumerations.Z3_parameter_kind.Z3_PARAMETER_RATIONAL
Z3_PARAMETER_RATIONAL
Definition: Z3_parameter_kind.java:16
Z3_parameter_kind
Z3_parameter_kind
The different kinds of parameters that can be associated with function symbols.
Definition: z3_api.h:133