Public Member Functions | |
long | getSize () throws Z3Exception |
Package Functions | |
FiniteDomainSort (Context ctx, long obj) throws Z3Exception | |
FiniteDomainSort (Context ctx, Symbol name, long size) throws Z3Exception |
Finite domain sorts.
Definition at line 23 of file FiniteDomainSort.java.
FiniteDomainSort | ( | Context | ctx, |
long | obj | ||
) | throws Z3Exception [inline, package] |
Definition at line 35 of file FiniteDomainSort.java.
{ super(ctx, obj); }
FiniteDomainSort | ( | Context | ctx, |
Symbol | name, | ||
long | size | ||
) | throws Z3Exception [inline, package] |
Definition at line 40 of file FiniteDomainSort.java.
{ super(ctx, Native.mkFiniteDomainSort(ctx.nCtx(), name.getNativeObject(), size)); }
long getSize | ( | ) | throws Z3Exception [inline] |
The size of the finite domain sort.
Definition at line 28 of file FiniteDomainSort.java.
{ Native.LongPtr res = new Native.LongPtr(); Native.getFiniteDomainSortSize(getContext().nCtx(), getNativeObject(), res); return res.value; }