TupleSort Class Reference

Inheritance diagram for TupleSort:

Public Member Functions
FuncDecl< TupleSort >	mkDecl ()
int	getNumFields ()
FuncDecl<?>[]	getFieldDecls ()
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

Tuple sorts.

Definition at line 23 of file TupleSort.java.

Member Function Documentation

getFieldDecls()

FuncDecl<?> [] getFieldDecls ( )

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

getNumFields()

int getNumFields ( )

inline

The number of fields in the tuple.

Definition at line 39 of file TupleSort.java.

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

Referenced by TupleSort.getFieldDecls().

mkDecl()

FuncDecl<TupleSort> mkDecl ( )

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