Public Member Functions | |
int | getSortSize () throws Z3Exception |
Package Functions | |
BitVecExpr (Context ctx) | |
BitVecExpr (Context ctx, long obj) throws Z3Exception |
Bit-vector expressions
Definition at line 23 of file BitVecExpr.java.
BitVecExpr | ( | Context | ctx | ) | [inline, package] |
BitVecExpr | ( | Context | ctx, |
long | obj | ||
) | throws Z3Exception [inline, package] |
Definition at line 43 of file BitVecExpr.java.
{ super(ctx, obj); }
int getSortSize | ( | ) | throws Z3Exception [inline] |
The size of the sort of a bit-vector term.
Z3Exception |
Definition at line 30 of file BitVecExpr.java.
{ return ((BitVecSort) getSort()).getSize(); }