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...
Data Structures | |
class | DecRefQueue |
Public Member Functions | |
ApplyResult | Apply (Goal g, Params p=null) |
Execute the tactic over the goal. | |
Properties | |
string | Help [get] |
A string containing a description of parameters accepted by the tactic. | |
ParamDescrs | ParameterDescriptions [get] |
Retrieves parameter descriptions for Tactics. | |
ApplyResult | this[Goal g] [get] |
Apply the tactic to a goal. | |
Solver | Solver [get] |
Creates a solver that is implemented using the given tactic. |
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.
ApplyResult Apply | ( | Goal | g, |
Params | p = null |
||
) | [inline] |
Execute the tactic over the goal.
Definition at line 60 of file Tactic.cs.
Referenced by Goal.Simplify().
{ Contract.Requires(g != null); Contract.Ensures(Contract.Result<ApplyResult>() != null); Context.CheckContextMatch(g); if (p == null) return new ApplyResult(Context, Native.Z3_tactic_apply(Context.nCtx, NativeObject, g.NativeObject)); else { Context.CheckContextMatch(p); return new ApplyResult(Context, Native.Z3_tactic_apply_ex(Context.nCtx, NativeObject, g.NativeObject, p.NativeObject)); } }
string Help [get] |
ParamDescrs ParameterDescriptions [get] |
Creates a solver that is implemented using the given tactic.
ApplyResult this[Goal g] [get] |