src/api/java/Model.java

Go to the documentation of this file.

package com.microsoft.z3;

import com.microsoft.z3.enumerations.Z3_sort_kind;

public class Model extends Z3Object
{
    public Expr getConstInterp(Expr a) throws Z3Exception
    {
        getContext().checkContextMatch(a);
        return getConstInterp(a.getFuncDecl());
    }

    public Expr getConstInterp(FuncDecl f) throws Z3Exception
    {
        getContext().checkContextMatch(f);
        if (f.getArity() != 0
                || Native.getSortKind(getContext().nCtx(),
                        Native.getRange(getContext().nCtx(), f.getNativeObject())) == Z3_sort_kind.Z3_ARRAY_SORT
                        .toInt())
            throw new Z3Exception(
                    "Non-zero arity functions and arrays have FunctionInterpretations as a model. Use FuncInterp.");

        long n = Native.modelGetConstInterp(getContext().nCtx(), getNativeObject(),
                f.getNativeObject());
        if (n == 0)
            return null;
        else
            return Expr.create(getContext(), n);
    }

    public FuncInterp getFuncInterp(FuncDecl f) throws Z3Exception
    {
        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) ^ true)
                        throw new Z3Exception(
                                "Argument was not an array constant");
                    long fd = Native.getAsArrayFuncDecl(getContext().nCtx(), n);
                    return getFuncInterp(new FuncDecl(getContext(), fd));
                }
            } else
            {
                throw new Z3Exception(
                        "Constant functions do not have a function interpretation; use ConstInterp");
            }
        } else
        {
            long n = Native.modelGetFuncInterp(getContext().nCtx(),
                    getNativeObject(), f.getNativeObject());
            if (n == 0)
                return null;
            else
                return new FuncInterp(getContext(), n);
        }
    }

    public int getNumConsts() throws Z3Exception
    {
        return Native.modelGetNumConsts(getContext().nCtx(), getNativeObject());
    }

    public FuncDecl[] getConstDecls() throws Z3Exception
    {
        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() throws Z3Exception
    {
        return Native.modelGetNumFuncs(getContext().nCtx(), getNativeObject());
    }

    public FuncDecl[] getFuncDecls() throws Z3Exception
    {
        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() throws Z3Exception
    {
        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 Expr eval(Expr t, boolean completion) throws Z3Exception
    {
        Native.LongPtr v = new Native.LongPtr();
        if (Native.modelEval(getContext().nCtx(), getNativeObject(),
                t.getNativeObject(), (completion) ? true : false, v) ^ true)
            throw new ModelEvaluationFailedException();
        else
            return Expr.create(getContext(), v.value);
    }

    public Expr evaluate(Expr t, boolean completion) throws Z3Exception
    {
        return eval(t, completion);
    }

    public int getNumSorts() throws Z3Exception
    {
        return Native.modelGetNumSorts(getContext().nCtx(), getNativeObject());
    }

    public Sort[] getSorts() throws Z3Exception
    {

        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 Expr[] getSortUniverse(Sort s) throws Z3Exception
    {

        ASTVector nUniv = new ASTVector(getContext(), Native.modelGetSortUniverse(
                getContext().nCtx(), getNativeObject(), s.getNativeObject()));
        int n = nUniv.size();
        Expr[] res = new Expr[n];
        for (int i = 0; i < n; i++)
            res[i] = Expr.create(getContext(), nUniv.get(i).getNativeObject());
        return res;
    }

    public String toString()
    {
        try
        {
            return Native.modelToString(getContext().nCtx(), getNativeObject());
        } catch (Z3Exception e)
        {
            return "Z3Exception: " + e.getMessage();
        }
    }

    Model(Context ctx, long obj) throws Z3Exception
    {
        super(ctx, obj);
    }

    void incRef(long o) throws Z3Exception
    {
        getContext().model_DRQ().incAndClear(getContext(), o);
        super.incRef(o);
    }

    void decRef(long o) throws Z3Exception
    {
        getContext().model_DRQ().add(o);
        super.decRef(o);
    }
}