Tactic Class Reference

Inheritance diagram for Tactic:

Public Member Functions
String	getHelp ()
ParamDescrs	getParameterDescriptions ()
ApplyResult	apply (Goal g)
ApplyResult	apply (Goal g, Params p)
Solver	getSolver ()

Additional Inherited Members
Static Public Member Functions inherited from Z3Object
static long[]	arrayToNative (Z3Object[] a)
static int	arrayLength (Z3Object[] a)

Detailed Description

Tactics are the basic building block for creating custom solvers for specific problem domains. The complete list of tactics may be obtained using

Context.NumTactics 

and

Context.TacticNames 

. It may also be obtained using the command

(help-tactic) 

in the SMT 2.0 front-end.

Definition at line 29 of file Tactic.java.

Member Function Documentation

apply() [1/2]

ApplyResult apply ( Goal  g )

inline

Execute the tactic over the goal.

Exceptions

Z3Exception

Definition at line 52 of file Tactic.java.

    {    
        return apply(g, null);
    }

Referenced by Tactic.__call__(), and Goal.simplify().

apply() [2/2]

ApplyResult apply ( Goal  g, Params  p  )

inline

Execute the tactic over the goal.

Exceptions

Z3Exception

Definition at line 61 of file Tactic.java.

    {
        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()));
        }
    }

Referenced by Tactic.__call__().

getHelp()

String getHelp ( )

inline

A string containing a description of parameters accepted by the tactic.

Definition at line 33 of file Tactic.java.

    {
        return Native.tacticGetHelp(getContext().nCtx(), getNativeObject());
    }

getParameterDescriptions()

ParamDescrs getParameterDescriptions ( )

inline

Retrieves parameter descriptions for Tactics.

Exceptions

Z3Exception

Definition at line 42 of file Tactic.java.

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

getSolver()

Solver getSolver ( )

inline

Creates a solver that is implemented using the given tactic.

See also

Context::mkSolver(Tactic)

Exceptions

Z3Exception

Definition at line 81 of file Tactic.java.

    {
        return getContext().mkSolver(this);
    }