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.
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().
◆ Help
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
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
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
95 }
96 }
Solver MkSolver(Symbol logic=null)
Creates a new (incremental) solver.
◆ this[Goal g]
Apply the tactic to a goal.
Definition at line 75 of file Tactic.cs.
76 {
77 get
78 {
79 Debug.Assert(g != null);
80
82 }
83 }
ApplyResult Apply(Goal g, Params p=null)
Execute the tactic over the goal.