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
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

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  }
com.microsoft.z3.FuncDecl<?>
com.microsoft.z3.FuncDecl.getDomainSize
int getDomainSize()
Definition: FuncDecl.java:87
com.microsoft.z3.DatatypeSort.getNumConstructors
int getNumConstructors()
Definition: DatatypeSort.java:30