Z3 |

Public Member Functions
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 27 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 50 of file Tactic.java.

51 {
52 return apply(g, null);
53 }
com.microsoft.z3.Tactic.apply
ApplyResult apply(Goal g)
Definition: Tactic.java:50

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

## ◆ apply() [2/2]

ApplyResult apply | ( | Goal | g,
|  | Params | p
| ) |  |
| inline

Execute the tactic over the goal.

Exceptions

  Z3Exception |

Definition at line 59 of file Tactic.java.

60 {
61 getContext().checkContextMatch(g);
62 if (p == null)
63 return new ApplyResult(getContext(), Native.tacticApply(getContext()
64 .nCtx(), getNativeObject(), g.getNativeObject()));
65 else
66 {
67 getContext().checkContextMatch(p);
68 return new ApplyResult(getContext(),
69 Native.tacticApplyEx(getContext().nCtx(), getNativeObject(),
70 g.getNativeObject(), p.getNativeObject()));
71 }
72 }

Referenced by Tactic.__call__().

## ◆ getHelp()

String getHelp | ( |  | ) |
| inline

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

Definition at line 31 of file Tactic.java.

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

## ◆ getParameterDescriptions()

ParamDescrs getParameterDescriptions | ( |  | ) |
| inline

Retrieves parameter descriptions for Tactics.

Exceptions

  Z3Exception |

Definition at line 40 of file Tactic.java.

41 {
42 return new ParamDescrs(getContext(), Native.tacticGetParamDescrs(getContext()
43 .nCtx(), getNativeObject()));
44 }

## ◆ getSolver()

Solver getSolver | ( |  | ) |
| inline

Creates a solver that is implemented using the given tactic.

See also
  Context::mkSolver(Tactic)

Exceptions

  Z3Exception |

Definition at line 79 of file Tactic.java.

80 {
81 return getContext().mkSolver(this);
82 }
com.microsoft.z3.Context.mkSolver
Solver mkSolver()
Definition: Context.java:3105