Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines
Public Member Functions | Protected Member Functions | Package Functions | Static Package Functions
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();
        }
    }
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines