Sort Class Reference

Inheritance diagram for Sort:

Public Member Functions
boolean	equals (Object o)
int	hashCode ()
int	getId () throws Z3Exception
Z3_sort_kind	getSortKind () throws Z3Exception
Symbol	getName () throws Z3Exception
String	toString ()
Protected Member Functions
	Sort (Context ctx) throws Z3Exception
Package Functions
	Sort (Context ctx, long obj) throws Z3Exception
void	checkNativeObject (long obj) throws Z3Exception
Static Package Functions
static Sort	create (Context ctx, long obj) throws Z3Exception

---

Detailed Description

The Sort class implements type information for ASTs.

Definition at line 26 of file Sort.java.

---

Constructor & Destructor Documentation

Sort

(

Context

ctx

)

throws Z3Exception [inline, protected]

Sort constructor

Definition at line 101 of file Sort.java.

    {
        super(ctx);
        {
        }
    }

Sort	(	Context	ctx,
		long	obj
	)		throws Z3Exception [inline, package]

Definition at line 108 of file Sort.java.

    {
        super(ctx, obj);
        {
        }
    }

---

Member Function Documentation

void checkNativeObject

(

long

obj

)

throws Z3Exception [inline, package]

Reimplemented from Z3Object.

Definition at line 115 of file Sort.java.

    {
        if (Native.getAstKind(getContext().nCtx(), obj) != Z3_ast_kind.Z3_SORT_AST
                .toInt())
            throw new Z3Exception("Underlying object is not a sort");
        super.checkNativeObject(obj);
    }

static Sort create	(	Context	ctx,
		long	obj
	)		throws Z3Exception [inline, static, package]

Reimplemented from AST.

Definition at line 123 of file Sort.java.

Referenced by AST.create(), Quantifier.getBoundVariableSorts(), RelationSort.getColumnSorts(), ArraySort.getDomain(), FuncDecl.getDomain(), FuncDecl.getParameters(), ArraySort.getRange(), FuncDecl.getRange(), Context.getSMTLIBSorts(), Expr.getSort(), and Model.getSorts().

    {
        Z3_sort_kind sk = Z3_sort_kind.fromInt(Native.getSortKind(ctx.nCtx(), obj));
        switch (sk)
        {
        case Z3_ARRAY_SORT:
            return new ArraySort(ctx, obj);
        case Z3_BOOL_SORT:
            return new BoolSort(ctx, obj);
        case Z3_BV_SORT:
            return new BitVecSort(ctx, obj);
        case Z3_DATATYPE_SORT:
            return new DatatypeSort(ctx, obj);
        case Z3_INT_SORT:
            return new IntSort(ctx, obj);
        case Z3_REAL_SORT:
            return new RealSort(ctx, obj);
        case Z3_UNINTERPRETED_SORT:
            return new UninterpretedSort(ctx, obj);
        case Z3_FINITE_DOMAIN_SORT:
            return new FiniteDomainSort(ctx, obj);
        case Z3_RELATION_SORT:
            return new RelationSort(ctx, obj);
        default:
            throw new Z3Exception("Unknown sort kind");
        }
    }

boolean equals

(

Object

o

)

[inline]

Equality operator for objects of type Sort.

Parameters:

o

Returns:

Reimplemented from AST.

Definition at line 35 of file Sort.java.

    {
        Sort casted = null;

        try {
            casted = Sort.class.cast(o);
        } catch (ClassCastException e) {
            return false;
        }

        return this.getNativeObject() == casted.getNativeObject();
    }

int getId

(

)

throws Z3Exception [inline]

Returns a unique identifier for the sort.

Reimplemented from AST.

Definition at line 61 of file Sort.java.

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

Symbol getName

(

)

throws Z3Exception [inline]

The name of the sort

Definition at line 78 of file Sort.java.

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

Z3_sort_kind getSortKind

(

)

throws Z3Exception [inline]

The kind of the sort.

Definition at line 69 of file Sort.java.

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

int hashCode

(

)

[inline]

Hash code generation for Sorts

Returns:

A hash code

Reimplemented from AST.

Definition at line 53 of file Sort.java.

    {
        return super.hashCode();
    }

String toString

(

)

[inline]

A string representation of the sort.

Reimplemented from AST.

Definition at line 87 of file Sort.java.

    {
        try
        {
            return Native.sortToString(getContext().nCtx(), getNativeObject());
        } catch (Z3Exception e)
        {
            return "Z3Exception: " + e.getMessage();
        }
    }