public abstract class AbstractBlastingMacro extends StrategyProofMacro
Modifier and Type | Class and Description |
---|---|
private class |
AbstractBlastingMacro.SemanticsBlastingStrategy |
ProofMacro.ProgressBarListener
Constructor and Description |
---|
AbstractBlastingMacro() |
Modifier and Type | Method and Description |
---|---|
protected void |
addInvariantFormula(Goal goal) |
ProofMacroFinishedInfo |
applyTo(UserInterfaceControl uic,
Proof proof,
ImmutableList<Goal> goals,
PosInOccurrence posInOcc,
ProverTaskListener listener)
Apply this macro on the given goals.
|
private boolean |
containsSubTypes(Sort s,
java.util.Set<Sort> sorts) |
private java.util.List<SequentFormula> |
createFormulae(Services services,
java.util.Set<Sort> sorts) |
protected Strategy |
createStrategy(Proof proof,
PosInOccurrence posInOcc) |
protected abstract java.util.Set<java.lang.String> |
getAllowedPullOut() |
protected abstract RuleFilter |
getEqualityRuleFilter() |
protected abstract RuleFilter |
getSemanticsRuleFilter() |
canApplyTo, doPostProcessing
applyTo, canApplyTo, getMaxSteps, getScriptCommandName, hasParameter, resetParams, setParameter
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
getCategory, getDescription, getName
protected abstract RuleFilter getSemanticsRuleFilter()
protected abstract RuleFilter getEqualityRuleFilter()
protected abstract java.util.Set<java.lang.String> getAllowedPullOut()
public ProofMacroFinishedInfo applyTo(UserInterfaceControl uic, Proof proof, ImmutableList<Goal> goals, PosInOccurrence posInOcc, ProverTaskListener listener) throws java.lang.InterruptedException
ProofMacro
InterruptedException
.
A ProverTaskListener
can be provided to which the progress will
be reported. If no reports are desired, null
cna be used for
this parameter. If more than one listener is needed, consider combining
them using a single listener object using the composite pattern.applyTo
in interface ProofMacro
applyTo
in class StrategyProofMacro
uic
- the UserInterfaceControl
to useproof
- the current Proof
(not null
)goals
- the goals (not null
)posInOcc
- the position in occurrence (may be null
)listener
- the listener to use for progress reports (may be
null
)java.lang.InterruptedException
- if the application of the macro has been interrupted.protected void addInvariantFormula(Goal goal)
protected Strategy createStrategy(Proof proof, PosInOccurrence posInOcc)
createStrategy
in class StrategyProofMacro
private java.util.List<SequentFormula> createFormulae(Services services, java.util.Set<Sort> sorts)