| java.lang.Object
 de.uka.ilkd.key.proof.incclosure.BufferSink
| BufferSink | | public class BufferSink implements Sink(Code) | | Sink buffering all constraints that are pushed using "put",
offering the possibility to reset the tree of sinks
|
| BufferSink | | public BufferSink(Sink p_parent)(Code) | | Initial value of the buffer will be the parent's value
|
| 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" |
| isSatisfiable | | public boolean isSatisfiable()(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"
|
| reset | | public void reset()(Code) | | |
|
|