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

339  {
340  Contract.Requires(args == null || Contract.ForAll(args, a => a != null));
341 
342  Context.CheckContextMatch<Expr>(args);
343  return Expr.Create(Context, this, args);
344  }
Expr this[params Expr[] args
Create expression that applies function to arguments.
Definition: FuncDecl.cs:324

◆ Equals()

override bool Equals ( object  o)
inline

Object comparison.

Definition at line 56 of file FuncDecl.cs.

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

◆ GetHashCode()

override int GetHashCode ( )
inline

A hash code.

Definition at line 66 of file FuncDecl.cs.

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

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

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

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

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

◆ ToString()

override string ToString ( )
inline

A string representations of the function declaration.

Definition at line 74 of file FuncDecl.cs.

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

Property Documentation

◆ args

Expr this[params Expr[] args
get

Create expression that applies function to arguments.

Parameters
args
Returns

Definition at line 324 of file FuncDecl.cs.

324  {
325  get
326  {
327  Contract.Requires(args == null || Contract.ForAll(args, a => a != null));
328 
329  return Apply(args);
330  }
331  }
Expr this[params Expr[] args
Create expression that applies function to arguments.
Definition: FuncDecl.cs:324
Expr Apply(params Expr[] args)
Create expression that applies function to arguments.
Definition: FuncDecl.cs:338

◆ Arity

uint Arity
get

The arity of the function declaration

Definition at line 91 of file FuncDecl.cs.

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

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

◆ DeclKind

Z3_decl_kind DeclKind
get

The kind of the function declaration.

Definition at line 138 of file FuncDecl.cs.

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

◆ Domain

Sort [] Domain
get

The domain of the function declaration

Definition at line 108 of file FuncDecl.cs.

108  {
109  get
110  {
111  Contract.Ensures(Contract.Result<Sort[]>() != null);
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:100

◆ DomainSize

uint DomainSize
get

The size of the domain of the function declaration

See also
Arity

Definition at line 100 of file FuncDecl.cs.

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

◆ Id

new uint Id
get

Returns a unique identifier for the function declaration.

Definition at line 83 of file FuncDecl.cs.

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

◆ Name

Symbol Name
get

The name of the function declaration

Definition at line 146 of file FuncDecl.cs.

146  {
147  get
148  {
149  Contract.Ensures(Contract.Result<Symbol>() != null);
150  return Symbol.Create(Context, Native.Z3_get_decl_name(Context.nCtx, NativeObject));
151  }
152  }

◆ NumParameters

uint NumParameters
get

The number of parameters of the function declaration

Definition at line 158 of file FuncDecl.cs.

158  {
159  get { return Native.Z3_get_decl_num_parameters(Context.nCtx, NativeObject); }
160  }

◆ Parameters

Parameter [] Parameters
get

The parameters of the function declaration

Definition at line 166 of file FuncDecl.cs.

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

◆ Range

Sort Range
get

The range of the function declaration

Definition at line 126 of file FuncDecl.cs.

126  {
127  get
128  {
129  Contract.Ensures(Contract.Result<Sort>() != null);
130  return Sort.Create(Context, Native.Z3_get_range(Context.nCtx, NativeObject));
131  }
132  }