public final class SemanticsBlastingMacro extends AbstractBlastingMacro
ProofMacro.ProgressBarListener
Constructor and Description |
---|
SemanticsBlastingMacro() |
Modifier and Type | Method and Description |
---|---|
protected java.util.Set<java.lang.String> |
getAllowedPullOut() |
java.lang.String |
getCategory()
Gets the category of this macro.
|
java.lang.String |
getDescription()
Gets the description of this macro.
|
protected RuleFilter |
getEqualityRuleFilter() |
java.lang.String |
getName()
Gets the name of this macro.
|
protected RuleFilter |
getSemanticsRuleFilter() |
addInvariantFormula, applyTo, createStrategy
canApplyTo, doPostProcessing
applyTo, canApplyTo, getMaxSteps, getScriptCommandName, hasParameter, resetParams, setParameter
protected RuleFilter getSemanticsRuleFilter()
getSemanticsRuleFilter
in class AbstractBlastingMacro
protected RuleFilter getEqualityRuleFilter()
getEqualityRuleFilter
in class AbstractBlastingMacro
protected java.util.Set<java.lang.String> getAllowedPullOut()
getAllowedPullOut
in class AbstractBlastingMacro
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 stringCopyright © 2003-2019 The KeY-Project.