Tactic.java

Go to the documentation of this file.

package com.microsoft.z3;

public class Tactic extends Z3Object
{
    public String getHelp()
    {
        return Native.tacticGetHelp(getContext().nCtx(), getNativeObject());
    }

    public ParamDescrs getParameterDescriptions()
    {
        return new ParamDescrs(getContext(), Native.tacticGetParamDescrs(getContext()
                .nCtx(), getNativeObject()));
    }

    public ApplyResult apply(Goal g)
    {    
        return apply(g, null);
    }

    public ApplyResult apply(Goal g, Params p)
    {
        getContext().checkContextMatch(g);
        if (p == null)
            return new ApplyResult(getContext(), Native.tacticApply(getContext()
                    .nCtx(), getNativeObject(), g.getNativeObject()));
        else
        {
            getContext().checkContextMatch(p);
            return new ApplyResult(getContext(),
                    Native.tacticApplyEx(getContext().nCtx(), getNativeObject(),
                            g.getNativeObject(), p.getNativeObject()));
        }
    }

    public Solver getSolver()
    {
        return getContext().mkSolver(this);
    }

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

    Tactic(Context ctx, String name)
    {
        super(ctx, Native.mkTactic(ctx.nCtx(), name));
    }

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

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