public class SymbolicExecutionGoalChooser extends DepthFirstGoalChooser
This GoalChooser
is a special implementation of the default
DepthFirstGoalChooser
. The difference is that a rule which
creates a new symbolic execution tree node on a Goal
is only applied
if all other Goal
s will also creates new symbolic execution tree
nodes. This has the advantage that invalid branches may closed before
new symbolic execution tree nodes are created.
The order in which new symbolic execution tree nodes are created is also
managed by this GoalChooser
. The idea is that on each Goal
a new symbolic execution tree node is created before on one Goal
a second one will be created. This has the affect that for instance on all
branches of a branch statement the next statement is evaluated before the first
branch executes the second statement.
A second criteria is the used custom StopCondition
of the current
Proof
. Goal
s on that the next set node is allowed are
preferred to branches on which is not allowed. This is required to make
sure that for instance a step over or step return result is completely
performed on all Goal
s before on one Goal
a further
set node is executed.
SymbolicExecutionGoalChooserBuilder
allGoalsSatisfiable, currentSubtreeRoot, goalList, nextGoalCounter, nextGoals, proof, selectedList
Constructor and Description |
---|
SymbolicExecutionGoalChooser() |
Modifier and Type | Method and Description |
---|---|
Goal |
getNextGoal() |
void |
init(Proof p_proof,
ImmutableList<Goal> p_goals)
Initialise this DefaultGoalChooser for use with a given Proof and a list of goals.
|
void |
removeGoal(Goal p_goal)
Remove p_goal from selectedList (e.g.
|
void |
updateGoalList(Node node,
ImmutableList<Goal> newGoals)
The given node has become an internal node of the proof tree, and the
children of the node are the given goals
|
insertNewGoals, updateGoalListHelp
findMinimalSubtree, findMinimalSubtreeBelow, isSatisfiableSubtree, removeClosedGoals, rotateList, setupGoals
public Goal getNextGoal()
getNextGoal
in interface GoalChooser
getNextGoal
in class DepthFirstGoalChooser
public void init(Proof p_proof, ImmutableList<Goal> p_goals)
init
in interface GoalChooser
init
in class DefaultGoalChooser
p_proof
- *param p_goals the initial list of goalspublic void removeGoal(Goal p_goal)
removeGoal
in interface GoalChooser
removeGoal
in class DefaultGoalChooser
public void updateGoalList(Node node, ImmutableList<Goal> newGoals)
updateGoalList
in interface GoalChooser
updateGoalList
in class DefaultGoalChooser
Copyright © 2003-2019 The KeY-Project.