| java.lang.Object
 de.uka.ilkd.key.proof.incclosure.Restricter
de.uka.ilkd.key.proof.incclosure.BranchRestricter
| BranchRestricter | | public class BranchRestricter extends Restricter (Code) | | Sink removing given metavariables from passing constraints, thus
making variables local
This derivative does also detect subtrees which are completely
closed
|
| pathConstraint | | Constraint pathConstraint(Code) | | Constraint holding the intersection of all branch constraints
(constraints held by the branch sinks) above and at this
restricter's node
this is undefined if node == null
|
| BranchRestricter | | public BranchRestricter(Sink p_parent)(Code) | | PRECONDITION: p_parent != null
|
| getPathConstraint | | public Constraint getPathConstraint()(Code) | | Constraint holding the intersection of all branchconstraints (constraints held by the branch sinks) above and atthis restricter's node |
| 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
|
| putPathConstraint | | protected void putPathConstraint(Constraint p_c)(Code) | | Intersect the "pathConstraint"-attribute with p_c, propagate
this change downwards
|
| 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"
|
| resetPathConstraint | | protected void resetPathConstraint()(Code) | | Set the "pathConstraint"-attribute to the intersection of all
branch constraints (constraints held by the branch sinks) above
and at this restricter's node, propagate this change downwards
PRECONDITION: the "pathConstraint"-attributes above this node
are up to date
|
| resetPathConstraint | | protected void resetPathConstraint(Constraint p_c)(Code) | | Set the "pathConstraint"-attribute to the intersection of p_c
with the local branch constraint, propagate this change
downwards
|
|
|