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
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
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:701
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  }