public final class SemanticsBlastingMacro extends AbstractBlastingMacro
Modifier and Type | Class and Description |
---|---|
private class |
SemanticsBlastingMacro.EqualityRuleFilter |
private class |
SemanticsBlastingMacro.SemanticsRuleFilter |
ProofMacro.ProgressBarListener
Modifier and Type | Field and Description |
---|---|
private HashSet<String> |
allowedPullOut |
private SemanticsBlastingMacro.EqualityRuleFilter |
equalityRuleFilter |
private SemanticsBlastingMacro.SemanticsRuleFilter |
semanticsFilter |
Constructor and Description |
---|
SemanticsBlastingMacro() |
Modifier and Type | Method and Description |
---|---|
protected Set<String> |
getAllowedPullOut() |
String |
getCategory()
Gets the category of this macro.
|
String |
getDescription()
Gets the description of this macro.
|
protected RuleFilter |
getEqualityRuleFilter() |
String |
getName()
Gets the name of this macro.
|
protected RuleFilter |
getSemanticsRuleFilter() |
addInvariantFormula, applyTo, createStrategy
canApplyTo, doPostProcessing
applyTo, canApplyTo, getMaxSteps, getScriptCommandName
private final SemanticsBlastingMacro.SemanticsRuleFilter semanticsFilter
private final SemanticsBlastingMacro.EqualityRuleFilter equalityRuleFilter
protected RuleFilter getSemanticsRuleFilter()
getSemanticsRuleFilter
in class AbstractBlastingMacro
protected RuleFilter getEqualityRuleFilter()
getEqualityRuleFilter
in class AbstractBlastingMacro
protected Set<String> getAllowedPullOut()
getAllowedPullOut
in class AbstractBlastingMacro
public String getName()
ProofMacro
null
constant stringpublic String getCategory()
ProofMacro
null
if no submenu is to be created.null
public String getDescription()
ProofMacro
null
constant string