Constructor< R > Class Template Reference

Inheritance diagram for Constructor< R >:

Public Member Functions
int	getNumFields ()
FuncDecl< DatatypeSort< R > >	ConstructorDecl ()
FuncDecl< BoolSort >	getTesterDecl ()
FuncDecl<?>[]	getAccessorDecls ()

Additional Inherited Members
Static Public Member Functions inherited from Z3Object
static long[]	arrayToNative (Z3Object[] a)
static int	arrayLength (Z3Object[] a)

Detailed Description

Constructors are used for datatype sorts.

Definition at line 25 of file Constructor.java.

Member Function Documentation

ConstructorDecl()

FuncDecl<DatatypeSort<R> > ConstructorDecl ( )

inline

The function declaration of the constructor.

Exceptions

Z3Exception
Z3Exception	on error

Definition at line 49 of file Constructor.java.

    {
        Native.LongPtr constructor = new Native.LongPtr();
        Native.LongPtr tester = new Native.LongPtr();
        long[] accessors = new long[n];
        Native.queryConstructor(getContext().nCtx(), getNativeObject(), n, constructor, tester, accessors);
        return new FuncDecl<>(getContext(), constructor.value);
    }

getAccessorDecls()

FuncDecl<?> [] getAccessorDecls ( )

inline

The function declarations of the accessors

Exceptions

Z3Exception
Z3Exception	on error

Definition at line 77 of file Constructor.java.

    {
        Native.LongPtr constructor = new Native.LongPtr();
        Native.LongPtr tester = new Native.LongPtr();
        long[] accessors = new long[n];
        Native.queryConstructor(getContext().nCtx(), getNativeObject(), n, constructor, tester, accessors);
        FuncDecl<?>[] t = new FuncDecl[n];
        for (int i = 0; i < n; i++)
            t[i] = new FuncDecl<>(getContext(), accessors[i]);
        return t;
    }

getNumFields()

int getNumFields ( )

inline

The number of fields of the constructor.

Exceptions

Z3Exception
Z3Exception	on error

Returns

an int

Definition at line 39 of file Constructor.java.

    {    
        return n;
    }

getTesterDecl()

FuncDecl<BoolSort> getTesterDecl ( )

inline

The function declaration of the tester.

Exceptions

Z3Exception
Z3Exception	on error

Definition at line 63 of file Constructor.java.

    {
        Native.LongPtr constructor = new Native.LongPtr();
        Native.LongPtr tester = new Native.LongPtr();
        long[] accessors = new long[n];
        Native.queryConstructor(getContext().nCtx(), getNativeObject(), n, constructor, tester, accessors);
        return new FuncDecl<>(getContext(), tester.value);
    }