Z3
Public Member Functions
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< BoolSortgetTesterDecl (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
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 ()
 

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
Z3Exceptionon error
Returns
an Expr

Definition at line 67 of file EnumSort.java.

68 {
69 return getContext().mkApp(getConstDecl(inx));
70 }
final< R extends Sort > Expr< R > mkApp(FuncDecl< R > f, Expr<?>... args)
Definition: Context.java:692
FuncDecl< EnumSort< R > > getConstDecl(int inx)
Definition: EnumSort.java:43

◆ getConstDecl()

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

Retrieves the inx'th constant declaration in the enumeration.

Exceptions
Z3Exceptionon error

Definition at line 43 of file EnumSort.java.

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

◆ getConstDecls()

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

The function declarations of the constants in the enumeration.

Exceptions
Z3Exceptionon error

Definition at line 30 of file EnumSort.java.

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

◆ getConsts()

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

The constants in the enumeration.

Exceptions
Z3Exceptionon error
Returns
an Expr[]

Definition at line 53 of file EnumSort.java.

54 {
55 FuncDecl<?>[] cds = getConstDecls();
56 Expr<?>[] t = new Expr[cds.length];
57 for (int i = 0; i < t.length; i++)
58 t[i] = getContext().mkApp(cds[i]);
59 return (Expr<EnumSort<R>>[]) t;
60 }
FuncDecl< EnumSort< R > >[] getConstDecls()
Definition: EnumSort.java:30

◆ getTesterDecl()

FuncDecl< BoolSort > getTesterDecl ( int  inx)
inline

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

Exceptions
Z3Exceptionon error

Definition at line 90 of file EnumSort.java.

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

◆ getTesterDecls()

FuncDecl< BoolSort >[] getTesterDecls ( )
inline

The test predicates for the constants in the enumeration.

Exceptions
Z3Exceptionon error

Definition at line 77 of file EnumSort.java.

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