src/api/java/Constructor.java

Go to the documentation of this file.

package com.microsoft.z3;

public class Constructor extends Z3Object
{
    public int getNumFields()
    {    
        return n;
    }

    public FuncDecl ConstructorDecl()
    {
        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);         
    }

    public FuncDecl getTesterDecl()
    {
        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);
    }

    public FuncDecl[] getAccessorDecls()
    {
        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;
    }

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

    private int n = 0;

    Constructor(Context ctx, Symbol name, Symbol recognizer,
            Symbol[] fieldNames, Sort[] sorts, int[] sortRefs)
           
    {
        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));

    }
}