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.*;
014: import de.uka.ilkd.key.logic.sort.Sort;
015: import de.uka.ilkd.key.util.Debug;
016:
017: /**
018: * In contrast to the distinction of formulas and terms as made by most of the
019: * inductive definition of the syntax of a logic, an instance of this class can
020: * stand for a term or a formula. This is done for implementation reasons, as
021: * their structure is quite similar and there are good reasons concerning the
022: * software's design/architecture (for example using same visitors, reduction of
023: * case distinction, unified interfaces etc.). However, they are strictly
024: * separated by their sorts. A formula (and just a formula) must have
025: * the sort {@link Sort#FORMULA}. Terms of a different sort are terms in the
026: * customary logic sense. A term of sort formula is allowed exact there, where a
027: * formuala in logic is allowed to appear, same for terms of different sorts.
028: * Some words about other design decisions:
029: * <ol>
030: * <li> terms are immutable, this means after a term object is created, it
031: * cannot be changed. The advantage is that we can use term sharing and
032: * saving a lot of memory space.
033: * </li>
034: * <li> Term has to be created using the {@link TermFactory} and
035: * <emph>not</emph> by using the constructors itself.
036: * </li>
037: * <li> Term is subclassed, but all subclasses have to be package private, so
038: * that all other classes except {@link TermFactory} know only the class
039: * Term and its interface. Even most classes of the logic package.
040: * </li>
041: * <li> as it is immutable, most (all) attributes should be declared final
042: * </li>
043: * </ol>
044: * Term supports the {@link Visitor} pattern. Two different visit strategies are
045: * currently supported: {@link Term#execPostOrder(Visitor)} and
046: * {@link Term#execPreOrder(Visitor)}.
047: */
048: public abstract class Term implements SVSubstitute {
049:
050: /** empty list of variables */
051: public static final ArrayOfQuantifiableVariable EMPTY_VAR_LIST = new ArrayOfQuantifiableVariable(
052: new QuantifiableVariable[0]);
053:
054: /** the top level operator of this term */
055: private final Operator op;
056:
057: /** caches the sort of this term */
058: private final Sort sort;
059:
060: /** caches the hashcode of the term */
061: private int hashcode;
062:
063: /** true iff this term is rigid */
064: private boolean rigid;
065:
066: /**
067: * caches the free variables of this term
068: */
069: protected SetOfQuantifiableVariable freeVars = SetAsListOfQuantifiableVariable.EMPTY_SET;
070:
071: /** caches the meta variables of this term */
072: protected SetOfMetavariable metaVars = SetAsListOfMetavariable.EMPTY_SET;
073:
074: /**
075: * creates a Term with top operator op
076: * @param op Operator at the top of the termstructure that starts
077: * here.
078: * @param sort the Sort of the term
079: */
080: protected Term(Operator op, Sort sort) {
081: this .op = op;
082: this .sort = sort;
083: }
084:
085: /**
086: * returns the arity of the term
087: * @return arity of the term
088: * */
089: public abstract int arity();
090:
091: protected int calculateHash() {
092: int hashValue = 5;
093: hashValue = hashValue * 17 + op().hashCode();
094: hashValue = hashValue * 17 + sort().hashCode();
095:
096: for (int i = 0, ar = arity(); i < ar; i++) {
097: hashValue = hashValue * 17 + varsBoundHere(i).size();
098: hashValue = hashValue * 17 + sub(i).hashCode();
099: }
100: hashValue = hashValue * 17 + javaBlock().hashCode();
101: if (hashValue == 0)
102: return 1;
103:
104: return hashValue;
105: }
106:
107: /**
108: * checks whether the Term is valid on the top level. If this is
109: * the case this method returns the Term unmodified. Otherwise a
110: * TermCreationException is thrown.
111: * @return this Term if the top level of the Term is valid.
112: */
113: public Term checked() {
114: if (op().validTopLevel(this )) {
115: return this ;
116: } else {
117: throw new TermCreationException(op(), this );
118: }
119: }
120:
121: /**
122: * returns the longest path from the top of the term to one of its leaves
123: * @return an int representing the depth of this term
124: */
125: public abstract int depth();
126:
127: /**
128: * this method has to be called by subclasses after they determined the
129: * arity of the term. The method then can determine the free vars of the
130: * term and put them in a cache.
131: */
132: private void determineFreeVars() {
133: for (int i = 0, ar = arity(); i < ar; i++) {
134: if (sub(i) == null) {
135: Debug.fail("FREE " + op + " " + i);
136: }
137: SetOfQuantifiableVariable subFreeVars = sub(i).freeVars;
138: for (int j = 0, sz = varsBoundHere(i).size(); j < sz; j++) {
139: subFreeVars = subFreeVars.remove(varsBoundHere(i)
140: .getQuantifiableVariable(j));
141: }
142: freeVars = freeVars.union(subFreeVars);
143: }
144: }
145:
146: /**
147: * computes the metavariables that are part of this term
148: */
149: private void determineMetaVars() {
150: for (int i = 0, ar = arity(); i < ar; i++) {
151: if (sub(i) == null) {
152: Debug.fail("FREE " + op + " " + i);
153: }
154: metaVars = metaVars.union(sub(i).metaVars);
155: }
156: }
157:
158: /**
159: * this method has to be called by subclasses after they have
160: * assigned the subterms of the term. The method then can
161: * determine whether the operator and the subterms are rigid and
162: * put this information in a cache.
163: *
164: * the implementation of this method uses the fact that
165: * quantifiable variables are rigid; otherwise, the results are
166: * too pessimistic (but still valid)
167: */
168: private void determineRigidness() {
169: this .rigid = op().isRigid(this );
170: }
171:
172: /**
173: * true if <code>o</code> is syntactical equal to this term
174: * @param o the Object to be compared with this term
175: * @return true iff the given Term has the same values in
176: * operator, sort, arity, varsBoundHere and javaBlock as this object.
177: */
178: public boolean equals(Object o) {
179: if (o == null)
180: return false;
181: if (o == this )
182: return true;
183: if (!(o instanceof Term))
184: return false;
185:
186: final Term t = (Term) o;
187:
188: if (!(t.hashCode() == hashCode() && sort() == t.sort()
189: && arity() == t.arity() && op().equals(t.op()) && javaBlock()
190: .equals(t.javaBlock()))) {
191: return false;
192: }
193:
194: for (int i = 0, ar = arity(); i < ar; i++) {
195: if (varsBoundHere(i).size() != t.varsBoundHere(i).size()) {
196: return false;
197: }
198: for (int j = 0, sz = varsBoundHere(i).size(); j < sz; j++) {
199: if (!varsBoundHere(i).getQuantifiableVariable(j)
200: .equals(
201: t.varsBoundHere(i)
202: .getQuantifiableVariable(j))) {
203: return false;
204: }
205: }
206:
207: if (!sub(i).equals(t.sub(i))) {
208: return false;
209: }
210: }
211:
212: return true;
213: }
214:
215: /**
216: * compares if two terms are equal modulo bound renaming
217: * @return true iff the given Term has the same values in
218: * operator, sort, arity, varsBoundHere and javaBlock as this object
219: * modulo bound renaming
220: */
221: public boolean equalsModRenaming(Object o) {
222: if (o == null || !(o instanceof Term)) {
223: return false;
224: }
225: if (o == this ) {
226: return true;
227: }
228: Term cmp = (Term) o;
229: final Constraint result = Constraint.BOTTOM.unify(this , cmp,
230: null);
231:
232: return result == Constraint.BOTTOM;
233: }
234:
235: /**
236: * the visitor is handed through till the bottom of the tree and
237: * then it walks upwards while at each upstep the method visit of
238: * the visitor is called
239: * @param visitor the Visitor
240: */
241: public void execPostOrder(Visitor visitor) {
242: visitor.subtreeEntered(this );
243: for (int i = 0, ar = arity(); i < ar; i++) {
244: sub(i).execPostOrder(visitor);
245: }
246: visitor.visit(this );
247: visitor.subtreeLeft(this );
248: }
249:
250: /** the visitor walks downwards the tree
251: * while at each downstep the method visit of
252: * the visitor is called
253: * @param visitor the Visitor
254: */
255: public void execPreOrder(Visitor visitor) {
256: visitor.subtreeEntered(this );
257: visitor.visit(this );
258: for (int i = 0, ar = arity(); i < ar; i++) {
259: sub(i).execPreOrder(visitor);
260: }
261: visitor.subtreeLeft(this );
262: }
263:
264: /**
265: * The primary diamond in this formula. Note that the default
266: * implementation is the same as <code>javaBlock()</code> but
267: * the semantics is different. See <code>SimultaneousUpdateTerm</code>.
268: */
269: public JavaBlock executableJavaBlock() {
270: return javaBlock();
271: }
272:
273: /**
274: * fills the cache variables
275: * must be called in the constructors
276: */
277: protected void fillCaches() {
278: determineFreeVars();
279: determineMetaVars();
280: determineRigidness();
281: hashcode = calculateHash();
282: }
283:
284: /**
285: * returns the set of free quantifiable variables occuring in this term
286: * @return the SetOfFree
287: */
288: public SetOfQuantifiableVariable freeVars() {
289: return freeVars;
290: }
291:
292: /**
293: * returns the hashcode of the term
294: * @return the hashcode of the Term.
295: */
296: public int hashCode() {
297: if (hashcode == 0) {
298: hashcode = calculateHash();
299: }
300: return hashcode;
301: }
302:
303: /**
304: * @return true iff all subterms of this term are rigid according
305: * to the value the method "isRigid" returns for them (this does
306: * not imply this term to be rigid itself!)
307: */
308: public boolean hasRigidSubterms() {
309: for (int i = 0, ar = arity(); i < ar; i++) {
310: if (sub(i) == null) {
311: Debug.fail("FREE " + op + " " + i);
312: }
313: if (!sub(i).isRigid())
314: return false;
315: }
316:
317: return true;
318: }
319:
320: /**
321: * retrieves if the evaluation of the term is state independant. It is
322: * guaranteed that if the result is <code>true</code> then the value is
323: * state independant. In case of <code>false</code> no such guarantee is
324: * given i.e. the terms value may be the same in all states or not.
325: * (safe approximation)
326: * @return false if the value of this term may be changed by
327: * modalities (otherwise, however, the result may also be false)
328: */
329: public final boolean isRigid() {
330: return rigid;
331: }
332:
333: /** @return JavaBlock if term has diamond at the top level */
334: public JavaBlock javaBlock() {
335: return JavaBlock.EMPTY_JAVABLOCK;
336: }
337:
338: /**
339: * returns the set of metavariables that are part of this term
340: * (metavariables are thought as placeholder for some gound term, whereas
341: * the variables in <code>freeVars</code> are bound by some quantifier above)
342: * @return the set of metavariables
343: */
344: public SetOfMetavariable metaVars() {
345: return metaVars;
346: }
347:
348: /**
349: * the top operator in "A and B" it is "and", in f(x,y) it is "f"
350: * @return operator at the top
351: */
352: public Operator op() {
353: return op;
354: }
355:
356: /**
357: * returns the sort of the term
358: * @return the sort of the term
359: */
360: public Sort sort() {
361: return sort;
362: }
363:
364: /**
365: * returns the <code>nr</code>-th direct subterm
366: * @param nr the int specifying the <tt>nr</tt>-th direct subterm
367: */
368: public abstract Term sub(int nr);
369:
370: /**
371: * returns subterm at the position specified by the given PosInTerm pos.
372: * @param pos the position of the wanted subterm
373: * @return the subterm that is specified by pos
374: */
375: public Term subAt(PosInTerm pos) {
376: Term sub = this ;
377: for (final IntIterator it = pos.iterator(); it.hasNext();) {
378: sub = sub.sub(it.next());
379: }
380: return sub;
381: }
382:
383: /**
384: * returns the array of variables the top level operator binds at the n-th
385: * sub term
386: * @return the bound variables for the n-th subterm
387: */
388: public abstract ArrayOfQuantifiableVariable varsBoundHere(int n);
389:
390: /**
391: * returns a linearized textual representation of this term
392: */
393: public String toString() {
394: StringBuffer sb = new StringBuffer(op().name().toString());
395: if (arity() == 0)
396: return sb.toString();
397: sb.append("(");
398: for (int i = 0, ar = arity(); i < ar; i++) {
399: for (int j = 0, vbSize = varsBoundHere(i).size(); j < vbSize; j++) {
400: if (j == 0) {
401: sb.append("{");
402: }
403: sb.append(varsBoundHere(i).getQuantifiableVariable(j));
404: if (j != varsBoundHere(i).size() - 1) {
405: sb.append(", ");
406: } else {
407: sb.append("}");
408: }
409: }
410: sb.append(sub(i));
411: if (i < ar - 1) {
412: sb.append(",");
413: }
414: }
415: sb.append(")");
416: return sb.toString();
417: }
418:
419: // =============== For debugging, used in Main (COMPUTE_SPEC_OP-Z) =================
420:
421: public void tree() {
422: System.out.println("==============================");
423: tree(this , 0);
424: }
425:
426: private void tree(Term t, int off) {
427: int i;
428: for (i = 0; i < off; i++)
429: System.out.print(" ");
430: String s = t.op().toString();
431: s = s.substring(s.lastIndexOf(".") + 1, s.length());
432: System.out.println(t + " [" + s + "]");
433: for (i = 0; i < t.arity(); i++)
434: tree(t.sub(i), off + 3);
435: }
436:
437: }
|