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
Protected Member Functions
void	finalize () throws Z3Exception
Package Functions
	Constructor (Context ctx, Symbol name, Symbol recognizer, Symbol[] fieldNames, Sort[] sorts, int[] sortRefs) throws Z3Exception

---

Detailed Description

Constructors are used for datatype sorts.

Definition at line 23 of file Constructor.java.

---

Constructor & Destructor Documentation

Constructor	(	Context	ctx,
		Symbol	name,
		Symbol	recognizer,
		Symbol[]	fieldNames,
		Sort[]	sorts,
		int[]	sortRefs
	)		throws Z3Exception [inline, package]

Definition at line 86 of file Constructor.java.

        {
                super(ctx);

                n = AST.arrayLength(fieldNames);

                if (n != AST.arrayLength(sorts))
                        throw new Z3Exception(
                                        "Number of field names does not match number of sorts");
                if (sortRefs != null && sortRefs.length != n)
                        throw new Z3Exception(
                                        "Number of field names does not match number of sort refs");

                if (sortRefs == null)
                        sortRefs = new int[n];

                setNativeObject(Native.mkConstructor(ctx.nCtx(), name.getNativeObject(),
                                recognizer.getNativeObject(), n, Symbol.arrayToNative(fieldNames),
                                Sort.arrayToNative(sorts), sortRefs));

        }

---

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 [inline, protected]

Destructor.

Reimplemented from Z3Object.

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);
        }