Public Member Functions | |
int | getNumConstructors () throws Z3Exception |
FuncDecl[] | getConstructors () throws Z3Exception |
FuncDecl[] | getRecognizers () throws Z3Exception |
FuncDecl[][] | getAccessors () throws Z3Exception |
Package Functions | |
DatatypeSort (Context ctx, long obj) throws Z3Exception | |
DatatypeSort (Context ctx, Symbol name, Constructor[] constructors) throws Z3Exception |
Datatype sorts.
Definition at line 23 of file DatatypeSort.java.
DatatypeSort | ( | Context | ctx, |
long | obj | ||
) | throws Z3Exception [inline, package] |
Definition at line 90 of file DatatypeSort.java.
{ super(ctx, obj); }
DatatypeSort | ( | Context | ctx, |
Symbol | name, | ||
Constructor[] | constructors | ||
) | throws Z3Exception [inline, package] |
Definition at line 95 of file DatatypeSort.java.
{ super(ctx, Native.mkDatatype(ctx.nCtx(), name.getNativeObject(), (int) constructors.length, arrayToNative(constructors))); }
FuncDecl [][] getAccessors | ( | ) | throws Z3Exception [inline] |
The constructor accessors.
Z3Exception |
Definition at line 69 of file DatatypeSort.java.
{ int n = getNumConstructors(); FuncDecl[][] res = new FuncDecl[n][]; for (int i = 0; i < n; i++) { FuncDecl fd = new FuncDecl(getContext(), Native.getDatatypeSortConstructor(getContext().nCtx(), getNativeObject(), i)); int ds = fd.getDomainSize(); FuncDecl[] tmp = new FuncDecl[ds]; for (int j = 0; j < ds; j++) tmp[j] = new FuncDecl(getContext(), Native.getDatatypeSortConstructorAccessor(getContext() .nCtx(), getNativeObject(), i, j)); res[i] = tmp; } return res; }
FuncDecl [] getConstructors | ( | ) | throws Z3Exception [inline] |
The constructors.
Z3Exception |
Definition at line 39 of file DatatypeSort.java.
{ int n = getNumConstructors(); FuncDecl[] res = new FuncDecl[n]; for (int i = 0; i < n; i++) res[i] = new FuncDecl(getContext(), Native.getDatatypeSortConstructor( getContext().nCtx(), getNativeObject(), i)); return res; }
int getNumConstructors | ( | ) | throws Z3Exception [inline] |
The number of constructors of the datatype sort.
Definition at line 28 of file DatatypeSort.java.
Referenced by DatatypeSort.getAccessors(), DatatypeSort.getConstructors(), and DatatypeSort.getRecognizers().
{ return Native.getDatatypeSortNumConstructors(getContext().nCtx(), getNativeObject()); }
FuncDecl [] getRecognizers | ( | ) | throws Z3Exception [inline] |
The recognizers.
Z3Exception |
Definition at line 54 of file DatatypeSort.java.
{ int n = getNumConstructors(); FuncDecl[] res = new FuncDecl[n]; for (int i = 0; i < n; i++) res[i] = new FuncDecl(getContext(), Native.getDatatypeSortRecognizer( getContext().nCtx(), getNativeObject(), i)); return res; }