src/api/java/ParamDescrs.java

Go to the documentation of this file.

package com.microsoft.z3;

import com.microsoft.z3.enumerations.Z3_param_kind;

public class ParamDescrs extends Z3Object
{
    public void validate(Params p)
    {

        Native.paramsValidate(getContext().nCtx(), p.getNativeObject(),
                getNativeObject());
    }

    public Z3_param_kind getKind(Symbol name)
    {

        return Z3_param_kind.fromInt(Native.paramDescrsGetKind(
                getContext().nCtx(), getNativeObject(), name.getNativeObject()));
    }

    public Symbol[] getNames()
    {
        int sz = Native.paramDescrsSize(getContext().nCtx(), getNativeObject());
        Symbol[] names = new Symbol[sz];
        for (int i = 0; i < sz; ++i)
        {
            names[i] = Symbol.create(getContext(), Native.paramDescrsGetName(
                    getContext().nCtx(), getNativeObject(), i));
        }
        return names;
    }

    public int size()
    {
        return Native.paramDescrsSize(getContext().nCtx(), getNativeObject());
    }

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

    ParamDescrs(Context ctx, long obj)
    {
        super(ctx, obj);
    }

    void incRef(long o)
    {
        getContext().getParamDescrsDRQ().incAndClear(getContext(), o);
        super.incRef(o);
    }

    void decRef(long o)
    {
        getContext().getParamDescrsDRQ().add(o);
        super.decRef(o);
    }
}