Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines
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.

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

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.

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

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();
        }
static bool operator!= ( FuncDecl  a,
FuncDecl  b 
) [inline, static]

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 
) [inline, static]

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.

Reimplemented from AST.

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 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().

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.

Reimplemented from AST.

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.

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.

 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines