| java.lang.Object
 de.uka.ilkd.key.proof.incclosure.Restricter
All known Subclasses: de.uka.ilkd.key.proof.incclosure.BranchRestricter,
| Restricter | | public class Restricter implements Sink(Code) | | Sink removing given metavariables from passing constraints, thus
making variables local
|
| Restricter | | public Restricter(Sink p_parent)(Code) | | PRECONDITION: p_parent != null
|
| addRestriction | | public void addRestriction(Metavariable p_mv)(Code) | | Tell the first restricter (possibly this sink) to remove "p_mv"
from any passing constraint
|
| getResetConstraint | | public Constraint getResetConstraint()(Code) | | a constraint that restores the current state of thissink and its parents if used with "reset" |
| getRestrictions | | public SetOfMetavariable getRestrictions()(Code) | | |
| put | | public void put(Constraint p_c)(Code) | | Add a constraint for which something (a goal or a subtree of
the proof) can be closed
|
| reset | | public void reset(Constraint p_c)(Code) | | Remove all constraints that have been inserted with "put" until
now, replacing them with the only constraint "p_c"
|
|
|