Z3
Properties
FuncDecl.Parameter Class Reference

Function declarations can have Parameters associated with them. More...

Properties

int Int [get]
 The int value of the parameter. More...
 
double Double [get]
 The double value of the parameter. More...
 
Symbol Symbol [get]
 The Symbol value of the parameter. More...
 
Sort Sort [get]
 The Sort value of the parameter. More...
 
AST AST [get]
 The AST value of the parameter. More...
 
FuncDecl FuncDecl [get]
 The FunctionDeclaration value of the parameter. More...
 
string Rational [get]
 The rational string value of the parameter. More...
 
Z3_parameter_kind ParameterKind [get]
 The kind of the parameter. More...
 

Detailed Description

Function declarations can have Parameters associated with them.

Definition at line 210 of file FuncDecl.cs.

Property Documentation

◆ AST

AST AST
get

The AST value of the parameter.

Definition at line 230 of file FuncDecl.cs.

230 { get { if (ParameterKind != Z3_parameter_kind.Z3_PARAMETER_AST) throw new Z3Exception("parameter is not an AST"); return ast; } }
Z3_parameter_kind
The different kinds of parameters that can be associated with function symbols.
Definition: z3_api.h:139
Z3_parameter_kind ParameterKind
The kind of the parameter.
Definition: FuncDecl.cs:239

◆ Double

double Double
get

The double value of the parameter.

Definition at line 224 of file FuncDecl.cs.

224 { get { if (ParameterKind != Z3_parameter_kind.Z3_PARAMETER_DOUBLE) throw new Z3Exception("parameter is not a double "); return d; } }
Z3_parameter_kind
The different kinds of parameters that can be associated with function symbols.
Definition: z3_api.h:139
Z3_parameter_kind ParameterKind
The kind of the parameter.
Definition: FuncDecl.cs:239

◆ FuncDecl

The FunctionDeclaration value of the parameter.

Definition at line 232 of file FuncDecl.cs.

232 { get { if (ParameterKind != Z3_parameter_kind.Z3_PARAMETER_FUNC_DECL) throw new Z3Exception("parameter is not a function declaration"); return fd; } }
Z3_parameter_kind
The different kinds of parameters that can be associated with function symbols.
Definition: z3_api.h:139
Z3_parameter_kind ParameterKind
The kind of the parameter.
Definition: FuncDecl.cs:239

◆ Int

int Int
get

The int value of the parameter.

Definition at line 222 of file FuncDecl.cs.

222 { get { if (ParameterKind != Z3_parameter_kind.Z3_PARAMETER_INT) throw new Z3Exception("parameter is not an int"); return i; } }
Z3_parameter_kind
The different kinds of parameters that can be associated with function symbols.
Definition: z3_api.h:139
Z3_parameter_kind ParameterKind
The kind of the parameter.
Definition: FuncDecl.cs:239

◆ ParameterKind

Z3_parameter_kind ParameterKind
get

The kind of the parameter.

Definition at line 239 of file FuncDecl.cs.

239 { get { return kind; } }

◆ Rational

string Rational
get

The rational string value of the parameter.

Definition at line 234 of file FuncDecl.cs.

234 { get { if (ParameterKind != Z3_parameter_kind.Z3_PARAMETER_RATIONAL) throw new Z3Exception("parameter is not a rational string"); return r; } }
Z3_parameter_kind
The different kinds of parameters that can be associated with function symbols.
Definition: z3_api.h:139
Z3_parameter_kind ParameterKind
The kind of the parameter.
Definition: FuncDecl.cs:239

◆ Sort

Sort Sort
get

The Sort value of the parameter.

Definition at line 228 of file FuncDecl.cs.

228 { get { if (ParameterKind != Z3_parameter_kind.Z3_PARAMETER_SORT) throw new Z3Exception("parameter is not a Sort"); return srt; } }
Z3_parameter_kind
The different kinds of parameters that can be associated with function symbols.
Definition: z3_api.h:139
Z3_parameter_kind ParameterKind
The kind of the parameter.
Definition: FuncDecl.cs:239

◆ Symbol

The Symbol value of the parameter.

Definition at line 226 of file FuncDecl.cs.

226 { get { if (ParameterKind != Z3_parameter_kind.Z3_PARAMETER_SYMBOL) throw new Z3Exception("parameter is not a Symbol"); return sym; } }
Z3_parameter_kind
The different kinds of parameters that can be associated with function symbols.
Definition: z3_api.h:139
Z3_parameter_kind ParameterKind
The kind of the parameter.
Definition: FuncDecl.cs:239