public class ApplyStrategy extends AbstractProverCore
Modifier and Type | Class and Description |
---|---|
private class |
ApplyStrategy.ProofListener |
Modifier and Type | Field and Description |
---|---|
private boolean |
autoModeActive
interrupted by the user?
|
private boolean |
cancelled
indicates whether the prover has been interrupted and should stop
|
private int |
closedGoals
the number of (so far) closed goal by the current running strategy
|
private GoalChooser |
defaultGoalChooser
The default
GoalChooser to choose goals to which rules are applied if the StrategySettings of the proof provides no customized one. |
private GoalChooser |
goalChooser
the goal choose picks the next goal to work on
|
private int |
maxApplications
the maximum of allowed rule applications
|
private Proof |
proof
the proof that is worked with
|
private boolean |
stopAtFirstNonClosableGoal
true if the prover should stop as soon as a non closable goal is detected
|
private StopCondition |
stopCondition
a configurable condition indicating that the prover has to stop,
|
private long |
time |
private long |
timeout
time in ms after which rule application shall be aborted, -1 disables timeout
|
countApplied
PROCESSING_STRATEGY
Constructor and Description |
---|
ApplyStrategy(GoalChooser defaultGoalChooser) |
Modifier and Type | Method and Description |
---|---|
private SingleRuleApplicationInfo |
applyAutomaticRule(GoalChooser goalChooser,
StopCondition 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 ApplyStrategyInfo |
doWork(GoalChooser goalChooser,
StopCondition stopCondition)
applies rules until this is no longer
possible or the thread is interrupted.
|
private ApplyStrategyInfo |
executeStrategy(ProofTreeListener treeListener) |
private void |
finishStrategy(ApplyStrategyInfo result) |
private GoalChooser |
getGoalChooserForProof(Proof proof)
Returns the
GoalChooser 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) |
private void |
setAutoModeActive(boolean autoModeActive) |
ApplyStrategyInfo |
start(Proof proof,
Goal goal)
starts a proof search for a given goals using the given strategy settings
instead the ones configures in the proof
|
ApplyStrategyInfo |
start(Proof proof,
ImmutableList<Goal> goals)
starts a proof search for a set of goals using the given strategy settings
instead the ones configures in the proof
|
ApplyStrategyInfo |
start(Proof proof,
ImmutableList<Goal> goals,
int maxSteps,
long timeout,
boolean stopAtFirstNonCloseableGoal)
This entry point to the proof may provide inconsistent data.
|
ApplyStrategyInfo |
start(Proof proof,
ImmutableList<Goal> goals,
StrategySettings stratSet)
starts a proof search for a set of goals using the given strategy settings
instead the ones configures in the proof
|
addProverTaskObserver, fireTaskFinished, fireTaskProgress, fireTaskStarted, removeProverTaskObserver
private Proof proof
private int maxApplications
private GoalChooser defaultGoalChooser
GoalChooser
to choose goals to which rules are applied if the StrategySettings
of the proof provides no customized one.private long time
private boolean autoModeActive
private long timeout
private boolean stopAtFirstNonClosableGoal
private int closedGoals
private boolean cancelled
private StopCondition stopCondition
private GoalChooser goalChooser
public ApplyStrategy(GoalChooser defaultGoalChooser)
private SingleRuleApplicationInfo applyAutomaticRule(GoalChooser goalChooser, StopCondition stopCondition, boolean stopAtFirstNonClosableGoal)
private ApplyStrategyInfo doWork(GoalChooser goalChooser, StopCondition stopCondition)
private void init(Proof newProof, ImmutableList<Goal> goals, int maxSteps, long timeout)
public ApplyStrategyInfo start(Proof proof, Goal goal)
ProverCore
proof
- the Proof instancegoal
- the goal to provepublic ApplyStrategyInfo start(Proof proof, ImmutableList<Goal> goals)
ProverCore
proof
- the Proof instancegoals
- list of goals to provepublic ApplyStrategyInfo start(Proof proof, ImmutableList<Goal> goals, StrategySettings stratSet)
ProverCore
proof
- the Proof instancegoals
- list of goals to provestratSet
- the strategy settings to usepublic ApplyStrategyInfo start(Proof proof, ImmutableList<Goal> goals, int maxSteps, long timeout, boolean stopAtFirstNonCloseableGoal)
ProverCore
proof
- the Proof instancegoals
- list of goals to provemaxSteps
- an int with the maximal number of rule applications to be performedtimeout
- a long with a timeout when tyo stop the proof search at lateststopAtFirstNonCloseableGoal
- true if the prover shall stop at the first
encountered non-closable goalprivate ProofTreeListener prepareStrategy(Proof proof, ImmutableList<Goal> goals, int maxSteps, long timeout)
private ApplyStrategyInfo executeStrategy(ProofTreeListener treeListener)
private void finishStrategy(ApplyStrategyInfo result)
private GoalChooser getGoalChooserForProof(Proof proof)
GoalChooser
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 GoalChooser
is required.GoalChooser
to use.private boolean isAutoModeActive()
private void setAutoModeActive(boolean autoModeActive)
public void clear()
ProverCore
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()
ProverCore
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.