RelationSort Class Reference

Inheritance diagram for RelationSort:

Public Member Functions
int	getArity ()
Sort[]	getColumnSorts ()
Public Member Functions inherited from Sort
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

Relation sorts.

Definition at line 23 of file RelationSort.java.

Member Function Documentation

getArity()

int getArity ( )

inline

The arity of the relation sort.

Definition at line 28 of file RelationSort.java.

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

Referenced by RelationSort.getColumnSorts().

getColumnSorts()

Sort [] getColumnSorts ( )

inline

The sorts of the columns of the relation sort.

Exceptions

Z3Exception

Definition at line 37 of file RelationSort.java.

    {
 
        if (m_columnSorts != null)
            return m_columnSorts;
 
        int n = getArity();
        Sort[] res = new Sort[n];
        for (int i = 0; i < n; i++)
            res[i] = Sort.create(getContext(), Native.getRelationColumn(getContext()
                    .nCtx(), getNativeObject(), i));
        return res;
    }