public class SelfcompositionStateExpansionMacro extends AbstractPropositionalExpansionMacro
ADMITTED_RULES
.Modifier and Type | Class and Description |
---|---|
private class |
SelfcompositionStateExpansionMacro.SelfCompExpansionStrategy
This strategy accepts all rule apps for which the rule name is in the
admitted set or has INF_FLOW_UNFOLD_PREFIX as a prefix and rejects everything else.
|
ProofMacro.ProgressBarListener
Modifier and Type | Field and Description |
---|---|
private static java.lang.String[] |
ADMITTED_RULES |
private static java.util.Set<java.lang.String> |
ADMITTED_RULES_SET |
private static java.lang.String |
INF_FLOW_UNFOLD_PREFIX |
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?
|
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
private static final java.lang.String[] ADMITTED_RULES
private static final java.lang.String INF_FLOW_UNFOLD_PREFIX
private static final java.util.Set<java.lang.String> ADMITTED_RULES_SET
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