Public Member Functions | |
int | getSize () throws Z3Exception |
Package Functions | |
BitVecSort (Context ctx, long obj) throws Z3Exception |
Bit-vector sorts.
Definition at line 23 of file BitVecSort.java.
BitVecSort | ( | Context | ctx, |
long | obj | ||
) | throws Z3Exception [inline, package] |
Definition at line 33 of file BitVecSort.java.
{ super(ctx, obj); }
int getSize | ( | ) | throws Z3Exception [inline] |
The size of the bit-vector sort.
Definition at line 28 of file BitVecSort.java.
{ return Native.getBvSortSize(getContext().nCtx(), getNativeObject()); }