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;
    }