Z3 |

Data Structures | Public Member Functions | Properties
Tactic Class Reference

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. More...

Inheritance diagram for Tactic:

## Data Structures
class | DecRefQueue
| DecRefQueue

## Public Member Functions
ApplyResult | Apply (Goal g, Params p=null)
| Execute the tactic over the goal. More...
Public Member Functions inherited from Z3Object
void | Dispose ()
| Disposes of the underlying native Z3 object. More...

## Properties
string | Help`[get]`
| A string containing a description of parameters accepted by the tactic. More...
ParamDescrs | ParameterDescriptions`[get]`
| Retrieves parameter descriptions for Tactics. More...
ApplyResult | this[Goal g]`[get]`
| Apply the tactic to a goal. More...
Solver | Solver`[get]`
| Creates a solver that is implemented using the given tactic. More...

## 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 31 of file Tactic.cs.

## Member Function Documentation

## ◆ Apply()

ApplyResult Apply | ( | Goal | g,
|  | Params | p = `null`
| ) |  |
| inline

Execute the tactic over the goal.

Definition at line 58 of file Tactic.cs.

59 {
60 Debug.Assert(g != null);
61
62 Context.CheckContextMatch(g);
63 if (p == null)
64 return new ApplyResult(Context, Native.Z3_tactic_apply(Context.nCtx, NativeObject, g.NativeObject));
65 else
66 {
67 Context.CheckContextMatch(p);
68 return new ApplyResult(Context, Native.Z3_tactic_apply_ex(Context.nCtx, NativeObject, g.NativeObject, p.NativeObject));
69 }
70 }

Referenced by Goal.Simplify().

## Property Documentation

## ◆ Help

string Help
| get

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

Definition at line 36 of file Tactic.cs.

37 {
38 get
39 {
40
41 return Native.Z3_tactic_get_help(Context.nCtx, NativeObject);
42 }
43 }

## ◆ ParameterDescriptions

ParamDescrs ParameterDescriptions
| get

Retrieves parameter descriptions for Tactics.

Definition at line 49 of file Tactic.cs.

50 {
51 get { return new ParamDescrs(Context, Native.Z3_tactic_get_param_descrs(Context.nCtx, NativeObject)); }
52 }

## ◆ Solver

Solver Solver
| get

Creates a solver that is implemented using the given tactic.

See also
  Context.MkSolver(Tactic)

Definition at line 89 of file Tactic.cs.

90 {
91 get
92 {
93
94 return Context.MkSolver(this);
95 }
96 }
Microsoft.Z3.Context.MkSolver
Solver MkSolver(Symbol logic=null)
Creates a new (incremental) solver.
Definition: Context.cs:3731

## ◆ this[Goal g]

ApplyResult this[Goal g]
| get

Apply the tactic to a goal.

Definition at line 75 of file Tactic.cs.

76 {
77 get
78 {
79 Debug.Assert(g != null);
80
81 return Apply(g);
82 }
83 }
Microsoft.Z3.Tactic.Apply
ApplyResult Apply(Goal g, Params p=null)
Execute the tactic over the goal.
Definition: Tactic.cs:58