de.uka.ilkd.key.prover.impl

Class DepthFirstGoalChooser

java.lang.Object

de.uka.ilkd.key.prover.impl.DefaultGoalChooser

de.uka.ilkd.key.prover.impl.DepthFirstGoalChooser

All Implemented Interfaces:

GoalChooser

Direct Known Subclasses:

SymbolicExecutionGoalChooser

public class DepthFirstGoalChooser
extends DefaultGoalChooser

Helper class for managing a list of goals on which rules are applied. The class provides methods for removing a goal, and for updating the internal data structures after a rule has been applied.

Nested Class Summary

Nested classes/interfaces inherited from class de.uka.ilkd.key.prover.impl.DefaultGoalChooser

DefaultGoalChooser.ProofTreeObserver

Field Summary

Fields inherited from class de.uka.ilkd.key.prover.impl.DefaultGoalChooser

allGoalsSatisfiable, currentSubtreeRoot, goalList, nextGoalCounter, nextGoals, proof, selectedList

Constructor Summary

Constructors

Constructor and Description
DepthFirstGoalChooser()

Method Summary

Modifier and Type	Method and Description
Goal	getNextGoal()
protected ImmutableList<Goal>	insertNewGoals(ImmutableList<Goal> newGoals, ImmutableList<Goal> prevGoalList)
protected void	updateGoalListHelp(Node node, ImmutableList<Goal> newGoals)

Methods inherited from class de.uka.ilkd.key.prover.impl.DefaultGoalChooser

findMinimalSubtree, findMinimalSubtreeBelow, init, isSatisfiableSubtree, removeClosedGoals, removeGoal, rotateList, setupGoals, updateGoalList

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Detail

DepthFirstGoalChooser

public DepthFirstGoalChooser()

Method Detail

getNextGoal

public Goal getNextGoal()

Specified by:

getNextGoal in interface GoalChooser

Overrides:

getNextGoal in class DefaultGoalChooser

Returns:

the next goal a taclet should be applied to

insertNewGoals

protected ImmutableList<Goal> insertNewGoals(ImmutableList<Goal> newGoals,
                                             ImmutableList<Goal> prevGoalList)

Overrides:

insertNewGoals in class DefaultGoalChooser

updateGoalListHelp

protected void updateGoalListHelp(Node node,
                                  ImmutableList<Goal> newGoals)

Overrides:

updateGoalListHelp in class DefaultGoalChooser