Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Macros Groups Pages
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.
 
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.
 
- Public Member Functions inherited from AST
override bool Equals (object o)
 Object comparison.
 
virtual int CompareTo (object other)
 Object Comparison.
 
override int GetHashCode ()
 The AST's hash code.
 
AST Translate (Context ctx)
 Translates (copies) the AST to the Context ctx .
 
override string ToString ()
 A string representation of the AST.
 
string SExpr ()
 A string representation of the AST in s-expression notation.
 
- Public Member Functions inherited from Z3Object
void Dispose ()
 Disposes of the underlying native Z3 object.
 

Static Public Member Functions

static bool operator== (FuncDecl a, FuncDecl b)
 Comparison operator.
 
static bool operator!= (FuncDecl a, FuncDecl b)
 Comparison operator.
 
- Static Public Member Functions inherited from AST
static bool operator== (AST a, AST b)
 Comparison operator.
 
static bool operator!= (AST a, AST 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

See Also
Arity

 
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.
 
- Properties inherited from AST
uint Id [get]
 A unique identifier for the AST (unique among all ASTs).
 
Z3_ast_kind ASTKind [get]
 The kind of the AST.
 
bool IsExpr [get]
 Indicates whether the AST is an Expr
 
bool IsVar [get]
 Indicates whether the AST is a BoundVariable
 
bool IsQuantifier [get]
 Indicates whether the AST is a Quantifier
 
bool IsSort [get]
 Indicates whether the AST is a Sort
 
bool IsFuncDecl [get]
 Indicates whether the AST is a FunctionDeclaration
 

Detailed Description

Function declarations.

Definition at line 29 of file FuncDecl.cs.

Member Function Documentation

Expr Apply ( params Expr[]  args)
inline

Create expression that applies function to arguments.

Parameters
args
Returns

Definition at line 342 of file FuncDecl.cs.

{
Contract.Requires(args == null || Contract.ForAll(args, a => a != null));
Context.CheckContextMatch(args);
return Expr.Create(Context, this, args);
}
override bool Equals ( object  o)
inline

Object comparison.

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.

Definition at line 66 of file FuncDecl.cs.

Referenced by FuncDecl.GetHashCode().

{
return base.GetHashCode();
}
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.

{
return !(a == b);
}
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.

{
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.

Definition at line 74 of file FuncDecl.cs.

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

Property Documentation

Expr this[params Expr[] args
get

Create expression that applies function to arguments.

Parameters
args
Returns

Definition at line 328 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.

Sort [] Domain
get

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

See Also
Arity

Definition at line 100 of file FuncDecl.cs.

new uint Id
get

Returns a unique identifier for the function declaration.

Definition at line 83 of file FuncDecl.cs.

Symbol Name
get

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.

Sort Range
get

The range of the function declaration

Definition at line 126 of file FuncDecl.cs.