Sort Class Reference

The Sort class implements type information for ASTs. More...

Inheritance diagram for Sort:

Public Member Functions
override bool	Equals (object o)
	Equality operator for objects of type Sort. More...
override int	GetHashCode ()
	Hash code generation for Sorts More...
override string	ToString ()
	A string representation of the sort. More...
new Sort	Translate (Context ctx)
	Translates (copies) the sort to the Context ctx . 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== (Sort a, Sort b)
	Comparison operator. More...
static bool	operator!= (Sort a, Sort 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 sort. More...
Z3_sort_kind	SortKind [get]
	The kind of the sort. More...
Symbol	Name [get]
	The name of the sort 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

The Sort class implements type information for ASTs.

Definition at line 28 of file Sort.cs.

Member Function Documentation

Equals()

override bool Equals ( object  o )

inline

Equality operator for objects of type Sort.

Parameters

o

Returns

Definition at line 63 of file Sort.cs.

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

GetHashCode()

override int GetHashCode ( )

inline

Hash code generation for Sorts

Returns

A hash code

Definition at line 74 of file Sort.cs.

        {
            return base.GetHashCode();
        }

operator!=()

static bool operator!= ( Sort  a, Sort  b  )

inlinestatic

Comparison operator.

Parameters

a	A Sort
b	A Sort

Returns

True if a and b are not from the same context or represent different sorts; false otherwise.

Definition at line 53 of file Sort.cs.

        {
            return !(a == b);
        }

operator==()

static bool operator== ( Sort  a, Sort  b  )

inlinestatic

Comparison operator.

Parameters

a	A Sort
b	A Sort

Returns

True if a and b are from the same context and represent the same sort; false otherwise.

Definition at line 37 of file Sort.cs.

        {
            return Object.ReferenceEquals(a, b) ||
                   (!Object.ReferenceEquals(a, null) &&
                    !Object.ReferenceEquals(b, null) &&
                    a.Context == b.Context &&
                    0 != Native.Z3_is_eq_sort(a.Context.nCtx, a.NativeObject, b.NativeObject));
        }

ToString()

override string ToString ( )

inline

A string representation of the sort.

Definition at line 109 of file Sort.cs.

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

Translate()

new Sort Translate ( Context  ctx )

inline

Translates (copies) the sort to the Context ctx .

Parameters

ctx

A context

Returns

A copy of the sort which is associated with ctx

Definition at line 119 of file Sort.cs.

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

Referenced by Sort.Translate().

Property Documentation

Id

new uint Id

get

Returns a unique identifier for the sort.

Definition at line 82 of file Sort.cs.

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

Name

Symbol Name

get

The name of the sort

Definition at line 98 of file Sort.cs.

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

SortKind

Z3_sort_kind SortKind

get

The kind of the sort.

Definition at line 90 of file Sort.cs.

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