Constructor.java

Go to the documentation of this file.

 
package com.microsoft.z3;
 
import java.lang.ref.ReferenceQueue;
 
public class Constructor<R> extends Z3Object {
    private final int n;
 
    Constructor(Context ctx, int n, long nativeObj) {
        super(ctx, nativeObj);
        this.n = n;
    }
 
    public int getNumFields()
    {    
        return n;
    }
 
    public FuncDecl<DatatypeSort<R>> 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<BoolSort> 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;
    }
 
    @Override
    void incRef() {
        // Datatype constructors are not reference counted.
    }
 
    @Override
    void addToReferenceQueue() {
        getContext().getReferenceQueue().storeReference(this, ConstructorRef::new);
    }
 
    static <R> Constructor<R> of(Context ctx, Symbol name, Symbol recognizer,
            Symbol[] fieldNames, Sort[] sorts, int[] sortRefs) {
        int 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];
 
        long nativeObj = Native.mkConstructor(ctx.nCtx(), name.getNativeObject(),
                recognizer.getNativeObject(), n, Symbol.arrayToNative(fieldNames),
                Sort.arrayToNative(sorts), sortRefs);
        return new Constructor<>(ctx, n, nativeObj);
 
    }
 
    private static class ConstructorRef extends Z3ReferenceQueue.Reference<Constructor<?>> {
 
        private ConstructorRef(Constructor<?> referent, ReferenceQueue<Z3Object> q) {
            super(referent, q);
        }
 
        @Override
        void decRef(Context ctx, long z3Obj) {
            Native.delConstructor(ctx.nCtx(), z3Obj);
        }
    }
}