public class UpdateSimplificationMacro extends AbstractPropositionalExpansionMacro
ProofMacro.ProgressBarListener
Modifier and Type | Field and Description |
---|---|
private static java.lang.String[] |
ADMITTED_RULE_NAMES |
private static java.util.Set<java.lang.String> |
ADMITTED_RULE_NAMES_AS_SET |
static java.lang.String |
UPDATE_SIMPLIFICATION_ONLY |
Constructor and Description |
---|
UpdateSimplificationMacro() |
Modifier and Type | Method and Description |
---|---|
protected boolean |
allowOSS()
Whether this macro includes One Step Simplification.
|
protected java.util.Set<java.lang.String> |
getAdmittedRuleNames()
Gets the set of admitted rule names.
|
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.
|
java.lang.String |
getScriptCommandName()
Gets a unique short name for this macro that can be used in proof
scripts.
|
asSet, createStrategy, ruleApplicationInContextAllowed
applyTo, canApplyTo, doPostProcessing
applyTo, canApplyTo, getMaxSteps, hasParameter, resetParams, setParameter
public static final java.lang.String UPDATE_SIMPLIFICATION_ONLY
private static final java.lang.String[] ADMITTED_RULE_NAMES
private static final java.util.Set<java.lang.String> ADMITTED_RULE_NAMES_AS_SET
public java.lang.String getName()
ProofMacro
null
constant stringpublic java.lang.String getCategory()
ProofMacro
null
if no submenu is to be created.getCategory
in interface ProofMacro
getCategory
in class AbstractPropositionalExpansionMacro
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
null
constant stringprotected java.util.Set<java.lang.String> getAdmittedRuleNames()
AbstractPropositionalExpansionMacro
getAdmittedRuleNames
in class AbstractPropositionalExpansionMacro
null
setprotected boolean allowOSS()
AbstractPropositionalExpansionMacro
allowOSS
in class AbstractPropositionalExpansionMacro