Public Member Functions | |
FuncDecl[] | getConstDecls () throws Z3Exception |
Expr[] | getConsts () throws Z3Exception |
FuncDecl[] | getTesterDecls () throws Z3Exception |
Package Functions | |
EnumSort (Context ctx, Symbol name, Symbol[] enumNames) throws Z3Exception |
Enumeration sorts.
Definition at line 23 of file EnumSort.java.
EnumSort | ( | Context | ctx, |
Symbol | name, | ||
Symbol[] | enumNames | ||
) | throws Z3Exception [inline, package] |
Definition at line 61 of file EnumSort.java.
{ super(ctx); int n = enumNames.length; long[] n_constdecls = new long[n]; long[] n_testers = new long[n]; setNativeObject(Native.mkEnumerationSort(ctx.nCtx(), name.getNativeObject(), (int) n, Symbol.arrayToNative(enumNames), n_constdecls, n_testers)); }
FuncDecl [] getConstDecls | ( | ) | throws Z3Exception [inline] |
The function declarations of the constants in the enumeration.
Definition at line 28 of file EnumSort.java.
Referenced by EnumSort.getConsts().
{ int n = Native.getDatatypeSortNumConstructors(getContext().nCtx(), getNativeObject()); FuncDecl[] t = new FuncDecl[n]; for (int i = 0; i < n; i++) t[i] = new FuncDecl(getContext(), Native.getDatatypeSortConstructor(getContext().nCtx(), getNativeObject(), i)); return t; }
Expr [] getConsts | ( | ) | throws Z3Exception [inline] |
The constants in the enumeration.
Definition at line 40 of file EnumSort.java.
{ FuncDecl[] cds = getConstDecls(); Expr[] t = new Expr[cds.length]; for (int i = 0; i < t.length; i++) t[i] = getContext().mkApp(cds[i]); return t; }
FuncDecl [] getTesterDecls | ( | ) | throws Z3Exception [inline] |
The test predicates for the constants in the enumeration.
Definition at line 52 of file EnumSort.java.
{ int n = Native.getDatatypeSortNumConstructors(getContext().nCtx(), getNativeObject()); FuncDecl[] t = new FuncDecl[n]; for (int i = 0; i < n; i++) t[i] = new FuncDecl(getContext(), Native.getDatatypeSortRecognizer(getContext().nCtx(), getNativeObject(), i)); return t; }