public class ApplyStrategy extends Object
Modifier and Type | Class and Description |
---|---|
static class |
ApplyStrategy.AppliedRuleStopCondition
Implementation of
ApplyStrategy.IStopCondition which stops the strategy
after a reached limit of rules or after a timeout in ms. |
static class |
ApplyStrategy.ApplyStrategyInfo
The final result of the strategy application is stored in this container
and returned to the instance that started the strategies.
|
static interface |
ApplyStrategy.IStopCondition
Implementation of this interface are used in
ApplyStrategy to
determine if the strategy should stop or continue. |
private class |
ApplyStrategy.ProofListener |
static class |
ApplyStrategy.SingleRuleApplicationInfo
Instances of this class are used to store if a rule could be applied automatically and if not
to store the reason why no rule applications could be performed.
|
Modifier and Type | Field and Description |
---|---|
private boolean |
autoModeActive
interrupted by the user?
|
private boolean |
cancelled |
protected int |
closedGoals |
private int |
countApplied
number of rules automatically applied
|
private IGoalChooser |
defaultGoalChooser
The default
IGoalChooser to choose goals to which rules are applied if the StrategySettings of the proof provides no customized one. |
(package private) IGoalChooser |
goalChooser |
private int |
maxApplications
the maximum of allowed rule applications
|
static String |
PROCESSING_STRATEGY |
private Proof |
proof
the proof that is worked with
|
private ImmutableList<ProverTaskListener> |
proverTaskObservers
We use an immutable list to store listeners to allow for
addition/removal within listener code
|
private boolean |
stopAtFirstNonCloseableGoal |
(package private) ApplyStrategy.IStopCondition |
stopCondition |
private long |
time |
private long |
timeout
time in ms after which rule application shall be aborted, -1 disables timeout
|
Constructor and Description |
---|
ApplyStrategy(IGoalChooser defaultGoalChooser) |
Modifier and Type | Method and Description |
---|---|
void |
addProverTaskObserver(ProverTaskListener observer) |
private ApplyStrategy.SingleRuleApplicationInfo |
applyAutomaticRule(IGoalChooser goalChooser,
ApplyStrategy.IStopCondition stopCondition,
boolean stopAtFirstNonClosableGoal)
applies rules that are chosen by the active strategy
|
void |
clear()
Used by, e.g.,
InteractiveProver.clear() in order to prevent memory leaking. |
private ApplyStrategy.ApplyStrategyInfo |
doWork(IGoalChooser goalChooser,
ApplyStrategy.IStopCondition stopCondition)
applies rules until this is no longer
possible or the thread is interrupted.
|
private ApplyStrategy.ApplyStrategyInfo |
executeStrategy(ProofTreeListener treeListener) |
private void |
finishStrategy(ApplyStrategy.ApplyStrategyInfo result) |
private void |
fireTaskFinished(TaskFinishedInfo info) |
private void |
fireTaskProgress() |
private void |
fireTaskStarted(int maxSteps) |
private IGoalChooser |
getGoalChooserForProof(Proof proof)
Returns the
IGoalChooser to use for the given Proof . |
boolean |
hasBeenInterrupted()
Returns true iff the last run has been stopped due to a received
InterruptedException . |
private void |
init(Proof newProof,
ImmutableList<Goal> goals,
int maxSteps,
long timeout) |
private boolean |
isAutoModeActive() |
private ProofTreeListener |
prepareStrategy(Proof proof,
ImmutableList<Goal> goals,
int maxSteps,
long timeout) |
void |
removeProverTaskObserver(ProverTaskListener observer) |
private void |
setAutoModeActive(boolean autoModeActive) |
ApplyStrategy.ApplyStrategyInfo |
start(Proof proof,
Goal goal) |
ApplyStrategy.ApplyStrategyInfo |
start(Proof proof,
ImmutableList<Goal> goals) |
ApplyStrategy.ApplyStrategyInfo |
start(Proof proof,
ImmutableList<Goal> goals,
int maxSteps,
long timeout,
boolean stopAtFirstNonCloseableGoal)
This entry point to the proof may provide inconsistent data.
|
ApplyStrategy.ApplyStrategyInfo |
start(Proof proof,
ImmutableList<Goal> goals,
StrategySettings stratSet) |
public static final String PROCESSING_STRATEGY
private Proof proof
private int maxApplications
private IGoalChooser defaultGoalChooser
IGoalChooser
to choose goals to which rules are applied if the StrategySettings
of the proof provides no customized one.private int countApplied
private long time
private boolean autoModeActive
private ImmutableList<ProverTaskListener> proverTaskObservers
private long timeout
private boolean stopAtFirstNonCloseableGoal
protected int closedGoals
private boolean cancelled
ApplyStrategy.IStopCondition stopCondition
IGoalChooser goalChooser
public ApplyStrategy(IGoalChooser defaultGoalChooser)
private ApplyStrategy.SingleRuleApplicationInfo applyAutomaticRule(IGoalChooser goalChooser, ApplyStrategy.IStopCondition stopCondition, boolean stopAtFirstNonClosableGoal)
private ApplyStrategy.ApplyStrategyInfo doWork(IGoalChooser goalChooser, ApplyStrategy.IStopCondition stopCondition)
private void fireTaskStarted(int maxSteps)
private void fireTaskProgress()
private void fireTaskFinished(TaskFinishedInfo info)
private void init(Proof newProof, ImmutableList<Goal> goals, int maxSteps, long timeout)
public ApplyStrategy.ApplyStrategyInfo start(Proof proof, Goal goal)
public ApplyStrategy.ApplyStrategyInfo start(Proof proof, ImmutableList<Goal> goals)
public ApplyStrategy.ApplyStrategyInfo start(Proof proof, ImmutableList<Goal> goals, StrategySettings stratSet)
public ApplyStrategy.ApplyStrategyInfo start(Proof proof, ImmutableList<Goal> goals, int maxSteps, long timeout, boolean stopAtFirstNonCloseableGoal)
private ProofTreeListener prepareStrategy(Proof proof, ImmutableList<Goal> goals, int maxSteps, long timeout)
private ApplyStrategy.ApplyStrategyInfo executeStrategy(ProofTreeListener treeListener)
private void finishStrategy(ApplyStrategy.ApplyStrategyInfo result)
private IGoalChooser getGoalChooserForProof(Proof proof)
IGoalChooser
to use for the given Proof
.
This is the custom one defined in the proof's StrategySettings
or the default one of this defaultGoalChooser
otherwise.proof
- The Proof
for which an IGoalChooser
is required.IGoalChooser
to use.public void addProverTaskObserver(ProverTaskListener observer)
public void removeProverTaskObserver(ProverTaskListener observer)
private boolean isAutoModeActive()
private void setAutoModeActive(boolean autoModeActive)
public void clear()
InteractiveProver.clear()
in order to prevent memory leaking.
When a proof obligation is abandoned all references to the proof must be reset.public boolean hasBeenInterrupted()
InterruptedException
. This exception would have been swallowed by
the system. However, the cancelled flag is set in this case which allows
detection of such a condition.