public abstract class ExhaustiveProofMacro extends AbstractProofMacro
getProofMacro()
directly, or
--if not directly applicable-- search on the sequent for any applicable
posInOcc and apply it on the first applicable one or --if not applicable
anywhere on the sequent-- do not apply it.ProofMacro.ProgressBarListener
Constructor and Description |
---|
ExhaustiveProofMacro() |
Modifier and Type | Method and Description |
---|---|
ProofMacroFinishedInfo |
applyTo(UserInterfaceControl uic,
Proof proof,
ImmutableList<Goal> goals,
PosInOccurrence posInOcc,
ProverTaskListener listener)
Apply this macro on the given goals.
|
boolean |
canApplyTo(Proof proof,
ImmutableList<Goal> goals,
PosInOccurrence posInOcc)
Can this macro be applied on the given goals?
|
private PosInOccurrence |
getApplicablePosInOcc(Proof proof,
Goal goal,
PosInOccurrence posInOcc,
ProofMacro macro) |
java.lang.String |
getDescription()
Gets the description of this macro.
|
java.lang.String |
getName()
Gets the name of this macro.
|
(package private) abstract ProofMacro |
getProofMacro()
Gets the proof macros.
|
applyTo, canApplyTo, getMaxSteps, getScriptCommandName, hasParameter, resetParams, setParameter
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
getCategory
private PosInOccurrence getApplicablePosInOcc(Proof proof, Goal goal, PosInOccurrence posInOcc, ProofMacro macro)
public java.lang.String getName()
ProofMacro
null
constant stringpublic java.lang.String getDescription()
ProofMacro
null
constant stringpublic boolean canApplyTo(Proof proof, ImmutableList<Goal> goals, PosInOccurrence posInOcc)
ProofMacro
proof
- the current Proof
(not null
)goals
- the goals (not null
)posInOcc
- the position in occurrence (may be null
)true
, if the macro is allowed to be appliedpublic ProofMacroFinishedInfo applyTo(UserInterfaceControl uic, Proof proof, ImmutableList<Goal> goals, PosInOccurrence posInOcc, ProverTaskListener listener) throws java.lang.InterruptedException, java.lang.Exception
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.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.java.lang.Exception
abstract ProofMacro getProofMacro()