ApplyResult.java

Go to the documentation of this file.

package com.microsoft.z3;

public class ApplyResult extends Z3Object {
    public int getNumSubgoals()
    {
        return Native.applyResultGetNumSubgoals(getContext().nCtx(),
                getNativeObject());
    }

    public Goal[] getSubgoals()
    {
        int n = getNumSubgoals();
        Goal[] res = new Goal[n];
        for (int i = 0; i < n; i++)
            res[i] = new Goal(getContext(), 
                Native.applyResultGetSubgoal(getContext().nCtx(), getNativeObject(), i));
        return res;
    }

    public Model convertModel(int i, Model m)
    {
        return new Model(getContext(), 
            Native.applyResultConvertModel(getContext().nCtx(), getNativeObject(), i, m.getNativeObject()));
    }

    @Override
    public String toString() {
        return Native.applyResultToString(getContext().nCtx(), getNativeObject());
    }

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

    @Override
    void incRef() {
        Native.applyResultIncRef(getContext().nCtx(), getNativeObject());
    }

    @Override
    void addToReferenceQueue() {
        getContext().getApplyResultDRQ().storeReference(getContext(), this);
    }
}