public abstract class AbstractPropositionalExpansionMacro extends StrategyProofMacro
getAdmittedRuleNames()
.
This is very helpful to perform many "andLeft", "impRight" or even "andRight"
steps at a time.Modifier and Type | Class and Description |
---|---|
private class |
AbstractPropositionalExpansionMacro.PropExpansionStrategy
This strategy accepts all rule apps for which the rule name is in the
admitted set and rejects everything else.
|
ProofMacro.ProgressBarListener
Constructor and Description |
---|
AbstractPropositionalExpansionMacro() |
Modifier and Type | Method and Description |
---|---|
protected abstract boolean |
allowOSS()
Whether this macro includes One Step Simplification.
|
protected static java.util.Set<java.lang.String> |
asSet(java.lang.String... strings) |
protected Strategy |
createStrategy(Proof proof,
PosInOccurrence posInOcc) |
protected abstract java.util.Set<java.lang.String> |
getAdmittedRuleNames()
Gets the set of admitted rule names.
|
java.lang.String |
getCategory()
Gets the category of this macro.
|
protected boolean |
ruleApplicationInContextAllowed(RuleApp ruleApp,
PosInOccurrence pio,
Goal goal)
Checks whether the application of the passed rule is ok in the given
context.
|
applyTo, canApplyTo, doPostProcessing
applyTo, canApplyTo, getMaxSteps, getScriptCommandName, hasParameter, resetParams, setParameter
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
getDescription, getName
protected static java.util.Set<java.lang.String> asSet(java.lang.String... strings)
public java.lang.String getCategory()
ProofMacro
null
if no submenu is to be created.null
protected abstract java.util.Set<java.lang.String> getAdmittedRuleNames()
null
setprotected abstract boolean allowOSS()
protected Strategy createStrategy(Proof proof, PosInOccurrence posInOcc)
createStrategy
in class StrategyProofMacro
protected boolean ruleApplicationInContextAllowed(RuleApp ruleApp, PosInOccurrence pio, Goal goal)
ruleApp
- rule to be appliedpio
- contextgoal
- context