Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines
Public Member Functions | Static Public Member Functions | Protected Member Functions | Properties
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:
aA Sort
bA 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:
aA Sort
bA 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.

The kind of the sort.

Definition at line 92 of file Sort.cs.

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