DatatypeSort< R > Class Template Reference

Inheritance diagram for DatatypeSort< R >:

Public Member Functions
int	getNumConstructors ()
boolean	isRecursive ()
FuncDecl< DatatypeSort< R > >[]	getConstructors ()
FuncDecl< BoolSort >[]	getRecognizers ()
FuncDecl<?>[][]	getAccessors ()
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)
int	getDepth ()
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

Datatype sorts.

Definition at line 23 of file DatatypeSort.java.

Member Function Documentation

getAccessors()

FuncDecl<?>[][] getAccessors ( )

inline

The constructor accessors.

Exceptions

Z3Exception
Z3Exception	on error

Definition at line 87 of file DatatypeSort.java.

    {
 
        int n = getNumConstructors();
        FuncDecl<?>[][] res = new FuncDecl[n][];
        for (int i = 0; i < n; i++)
        {
            FuncDecl<?> fd = new FuncDecl<>(getContext(),
                    Native.getDatatypeSortConstructor(getContext().nCtx(),
                            getNativeObject(), i));
            int ds = fd.getDomainSize();
            FuncDecl<?>[] tmp = new FuncDecl[ds];
            for (int j = 0; j < ds; j++)
                tmp[j] = new FuncDecl<>(getContext(),
                        Native.getDatatypeSortConstructorAccessor(getContext()
                                .nCtx(), getNativeObject(), i, j));
            res[i] = tmp;
        }
        return res;
    }

getConstructors()

FuncDecl< DatatypeSort< R > >[] getConstructors ( )

inline

The constructors.

Exceptions

Z3Exception
Z3Exception	on error

Definition at line 54 of file DatatypeSort.java.

    {
        int n = getNumConstructors();
        FuncDecl<DatatypeSort<R>>[] res = new FuncDecl[n];
        for (int i = 0; i < n; i++)
            res[i] = new FuncDecl<>(getContext(), Native.getDatatypeSortConstructor(
                    getContext().nCtx(), getNativeObject(), i));
        return res;
    }

getNumConstructors()

int getNumConstructors ( )

inline

The number of constructors of the datatype sort.

Exceptions

Z3Exception

on error

Returns

an int

Definition at line 30 of file DatatypeSort.java.

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

Referenced by DatatypeSort< R >.getAccessors(), DatatypeSort< R >.getConstructors(), and DatatypeSort< R >.getRecognizers().

getRecognizers()

FuncDecl< BoolSort >[] getRecognizers ( )

inline

The recognizers.

Exceptions

Z3Exception
Z3Exception	on error

Definition at line 71 of file DatatypeSort.java.

    {
        int n = getNumConstructors();
        FuncDecl<BoolSort>[] res = new FuncDecl[n];
        for (int i = 0; i < n; i++)
            res[i] = new FuncDecl<>(getContext(), Native.getDatatypeSortRecognizer(
                    getContext().nCtx(), getNativeObject(), i));
        return res;
    }

isRecursive()

boolean isRecursive ( )

inline

Indicates whether the datatype sort is recursive.

Exceptions

Z3Exception

on error

Returns

a boolean

Definition at line 41 of file DatatypeSort.java.

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