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.Metavariable;
015: import de.uka.ilkd.key.logic.op.Operator;
016: import de.uka.ilkd.key.logic.op.QuantifiableVariable;
017:
018: /**
019: * Used for OCL Simplification.
020: * A BoundVarsTerm is an object that contains an Operator and several subterms.
021: * It can also have a number of bound variables for each subterm.
022: * Instances should never be accessed via
023: * this interface, use the interface of the superclass Term and construct instances only via
024: * a TermFactory instead.
025: */
026: class BoundVarsTerm extends Term {
027:
028: /**
029: * @supplierCardinality *
030: * @supplierRole subterm
031: * @link aggregation
032: */
033: private final ArrayOfTerm subTerm;
034:
035: /** variables that are bound in this term*/
036: private final ArrayOfQuantifiableVariable[] boundVars;
037:
038: /** depth of the term */
039: private final int depth;
040:
041: /**
042: * Creates an BoundVarsTerm with top operator op, some subterms,
043: * zero or more bound variables for each subterm, and a sort.
044: * @param op Operator at the top of the termstructure that starts
045: * here.
046: * @param subTerm An array containing subTerms (an array with length 0 if
047: * there are no more subterms).
048: * @param boundVars An array containing the bound variables.
049: */
050: public BoundVarsTerm(Operator op, Term[] subTerm,
051: ArrayOfQuantifiableVariable[] boundVars) {
052: super (op, op.sort(subTerm));
053: this .subTerm = new ArrayOfTerm(subTerm);
054: this .boundVars = boundVars;
055: int max_depth = -1;
056: for (int i = 0; i < subTerm.length; i++) {
057: if (subTerm[i].depth() > max_depth) {
058: max_depth = subTerm[i].depth();
059: }
060: }
061: depth = max_depth + 1;
062: if (op instanceof QuantifiableVariable) {
063: freeVars = freeVars.add((QuantifiableVariable) op);
064: } else if (op instanceof Metavariable) {
065: metaVars = metaVars.add((Metavariable) op);
066: }
067:
068: fillCaches();
069: }
070:
071: /** @return arity of the term */
072: public int arity() {
073: return subTerm.size();
074: }
075:
076: /**@return depth of the term */
077: public int depth() {
078: return depth;
079: }
080:
081: /** the nr-th subterm */
082: public Term sub(int nr) {
083: return subTerm.getTerm(nr);
084: }
085:
086: /**
087: * @return The array of variables bound for subterm n.
088: */
089: public ArrayOfQuantifiableVariable varsBoundHere(int n) {
090: if (n < 0 || n > boundVars.length - 1) {
091: return EMPTY_VAR_LIST;
092: } else {
093: return boundVars[n];
094: }
095: }
096:
097: // WATCHOUT: Woj: This is probably not necessary
098: /**
099: * returns a linearized textual representation of this term
100: */
101: /*
102: public String toString() {
103: StringBuffer sb = new StringBuffer(op().name().toString());
104: if (arity()==0) return sb.toString();
105: sb.append("(");
106: QuantifiableVariable qvar = null;
107: for (int i=0;i<arity();i++) {
108: if(varsBoundHere(i).size()==1){
109: sb.append("\\bind ");
110: qvar = varsBoundHere(i).getQuantifiableVariable(0);
111: if(qvar instanceof LogicVariable)
112: sb.append(((LogicVariable)qvar).sort()+" "+((LogicVariable)qvar).name());
113: else
114: sb.append(qvar);
115: sb.append("; ");
116: }else{
117: for (int j=0; j<varsBoundHere(i).size(); j++) {
118: if (j==0) {
119: sb.append("\\bind(");
120: }
121: qvar = varsBoundHere(i).getQuantifiableVariable(j);
122: if(qvar instanceof LogicVariable)
123: sb.append(((LogicVariable)qvar).sort()+" "+((LogicVariable)qvar).name());
124: else
125: sb.append(qvar);
126: if (j!=varsBoundHere(i).size()-1) {
127: sb.append("; ");
128: } else {
129: sb.append(")");
130: }
131: }
132: }
133: sb.append(sub(i));
134: if (i<arity()-1) {
135: sb.append(",");
136: }
137: }
138: sb.append(")");
139: return sb.toString();
140: }
141: */
142: }
|