EnumSort< R > Class Template Reference

Inheritance diagram for EnumSort< R >:

Public Member Functions
FuncDecl< EnumSort< R > >[]	getConstDecls ()
FuncDecl< EnumSort< R > >	getConstDecl (int inx)
Expr< EnumSort< R > >[]	getConsts ()
Expr< EnumSort< R > >	getConst (int inx)
FuncDecl< BoolSort >[]	getTesterDecls ()
FuncDecl< BoolSort >	getTesterDecl (int inx)
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

Enumeration sorts.

Definition at line 24 of file EnumSort.java.

Member Function Documentation

getConst()

Expr<EnumSort<R> > getConst ( int  inx )

inline

Retrieves the inx'th constant in the enumeration.

Exceptions

Z3Exception

on error

Returns

an Expr

Definition at line 67 of file EnumSort.java.

    {        
        return getContext().mkApp(getConstDecl(inx));
    }

getConstDecl()

FuncDecl<EnumSort<R> > getConstDecl ( int  inx )

inline

Retrieves the inx'th constant declaration in the enumeration.

Exceptions

Z3Exception

on error

Definition at line 43 of file EnumSort.java.

    {
        return new FuncDecl<>(getContext(), Native.getDatatypeSortConstructor(getContext().nCtx(), getNativeObject(), inx));
    }

getConstDecls()

FuncDecl<EnumSort<R> > [] getConstDecls ( )

inline

The function declarations of the constants in the enumeration.

Exceptions

Z3Exception

on error

Definition at line 30 of file EnumSort.java.

    {
        int n = Native.getDatatypeSortNumConstructors(getContext().nCtx(), getNativeObject());
        FuncDecl<?>[] t = new FuncDecl[n];
        for (int i = 0; i < n; i++)
            t[i] = new FuncDecl<>(getContext(), Native.getDatatypeSortConstructor(getContext().nCtx(), getNativeObject(), i));
        return (FuncDecl<EnumSort<R>>[]) t;
    }

getConsts()

Expr<EnumSort<R> > [] getConsts ( )

inline

The constants in the enumeration.

Exceptions

Z3Exception

on error

Returns

an Expr[]

Definition at line 53 of file EnumSort.java.

    {        
        FuncDecl<?>[] cds = getConstDecls();
        Expr<?>[] t = new Expr[cds.length];
        for (int i = 0; i < t.length; i++)
            t[i] = getContext().mkApp(cds[i]);
        return (Expr<EnumSort<R>>[]) t;
    }

getTesterDecl()

FuncDecl<BoolSort> getTesterDecl ( int  inx )

inline

Retrieves the inx'th tester/recognizer declaration in the enumeration.

Exceptions

Z3Exception

on error

Definition at line 90 of file EnumSort.java.

    {
        return new FuncDecl<>(getContext(), Native.getDatatypeSortRecognizer(getContext().nCtx(), getNativeObject(), inx));
    }

getTesterDecls()

FuncDecl<BoolSort> [] getTesterDecls ( )

inline

The test predicates for the constants in the enumeration.

Exceptions

Z3Exception

on error

Definition at line 77 of file EnumSort.java.

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