BitVecExpr Class Reference

Inheritance diagram for BitVecExpr:

Public Member Functions
int	getSortSize () throws Z3Exception
Package Functions
	BitVecExpr (Context ctx)
	BitVecExpr (Context ctx, long obj) throws Z3Exception

---

Detailed Description

Bit-vector expressions

Definition at line 23 of file BitVecExpr.java.

---

Constructor & Destructor Documentation

BitVecExpr

(

Context

ctx

)

[inline, package]

Constructor for BitVecExpr

Definition at line 38 of file BitVecExpr.java.

        {
                super(ctx);
        }

BitVecExpr	(	Context	ctx,
		long	obj
	)		throws Z3Exception [inline, package]

Definition at line 43 of file BitVecExpr.java.

        {
                super(ctx, obj);
        }

---

Member Function Documentation

int getSortSize

(

)

throws Z3Exception [inline]

The size of the sort of a bit-vector term.

Exceptions:

Z3Exception

Definition at line 30 of file BitVecExpr.java.

        {
                return ((BitVecSort) getSort()).getSize();
        }