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.SetAsListOfQuantifiableVariable;
14: import de.uka.ilkd.key.logic.op.SetOfQuantifiableVariable;
15:
16: /**
17: * Visitor traversing a term and collecting all variables that occur bound.
18: * The visitor implements also a continuation on sequents, traversing all of
19: * the formulas occuring in the sequent.
20: */
21: public class BoundVarsVisitor extends Visitor {
22:
23: private SetOfQuantifiableVariable bdVars = SetAsListOfQuantifiableVariable.EMPTY_SET;
24:
25: /**
26: * creates a Visitor that collects all bound variables for the subterms
27: * of the term it is called from.
28: */
29: public BoundVarsVisitor() {
30: }
31:
32: /**
33: * only called by execPostOrder in Term.
34: */
35: public void visit(Term visited) {
36: for (int i = 0, ar = visited.arity(); i < ar; i++) {
37: for (int j = 0, boundVarsSize = visited.varsBoundHere(i)
38: .size(); j < boundVarsSize; j++) {
39: bdVars = bdVars.add(visited.varsBoundHere(i)
40: .getQuantifiableVariable(j));
41: }
42: }
43: }
44:
45: /**
46: * visits a sequent
47: */
48: public void visit(Sequent visited) {
49: final IteratorOfConstrainedFormula it = visited.iterator();
50: while (it.hasNext()) {
51: visit(it.next().formula());
52: }
53: }
54:
55: /**
56: * returns all the bound variables that have been stored
57: */
58: public SetOfQuantifiableVariable getBoundVariables() {
59: return bdVars;
60: }
61:
62: }
|