Constructor Class Reference

Inheritance diagram for Constructor:

Public Member Functions
int	getNumFields ()
FuncDecl	ConstructorDecl ()
FuncDecl	getTesterDecl ()
FuncDecl[]	getAccessorDecls ()
Public Member Functions inherited from Z3Object
void	dispose ()
Public Member Functions inherited from IDisposable
void	dispose ()

Protected Member Functions
void	finalize ()
Protected Member Functions inherited from Z3Object
void	finalize ()

Detailed Description

Constructors are used for datatype sorts.

Definition at line 23 of file Constructor.java.

Member Function Documentation

FuncDecl ConstructorDecl ( )

inline

The function declaration of the constructor.

Exceptions

Z3Exception
Z3Exception	on error

Definition at line 41 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);         
    }

void finalize ( )

inlineprotected

Destructor.

Exceptions

Z3Exception

on error

Definition at line 85 of file Constructor.java.

    {
        Native.delConstructor(getContext().nCtx(), getNativeObject());
    }

FuncDecl [] getAccessorDecls ( )

inline

The function declarations of the accessors

Exceptions

Z3Exception
Z3Exception	on error

Definition at line 69 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;
    }

int getNumFields ( )

inline

The number of fields of the constructor.

Exceptions

Z3Exception
Z3Exception	on error

Returns

an int

Definition at line 31 of file Constructor.java.

    {    
        return n;
    }

FuncDecl getTesterDecl ( )

inline

The function declaration of the tester.

Exceptions

Z3Exception
Z3Exception	on error

Definition at line 55 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);
    }