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.Operator;
15: import de.uka.ilkd.key.logic.op.QuantifiableVariable;
16:
17: /**
18: * A SubstitutionTerm is an object that contains an Operator two subterms.
19: * and one variable
20: * Instances should never be accessed via
21: * this interface, use the interface of the superclass Term and construct
22: * instances only via
23: * a TermFactory instead.
24: */
25: class SubstitutionTerm extends Term {
26:
27: /**
28: * variable to substitute
29: */
30: private final ArrayOfQuantifiableVariable substVar;
31:
32: /**
33: * The two sub terms of the substitution term, where subs[0] is the term
34: * with which the variable is substituted and subs[1] is the term on
35: * which the substitution is applied.
36: * <code> {x/subs[0]}subs[1]</code>
37: */
38: private final ArrayOfTerm subs;
39:
40: /** depth of the term */
41: private final int depth;
42:
43: /** creates a substitution term
44: * @param substVar the Variable to be substituted
45: * @param substTerm the Term that replaces substVar
46: * @param origTerm the Term that is substituted
47: */
48: public SubstitutionTerm(Operator op, QuantifiableVariable substVar,
49: Term[] subs) {
50: super (op, op.sort(subs));
51:
52: this .subs = new ArrayOfTerm(subs);
53: this .substVar = new ArrayOfQuantifiableVariable(
54: new QuantifiableVariable[] { substVar });
55: this .depth = 1 + (subs[0].depth() > subs[1].depth() ? subs[0]
56: .depth() : subs[1].depth());
57:
58: fillCaches();
59: }
60:
61: /**
62: * returns the <code>n-th</code> subterm
63: * @return n-th subterm ( e.g. {x s} t (0:s , 1: t)
64: */
65: public Term sub(int n) {
66: return subs.getTerm(n);
67: }
68:
69: /**
70: * returns the longest path from the root to the leaves
71: * @return depth of the term
72: */
73: public int depth() {
74: return depth;
75: }
76:
77: /**
78: * returns <code>2<code> as arity of a substitution term
79: * @return arity of the substitution term 1 as int
80: */
81: public int arity() {
82: return 2;
83: }
84:
85: /**
86: * the substitution term bound the substituted variable in second
87: * (attention: i.e. <code>n=1<code>) subterm
88: * @return the bound variables of the n-th subterm
89: */
90: public ArrayOfQuantifiableVariable varsBoundHere(int n) {
91: return (n == 0 ? EMPTY_VAR_LIST : substVar);
92: }
93:
94: }
|