Sort Class Reference

Inheritance diagram for Sort:

Public Member Functions
boolean	equals (Object o)
int	hashCode ()
int	getId ()
Z3_sort_kind	getSortKind ()
Symbol	getName ()
String	toString ()
Sort	translate (Context ctx)
Public Member Functions inherited from AST
int	compareTo (AST other)
Z3_ast_kind	getASTKind ()
boolean	isExpr ()
boolean	isApp ()
boolean	isVar ()
boolean	isQuantifier ()
boolean	isSort ()
boolean	isFuncDecl ()
String	getSExpr ()

Additional Inherited Members
Static Public Member Functions inherited from Z3Object
static long[]	arrayToNative (Z3Object[] a)
static int	arrayLength (Z3Object[] a)

Detailed Description

The Sort class implements type information for ASTs.

Definition at line 26 of file Sort.java.

Member Function Documentation

equals()

boolean equals ( Object  o )

inline

Equality operator for objects of type Sort.

Reimplemented from AST.

Definition at line 32 of file Sort.java.

    {
        if (o == this) return true;
        if (!(o instanceof Sort)) return false;
        Sort other = (Sort) o;
 
        return (getContext().nCtx() == other.getContext().nCtx()) &&
            (Native.isEqSort(getContext().nCtx(), getNativeObject(), other.getNativeObject()));
    }

getId()

int getId ( )

inline

Returns a unique identifier for the sort.

Reimplemented from AST.

Definition at line 55 of file Sort.java.

    {
        return Native.getSortId(getContext().nCtx(), getNativeObject());
    }

getName()

Symbol getName ( )

inline

The name of the sort

Definition at line 72 of file Sort.java.

    {
        return Symbol.create(getContext(),
                Native.getSortName(getContext().nCtx(), getNativeObject()));
    }

getSortKind()

Z3_sort_kind getSortKind ( )

inline

The kind of the sort.

Definition at line 63 of file Sort.java.

    {
        return Z3_sort_kind.fromInt(Native.getSortKind(getContext().nCtx(),
                getNativeObject()));
    }

hashCode()

int hashCode ( )

inline

Hash code generation for Sorts

Returns

A hash code

Reimplemented from AST.

Definition at line 47 of file Sort.java.

    {
        return super.hashCode();
    }

toString()

String toString ( )

inline

A string representation of the sort.

Reimplemented from AST.

Definition at line 82 of file Sort.java.

                             {
        return Native.sortToString(getContext().nCtx(), getNativeObject());
    }

translate()

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 

Exceptions

Z3Exception

on error

Reimplemented from AST.

Definition at line 94 of file Sort.java.

    {
        return (Sort) super.translate(ctx);
    }

Referenced by AstRef.__copy__(), Goal.__copy__(), AstVector.__copy__(), FuncInterp.__copy__(), ModelRef.__copy__(), Solver.__copy__(), Goal.__deepcopy__(), AstVector.__deepcopy__(), FuncInterp.__deepcopy__(), ModelRef.__deepcopy__(), Solver.__deepcopy__(), and Sort.translate().