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.proof;
012:
013: import java.util.Map;
014:
015: import de.uka.ilkd.key.logic.BasicLocationDescriptor;
016: import de.uka.ilkd.key.logic.IteratorOfLocationDescriptor;
017: import de.uka.ilkd.key.logic.LocationDescriptor;
018: import de.uka.ilkd.key.logic.SetAsListOfLocationDescriptor;
019: import de.uka.ilkd.key.logic.SetOfLocationDescriptor;
020: import de.uka.ilkd.key.logic.Term;
021: import de.uka.ilkd.key.logic.TermFactory;
022: import de.uka.ilkd.key.logic.op.ArrayOfQuantifiableVariable;
023: import de.uka.ilkd.key.logic.op.Operator;
024:
025: /**
026: * Replaces operators in a term by other operators with the same signature,
027: * or subterms of the term by other terms with the same sort.
028: */
029: public class OpReplacer {
030: private static final TermFactory TF = TermFactory.DEFAULT;
031:
032: private final Map /*Operator -> Operator, Term -> Term*/map;
033:
034: /**
035: * @param map mapping from the operators/terms to be replaced to the ones to
036: * replace them with
037: */
038: public OpReplacer(Map /*Operator -> Operator, Term -> Term*/map) {
039: assert map != null;
040: this .map = map;
041: }
042:
043: /**
044: * Replaces in a term.
045: */
046: public Term replace(Term term) {
047: Term newTerm = (Term) map.get(term);
048: if (newTerm != null) {
049: return newTerm;
050: }
051:
052: Operator newOp = (Operator) map.get(term.op());
053: if (newOp == null) {
054: newOp = term.op();
055: }
056:
057: int arity = term.arity();
058: Term newSubTerms[] = new Term[arity];
059: ArrayOfQuantifiableVariable[] boundVars = new ArrayOfQuantifiableVariable[arity];
060:
061: boolean changedSubTerm = false;
062: for (int i = 0; i < arity; i++) {
063: Term subTerm = term.sub(i);
064: newSubTerms[i] = replace(subTerm);
065: boundVars[i] = term.varsBoundHere(i);
066:
067: if (newSubTerms[i] != subTerm) {
068: changedSubTerm = true;
069: }
070: }
071:
072: Term result = term;
073:
074: if (newOp != term.op() || changedSubTerm) {
075: result = TF.createTerm(newOp, newSubTerms, boundVars, term
076: .javaBlock());
077: }
078:
079: return result;
080: }
081:
082: /**
083: * Replaces in a location descriptor.
084: */
085: public LocationDescriptor replace(LocationDescriptor loc) {
086: if (loc instanceof BasicLocationDescriptor) {
087: BasicLocationDescriptor bloc = (BasicLocationDescriptor) loc;
088: return new BasicLocationDescriptor(replace(bloc
089: .getFormula()), replace(bloc.getLocTerm()));
090: } else {
091: return loc;
092: }
093: }
094:
095: /**
096: * Replaces in a set of location descriptors.
097: */
098: public SetOfLocationDescriptor replace(SetOfLocationDescriptor locs) {
099: SetOfLocationDescriptor result = SetAsListOfLocationDescriptor.EMPTY_SET;
100: IteratorOfLocationDescriptor it = locs.iterator();
101: while (it.hasNext()) {
102: result = result.add(replace(it.next()));
103: }
104: return result;
105: }
106: }
|