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  }

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

Referenced by FuncDecl.Apply().

◆ Arity

uint Arity
get

The arity of the function declaration

Definition at line 92 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 137 of file FuncDecl.cs.

137  {
138  get { return (Z3_decl_kind)Native.Z3_get_decl_kind(Context.nCtx, NativeObject); }
139  }

◆ Domain

Sort [] Domain
get

The domain of the function declaration

Definition at line 109 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  }

◆ DomainSize

uint DomainSize
get

The size of the domain of the function declaration

See also
Arity

Definition at line 101 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 84 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 145 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 156 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 164 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  }

◆ Range

Sort Range
get

The range of the function declaration

Definition at line 126 of file FuncDecl.cs.

126  {
127  get
128  {
129  return Sort.Create(Context, Native.Z3_get_range(Context.nCtx, NativeObject));
130  }
131  }
Microsoft.Z3.FuncDecl.Apply
Expr Apply(params Expr[] args)
Create expression that applies function to arguments.
Definition: FuncDecl.cs:355
Microsoft.Z3.FuncDecl.NumParameters
uint NumParameters
The number of parameters of the function declaration
Definition: FuncDecl.cs:156
Microsoft.Z3.FuncDecl.args
Expr this[params Expr[] args
Create expression that applies function to arguments.
Definition: FuncDecl.cs:341
Microsoft.Z3.FuncDecl.DomainSize
uint DomainSize
The size of the domain of the function declaration Arity
Definition: FuncDecl.cs:101
Z3_decl_kind
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:1000
Z3_parameter_kind
Z3_parameter_kind
The different kinds of parameters that can be associated with function symbols.
Definition: z3_api.h:135