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.logic;
12:
13: import de.uka.ilkd.key.logic.op.IteratorOfMetavariable;
14: import de.uka.ilkd.key.logic.op.ListOfMetavariable;
15: import de.uka.ilkd.key.logic.op.Metavariable;
16: import de.uka.ilkd.key.logic.op.SLListOfMetavariable;
17:
18: /** This class is used to collect all appearing metavariables in a
19: * term. Duplicates are not removed becaues the use of persistent
20: * datastructure and up to now we just have a SetAsList-implementaion
21: * causing to have O(sqr(n)) if it would used.
22: */
23:
24: public class MVCollector extends Visitor {
25: /** collects all found Metavraibles */
26: private ListOfMetavariable mvList;
27:
28: /** creates the metavariable collector */
29: public MVCollector() {
30: mvList = SLListOfMetavariable.EMPTY_LIST;
31: }
32:
33: /** is called by the execPostOrder-method of a term
34: * @param t the Term to checked if it is a Metavariable and if true the
35: * Metavariable is added to the list of found Metavariables
36: */
37: public void visit(Term t) {
38: if (t.op() instanceof Metavariable) {
39: mvList = mvList.prepend((Metavariable) t.op());
40: }
41: }
42:
43: /** @return iterator of the found metavariables */
44: public IteratorOfMetavariable mv() {
45: return mvList.iterator();
46: }
47: }
|