001: // This file is part of KeY - Integrated Deductive Software Design
002: // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
003: // Universitaet Koblenz-Landau, Germany
004: // Chalmers University of Technology, Sweden
005: //
006: // The KeY system is protected by the GNU General Public License.
007: // See LICENSE.TXT for details.
008: //
009: //
010:
011: package de.uka.ilkd.key.logic;
012:
013: import java.util.HashMap;
014: import java.util.Iterator;
015:
016: import de.uka.ilkd.key.logic.ldt.AbstractIntegerLDT;
017: import de.uka.ilkd.key.logic.op.*;
018:
019: /**
020: * This class is used to collect all appearing metavariables and logic
021: * variables in a term, together with their maximum term depth. The
022: * maximum depth of the term itself is also determined
023: */
024:
025: public class DepthCollector extends Visitor {
026:
027: /**
028: * Special depths for some operators (used to make numbers and
029: * signs flat)
030: *
031: * Keys: <code>Operator</code>
032: *
033: * Values: <code>Integer</code>
034: */
035: // private HashMap symbolsDepths = new HashMap ();
036: /**
037: * Map of the current maximum depths of variables
038: *
039: * Keys: <code>Operator</code>
040: *
041: * Values: <code>Integer</code>
042: */
043: private HashMap varDepths = new HashMap();
044:
045: /**
046: * Current maximum depth of the term
047: */
048: private int termDepth = 0;
049:
050: /**
051: * Depth of the current position within the term
052: */
053: private int curDepth = 0;
054:
055: /**
056: * If this is set to a value not zero, we treat the current
057: * subterm as flat
058: */
059: private int flat = 0;
060:
061: public DepthCollector() {
062:
063: }
064:
065: /**
066: * is called by the execPostOrder-method of a term
067: */
068: public void visit(Term t) {
069: Operator op = t.op();
070:
071: if (op instanceof Metavariable
072: || op instanceof QuantifiableVariable) {
073: Integer oldDepth = (Integer) varDepths.get(op);
074:
075: if (oldDepth == null || oldDepth.intValue() < curDepth)
076: varDepths.put(op, new Integer(curDepth));
077: }
078: }
079:
080: /**
081: * We current regard each term with a top-level operator within
082: * this set to be flat (this should be better established by
083: * inserting the symbols used for numbers and characters into the
084: * hashmap above)
085: */
086: private boolean isFlat(Operator p_op) {
087: return p_op.name().equals(AbstractIntegerLDT.NUMBERS_NAME)
088: || p_op.name().equals(AbstractIntegerLDT.CHAR_ID_NAME);
089: }
090:
091: /**
092: * this method is called in execPreOrder and execPostOrder in class Term
093: * when entering the subtree rooted in the term subtreeRoot.
094: * when the visitor behaviour depends on informations bound to subtrees.
095: * @param subtreeRoot root of the subtree which the visitor enters.
096: */
097: public void subtreeEntered(Term subtreeRoot) {
098: if (flat == 0) {
099: ++curDepth;
100: if (curDepth > termDepth)
101: termDepth = curDepth;
102: }
103:
104: if (isFlat(subtreeRoot.op()))
105: // We treat numbers as flat structures: THIS ONLY WORKS IF
106: // THE NUMBER TERM DOES NOT CONTAIN VARIABLES
107: ++flat;
108: }
109:
110: /**
111: * this method is called in execPreOrder and execPostOrder in class Term
112: * when leaving the subtree rooted in the term subtreeRoot.
113: * when the visitor behaviour depends on informations bound to subtrees.
114: * @param subtreeRoot root of the subtree which the visitor leaves.
115: */
116: public void subtreeLeft(Term subtreeRoot) {
117: if (isFlat(subtreeRoot.op()))
118: // We treat numbers as flat structures: THIS ONLY WORKS IF
119: // THE NUMBER TERM DOES NOT CONTAIN VARIABLES
120: --flat;
121:
122: if (flat == 0)
123: --curDepth;
124: }
125:
126: /**
127: * @return the maximum depth of a leaf of the term visited
128: */
129: public int getMaxDepth() {
130: return termDepth;
131: }
132:
133: /**
134: * @return the maximum depth of an occurrence of
135: * <code>p_var</code>, if this variable has been found, or
136: * <code>-1</code>
137: */
138: public int getMaxDepth(Operator p_var) {
139: Integer depth = (Integer) varDepths.get(p_var);
140: return depth == null ? -1 : depth.intValue();
141: }
142:
143: /**
144: * @return an iterator iterating the found variables
145: */
146: public IteratorOfOperator getVariables() {
147: return new OperatorIterator(varDepths.keySet().iterator());
148: }
149:
150: private static class OperatorIterator implements IteratorOfOperator {
151:
152: private Iterator it;
153:
154: private OperatorIterator(Iterator p_it) {
155: it = p_it;
156: }
157:
158: public boolean hasNext() {
159: return it.hasNext();
160: }
161:
162: public Operator next() {
163: return (Operator) it.next();
164: }
165:
166: }
167:
168: }
|