Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines
Public Member Functions | Protected Member Functions | Package Functions
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);
        }
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines