Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines
Public Member Functions | Package Functions
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();
        }
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines