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 de.uka.ilkd.key.logic.op.ArrayOfQuantifiableVariable;
014: import de.uka.ilkd.key.logic.op.LogicVariable;
015: import de.uka.ilkd.key.logic.op.QuanUpdateOperator;
016: import de.uka.ilkd.key.logic.op.QuantifiableVariable;
017: import de.uka.ilkd.key.util.Debug;
018:
019: /**
020: *
021: */
022: class QuanUpdateTerm extends Term {
023:
024: /**
025: * contains the subterms of the represented term
026: */
027: private final ArrayOfTerm subTerm;
028:
029: /** depth of the term */
030: private final int depth;
031:
032: private final ArrayOfQuantifiableVariable[] quanUpdateVars;
033:
034: /**
035: * creates a UpdateTerm
036: * @param op the UpdateOperator
037: * @param subs an array of Term
038: */
039: QuanUpdateTerm(QuanUpdateOperator op, Term[] subs,
040: ArrayOfQuantifiableVariable[] quanUpdateVars) {
041: super (op, op.sort(subs));
042:
043: this .quanUpdateVars = quanUpdateVars;
044: this .subTerm = new ArrayOfTerm(subs);
045:
046: // move this to <code>QuanUpdateOperator.validTopLevel</code>?
047: Debug.assertTrue(quanUpdateVars.length == op.locationCount());
048: Debug.assertTrue(subs.length == op.arity());
049:
050: int max_depth = -1;
051: for (int i = 0; i < subs.length; i++) {
052: if (subs[i].depth() > max_depth) {
053: max_depth = subs[i].depth();
054: }
055: }
056: depth = max_depth + 1;
057:
058: fillCaches();
059: }
060:
061: public JavaBlock executableJavaBlock() {
062: return sub(arity() - 1).javaBlock();
063: }
064:
065: /** toString */
066: public String toString() {
067: final QuanUpdateOperator op = (QuanUpdateOperator) op();
068: StringBuffer sb = new StringBuffer("{");
069: QuantifiableVariable qvar = null;
070: for (int i = 0; i < op.locationCount(); i++) {
071: if (quanUpdateVars[i].size() > 0)
072: sb.append("\\for ");
073: if (quanUpdateVars[i].size() == 1) {
074: qvar = quanUpdateVars[i].getQuantifiableVariable(0);
075: if (qvar instanceof LogicVariable) {
076: sb.append(((LogicVariable) qvar).sort() + " "
077: + ((LogicVariable) qvar).name());
078: } else {
079: sb.append(qvar);
080: }
081: sb.append("; ");
082: } else {
083: for (int j = 0; j < quanUpdateVars[i].size(); j++) {
084: if (j == 0)
085: sb.append("(");
086: qvar = quanUpdateVars[i].getQuantifiableVariable(j);
087: if (qvar instanceof LogicVariable) {
088: sb.append(((LogicVariable) qvar).sort() + " "
089: + ((LogicVariable) qvar).name());
090: } else {
091: sb.append(qvar);
092: }
093: if (j < quanUpdateVars[i].size() - 1)
094: sb.append("; ");
095: else
096: sb.append(")");
097: }
098: }
099: if (op.guardExists(i)) {
100: sb.append("\\if (");
101: sb.append(sub(op.guardPos(i)));
102: sb.append(") ");
103: }
104: sb.append(op.location(this , i));
105: sb.append(":=");
106: sb.append(op.value(this , i));
107: if (i < op.locationCount() - 1) {
108: sb.append(" || ");
109: }
110: }
111: sb.append("}");
112: sb.append(sub(arity() - 1));
113: return sb.toString();
114: }
115:
116: private ArrayOfQuantifiableVariable[] boundVarsCache = null;
117:
118: /* (non-Javadoc)
119: * @see de.uka.ilkd.key.logic.Term#varsBoundHere(int)
120: */
121: public ArrayOfQuantifiableVariable varsBoundHere(int n) {
122: if (n >= arity() - 1)
123: return new ArrayOfQuantifiableVariable();
124:
125: if (boundVarsCache == null) {
126: boundVarsCache = new ArrayOfQuantifiableVariable[arity() - 1];
127:
128: final QuanUpdateOperator this Op = (QuanUpdateOperator) op();
129: for (int i = 0; i != this Op.locationCount(); ++i) {
130: for (int j = this Op.entryBegin(i), end = this Op
131: .entryEnd(i); j != end; ++j) {
132: boundVarsCache[j] = quanUpdateVars[i];
133: }
134: }
135: }
136:
137: return boundVarsCache[n];
138: }
139:
140: /* (non-Javadoc)
141: * @see de.uka.ilkd.key.logic.Term#arity()
142: */
143: public int arity() {
144: return subTerm.size();
145: }
146:
147: /* (non-Javadoc)
148: * @see de.uka.ilkd.key.logic.Term#depth()
149: */
150: public int depth() {
151: return depth;
152: }
153:
154: /* (non-Javadoc)
155: * @see de.uka.ilkd.key.logic.Term#sub(int)
156: */
157: public Term sub(int nr) {
158: return subTerm.getTerm(nr);
159: }
160: }
|