public class PrepareInfFlowContractPreBranchesMacro extends StrategyProofMacro
The rules that are applied can be set in #ADMITTED_RULENAMES
.
Modifier and Type | Class and Description |
---|---|
protected class |
PrepareInfFlowContractPreBranchesMacro.RemovePostStrategy
This strategy accepts all rule apps for which the rule name starts with a
string in the admitted set and rejects everything else.
|
ProofMacro.ProgressBarListener
Modifier and Type | Field and Description |
---|---|
private static java.lang.String |
AND_RIGHT_RULENAME |
private static java.lang.String |
DOUBLE_IMP_LEFT_RULENAME |
private static java.lang.String |
IMP_LEFT_RULENAME |
private static java.lang.String |
INF_FLOW_RULENAME_PREFIX |
Constructor and Description |
---|
PrepareInfFlowContractPreBranchesMacro() |
Modifier and Type | Method and Description |
---|---|
protected Strategy |
createStrategy(Proof proof,
PosInOccurrence posInOcc) |
java.lang.String |
getCategory()
Gets the category of this macro.
|
java.lang.String |
getDescription()
Gets the description of this macro.
|
java.lang.String |
getName()
Gets the name of this macro.
|
applyTo, canApplyTo, doPostProcessing
applyTo, canApplyTo, getMaxSteps, getScriptCommandName, hasParameter, resetParams, setParameter
private static final java.lang.String INF_FLOW_RULENAME_PREFIX
private static final java.lang.String IMP_LEFT_RULENAME
private static final java.lang.String DOUBLE_IMP_LEFT_RULENAME
private static final java.lang.String AND_RIGHT_RULENAME
public PrepareInfFlowContractPreBranchesMacro()
public java.lang.String getName()
ProofMacro
null
constant stringpublic java.lang.String getCategory()
ProofMacro
null
if no submenu is to be created.null
public java.lang.String getDescription()
ProofMacro
null
constant stringprotected Strategy createStrategy(Proof proof, PosInOccurrence posInOcc)
createStrategy
in class StrategyProofMacro