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

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(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
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  }
override int GetHashCode ( )
inline

A hash code.

Definition at line 66 of file FuncDecl.cs.

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

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

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.