Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines
Public Member Functions | Package Functions
RelationSort Class Reference
+ Inheritance diagram for RelationSort:

Public Member Functions

int getArity () throws Z3Exception
Sort[] getColumnSorts () throws Z3Exception

Package Functions

 RelationSort (Context ctx, long obj) throws Z3Exception

Detailed Description

Relation sorts.

Definition at line 23 of file RelationSort.java.


Constructor & Destructor Documentation

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

Definition at line 53 of file RelationSort.java.

    {
        super(ctx, obj);
    }

Member Function Documentation

int getArity ( ) throws Z3Exception [inline]

The arity of the relation sort.

Definition at line 28 of file RelationSort.java.

Referenced by RelationSort.getColumnSorts().

    {
        return Native.getRelationArity(getContext().nCtx(), getNativeObject());
    }
Sort [] getColumnSorts ( ) throws Z3Exception [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;
    }
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines