Constructor Class Reference

Inheritance diagram for Constructor:

Public Member Functions
int	getNumFields ()
FuncDecl	ConstructorDecl ()
FuncDecl	getTesterDecl ()
FuncDecl []	getAccessorDecls ()

Detailed Description

Constructors are used for datatype sorts.

Definition at line 23 of file Constructor.java.

Member Function Documentation

ConstructorDecl()

FuncDecl ConstructorDecl ( )

inline

The function declaration of the constructor.

Exceptions

Z3Exception
Z3Exception	on error

Definition at line 47 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 75 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 37 of file Constructor.java.

    {    
        return n;
    }

getTesterDecl()

FuncDecl getTesterDecl ( )

inline

The function declaration of the tester.

Exceptions

Z3Exception
Z3Exception	on error

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