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 207 of file FuncDecl.cs.

## Property Documentation

## ◆ AST

AST AST
| get

The AST value of the parameter.

Definition at line 227 of file FuncDecl.cs.

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

## ◆ Double

double Double
| get

The double value of the parameter.

Definition at line 221 of file FuncDecl.cs.

221{ get { if (ParameterKind != Z3_parameter_kind.Z3_PARAMETER_DOUBLE) throw new Z3Exception("parameter is not a double "); return d; } }

## ◆ FuncDecl

FuncDecl FuncDecl
| get

The FunctionDeclaration value of the parameter.

Definition at line 229 of file FuncDecl.cs.

229{ get { if (ParameterKind != Z3_parameter_kind.Z3_PARAMETER_FUNC_DECL) throw new Z3Exception("parameter is not a function declaration"); return fd; } }

## ◆ Int

int Int
| get

The int value of the parameter.

Definition at line 219 of file FuncDecl.cs.

219{ get { if (ParameterKind != Z3_parameter_kind.Z3_PARAMETER_INT) throw new Z3Exception("parameter is not an int"); return i; } }

## ◆ ParameterKind

Z3_parameter_kind ParameterKind
| get

The kind of the parameter.

Definition at line 236 of file FuncDecl.cs.

236{ get { return kind; } }

## ◆ Rational

string Rational
| get

The rational string value of the parameter.

Definition at line 231 of file FuncDecl.cs.

231{ get { if (ParameterKind != Z3_parameter_kind.Z3_PARAMETER_RATIONAL) throw new Z3Exception("parameter is not a rational string"); return r; } }

## ◆ Sort

Sort Sort
| get

The Sort value of the parameter.

Definition at line 225 of file FuncDecl.cs.

225{ get { if (ParameterKind != Z3_parameter_kind.Z3_PARAMETER_SORT) throw new Z3Exception("parameter is not a Sort"); return srt; } }

## ◆ Symbol

Symbol Symbol
| get

The Symbol value of the parameter.

Definition at line 223 of file FuncDecl.cs.

223{ get { if (ParameterKind != Z3_parameter_kind.Z3_PARAMETER_SYMBOL) throw new Z3Exception("parameter is not a Symbol"); return sym; } }