FuncInterp.java

Go to the documentation of this file.

 
package com.microsoft.z3;
 
import java.lang.ref.ReferenceQueue;
 
@SuppressWarnings("unchecked")
public class FuncInterp<R extends Sort> extends Z3Object {
 
    public static class Entry<R extends Sort> extends Z3Object {
 
        public Expr<R> getValue()
        {
            return (Expr<R>) Expr.create(getContext(),
                    Native.funcEntryGetValue(getContext().nCtx(), getNativeObject()));
        }
 
        public int getNumArgs()
        {
            return Native.funcEntryGetNumArgs(getContext().nCtx(), getNativeObject());
        }
 
        public Expr<?>[] getArgs()
        {
            int n = getNumArgs();
            Expr<?>[] res = new Expr[n];
            for (int i = 0; i < n; i++)
                res[i] = Expr.create(getContext(), Native.funcEntryGetArg(
                        getContext().nCtx(), getNativeObject(), i));
            return res;
        }
 
        @Override
        public String toString()
        {
            int n = getNumArgs();
            String res = "[";
            Expr<?>[] args = getArgs();
            for (int i = 0; i < n; i++)
                res += args[i] + ", ";
            return res + getValue() + "]";
        }
 
        Entry(Context ctx, long obj) {
            super(ctx, obj);
        }
 
        @Override
        void incRef() {
            Native.funcEntryIncRef(getContext().nCtx(), getNativeObject());
        }
 
        @Override
        void addToReferenceQueue() {
            getContext().getReferenceQueue().storeReference(this, FuncEntryRef::new);
        }
 
        private static class FuncEntryRef extends Z3ReferenceQueue.Reference<Entry<?>> {
 
            private FuncEntryRef(Entry<?> referent, ReferenceQueue<Z3Object> q) {
                super(referent, q);
            }
 
            @Override
            void decRef(Context ctx, long z3Obj) {
                Native.funcEntryDecRef(ctx.nCtx(), z3Obj);
            }
        }
    }
 
    public int getNumEntries()
    {
        return Native.funcInterpGetNumEntries(getContext().nCtx(), getNativeObject());
    }
 
    public Entry<R>[] getEntries()
    {
        int n = getNumEntries();
        Entry<R>[] res = new Entry[n];
        for (int i = 0; i < n; i++)
            res[i] = new Entry<>(getContext(), Native.funcInterpGetEntry(getContext()
                    .nCtx(), getNativeObject(), i));
        return res;
    }
 
    public Expr<R> getElse()
    {
        return (Expr<R>) Expr.create(getContext(),
                Native.funcInterpGetElse(getContext().nCtx(), getNativeObject()));
    }
 
    public int getArity()
    {
        return Native.funcInterpGetArity(getContext().nCtx(), getNativeObject());
    }
 
    public String toString()
    {
        String res = "";
        res += "[";
        for (Entry<R> e : getEntries())
        {
            int n = e.getNumArgs();
            if (n > 1)
                res += "[";
            Expr<?>[] args = e.getArgs();
            for (int i = 0; i < n; i++)
            {
                if (i != 0)
                    res += ", ";
                res += args[i];
            }
            if (n > 1)
                res += "]";
            res += " -> " + e.getValue() + ", ";
        }
        res += "else -> " + getElse();
        res += "]";
        return res;
    }
 
    FuncInterp(Context ctx, long obj)
    {
        super(ctx, obj);
    }
 
    @Override
    void incRef() {
        Native.funcInterpIncRef(getContext().nCtx(), getNativeObject());
    }
 
    @Override
    void addToReferenceQueue() {
        getContext().getReferenceQueue().storeReference(this, FuncInterpRef::new);
    }
 
    private static class FuncInterpRef extends Z3ReferenceQueue.Reference<FuncInterp<?>> {
 
        private FuncInterpRef(FuncInterp<?> referent, ReferenceQueue<Z3Object> q) {
            super(referent, q);
        }
 
        @Override
        void decRef(Context ctx, long z3Obj) {
            Native.funcInterpDecRef(ctx.nCtx(), z3Obj);
        }
    }
}