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:
16: /**
17: * Interface for the closure constraint consuming classes
18: */
19: public interface Sink {
20:
21: /**
22: * Add a constraint for which something (a goal or a subtree of
23: * the proof) can be closed
24: * @return the sink with least distance to the root whose buffer
25: * contains the bottom constraint, i.e. which is the root of a
26: * completely closed subtree; null if no such sink exists
27: */
28: void put(Constraint p_c);
29:
30: /**
31: * Tell the first restricter (possibly this sink) to remove "p_mv"
32: * from any passing constraint
33: */
34: void addRestriction(Metavariable p_mv);
35:
36: /**
37: * @return a constraint that restores the current state of this
38: * sink and its parents if used with "reset"
39: */
40: Constraint getResetConstraint();
41:
42: /**
43: * Remove all constraints that have been inserted with "put" until
44: * now, replacing them with the only constraint "p_c"
45: */
46: void reset(Constraint p_c);
47:
48: }
|