Package com.microsoft.z3

Class Tactic

java.lang.Object

com.microsoft.z3.Z3Object

com.microsoft.z3.Tactic

public class Tactic
extends Z3Object

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.

Method Summary

Modifier and Type	Method	Description
ApplyResult	apply(Goal g)	Execute the tactic over the goal.
ApplyResult	apply(Goal g, Params p)	Execute the tactic over the goal.
String	getHelp()	A string containing a description of parameters accepted by the tactic.
ParamDescrs	getParameterDescriptions()	Retrieves parameter descriptions for Tactics.
Solver	getSolver()	Creates a solver that is implemented using the given tactic.

Methods inherited from class com.microsoft.z3.Z3Object

arrayLength, arrayToNative

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Method Details

getHelp

public String getHelp()

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

getParameterDescriptions

public ParamDescrs getParameterDescriptions()

Retrieves parameter descriptions for Tactics.

Throws:

Z3Exception

apply

public ApplyResult apply(Goal g)

Execute the tactic over the goal.

Throws:

Z3Exception

apply

public ApplyResult apply(Goal g,
 Params p)

Execute the tactic over the goal.

Throws:

Z3Exception

getSolver

public Solver getSolver()

Creates a solver that is implemented using the given tactic.

Throws:

Z3Exception

See Also:

• Context.mkSolver(Tactic)