TupleSort Class Reference

Inheritance diagram for TupleSort:

Public Member Functions
FuncDecl	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 ()
Public Member Functions inherited from AST
boolean	equals (Object o)
int	compareTo (AST other)
int	hashCode ()
int	getId ()
AST	translate (Context ctx)
Z3_ast_kind	getASTKind ()
boolean	isExpr ()
boolean	isApp ()
boolean	isVar ()
boolean	isQuantifier ()
boolean	isSort ()
boolean	isFuncDecl ()
String	toString ()
String	getSExpr ()

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