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

Public Member Functions

int getNumConstructors () throws Z3Exception
FuncDecl[] getConstructors () throws Z3Exception
FuncDecl[] getRecognizers () throws Z3Exception
FuncDecl[][] getAccessors () throws Z3Exception

Package Functions

 DatatypeSort (Context ctx, long obj) throws Z3Exception
 DatatypeSort (Context ctx, Symbol name, Constructor[] constructors) throws Z3Exception

Detailed Description

Datatype sorts.

Definition at line 23 of file DatatypeSort.java.


Constructor & Destructor Documentation

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

Definition at line 90 of file DatatypeSort.java.

        {
                super(ctx, obj);
        }
DatatypeSort ( Context  ctx,
Symbol  name,
Constructor[]  constructors 
) throws Z3Exception [inline, package]

Definition at line 95 of file DatatypeSort.java.

        {
                super(ctx, Native.mkDatatype(ctx.nCtx(), name.getNativeObject(),
                                (int) constructors.length, arrayToNative(constructors)));

        }

Member Function Documentation

FuncDecl [][] getAccessors ( ) throws Z3Exception [inline]

The constructor accessors.

Exceptions:
Z3Exception

Definition at line 69 of file DatatypeSort.java.

        {

                int n = getNumConstructors();
                FuncDecl[][] res = new FuncDecl[n][];
                for (int i = 0; i < n; i++)
                {
                        FuncDecl fd = new FuncDecl(getContext(),
                                        Native.getDatatypeSortConstructor(getContext().nCtx(),
                                                        getNativeObject(), i));
                        int ds = fd.getDomainSize();
                        FuncDecl[] tmp = new FuncDecl[ds];
                        for (int j = 0; j < ds; j++)
                                tmp[j] = new FuncDecl(getContext(),
                                                Native.getDatatypeSortConstructorAccessor(getContext()
                                                                .nCtx(), getNativeObject(), i, j));
                        res[i] = tmp;
                }
                return res;
        }
FuncDecl [] getConstructors ( ) throws Z3Exception [inline]

The constructors.

Exceptions:
Z3Exception

Definition at line 39 of file DatatypeSort.java.

        {
                int n = getNumConstructors();
                FuncDecl[] res = new FuncDecl[n];
                for (int i = 0; i < n; i++)
                        res[i] = new FuncDecl(getContext(), Native.getDatatypeSortConstructor(
                                        getContext().nCtx(), getNativeObject(), i));
                return res;
        }
int getNumConstructors ( ) throws Z3Exception [inline]

The number of constructors of the datatype sort.

Definition at line 28 of file DatatypeSort.java.

Referenced by DatatypeSort.getAccessors(), DatatypeSort.getConstructors(), and DatatypeSort.getRecognizers().

        {
                return Native.getDatatypeSortNumConstructors(getContext().nCtx(),
                                getNativeObject());
        }
FuncDecl [] getRecognizers ( ) throws Z3Exception [inline]

The recognizers.

Exceptions:
Z3Exception

Definition at line 54 of file DatatypeSort.java.

        {
                int n = getNumConstructors();
                FuncDecl[] res = new FuncDecl[n];
                for (int i = 0; i < n; i++)
                        res[i] = new FuncDecl(getContext(), Native.getDatatypeSortRecognizer(
                                        getContext().nCtx(), getNativeObject(), i));
                return res;
        }
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines