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.IfExThenElse;
15:
16: /**
17: *
18: */
19: class IfExThenElseTerm extends Term {
20:
21: private final ArrayOfTerm subTerm;
22:
23: /** depth of the term */
24: private final int depth;
25:
26: private final ArrayOfQuantifiableVariable exVariables;
27:
28: public IfExThenElseTerm(IfExThenElse op, Term[] subs,
29: ArrayOfQuantifiableVariable exVariables) {
30: super (op, op.sort(subs));
31:
32: this .exVariables = exVariables;
33: this .subTerm = new ArrayOfTerm(subs);
34:
35: int max_depth = -1;
36: for (int i = 0; i < subs.length; i++) {
37: if (subs[i].depth() > max_depth) {
38: max_depth = subs[i].depth();
39: }
40: }
41: depth = max_depth + 1;
42:
43: fillCaches();
44: }
45:
46: /* (non-Javadoc)
47: * @see de.uka.ilkd.key.logic.Term#varsBoundHere(int)
48: */
49: public ArrayOfQuantifiableVariable varsBoundHere(int n) {
50: if (n == 0 || n == 1)
51: return exVariables;
52: return new ArrayOfQuantifiableVariable();
53: }
54:
55: /* (non-Javadoc)
56: * @see de.uka.ilkd.key.logic.Term#arity()
57: */
58: public int arity() {
59: return subTerm.size();
60: }
61:
62: /* (non-Javadoc)
63: * @see de.uka.ilkd.key.logic.Term#depth()
64: */
65: public int depth() {
66: return depth;
67: }
68:
69: /* (non-Javadoc)
70: * @see de.uka.ilkd.key.logic.Term#sub(int)
71: */
72: public Term sub(int nr) {
73: return subTerm.getTerm(nr);
74: }
75: }
|