Constructor Class Reference

Inheritance diagram for Constructor:

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

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

Detailed Description

Constructors are used for datatype sorts.

Definition at line 23 of file Constructor.java.

Member Function Documentation

FuncDecl ConstructorDecl ( ) throws Z3Exception

inline

The function declaration of the constructor.

Exceptions

Z3Exception

Definition at line 38 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 ( ) throws Z3Exception

inlineprotected

Destructor.

Definition at line 79 of file Constructor.java.

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

FuncDecl [] getAccessorDecls ( ) throws Z3Exception

inline

The function declarations of the accessors

Exceptions

Z3Exception

Definition at line 64 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 ( ) throws Z3Exception

inline

The number of fields of the constructor.

Exceptions

Z3Exception

Definition at line 29 of file Constructor.java.

        {       
                return n;
        }

FuncDecl getTesterDecl ( ) throws Z3Exception

inline

The function declaration of the tester.

Exceptions

Z3Exception

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