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 }
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 
)
inlinestatic

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 
)
inlinestatic

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
ctxA 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 }
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
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 }
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 }
uint NumParameters
The number of parameters of the function declaration
Definition: FuncDecl.cs:156
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 }