public abstract class StrategyProofMacro extends AbstractProofMacro
StrategyProofMacro
, override
#createStrategy(KeYMediator, PosInOccurrence)
.
This class is aware of Position in occurrences and can also be applied to
inner nodes. Both AutomatedRuleApplicationManager
and
Strategy
are changed for the course of the macro but are restored
afterwards using a ProverTaskListener
.ProverTaskListener
,
Strategy
ProofMacro.ProgressBarListener
Constructor and Description |
---|
StrategyProofMacro() |
Modifier and Type | Method and Description |
---|---|
ProofMacroFinishedInfo |
applyTo(UserInterfaceControl uic,
Proof proof,
ImmutableList<Goal> goals,
PosInOccurrence posInOcc,
ProverTaskListener listener)
Apply this macro on the given goals.
|
boolean |
canApplyTo(Proof proof,
ImmutableList<Goal> goals,
PosInOccurrence posInOcc)
Can this macro be applied on the given goals?
|
protected abstract Strategy |
createStrategy(Proof proof,
PosInOccurrence posInOcc) |
protected void |
doPostProcessing(Proof proof)
Subclasses can use this method to do some postprocessing on the
proof-object after the strategy has finished.
|
private static ImmutableList<Goal> |
setDifference(ImmutableList<Goal> goals1,
ImmutableList<Goal> goals2) |
applyTo, canApplyTo, getMaxSteps, getScriptCommandName, hasParameter, resetParams, setParameter
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
getCategory, getDescription, getName
protected abstract Strategy createStrategy(Proof proof, PosInOccurrence posInOcc)
public boolean canApplyTo(Proof proof, ImmutableList<Goal> goals, PosInOccurrence posInOcc)
proof
- the current Proof
(not null
)goals
- the goals (not null
)posInOcc
- the position in occurrence (may be null
)true
, if the macro is allowed to be appliedprotected void doPostProcessing(Proof proof)
proof
- The proof object.public ProofMacroFinishedInfo applyTo(UserInterfaceControl uic, Proof proof, ImmutableList<Goal> goals, PosInOccurrence posInOcc, ProverTaskListener listener) throws java.lang.InterruptedException
ProofMacro
InterruptedException
.
A ProverTaskListener
can be provided to which the progress will
be reported. If no reports are desired, null
cna be used for
this parameter. If more than one listener is needed, consider combining
them using a single listener object using the composite pattern.uic
- the UserInterfaceControl
to useproof
- the current Proof
(not null
)goals
- the goals (not null
)posInOcc
- the position in occurrence (may be null
)listener
- the listener to use for progress reports (may be
null
)java.lang.InterruptedException
- if the application of the macro has been interrupted.private static ImmutableList<Goal> setDifference(ImmutableList<Goal> goals1, ImmutableList<Goal> goals2)