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.*;
14:
15: /**
16: * This class is used to collect all appearing variables that can
17: * represent logic variables in a term. Duplicates are not removed
18: * because the use of persistent datastructure and up to now we just
19: * have a SetAsList-implementation causing to
20: * have O(sqr(n)) if it would used.
21: */
22:
23: public class LVRCollector extends Visitor {
24: /** collects all found variables */
25: private ListOfQuantifiableVariable varList;
26:
27: /** creates the Variable collector */
28: public LVRCollector() {
29: varList = SLListOfQuantifiableVariable.EMPTY_LIST;
30: }
31:
32: /** is called by the execPostOrder-method of a term
33: * @param t the Term to checked if it is a Variable and if true the
34: * Variable is added to the list of found Variables
35: */
36: public void visit(Term t) {
37: if (t.op() instanceof QuantifiableVariable) {
38: varList = varList.prepend((QuantifiableVariable) t.op());
39: } else if (t.op() instanceof Quantifier) {
40: for (int j = 0, ar = ((Quantifier) t.op()).arity(); j < ar; j++) {
41: for (int i = 0, sz = t.varsBoundHere(j).size(); i < sz; i++) {
42: varList = varList.prepend(t.varsBoundHere(j)
43: .getQuantifiableVariable(i));
44: }
45: }
46: }
47: }
48:
49: /** @return iterator of the found Variables */
50: public IteratorOfQuantifiableVariable varIterator() {
51: return varList.iterator();
52: }
53:
54: /** @return true iff term contains the given variable */
55: public boolean contains(QuantifiableVariable var) {
56: return varList.contains(var);
57: }
58:
59: }
|