Z3
Public Member Functions
DatatypeSort< R > Class Template Reference
+ Inheritance diagram for DatatypeSort< R >:

Public Member Functions

int getNumConstructors ()
 
FuncDecl< DatatypeSort< R > >[] getConstructors ()
 
FuncDecl< BoolSort >[] getRecognizers ()
 
FuncDecl<?>[][] getAccessors ()
 
- 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

Datatype sorts.

Definition at line 23 of file DatatypeSort.java.

Member Function Documentation

◆ getAccessors()

FuncDecl<?>[][] getAccessors ( )
inline

The constructor accessors.

Exceptions
Z3Exception
Z3Exceptionon error

Definition at line 76 of file DatatypeSort.java.

77 {
78
79 int n = getNumConstructors();
80 FuncDecl<?>[][] res = new FuncDecl[n][];
81 for (int i = 0; i < n; i++)
82 {
83 FuncDecl<?> fd = new FuncDecl<>(getContext(),
84 Native.getDatatypeSortConstructor(getContext().nCtx(),
85 getNativeObject(), i));
86 int ds = fd.getDomainSize();
87 FuncDecl<?>[] tmp = new FuncDecl[ds];
88 for (int j = 0; j < ds; j++)
89 tmp[j] = new FuncDecl<>(getContext(),
90 Native.getDatatypeSortConstructorAccessor(getContext()
91 .nCtx(), getNativeObject(), i, j));
92 res[i] = tmp;
93 }
94 return res;
95 }

◆ getConstructors()

FuncDecl< DatatypeSort< R > >[] getConstructors ( )
inline

The constructors.

Exceptions
Z3Exception
Z3Exceptionon error

Definition at line 43 of file DatatypeSort.java.

44 {
45 int n = getNumConstructors();
46 FuncDecl<DatatypeSort<R>>[] res = new FuncDecl[n];
47 for (int i = 0; i < n; i++)
48 res[i] = new FuncDecl<>(getContext(), Native.getDatatypeSortConstructor(
49 getContext().nCtx(), getNativeObject(), i));
50 return res;
51 }

◆ getNumConstructors()

int getNumConstructors ( )
inline

The number of constructors of the datatype sort.

Exceptions
Z3Exceptionon error
Returns
an int

Definition at line 30 of file DatatypeSort.java.

31 {
32 return Native.getDatatypeSortNumConstructors(getContext().nCtx(),
33 getNativeObject());
34 }

Referenced by DatatypeSort< R >.getAccessors(), DatatypeSort< R >.getConstructors(), and DatatypeSort< R >.getRecognizers().

◆ getRecognizers()

FuncDecl< BoolSort >[] getRecognizers ( )
inline

The recognizers.

Exceptions
Z3Exception
Z3Exceptionon error

Definition at line 60 of file DatatypeSort.java.

61 {
62 int n = getNumConstructors();
63 FuncDecl<BoolSort>[] res = new FuncDecl[n];
64 for (int i = 0; i < n; i++)
65 res[i] = new FuncDecl<>(getContext(), Native.getDatatypeSortRecognizer(
66 getContext().nCtx(), getNativeObject(), i));
67 return res;
68 }