Model.java

Go to the documentation of this file.

 
package com.microsoft.z3;
 
import com.microsoft.z3.enumerations.Z3_sort_kind;
 
import java.lang.ref.ReferenceQueue;
 
@SuppressWarnings("unchecked")
public class Model extends Z3Object {
    public <R extends Sort> Expr<R> getConstInterp(Expr<R> a)
    {
        getContext().checkContextMatch(a);
        return getConstInterp(a.getFuncDecl());
    }
 
    public <R extends Sort> Expr<R> getConstInterp(FuncDecl<R> f)
    {
        getContext().checkContextMatch(f);
        if (f.getArity() != 0)
            throw new Z3Exception(
                    "Non-zero arity functions have FunctionInterpretations as a model. Use getFuncInterp.");
 
        long n = Native.modelGetConstInterp(getContext().nCtx(), getNativeObject(),
                f.getNativeObject());
        if (n == 0)
            return null;
        else
            return (Expr<R>) Expr.create(getContext(), n);
    }
 
    public <R extends Sort> FuncInterp<R> getFuncInterp(FuncDecl<R> f)
    {
        getContext().checkContextMatch(f);
 
        Z3_sort_kind sk = Z3_sort_kind.fromInt(Native.getSortKind(getContext()
                .nCtx(), Native.getRange(getContext().nCtx(), f.getNativeObject())));
 
        if (f.getArity() == 0)
        {
            long n = Native.modelGetConstInterp(getContext().nCtx(),
                    getNativeObject(), f.getNativeObject());
 
            if (sk == Z3_sort_kind.Z3_ARRAY_SORT)
            {
                if (n == 0)
                    return null;
                else
                {
                    if (Native.isAsArray(getContext().nCtx(), n)) {
                      long fd = Native.getAsArrayFuncDecl(getContext().nCtx(), n);
                      return getFuncInterp(new FuncDecl<>(getContext(), fd));
                    }
                    return null;
                }
            } else
            {
                throw new Z3Exception(
                        "Constant functions do not have a function interpretation; use getConstInterp");
            }
        } else
        {
            long n = Native.modelGetFuncInterp(getContext().nCtx(),
                    getNativeObject(), f.getNativeObject());
            if (n == 0)
                return null;
            else
                return new FuncInterp<>(getContext(), n);
        }
    }
 
    public int getNumConsts()
    {
        return Native.modelGetNumConsts(getContext().nCtx(), getNativeObject());
    }
 
    public FuncDecl<?>[] getConstDecls()
    {
        int n = getNumConsts();
        FuncDecl<?>[] res = new FuncDecl[n];
        for (int i = 0; i < n; i++)
            res[i] = new FuncDecl<>(getContext(), Native.modelGetConstDecl(getContext()
                    .nCtx(), getNativeObject(), i));
        return res;
    }
 
    public int getNumFuncs()
    {
        return Native.modelGetNumFuncs(getContext().nCtx(), getNativeObject());
    }
 
    public FuncDecl<?>[] getFuncDecls()
    {
        int n = getNumFuncs();
        FuncDecl<?>[] res = new FuncDecl[n];
        for (int i = 0; i < n; i++)
            res[i] = new FuncDecl<>(getContext(), Native.modelGetFuncDecl(getContext()
                    .nCtx(), getNativeObject(), i));
        return res;
    }
 
    public FuncDecl<?>[] getDecls()
    {
        int nFuncs = getNumFuncs();
        int nConsts = getNumConsts();
        int n = nFuncs + nConsts;
        FuncDecl<?>[] res = new FuncDecl[n];
        for (int i = 0; i < nConsts; i++)
            res[i] = new FuncDecl<>(getContext(), Native.modelGetConstDecl(getContext()
                    .nCtx(), getNativeObject(), i));
        for (int i = 0; i < nFuncs; i++)
            res[nConsts + i] = new FuncDecl<>(getContext(), Native.modelGetFuncDecl(
                    getContext().nCtx(), getNativeObject(), i));
        return res;
    }
 
    @SuppressWarnings("serial")
    public class ModelEvaluationFailedException extends Z3Exception
    {
        public ModelEvaluationFailedException()
        {
            super();
        }
    }
 
    public <R extends Sort> Expr<R> eval(Expr<R> t, boolean completion)
    {
        Native.LongPtr v = new Native.LongPtr();
        if (!Native.modelEval(getContext().nCtx(), getNativeObject(),
            t.getNativeObject(), (completion), v))
            throw new ModelEvaluationFailedException();
        else
            return (Expr<R>) Expr.create(getContext(), v.value);
    }
 
    public <R extends Sort> Expr<R> evaluate(Expr<R> t, boolean completion)
    {
        return eval(t, completion);
    }
 
    public int getNumSorts()
    {
        return Native.modelGetNumSorts(getContext().nCtx(), getNativeObject());
    }
 
    public Sort[] getSorts()
    {
 
        int n = getNumSorts();
        Sort[] res = new Sort[n];
        for (int i = 0; i < n; i++)
            res[i] = Sort.create(getContext(),
                    Native.modelGetSort(getContext().nCtx(), getNativeObject(), i));
        return res;
    }
 
    public <R extends Sort>  Expr<R>[] getSortUniverse(R s)
    {
 
        ASTVector nUniv = new ASTVector(getContext(), Native.modelGetSortUniverse(
                getContext().nCtx(), getNativeObject(), s.getNativeObject()));
        return (Expr<R>[]) nUniv.ToExprArray();
    }
 
    @Override
    public String toString() {
        return Native.modelToString(getContext().nCtx(), getNativeObject());
    }
 
    Model(Context ctx, long obj)
    {
        super(ctx, obj);
    }
 
    @Override
    void incRef() {
        Native.modelIncRef(getContext().nCtx(), getNativeObject());
    }
 
    @Override
    void addToReferenceQueue() {
        getContext().getReferenceQueue().storeReference(this, ModelRef::new);
    }
 
    private static class ModelRef extends Z3ReferenceQueue.Reference<Model> {
 
        private ModelRef(Model referent, ReferenceQueue<Z3Object> q) {
            super(referent, q);
        }
 
        @Override
        void decRef(Context ctx, long z3Obj) {
            Native.modelDecRef(ctx.nCtx(), z3Obj);
        }
    }
}