EnumSort Class Reference

Inheritance diagram for EnumSort:

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

Enumeration sorts.

Definition at line 23 of file EnumSort.java.

Member Function Documentation

getConst()

Expr getConst ( int  inx )

inline

Retrieves the inx'th constant in the enumeration.

Exceptions

Z3Exception

on error

Returns

an Expr

Definition at line 66 of file EnumSort.java.

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

getConstDecl()

FuncDecl getConstDecl ( int  inx )

inline

Retrieves the inx'th constant declaration in the enumeration.

Exceptions

Z3Exception

on error

Definition at line 42 of file EnumSort.java.

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

Referenced by EnumSort.getConst().

getConstDecls()

FuncDecl [] getConstDecls ( )

inline

The function declarations of the constants in the enumeration.

Exceptions

Z3Exception

on error

Definition at line 29 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 t;
    }

Referenced by EnumSort.getConsts().

getConsts()

Expr [] getConsts ( )

inline

The constants in the enumeration.

Exceptions

Z3Exception

on error

Returns

an Expr[]

Definition at line 52 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 t;
    }

getTesterDecl()

FuncDecl getTesterDecl ( int  inx )

inline

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

Exceptions

Z3Exception

on error

Definition at line 88 of file EnumSort.java.

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

getTesterDecls()

FuncDecl [] getTesterDecls ( )

inline

The test predicates for the constants in the enumeration.

Exceptions

Z3Exception

on error

Definition at line 75 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.getDatatypeSortRecognizer(getContext().nCtx(), getNativeObject(), i));
        return t;
    }