z3/src/api/java/Tactic.java

/**
Copyright (c) 2012-2014 Microsoft Corporation
   
Module Name:

    Tactic.java

Abstract:

Author:

    @author Christoph Wintersteiger (cwinter) 2012-03-15

Notes:
    
**/ 

package com.microsoft.z3;

import java.lang.ref.ReferenceQueue;

/**
 * Tactics are the basic building block for creating custom solvers for specific
 * problem domains. The complete list of tactics may be obtained using
 * {@code Context.NumTactics} and {@code Context.TacticNames}. It may
 * also be obtained using the command {@code (help-tactic)} in the SMT 2.0
 * front-end.
 **/
public class Tactic extends Z3Object {
    /**
     * A string containing a description of parameters accepted by the tactic.
     **/
    public String getHelp()
    {
        return Native.tacticGetHelp(getContext().nCtx(), getNativeObject());
    }

    /**
     * Retrieves parameter descriptions for Tactics.
     * @throws Z3Exception 
     **/
    public ParamDescrs getParameterDescriptions()
    {
        return new ParamDescrs(getContext(), Native.tacticGetParamDescrs(getContext()
                .nCtx(), getNativeObject()));
    }

    /**
     * Execute the tactic over the goal.
     * @throws Z3Exception 
     **/
    public ApplyResult apply(Goal g)
    {    
        return apply(g, null);
    }

    /**
     * Execute the tactic over the goal.
     * @throws Z3Exception 
     **/
    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()));
        }
    }

    /**
     * Creates a solver that is implemented using the given tactic. 
     * @see Context#mkSolver(Tactic)
     * @throws Z3Exception 
     **/
    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));
    }

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

    @Override
    void addToReferenceQueue() {
        //getContext().getTacticDRQ().storeReference(getContext(), this);
        getContext().getReferenceQueue().storeReference(this, TacticRef::new);
    }

    private static class TacticRef extends Z3ReferenceQueue.Reference<Tactic> {

        private TacticRef(Tactic referent, ReferenceQueue<Z3Object> q) {
            super(referent, q);
        }

        @Override
        void decRef(Context ctx, long z3Obj) {
            Native.tacticDecRef(ctx.nCtx(), z3Obj);
        }
    }
}