| java.lang.Object
 de.uka.ilkd.key.strategy.feature.instantiator.BackTrackingManager
| BackTrackingManager | | public class BackTrackingManager (Code) | | Manager for the ChoicePoints that can occur during the
evaluation of a feature term, taking care of the different branches offered
by the points, and that is able to systematically explore the resulting
search space and enumerate all resulting rule applications.
ChoicePoints have to register themselves (using method
passChoicePoint) each time they are invoked during evaluation
of the feature term, and are asked by the manager for their branches. The
manager simulates a backtracking behaviour by repeated evaluation of the
feature term.
|
| Method Summary | |
| public boolean | backtrack()
| | public RuleApp | getResultingapp()
| | public void | passChoicePoint(ChoicePoint cp, Object ticket)
Method that has to be invoked by each feature that represents a choice
point, each time the feature is invoked during evaluation of the feature
term
Parameters:
cp - the ChoicePoint in question (which does nothave to be the same object as the feature, and which does nothave to be the same object over different evaluations of thefeature term)
Parameters:
ticket - a unique object (as unique as possible) that has to beprovided by the feature in order to ensure that the samesequence of choice points occurs during the next evaluationrun (after backtracking). | | public void | setup(RuleApp initialApp)
Method that has to be called before a sequence of evaluation runs of a
feature term. |
| backtrack | | public boolean backtrack()(Code) | | In the end of an evaluation run of a feature term, this method has to be
called for checking whether it is possible to backtrack and whether a
further evaluation run is necessary
true iff there are paths left to explore, i.e., ifevaluation should run a further time |
| getResultingapp | | public RuleApp getResultingapp()(Code) | | the resulting rule application when all choice points haveapplied their modifications |
| passChoicePoint | | public void passChoicePoint(ChoicePoint cp, Object ticket)(Code) | | Method that has to be invoked by each feature that represents a choice
point, each time the feature is invoked during evaluation of the feature
term
Parameters:
cp - the ChoicePoint in question (which does nothave to be the same object as the feature, and which does nothave to be the same object over different evaluations of thefeature term)
Parameters:
ticket - a unique object (as unique as possible) that has to beprovided by the feature in order to ensure that the samesequence of choice points occurs during the next evaluationrun (after backtracking). The ticket must notchange between two evaluation runs of the feature term |
| setup | | public void setup(RuleApp initialApp)(Code) | | Method that has to be called before a sequence of evaluation runs of a
feature term.
Parameters:
initialApp - the original rule application in question |
|
|