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

The different kinds of parameters that can be associated with function symbols.

Definition: z3_api.h:94

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

Properties