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

new FuncDecl	Translate (Context ctx)
	Translates (copies) the function declaration to the Context ctx . 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...

Properties inherited from Z3Object
Context	Context `[get]`
	Access Context object More...

Detailed Description

Function declarations.

Definition at line 30 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 355 of file FuncDecl.cs.

         {
             Debug.Assert(args == null || args.All(a => a != null));
  
             Context.CheckContextMatch<Expr>(args);
             return Expr.Create(Context, this, args);
         }

◆ Equals()

override bool Equals ( object o )

inline

Object comparison.

Definition at line 57 of file FuncDecl.cs.

         {
             FuncDecl casted = o as FuncDecl;
             if (casted == null) return false;
             return this == casted;
         }

◆ GetHashCode()

override int GetHashCode ( )

inline

A hash code.

Definition at line 67 of file FuncDecl.cs.

         {
             return base.GetHashCode();
         }

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

         {
             return !(a == b);
         }

◆ 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 36 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);
         }

◆ ToString()

override string ToString ( )

inline

A string representations of the function declaration.

Definition at line 75 of file FuncDecl.cs.

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

◆ Translate()

new FuncDecl Translate ( Context ctx )

inline

Translates (copies) the function declaration to the Context ctx .

Parameters

ctx A context

Returns: A copy of the function declaration which is associated with ctx

Definition at line 329 of file FuncDecl.cs.

         {
             return (FuncDecl) base.Translate(ctx);
         }

Referenced by FuncDecl.Translate().

Property Documentation

◆ args

Expr this[params Expr[] args

get

Create expression that applies function to arguments.

Parameters

args

Returns

Definition at line 340 of file FuncDecl.cs.

         {
             get
             {
                 Debug.Assert(args == null || args.All(a => a != null));
  
                 return Apply(args);
             }
         }

Referenced by FuncDecl.Apply().

◆ Arity

uint Arity

get

The arity of the function declaration

Definition at line 91 of file FuncDecl.cs.

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

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

◆ DeclKind

Z3_decl_kind DeclKind

get

The kind of the function declaration.

Definition at line 136 of file FuncDecl.cs.

         {
             get { return (Z3_decl_kind)Native.Z3_get_decl_kind(Context.nCtx, NativeObject); }
         }

◆ Domain

Sort [] Domain

get

The domain of the function declaration

Definition at line 108 of file FuncDecl.cs.

         {
             get
             {
  
                 uint n = DomainSize;
  
                 Sort[] res = new Sort[n];
                 for (uint i = 0; i < n; i++)
                     res[i] = Sort.Create(Context, Native.Z3_get_domain(Context.nCtx, NativeObject, i));
                 return res;
             }
         }

◆ DomainSize

uint DomainSize

get

The size of the domain of the function declaration

See also: Arity

Definition at line 100 of file FuncDecl.cs.

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

◆ Id

new uint Id

get

Returns a unique identifier for the function declaration.

Definition at line 83 of file FuncDecl.cs.

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

◆ Name

Symbol Name

get

The name of the function declaration

Definition at line 144 of file FuncDecl.cs.

         {
             get
             {
                 return Symbol.Create(Context, Native.Z3_get_decl_name(Context.nCtx, NativeObject));
             }
         }

◆ NumParameters

uint NumParameters

get

The number of parameters of the function declaration

Definition at line 155 of file FuncDecl.cs.

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

◆ Parameters

Parameter [] Parameters

get

The parameters of the function declaration

Definition at line 163 of file FuncDecl.cs.

         {
             get
             {
  
                 uint num = NumParameters;
                 Parameter[] res = new Parameter[num];
                 for (uint i = 0; i < num; i++)
                 {
                     Z3_parameter_kind k = (Z3_parameter_kind)Native.Z3_get_decl_parameter_kind(Context.nCtx, NativeObject, i);
                     switch (k)
                     {
                         case Z3_parameter_kind.Z3_PARAMETER_INT:
                             res[i] = new Parameter(k, Native.Z3_get_decl_int_parameter(Context.nCtx, NativeObject, i));
                             break;
                         case Z3_parameter_kind.Z3_PARAMETER_DOUBLE:
                             res[i] = new Parameter(k, Native.Z3_get_decl_double_parameter(Context.nCtx, NativeObject, i));
                             break;
                         case Z3_parameter_kind.Z3_PARAMETER_SYMBOL:
                             res[i] = new Parameter(k, Symbol.Create(Context, Native.Z3_get_decl_symbol_parameter(Context.nCtx, NativeObject, i)));
                             break;
                         case Z3_parameter_kind.Z3_PARAMETER_SORT:
                             res[i] = new Parameter(k, Sort.Create(Context, Native.Z3_get_decl_sort_parameter(Context.nCtx, NativeObject, i)));
                             break;
                         case Z3_parameter_kind.Z3_PARAMETER_AST:
                             res[i] = new Parameter(k, new AST(Context, Native.Z3_get_decl_ast_parameter(Context.nCtx, NativeObject, i)));
                             break;
                         case Z3_parameter_kind.Z3_PARAMETER_FUNC_DECL:
                             res[i] = new Parameter(k, new FuncDecl(Context, Native.Z3_get_decl_func_decl_parameter(Context.nCtx, NativeObject, i)));
                             break;
                         case Z3_parameter_kind.Z3_PARAMETER_RATIONAL:
                             res[i] = new Parameter(k, Native.Z3_get_decl_rational_parameter(Context.nCtx, NativeObject, i));
                             break;
                         default:
                             throw new Z3Exception("Unknown function declaration parameter kind encountered");
                     }
                 }
                 return res;
             }
         }

◆ Range

Sort Range

get

The range of the function declaration

Definition at line 125 of file FuncDecl.cs.

         {
             get
             {
                 return Sort.Create(Context, Native.Z3_get_range(Context.nCtx, NativeObject));
             }
         }

Data Structures

Public Member Functions

Static Public Member Functions

Properties

Detailed Description

Member Function Documentation

◆ Apply()

◆ Equals()

◆ GetHashCode()

◆ operator!=()

◆ operator==()

◆ ToString()

◆ Translate()

Property Documentation

◆ args

◆ Arity

◆ DeclKind

◆ Domain

◆ DomainSize

◆ Id

◆ Name

◆ NumParameters

◆ Parameters

◆ Range