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 java.util.HashSet<java.lang.String> |
allowedPullOut |
private SemanticsBlastingMacro.EqualityRuleFilter |
equalityRuleFilter |
private SemanticsBlastingMacro.SemanticsRuleFilter |
semanticsFilter |
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
private final SemanticsBlastingMacro.SemanticsRuleFilter semanticsFilter
private final SemanticsBlastingMacro.EqualityRuleFilter equalityRuleFilter
private final java.util.HashSet<java.lang.String> allowedPullOut
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 string