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.
override int	GetHashCode ()
	Hash code generation for Sorts.
override string	ToString ()
	A string representation of the sort.
Static Public Member Functions
static bool	operator== (Sort a, Sort b)
	Comparison operator.
static bool	operator!= (Sort a, Sort b)
	Comparison operator.
Protected Member Functions
internal	Sort (Context ctx)
	Sort constructor.
Properties
new uint	Id [get]
	Returns a unique identifier for the sort.
Z3_sort_kind	SortKind [get]
	The kind of the sort.
Symbol	Name [get]
	The name of the sort.

---

Detailed Description

The Sort class implements type information for ASTs.

Definition at line 29 of file Sort.cs.

---

Constructor & Destructor Documentation

internal Sort

(

Context

ctx

)

[inline, protected]

Sort constructor.

Definition at line 120 of file Sort.cs.

: base(ctx) { Contract.Requires(ctx != null); }

---

Member Function Documentation

override bool Equals

(

object

o

)

[inline]

Equality operator for objects of type Sort.

Parameters:

o

Returns:

Reimplemented from AST.

Definition at line 64 of file Sort.cs.

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

override int GetHashCode

(

)

[inline]

Hash code generation for Sorts.

Returns:

A hash code

Reimplemented from AST.

Definition at line 75 of file Sort.cs.

Referenced by Sort.GetHashCode().

        {
            return base.GetHashCode();
        }

static bool operator!=	(	Sort	a,
		Sort	b
	)		[inline, static]

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 54 of file Sort.cs.

        {
            return !(a == b);
        }

static bool operator==	(	Sort	a,
		Sort	b
	)		[inline, static]

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 38 of file Sort.cs.

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

override string ToString

(

)

[inline]

A string representation of the sort.

Reimplemented from AST.

Definition at line 111 of file Sort.cs.

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

---

Property Documentation

new uint Id [get]

Returns a unique identifier for the sort.

Reimplemented from AST.

Definition at line 84 of file Sort.cs.

Symbol Name [get]

The name of the sort.

Definition at line 100 of file Sort.cs.

Z3_sort_kind SortKind [get]

The kind of the sort.

Definition at line 92 of file Sort.cs.