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.strategy.quantifierHeuristics;
012:
013: import de.uka.ilkd.key.logic.ClashFreeSubst;
014: import de.uka.ilkd.key.logic.IteratorOfTerm;
015: import de.uka.ilkd.key.logic.Term;
016: import de.uka.ilkd.key.logic.TermBuilder;
017: import de.uka.ilkd.key.logic.TermCreationException;
018: import de.uka.ilkd.key.logic.op.CastFunctionSymbol;
019: import de.uka.ilkd.key.logic.op.IteratorOfQuantifiableVariable;
020: import de.uka.ilkd.key.logic.op.MapFromQuantifiableVariableToTerm;
021: import de.uka.ilkd.key.logic.op.QuantifiableVariable;
022: import de.uka.ilkd.key.logic.op.SetOfQuantifiableVariable;
023: import de.uka.ilkd.key.logic.sort.AbstractSort;
024: import de.uka.ilkd.key.logic.sort.Sort;
025:
026: /**
027: * This class decribes a substitution,which store a map(varMap) from quantifiable
028: * variable to a term(instance).
029: */
030: class Substitution {
031:
032: private final TermBuilder tb = TermBuilder.DF;
033:
034: private MapFromQuantifiableVariableToTerm varMap;
035:
036: public Substitution(MapFromQuantifiableVariableToTerm map) {
037: varMap = map;
038: }
039:
040: public MapFromQuantifiableVariableToTerm getVarMap() {
041: return varMap;
042: }
043:
044: public Term getSubstitutedTerm(QuantifiableVariable var) {
045: return varMap.get(var);
046: }
047:
048: public boolean isTotalOn(SetOfQuantifiableVariable vars) {
049: IteratorOfQuantifiableVariable it = vars.iterator();
050: while (it.hasNext()) {
051: if (!varMap.containsKey(it.next()))
052: return false;
053: }
054: return true;
055: }
056:
057: /**
058: * @return true if every instance in the varMap does not contain variable.
059: */
060: public boolean isGround() {
061: final IteratorOfQuantifiableVariable it = varMap.keyIterator();
062: while (it.hasNext()) {
063: if (getSubstitutedTerm(it.next()).freeVars().size() != 0)
064: return false;
065: }
066: return true;
067: }
068:
069: public Term apply(Term t) {
070: assert isGround() : "non-ground substitutions are not yet implemented";
071: final IteratorOfQuantifiableVariable it = varMap.keyIterator();
072: while (it.hasNext()) {
073: final QuantifiableVariable var = it.next();
074: final Sort quantifiedVarSort = var.sort();
075: final CastFunctionSymbol quantifiedVarSortCast = ((AbstractSort) quantifiedVarSort)
076: .getCastSymbol();
077: Term instance = getSubstitutedTerm(var);
078: if (!instance.sort().extendsTrans(quantifiedVarSort))
079: instance = tb.func(quantifiedVarSortCast, instance);
080: t = applySubst(var, instance, t);
081: }
082: return t;
083: }
084:
085: private Term applySubst(QuantifiableVariable var, Term instance,
086: Term t) {
087: final ClashFreeSubst subst = new ClashFreeSubst(var, instance);
088: return subst.apply(t);
089: }
090:
091: /**
092: * Try to apply the substitution to a term, widening by removing casts to
093: * jbyte, jint whenever possible
094: */
095: public Term applyWithoutCasts(Term t) {
096: assert isGround() : "non-ground substitutions are not yet implemented";
097: final IteratorOfQuantifiableVariable it = varMap.keyIterator();
098: while (it.hasNext()) {
099: final QuantifiableVariable var = it.next();
100: Term instance = getSubstitutedTerm(var);
101:
102: try {
103: t = applySubst(var, instance, t);
104: } catch (TermCreationException e) {
105: final Sort quantifiedVarSort = var.sort();
106: if (!instance.sort().extendsTrans(quantifiedVarSort)) {
107: final CastFunctionSymbol quantifiedVarSortCast = ((AbstractSort) quantifiedVarSort)
108: .getCastSymbol();
109: instance = tb.func(quantifiedVarSortCast, instance);
110: t = applySubst(var, instance, t);
111: } else {
112: throw e;
113: }
114: }
115: }
116: return t;
117: }
118:
119: public boolean equals(Object arg0) {
120: if (!(arg0 instanceof Substitution))
121: return false;
122: final Substitution s = (Substitution) arg0;
123: return varMap.equals(s.varMap);
124: }
125:
126: public int hashCode() {
127: return varMap.hashCode();
128: }
129:
130: public String toString() {
131: return "" + varMap;
132: }
133:
134: public boolean termContainsValue(Term term) {
135: IteratorOfTerm it = varMap.valueIterator();
136: while (it.hasNext()) {
137: if (recOccurCheck(it.next(), term))
138: return true;
139: }
140: return false;
141: }
142:
143: /**
144: * check whether term "sub" is in term "term"
145: */
146: private boolean recOccurCheck(Term sub, Term term) {
147: if (sub.equals(term))
148: return true;
149: for (int i = 0; i < term.arity(); i++) {
150: if (recOccurCheck(sub, term.sub(i)))
151: return true;
152: }
153: return false;
154: }
155: }
|