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

Public Member Functions

long getSize () throws Z3Exception

Package Functions

 FiniteDomainSort (Context ctx, long obj) throws Z3Exception
 FiniteDomainSort (Context ctx, Symbol name, long size) throws Z3Exception

Detailed Description

Finite domain sorts.

Definition at line 23 of file FiniteDomainSort.java.


Constructor & Destructor Documentation

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

Definition at line 35 of file FiniteDomainSort.java.

        {
                super(ctx, obj);
        }
FiniteDomainSort ( Context  ctx,
Symbol  name,
long  size 
) throws Z3Exception [inline, package]

Definition at line 40 of file FiniteDomainSort.java.

        {
                super(ctx, Native.mkFiniteDomainSort(ctx.nCtx(), name.getNativeObject(),
                                size));
        }

Member Function Documentation

long getSize ( ) throws Z3Exception [inline]

The size of the finite domain sort.

Definition at line 28 of file FiniteDomainSort.java.

        {
                Native.LongPtr res = new Native.LongPtr();
                Native.getFiniteDomainSortSize(getContext().nCtx(), getNativeObject(), res);
                return res.value;
        }
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines