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...
|
class | DecRefQueue |
| DecRefQueue
|
|
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 32 of file Tactic.cs.
◆ Apply()
Execute the tactic over the goal.
Definition at line 60 of file Tactic.cs.
Referenced by Goal.Simplify().
62 Contract.Requires(g != null);
63 Contract.Ensures(Contract.Result<ApplyResult>() != null);
65 Context.CheckContextMatch(g);
67 return new ApplyResult(Context, Native.Z3_tactic_apply(Context.nCtx, NativeObject, g.NativeObject));
70 Context.CheckContextMatch(p);
71 return new ApplyResult(Context, Native.Z3_tactic_apply_ex(Context.nCtx, NativeObject, g.NativeObject, p.NativeObject));
◆ Help
A string containing a description of parameters accepted by the tactic.
Definition at line 38 of file Tactic.cs.
41 Contract.Ensures(Contract.Result<
string>() != null);
43 return Native.Z3_tactic_get_help(Context.nCtx, NativeObject);
◆ ParameterDescriptions
Retrieves parameter descriptions for Tactics.
Definition at line 52 of file Tactic.cs.
53 get {
return new ParamDescrs(Context, Native.Z3_tactic_get_param_descrs(Context.nCtx, NativeObject)); }
◆ Solver
Creates a solver that is implemented using the given tactic.
- See also
- Context.MkSolver(Tactic)
Definition at line 94 of file Tactic.cs.
97 Contract.Ensures(Contract.Result<
Solver>() != null);
Solver Solver
Creates a solver that is implemented using the given tactic.
Solver MkSolver(Symbol logic=null)
Creates a new (incremental) solver.
◆ this[Goal g]
Apply the tactic to a goal.
Definition at line 79 of file Tactic.cs.
82 Contract.Requires(g != null);
83 Contract.Ensures(Contract.Result<ApplyResult>() != null);
ApplyResult Apply(Goal g, Params p=null)
Execute the tactic over the goal.