Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines
Public Member Functions | Package Functions
BitVecSort Class Reference
+ Inheritance diagram for BitVecSort:

Public Member Functions

int getSize () throws Z3Exception

Package Functions

 BitVecSort (Context ctx, long obj) throws Z3Exception

Detailed Description

Bit-vector sorts.

Definition at line 23 of file BitVecSort.java.


Constructor & Destructor Documentation

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

Definition at line 33 of file BitVecSort.java.

        {
                super(ctx, obj);
        }

Member Function Documentation

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