Package com.microsoft.z3

Class EnumSort<R>

java.lang.Object

com.microsoft.z3.Z3Object

com.microsoft.z3.AST

com.microsoft.z3.Sort

com.microsoft.z3.EnumSort<R>

All Implemented Interfaces:

Comparable<AST>

public class EnumSort<R>
extends Sort

Enumeration sorts.

Method Summary

Modifier and Type	Method	Description
Expr<EnumSort<R>>	getConst(int inx)	Retrieves the inx'th constant in the enumeration.
FuncDecl<EnumSort<R>>	getConstDecl(int inx)	Retrieves the inx'th constant declaration in the enumeration.
FuncDecl<EnumSort<R>>[]	getConstDecls()	The function declarations of the constants in the enumeration.
Expr<EnumSort<R>>[]	getConsts()	The constants in the enumeration.
FuncDecl<BoolSort>	getTesterDecl(int inx)	Retrieves the inx'th tester/recognizer declaration in the enumeration.
FuncDecl<BoolSort>[]	getTesterDecls()	The test predicates for the constants in the enumeration.

Methods inherited from class com.microsoft.z3.Sort

equals, getId, getName, getSortKind, hashCode, toString, translate

Methods inherited from class com.microsoft.z3.AST

compareTo, getASTKind, getSExpr, isApp, isExpr, isFuncDecl, isQuantifier, isSort, isVar

Methods inherited from class com.microsoft.z3.Z3Object

arrayLength, arrayToNative

Methods inherited from class java.lang.Object

clone, finalize, getClass, notify, notifyAll, wait, wait, wait

Method Details

getConstDecls

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

The function declarations of the constants in the enumeration.

Throws:

Z3Exception - on error

getConstDecl

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

Retrieves the inx'th constant declaration in the enumeration.

Throws:

Z3Exception - on error

getConsts

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

The constants in the enumeration.

Returns:

an Expr[]

Throws:

Z3Exception - on error

getConst

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

Retrieves the inx'th constant in the enumeration.

Returns:

an Expr

Throws:

Z3Exception - on error

getTesterDecls

public FuncDecl<BoolSort>[] getTesterDecls()

The test predicates for the constants in the enumeration.

Throws:

Z3Exception - on error

getTesterDecl

public FuncDecl<BoolSort> getTesterDecl(int inx)

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

Throws:

Z3Exception - on error