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-tactics)
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-tactics)
in the SMT 2.0 front-end.
Definition at line 32 of file Tactic.cs.
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));
A string containing a description of parameters accepted by the tactic.
Definition at line 38 of file Tactic.cs.
Retrieves parameter descriptions for Tactics.
Definition at line 52 of file Tactic.cs.
Apply the tactic to a goal.
Definition at line 79 of file Tactic.cs.