Public Member Functions | |
FuncDecl | mkDecl () throws Z3Exception |
int | getNumFields () throws Z3Exception |
FuncDecl[] | getFieldDecls () throws Z3Exception |
Package Functions | |
TupleSort (Context ctx, Symbol name, int numFields, Symbol[] fieldNames, Sort[] fieldSorts) throws Z3Exception |
Tuple sorts.
Definition at line 23 of file TupleSort.java.
TupleSort | ( | Context | ctx, |
Symbol | name, | ||
int | numFields, | ||
Symbol[] | fieldNames, | ||
Sort[] | fieldSorts | ||
) | throws Z3Exception [inline, package] |
Definition at line 59 of file TupleSort.java.
{ super(ctx); Native.LongPtr t = new Native.LongPtr(); setNativeObject(Native.mkTupleSort(ctx.nCtx(), name.getNativeObject(), numFields, Symbol.arrayToNative(fieldNames), AST.arrayToNative(fieldSorts), t, new long[numFields])); }
FuncDecl [] getFieldDecls | ( | ) | throws Z3Exception [inline] |
The field declarations.
Z3Exception |
Definition at line 48 of file TupleSort.java.
{ int n = getNumFields(); FuncDecl[] res = new FuncDecl[n]; for (int i = 0; i < n; i++) res[i] = new FuncDecl(getContext(), Native.getTupleSortFieldDecl( getContext().nCtx(), getNativeObject(), i)); return res; }
int getNumFields | ( | ) | throws Z3Exception [inline] |
The number of fields in the tuple.
Definition at line 39 of file TupleSort.java.
Referenced by TupleSort.getFieldDecls().
{ return Native.getTupleSortNumFields(getContext().nCtx(), getNativeObject()); }
FuncDecl mkDecl | ( | ) | throws Z3Exception [inline] |
The constructor function of the tuple.
Z3Exception |
Definition at line 29 of file TupleSort.java.
{ return new FuncDecl(getContext(), Native.getTupleSortMkDecl(getContext() .nCtx(), getNativeObject())); }