| de.uka.ilkd.key.strategy.feature.instantiator |
|
| Java Source File Name | Type | Comment |
| BackTrackingManager.java | Class | 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. |
| ChoicePoint.java | Interface | Interface encapsulating points during the evaluation of a feature term where
it is either possible to take different branches, or where the feature has to
change the rule application in question (e.g. |
| CPBranch.java | Interface | One branch of a ChoicePoint. |
| ForEachCP.java | Class | Feature representing a ChoicePoint that iterates over the
terms returned by a TermGenerator. |
| OneOfCP.java | Class | |
| SVInstantiationCP.java | Class | Feature representing a ChoicePoint for instantiating a schema
variable of a taclet with the term that is returned by a
ProjectionToTerm. |