TupleSort Class Reference

Inheritance diagram for TupleSort:

Public Member Functions
FuncDecl	mkDecl () throws Z3Exception
int	getNumFields () throws Z3Exception
FuncDecl[]	getFieldDecls () throws Z3Exception
Package Functions
	TupleSort (Context ctx, Symbol name, int numFields, Symbol[] fieldNames, Sort[] fieldSorts) throws Z3Exception

---

Detailed Description

Tuple sorts.

Definition at line 23 of file TupleSort.java.

---

Constructor & Destructor Documentation

TupleSort	(	Context	ctx,
		Symbol	name,
		int	numFields,
		Symbol[]	fieldNames,
		Sort[]	fieldSorts
	)		throws Z3Exception [inline, package]

Definition at line 59 of file TupleSort.java.

    {
        super(ctx);

        Native.LongPtr t = new Native.LongPtr();
        setNativeObject(Native.mkTupleSort(ctx.nCtx(), name.getNativeObject(),
                numFields, Symbol.arrayToNative(fieldNames),
                AST.arrayToNative(fieldSorts), t, new long[numFields]));
    }

---

Member Function Documentation

FuncDecl [] getFieldDecls

(

)

throws Z3Exception [inline]

The field declarations.

Exceptions:

Z3Exception

Definition at line 48 of file TupleSort.java.

    {

        int n = getNumFields();
        FuncDecl[] res = new FuncDecl[n];
        for (int i = 0; i < n; i++)
            res[i] = new FuncDecl(getContext(), Native.getTupleSortFieldDecl(
                    getContext().nCtx(), getNativeObject(), i));
        return res;
    }

int getNumFields

(

)

throws Z3Exception [inline]

The number of fields in the tuple.

Definition at line 39 of file TupleSort.java.

Referenced by TupleSort.getFieldDecls().

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

FuncDecl mkDecl

(

)

throws Z3Exception [inline]

The constructor function of the tuple.

Exceptions:

Z3Exception

Definition at line 29 of file TupleSort.java.

    {

        return new FuncDecl(getContext(), Native.getTupleSortMkDecl(getContext()
                .nCtx(), getNativeObject()));
    }