Function declarations. More...
Data Structures | |
class | Parameter |
Function declarations can have Parameters associated with them. More... | |
Public Member Functions | |
override bool | Equals (object o) |
Object comparison. | |
override int | GetHashCode () |
A hash code. | |
override string | ToString () |
A string representations of the function declaration. | |
Expr | Apply (params Expr[] args) |
Create expression that applies function to arguments. | |
Static Public Member Functions | |
static bool | operator== (FuncDecl a, FuncDecl b) |
Comparison operator. | |
static bool | operator!= (FuncDecl a, FuncDecl b) |
Comparison operator. | |
Properties | |
new uint | Id [get] |
Returns a unique identifier for the function declaration. | |
uint | Arity [get] |
The arity of the function declaration. | |
uint | DomainSize [get] |
The size of the domain of the function declaration
| |
Sort[] | Domain [get] |
The domain of the function declaration. | |
Sort | Range [get] |
The range of the function declaration. | |
Z3_decl_kind | DeclKind [get] |
The kind of the function declaration. | |
Symbol | Name [get] |
The name of the function declaration. | |
uint | NumParameters [get] |
The number of parameters of the function declaration. | |
Parameter[] | Parameters [get] |
The parameters of the function declaration. | |
Expr this[params Expr[] | args [get] |
Create expression that applies function to arguments. |
Function declarations.
Definition at line 29 of file FuncDecl.cs.
override bool Equals | ( | object | o | ) | [inline] |
Object comparison.
Reimplemented from AST.
Definition at line 56 of file FuncDecl.cs.
{ FuncDecl casted = o as FuncDecl; if (casted == null) return false; return this == casted; }
override int GetHashCode | ( | ) | [inline] |
A hash code.
Reimplemented from AST.
Definition at line 66 of file FuncDecl.cs.
Referenced by FuncDecl.GetHashCode().
{
return base.GetHashCode();
}
Comparison operator.
Definition at line 48 of file FuncDecl.cs.
{
return !(a == b);
}
Comparison operator.
Definition at line 35 of file FuncDecl.cs.
{
return Object.ReferenceEquals(a, b) ||
(!Object.ReferenceEquals(a, null) &&
!Object.ReferenceEquals(b, null) &&
a.Context.nCtx == b.Context.nCtx &&
Native.Z3_is_eq_func_decl(a.Context.nCtx, a.NativeObject, b.NativeObject) != 0);
}
override string ToString | ( | ) | [inline] |
A string representations of the function declaration.
Reimplemented from AST.
Definition at line 74 of file FuncDecl.cs.
{
return Native.Z3_func_decl_to_string(Context.nCtx, NativeObject);
}
Create expression that applies function to arguments.
args |
Definition at line 324 of file FuncDecl.cs.
uint Arity [get] |
The arity of the function declaration.
Definition at line 91 of file FuncDecl.cs.
Referenced by Model.ConstInterp(), and Model.FuncInterp().
Z3_decl_kind DeclKind [get] |
The kind of the function declaration.
Definition at line 138 of file FuncDecl.cs.
The domain of the function declaration.
Definition at line 108 of file FuncDecl.cs.
uint DomainSize [get] |
The size of the domain of the function declaration
Definition at line 100 of file FuncDecl.cs.
new uint Id [get] |
Returns a unique identifier for the function declaration.
Reimplemented from AST.
Definition at line 83 of file FuncDecl.cs.
The name of the function declaration.
Definition at line 146 of file FuncDecl.cs.
uint NumParameters [get] |
The number of parameters of the function declaration.
Definition at line 158 of file FuncDecl.cs.
Parameter [] Parameters [get] |
The parameters of the function declaration.
Definition at line 166 of file FuncDecl.cs.
The range of the function declaration.
Definition at line 126 of file FuncDecl.cs.