| de.uka.ilkd.key.proof.incclosure.Sink
All known Subclasses: de.uka.ilkd.key.proof.incclosure.Restricter, de.uka.ilkd.key.proof.incclosure.BufferSink,
| Sink | | public interface Sink (Code) | | Interface for the closure constraint consuming classes
|
| addRestriction | | void addRestriction(Metavariable p_mv)(Code) | | Tell the first restricter (possibly this sink) to remove "p_mv"
from any passing constraint
|
| getResetConstraint | | Constraint getResetConstraint()(Code) | | a constraint that restores the current state of thissink and its parents if used with "reset" |
| put | | void put(Constraint p_c)(Code) | | Add a constraint for which something (a goal or a subtree of
the proof) can be closed
the sink with least distance to the root whose buffercontains the bottom constraint, i.e. which is the root of acompletely closed subtree; null if no such sink exists |
| reset | | 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"
|
|
|