Tactic class
A tactic used to solve Goals.
- Implementers
Constructors
- Tactic.fail(Context c)
-
Creates a tactic that always fails.
factory
- Tactic.failIf(Probe p)
-
Creates a tactic that always fails if the given probe returns true.
factory
- Tactic.failIfNotDecided(Context c)
-
Creates a tactic that always fails if the given goal is not trivially
decidable.
factory
-
Tactic.parallelOr(List<
Tactic> tactics) -
Creates a tactic that applies the given tactics in parallel.
factory
- Tactic.skip(Context c)
-
Creates a tactic that just returns the given goal.
factory
Properties
- hashCode → int
-
The hash code for this object.
no setterinherited
- runtimeType → Type
-
A representation of the runtime type of the object.
no setterinherited
Methods
-
andThen(
Tactic other) → Tactic -
Returns a tactic that applies this then
other
to every subgoal. -
apply(
Goal g, {Params? params}) → ApplyResult - Applies this tactic to the given goal.
-
cond(
Tactic other, Probe p) → Tactic -
Returns a tactic that applies this if
p
returns true,other
otherwise. -
getParamDescriptions(
) → ParamDescs - Gets a description of the parameters accepted by this tactic.
-
getParamHelp(
) → String - Gets a description of the parameters accepted by this tactic.
-
noSuchMethod(
Invocation invocation) → dynamic -
Invoked when a nonexistent method or property is accessed.
inherited
-
orElse(
Tactic other) → Tactic -
Returns a tactic that applies this or
other
if this fails. -
parAndThen(
Tactic other) → Tactic -
Returns a tactic that applies this then
other
to every subgoal in parallel. -
repeat(
int max) → Tactic -
Returns a tactic that repeatedly applies this a maximum of
max
times. -
toSolver(
) → Solver - Create a Solver that uses this tactic.
-
toString(
) → String -
A string representation of this object.
inherited
-
tryFor(
Duration duration) → Tactic - Returns a tactic that applies this for the given duration.
-
usingParams(
Params params) → Tactic - Returns a tactic that applies this with the given parameters.
-
when(
Probe p) → Tactic - Returns a tactic that applies this when the given probe returns true.
Operators
-
operator ==(
Object other) → bool -
The equality operator.
inherited