Z3 |

Data Structures | Public Member Functions | Static Public Member Functions | Properties
FuncDecl Class Reference

Function declarations. More...

Inheritance diagram for FuncDecl:

## Data Structures
class | Parameter
| Function declarations can have Parameters associated with them. More...

## Public Member Functions
override bool | Equals (object o)
| Object comparison. More...
override int | GetHashCode ()
| A hash code. More...
override string | ToString ()
| A string representations of the function declaration. More...
new FuncDecl | Translate (Context ctx)
| Translates (copies) the function declaration to the Context ctx . More...
Expr | Apply (params Expr[] args)
| Create expression that applies function to arguments. More...
Public Member Functions inherited from AST
override bool | Equals (object o)
| Object comparison. More...
virtual int | CompareTo (object other)
| Object Comparison. More...
override int | GetHashCode ()
| The AST's hash code. More...
AST | Translate (Context ctx)
| Translates (copies) the AST to the Context ctx . More...
override string | ToString ()
| A string representation of the AST. More...
string | SExpr ()
| A string representation of the AST in s-expression notation. More...
Public Member Functions inherited from Z3Object
void | Dispose ()
| Disposes of the underlying native Z3 object. More...

## Static Public Member Functions
static bool | operator== (FuncDecl a, FuncDecl b)
| Comparison operator. More...
static bool | operator!= (FuncDecl a, FuncDecl b)
| Comparison operator. More...
Static Public Member Functions inherited from AST
static bool | operator== (AST a, AST b)
| Comparison operator. More...
static bool | operator!= (AST a, AST b)
| Comparison operator. More...

## Properties
new uint | Id`[get]`
| Returns a unique identifier for the function declaration. More...
uint | Arity`[get]`
| The arity of the function declaration More...
uint | DomainSize`[get]`
| The size of the domain of the function declaration See also Arity More...
Sort[] | Domain`[get]`
| The domain of the function declaration More...
Sort | Range`[get]`
| The range of the function declaration More...
Z3_decl_kind | DeclKind`[get]`
| The kind of the function declaration. More...
Symbol | Name`[get]`
| The name of the function declaration More...
uint | NumParameters`[get]`
| The number of parameters of the function declaration More...
Parameter[] | Parameters`[get]`
| The parameters of the function declaration More...
Expr this[params Expr[] | args`[get]`
| Create expression that applies function to arguments. More...
Properties inherited from AST
uint | Id`[get]`
| A unique identifier for the AST (unique among all ASTs). More...
Z3_ast_kind | ASTKind`[get]`
| The kind of the AST. More...
bool | IsExpr`[get]`
| Indicates whether the AST is an Expr More...
bool | IsApp`[get]`
| Indicates whether the AST is an application More...
bool | IsVar`[get]`
| Indicates whether the AST is a BoundVariable More...
bool | IsQuantifier`[get]`
| Indicates whether the AST is a Quantifier More...
bool | IsSort`[get]`
| Indicates whether the AST is a Sort More...
bool | IsFuncDecl`[get]`
| Indicates whether the AST is a FunctionDeclaration More...

## Detailed Description

Function declarations.

Definition at line 30 of file FuncDecl.cs.

## Member Function Documentation

## ◆ Apply()

Expr Apply | ( | params Expr[] | args | ) |
| inline

Create expression that applies function to arguments.

Parameters

  args |

Returns

Definition at line 355 of file FuncDecl.cs.

356 {
357 Debug.Assert(args == null || args.All(a => a != null));
358
359 Context.CheckContextMatch<Expr>(args);
360 return Expr.Create(Context, this, args);
361 }
Microsoft.Z3.FuncDecl.args
Expr this[params Expr[] args
Create expression that applies function to arguments.
Definition: FuncDecl.cs:341

## ◆ Equals()

override bool Equals | ( | object | o | ) |
| inline

Object comparison.

Definition at line 57 of file FuncDecl.cs.

58 {
59 FuncDecl casted = o as FuncDecl;
60 if (casted == null) return false;
61 return this == casted;
62 }

## ◆ GetHashCode()

override int GetHashCode | ( |  | ) |
| inline

A hash code.

Definition at line 67 of file FuncDecl.cs.

68 {
69 return base.GetHashCode();
70 }

## ◆ operator!=()

static bool operator!= | ( | FuncDecl | a,
|  | FuncDecl | b
| ) |  |
| inline static

Comparison operator.

Returns
  True if a and b do not share the same context or are not equal, false otherwise.

Definition at line 49 of file FuncDecl.cs.

50 {
51 return !(a == b);
52 }

## ◆ operator==()

static bool operator== | ( | FuncDecl | a,
|  | FuncDecl | b
| ) |  |
| inline static

Comparison operator.

Returns
  True if a and b share the same context and are equal, false otherwise.

Definition at line 36 of file FuncDecl.cs.

37 {
38 return Object.ReferenceEquals(a, b) ||
39 (!Object.ReferenceEquals(a, null) &&
40 !Object.ReferenceEquals(b, null) &&
41 a.Context.nCtx == b.Context.nCtx &&
42 Native.Z3_is_eq_func_decl(a.Context.nCtx, a.NativeObject, b.NativeObject) != 0);
43 }

## ◆ ToString()

override string ToString | ( |  | ) |
| inline

A string representations of the function declaration.

Definition at line 75 of file FuncDecl.cs.

76 {
77 return Native.Z3_func_decl_to_string(Context.nCtx, NativeObject);
78 }

## ◆ Translate()

new FuncDecl Translate | ( | Context | ctx | ) |
| inline

Translates (copies) the function declaration to the Context ctx .

Parameters

  ctx | A context

Returns
  A copy of the function declaration which is associated with ctx

Definition at line 329 of file FuncDecl.cs.

330 {
331 return (FuncDecl) base.Translate(ctx);
332 }

Referenced by FuncDecl.Translate().

## Property Documentation

## ◆ args

Expr this[params Expr[] args
| get

Create expression that applies function to arguments.

Parameters

  args |

Returns

Definition at line 340 of file FuncDecl.cs.

341 {
342 get
343 {
344 Debug.Assert(args == null || args.All(a => a != null));
345
346 return Apply(args);
347 }
348 }
Microsoft.Z3.FuncDecl.Apply
Expr Apply(params Expr[] args)
Create expression that applies function to arguments.
Definition: FuncDecl.cs:355

Referenced by FuncDecl.Apply().

## ◆ Arity

uint Arity
| get

The arity of the function declaration

Definition at line 91 of file FuncDecl.cs.

92 {
93 get { return Native.Z3_get_arity(Context.nCtx, NativeObject); }
94 }

Referenced by Model.ConstInterp(), and Model.FuncInterp().

## ◆ DeclKind

Z3_decl_kind DeclKind
| get

The kind of the function declaration.

Definition at line 136 of file FuncDecl.cs.

137 {
138 get { return (Z3_decl_kind)Native.Z3_get_decl_kind(Context.nCtx, NativeObject); }
139 }
Z3_decl_kind
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:1000

## ◆ Domain

Sort [] Domain
| get

The domain of the function declaration

Definition at line 108 of file FuncDecl.cs.

109 {
110 get
111 {
112
113 uint n = DomainSize;
114
115 Sort[] res = new Sort[n];
116 for (uint i = 0; i < n; i++)
117 res[i] = Sort.Create(Context, Native.Z3_get_domain(Context.nCtx, NativeObject, i));
118 return res;
119 }
120 }
Microsoft.Z3.FuncDecl.DomainSize
uint DomainSize
The size of the domain of the function declaration Arity
Definition: FuncDecl.cs:101

## ◆ DomainSize

uint DomainSize
| get

The size of the domain of the function declaration

See also
  Arity

Definition at line 100 of file FuncDecl.cs.

101 {
102 get { return Native.Z3_get_domain_size(Context.nCtx, NativeObject); }
103 }

## ◆ Id

new uint Id
| get

Returns a unique identifier for the function declaration.

Definition at line 83 of file FuncDecl.cs.

84 {
85 get { return Native.Z3_get_func_decl_id(Context.nCtx, NativeObject); }
86 }

## ◆ Name

Symbol Name
| get

The name of the function declaration

Definition at line 144 of file FuncDecl.cs.

145 {
146 get
147 {
148 return Symbol.Create(Context, Native.Z3_get_decl_name(Context.nCtx, NativeObject));
149 }
150 }

## ◆ NumParameters

uint NumParameters
| get

The number of parameters of the function declaration

Definition at line 155 of file FuncDecl.cs.

156 {
157 get { return Native.Z3_get_decl_num_parameters(Context.nCtx, NativeObject); }
158 }

## ◆ Parameters

Parameter [] Parameters
| get

The parameters of the function declaration

Definition at line 163 of file FuncDecl.cs.

164 {
165 get
166 {
167
168 uint num = NumParameters;
169 Parameter[] res = new Parameter[num];
170 for (uint i = 0; i < num; i++)
171 {
172 Z3_parameter_kind k = (Z3_parameter_kind)Native.Z3_get_decl_parameter_kind(Context.nCtx, NativeObject, i);
173 switch (k)
174 {
175 case Z3_parameter_kind.Z3_PARAMETER_INT:
176 res[i] = new Parameter(k, Native.Z3_get_decl_int_parameter(Context.nCtx, NativeObject, i));
177 break;
178 case Z3_parameter_kind.Z3_PARAMETER_DOUBLE:
179 res[i] = new Parameter(k, Native.Z3_get_decl_double_parameter(Context.nCtx, NativeObject, i));
180 break;
181 case Z3_parameter_kind.Z3_PARAMETER_SYMBOL:
182 res[i] = new Parameter(k, Symbol.Create(Context, Native.Z3_get_decl_symbol_parameter(Context.nCtx, NativeObject, i)));
183 break;
184 case Z3_parameter_kind.Z3_PARAMETER_SORT:
185 res[i] = new Parameter(k, Sort.Create(Context, Native.Z3_get_decl_sort_parameter(Context.nCtx, NativeObject, i)));
186 break;
187 case Z3_parameter_kind.Z3_PARAMETER_AST:
188 res[i] = new Parameter(k, new AST(Context, Native.Z3_get_decl_ast_parameter(Context.nCtx, NativeObject, i)));
189 break;
190 case Z3_parameter_kind.Z3_PARAMETER_FUNC_DECL:
191 res[i] = new Parameter(k, new FuncDecl(Context, Native.Z3_get_decl_func_decl_parameter(Context.nCtx, NativeObject, i)));
192 break;
193 case Z3_parameter_kind.Z3_PARAMETER_RATIONAL:
194 res[i] = new Parameter(k, Native.Z3_get_decl_rational_parameter(Context.nCtx, NativeObject, i));
195 break;
196 default:
197 throw new Z3Exception("Unknown function declaration parameter kind encountered");
198 }
199 }
200 return res;
201 }
202 }
Microsoft.Z3.FuncDecl.NumParameters
uint NumParameters
The number of parameters of the function declaration
Definition: FuncDecl.cs:156
Z3_parameter_kind
Z3_parameter_kind
The different kinds of parameters that can be associated with function symbols.
Definition: z3_api.h:136

## ◆ Range

Sort Range
| get

The range of the function declaration

Definition at line 125 of file FuncDecl.cs.

126 {
127 get
128 {
129 return Sort.Create(Context, Native.Z3_get_range(Context.nCtx, NativeObject));
130 }
131 }