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 31 of file Tactic.cs.
◆ Apply()
Execute the tactic over the goal.
Definition at line 58 of file Tactic.cs.
60 Debug.Assert(g !=
null);
62 Context.CheckContextMatch(g);
64 return new ApplyResult(Context, Native.Z3_tactic_apply(Context.nCtx, NativeObject, g.NativeObject));
67 Context.CheckContextMatch(p);
68 return new ApplyResult(Context, Native.Z3_tactic_apply_ex(Context.nCtx, NativeObject, g.NativeObject, p.NativeObject));
Referenced by Goal.Simplify().
◆ Help
A string containing a description of parameters accepted by the tactic.
Definition at line 37 of file Tactic.cs.
41 return Native.Z3_tactic_get_help(Context.nCtx, NativeObject);
◆ ParameterDescriptions
Retrieves parameter descriptions for Tactics.
Definition at line 50 of file Tactic.cs.
51 get {
return new ParamDescrs(Context, Native.Z3_tactic_get_param_descrs(Context.nCtx, NativeObject)); }
◆ Solver
◆ this[Goal g]
Apply the tactic to a goal.
Definition at line 76 of file Tactic.cs.
79 Debug.Assert(g !=
null);
Solver MkSolver(Symbol logic=null)
Creates a new (incremental) solver.