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.ArrayOfQuantifiableVariable;
14: import de.uka.ilkd.key.logic.op.Metavariable;
15: import de.uka.ilkd.key.logic.op.Operator;
16: import de.uka.ilkd.key.logic.op.QuantifiableVariable;
17:
18: /** An OpTerm is an object that contains an Operator and several subterms. Can be used
19: * to represent e.g., function terms or quantifier terms. Instances should never be
20: * accessed via
21: * this interface, use the interface of the superclass Term and construct instances only via
22: * a TermFactory instead.
23: */
24: class OpTerm extends Term {
25:
26: private final ArrayOfTerm subTerm;
27:
28: /** depth of the term */
29: private final int depth;
30:
31: /** creates an OpTerm with top operator op, some subterms and a sort
32: * @param op Operator at the top of the termstructure that starts
33: * here
34: * @param subTerm an array containing subTerms (an array with length 0 if
35: * there are no more subterms
36: */
37: public OpTerm(Operator op, Term[] subTerm) {
38: super (op, op.sort(subTerm));
39: this .subTerm = new ArrayOfTerm(subTerm);
40: int max_depth = -1;
41: for (int i = 0, sz = subTerm.length; i < sz; i++) {
42: final int subTermDepth = subTerm[i].depth();
43: if (subTermDepth > max_depth) {
44: max_depth = subTermDepth;
45: }
46: }
47:
48: depth = max_depth + 1;
49:
50: if (op instanceof QuantifiableVariable) {
51: freeVars = freeVars.add((QuantifiableVariable) op);
52: } else if (op instanceof Metavariable) {
53: metaVars = metaVars.add((Metavariable) op);
54: }
55:
56: fillCaches();
57: }
58:
59: /** @return arity of the term */
60: public int arity() {
61: return subTerm.size();
62: }
63:
64: /**@return depth of the term */
65: public int depth() {
66: return depth;
67: }
68:
69: /** the nr-th subterm */
70: public Term sub(int nr) {
71: return subTerm.getTerm(nr);
72: }
73:
74: /** @return an empty variable list */
75: public ArrayOfQuantifiableVariable varsBoundHere(int n) {
76: return EMPTY_VAR_LIST;
77: }
78:
79: }
|