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 String[] |
ADMITTED_RULES |
private static Set<String> |
ADMITTED_RULES_SET |
private static 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 Set<String> |
getAdmittedRuleNames()
Gets the set of admitted rule names.
|
String |
getDescription()
Gets the description of this macro.
|
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
private static final String[] ADMITTED_RULES
private static final String INF_FLOW_UNFOLD_PREFIX
public String getName()
ProofMacro
null
constant stringpublic String getDescription()
ProofMacro
null
constant stringprotected Set<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