de.uka.ilkd.key.strategy.feature.instantiator

Class SVInstantiationCP.CP

java.lang.Object

de.uka.ilkd.key.strategy.feature.instantiator.SVInstantiationCP.CP

All Implemented Interfaces:

ChoicePoint

Enclosing class:

SVInstantiationCP

private class SVInstantiationCP.CP
extends java.lang.Object
implements ChoicePoint

Field Summary

Fields

Modifier and Type	Field and Description
private RuleApp	app
private Goal	goal
private PosInOccurrence	pos

Constructor Summary

Constructors

Modifier	Constructor and Description
private	CP(RuleApp app, PosInOccurrence pos, Goal goal)

Method Summary

Modifier and Type	Method and Description
java.util.Iterator<CPBranch>	getBranches(RuleApp oldApp) Obtain the branches that can be taken at this point.

Methods inherited from class java.lang.Object

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

Field Detail

pos

private final PosInOccurrence pos

app

private final RuleApp app

goal

private final Goal goal

Constructor Detail

CP

private CP(RuleApp app,
           PosInOccurrence pos,
           Goal goal)

Method Detail

getBranches

public java.util.Iterator<CPBranch> getBranches(RuleApp oldApp)

Description copied from interface: ChoicePoint

Obtain the branches that can be taken at this point.

Specified by:

getBranches in interface ChoicePoint

Parameters:

oldApp - the current rule application, which can already have been modified by earlier ChoicePoints

Returns:

an iterator over the branches of the ChoicePoint