01: // This file is part of KeY - Integrated Deductive Software Design
02: // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
03: // Universitaet Koblenz-Landau, Germany
04: // Chalmers University of Technology, Sweden
05: //
06: // The KeY system is protected by the GNU General Public License.
07: // See LICENSE.TXT for details.
08: //
09: //
10:
11: package de.uka.ilkd.key.proof.incclosure;
12:
13: import de.uka.ilkd.key.logic.Constraint;
14: import de.uka.ilkd.key.logic.op.Metavariable;
15: import de.uka.ilkd.key.logic.op.SetAsListOfMetavariable;
16: import de.uka.ilkd.key.logic.op.SetOfMetavariable;
17:
18: /**
19: * Sink removing given metavariables from passing constraints, thus
20: * making variables local
21: */
22: public class Restricter implements Sink {
23:
24: /**
25: * Variables to remove from passing constraints
26: */
27: private SetOfMetavariable removedVariables = SetAsListOfMetavariable.EMPTY_SET;
28:
29: /**
30: * Parent sink within the tree of sinks
31: */
32: private Sink parent;
33:
34: /**
35: * PRECONDITION: p_parent != null
36: */
37: public Restricter(Sink p_parent) {
38: parent = p_parent;
39: }
40:
41: /**
42: * Add a constraint for which something (a goal or a subtree of
43: * the proof) can be closed
44: */
45: public void put(Constraint p_c) {
46: if (p_c.isSatisfiable())
47: parent.put(p_c.removeVariables(removedVariables));
48: }
49:
50: /**
51: * Tell the first restricter (possibly this sink) to remove "p_mv"
52: * from any passing constraint
53: */
54: public void addRestriction(Metavariable p_mv) {
55: removedVariables = removedVariables.add(p_mv);
56: }
57:
58: public SetOfMetavariable getRestrictions() {
59: return removedVariables;
60: }
61:
62: /**
63: * @return a constraint that restores the current state of this
64: * sink and its parents if used with "reset"
65: */
66: public Constraint getResetConstraint() {
67: return parent.getResetConstraint();
68: }
69:
70: /**
71: * Remove all constraints that have been inserted with "put" until
72: * now, replacing them with the only constraint "p_c"
73: */
74: public void reset(Constraint p_c) {
75: // The set of removed variables is currently not resetted
76: parent.reset(p_c);
77: }
78:
79: protected Sink getParent() {
80: return parent;
81: }
82:
83: }
|