public class FullInformationFlowAutoPilotMacro extends DoWhileFinallyMacro
ProofMacro.ProgressBarListener
Modifier and Type | Field and Description |
---|---|
private static int |
NUMBER_OF_TRY_STEPS
The number of proof steps that should be run by the
TryCloseMacro
before retracting. |
Constructor and Description |
---|
FullInformationFlowAutoPilotMacro() |
Modifier and Type | Method and Description |
---|---|
boolean |
canApplyTo(Proof proof,
ImmutableList<Goal> goals,
PosInOccurrence posInOcc)
Can this macro be applied on the given goals?
|
protected ProofMacro |
getAltProofMacro()
Gets the alternative proof macro for the else-branch.
|
java.lang.String |
getCategory()
Gets the category of this macro.
|
protected boolean |
getCondition() |
java.lang.String |
getDescription()
Gets the description of this macro.
|
java.lang.String |
getName()
Gets the name of this macro.
|
protected ProofMacro |
getProofMacro()
Gets the proof macro.
|
java.lang.String |
getScriptCommandName()
Gets a unique short name for this macro that can be used in proof
scripts.
|
applyTo
applyTo, canApplyTo, getMaxSteps, hasParameter, resetParams, setParameter
private static final int NUMBER_OF_TRY_STEPS
TryCloseMacro
before retracting. This overrides the strategy setting if set to a value
greater or equal to 0.public java.lang.String getName()
ProofMacro
getName
in interface ProofMacro
getName
in class DoWhileFinallyMacro
null
constant stringpublic java.lang.String getCategory()
ProofMacro
null
if no submenu is to be created.null
public java.lang.String getScriptCommandName()
AbstractProofMacro
null
is returned, the macro cannot be addressed from
within scripts.
By default, proof macros do not support scripts, thus null
is returned.getScriptCommandName
in interface ProofMacro
getScriptCommandName
in class AbstractProofMacro
null
if not supported, or a non-null
constant string as the short namepublic java.lang.String getDescription()
ProofMacro
getDescription
in interface ProofMacro
getDescription
in class DoWhileFinallyMacro
null
constant stringprotected ProofMacro getProofMacro()
DoWhileFinallyMacro
getProofMacro
in class DoWhileFinallyMacro
protected ProofMacro getAltProofMacro()
DoWhileFinallyMacro
getAltProofMacro
in class DoWhileFinallyMacro
protected boolean getCondition()
getCondition
in class DoWhileFinallyMacro
public 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 DoWhileFinallyMacro
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 applied