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

## ◆ getConstructors()

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

The constructors.

Exceptions

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

  Z3Exception | on 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 |
  Z3Exception | on 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 }