public class SelfcompositionStateExpansionMacro extends AbstractPropositionalExpansionMacro
ADMITTED_RULES
.ProofMacro.ProgressBarListener
Constructor and Description |
---|
SelfcompositionStateExpansionMacro() |
Modifier and Type | Method and Description |
---|---|
protected boolean |
allowOSS()
Whether this macro includes One Step Simplification.
|
boolean |
canApplyTo(Proof proof,
ImmutableList<Goal> goals,
PosInOccurrence posInOcc)
Can this macro be applied on the given goals?
This method should not make any changes but check if the macro can be
applied or not on the given goals.
|
protected Strategy |
createStrategy(Proof proof,
PosInOccurrence posInOcc) |
protected java.util.Set<java.lang.String> |
getAdmittedRuleNames()
Gets the set of admitted rule names.
|
java.lang.String |
getDescription()
Gets the description of this macro.
|
java.lang.String |
getName()
Gets the name of this macro.
|
protected boolean |
ruleApplicationInContextAllowed(RuleApp ruleApp,
PosInOccurrence pio,
Goal goal)
Checks whether the application of the passed rule is ok in the given
context.
|
asSet, getCategory
applyTo, doPostProcessing
applyTo, canApplyTo, getMaxSteps, getScriptCommandName, hasParameter, resetParams, setParameter
public java.lang.String getName()
ProofMacro
null
constant stringpublic java.lang.String getDescription()
ProofMacro
null
constant stringprotected java.util.Set<java.lang.String> getAdmittedRuleNames()
AbstractPropositionalExpansionMacro
getAdmittedRuleNames
in class AbstractPropositionalExpansionMacro
null
setprotected Strategy createStrategy(Proof proof, PosInOccurrence posInOcc)
createStrategy
in class AbstractPropositionalExpansionMacro
protected boolean ruleApplicationInContextAllowed(RuleApp ruleApp, PosInOccurrence pio, Goal goal)
AbstractPropositionalExpansionMacro
ruleApplicationInContextAllowed
in class AbstractPropositionalExpansionMacro
ruleApp
- rule to be appliedpio
- contextgoal
- contextpublic boolean canApplyTo(Proof proof, ImmutableList<Goal> goals, PosInOccurrence posInOcc)
This compound macro is applicable if and only if the first macro is applicable. If there is no first macro, this is not applicable.
canApplyTo
in interface ProofMacro
canApplyTo
in class StrategyProofMacro
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 boolean allowOSS()
AbstractPropositionalExpansionMacro
allowOSS
in class AbstractPropositionalExpansionMacro
Copyright © 2003-2019 The KeY-Project.