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