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.rule.updatesimplifier;
012:
013: import de.uka.ilkd.key.logic.Term;
014: import de.uka.ilkd.key.logic.TermFactory;
015: import de.uka.ilkd.key.logic.WaryClashFreeSubst;
016: import de.uka.ilkd.key.logic.op.*;
017:
018: /**
019: *
020: */
021: public abstract class GuardSimplifier {
022:
023: private Term condition;
024:
025: private ListOfQuantifiableVariable minimizedVars;
026:
027: public GuardSimplifier(Term condition,
028: ArrayOfQuantifiableVariable arMinimizedVars) {
029: this .condition = condition;
030: this .minimizedVars = toList(arMinimizedVars);
031: }
032:
033: public boolean bindsVariables() {
034: return !getMinimizedVars().isEmpty();
035: }
036:
037: public boolean isValidGuard() {
038: return getCondition().op() == Op.TRUE;
039: }
040:
041: public boolean isUnsatisfiableGuard() {
042: return getCondition().op() == Op.FALSE;
043: }
044:
045: /**
046: * @return the formula that is simplified by <code>this</code>
047: */
048: public Term getCondition() {
049: return condition;
050: }
051:
052: /**
053: * @return variables that are supposed to represent minimum individuals for
054: * which the guard is satisfied
055: */
056: protected ListOfQuantifiableVariable getMinimizedVars() {
057: return minimizedVars;
058: }
059:
060: private boolean isMinimizedVar(Operator op) {
061: if (!(op instanceof QuantifiableVariable))
062: return false;
063: return getMinimizedVars().contains((QuantifiableVariable) op);
064: }
065:
066: /**
067: * Simplify the treated formula. This removes trivial equations (same left
068: * and right term) and employs equations of the shape <tt> x = t </tt>
069: * (where <tt>x</tt> is a minimized variable) to substitute the variable
070: * with the term <tt>t</tt>. This method is supposed to be called in the
071: * end of constructors of subclasses
072: */
073: protected void simplify() {
074: while (!getMinimizedVars().isEmpty()) {
075: final PairOfQuantifiableVariableAndTerm definingPair = findSimpleEquation(getCondition());
076: if (definingPair == null)
077: break;
078: substituteTempl(definingPair.variable, definingPair.term);
079: }
080:
081: this .condition = elimSimpleStuff(getCondition());
082:
083: this .minimizedVars = neededVars(getMinimizedVars());
084: }
085:
086: /**
087: * Method that needs to be implemented by subclasses, this determines which
088: * of the bound/minimized variables are actually needed. The method is
089: * supposed to select certain elements of <code>allVars</code> without
090: * changing their order
091: */
092: private ListOfQuantifiableVariable neededVars(
093: ListOfQuantifiableVariable allVars) {
094: ListOfQuantifiableVariable needed = SLListOfQuantifiableVariable.EMPTY_LIST;
095:
096: ListOfQuantifiableVariable innerVars = allVars;
097: while (!innerVars.isEmpty()) {
098: final QuantifiableVariable var = innerVars.head();
099: innerVars = innerVars.tail();
100: // order is important
101: if (!innerVars.contains(var) && isNeededVarTempl(var))
102: needed = needed.append(var);
103: }
104: return needed;
105: }
106:
107: /**
108: * Template method for deciding whether <code>var</code> is a variable
109: * that is necessary or that can be removed
110: */
111: private boolean isNeededVarTempl(final QuantifiableVariable var) {
112: return getCondition().freeVars().contains(var)
113: || isNeededVar(var);
114: }
115:
116: /**
117: * Supposed to be overridding in subclasses
118: */
119: protected boolean isNeededVar(QuantifiableVariable var) {
120: return false;
121: }
122:
123: /**
124: * Used to implement <code>simplify()</code>, find trivial parts of the
125: * guard and remove them
126: */
127: private Term elimSimpleStuff(Term formula) {
128: final UpdateSimplifierTermFactory utf = UpdateSimplifierTermFactory.DEFAULT;
129: final TermFactory tf = utf.getBasicTermFactory();
130:
131: if (formula.op() == Op.EQUALS) {
132: if (formula.sub(0).equalsModRenaming(formula.sub(1)))
133: return utf.getValidGuard();
134: } else if (formula.op() instanceof Junctor) {
135: final Junctor junc = (Junctor) formula.op();
136: final Term[] subTerms = new Term[formula.arity()];
137: for (int i = 0; i != subTerms.length; ++i)
138: subTerms[i] = elimSimpleStuff(formula.sub(i));
139: if (subTerms.length == 2)
140: return tf.createJunctorTermAndSimplify(junc,
141: subTerms[0], subTerms[1]);
142: return tf.createJunctorTerm(junc, subTerms);
143: }
144:
145: return formula;
146: }
147:
148: /**
149: * Template method to substitute <code>var</code> with
150: * <code>substTerm</code> (called from <code>simplify()</code>)
151: * wherever this is necessary. The hole <code>substitute()</code> can be
152: * filled by subclasses
153: */
154: private void substituteTempl(QuantifiableVariable var,
155: Term substTerm) {
156: this .minimizedVars = getMinimizedVars().removeAll(var);
157:
158: this .condition = subst(var, substTerm, getCondition());
159:
160: substitute(var, substTerm);
161: }
162:
163: protected Term subst(QuantifiableVariable var, Term substTerm,
164: Term termToBeModified) {
165: final WaryClashFreeSubst subst = new WaryClashFreeSubst(var,
166: substTerm);
167: return subst.apply(termToBeModified);
168: }
169:
170: /**
171: * Substitute <code>var</code> with <code>substTerm</code> (called from
172: * <code>doSubstitute()</code>) wherever this is necessary. This can be
173: * overridden by subclasses that need this information
174: */
175: protected void substitute(QuantifiableVariable var, Term substTerm) {
176: }
177:
178: private ListOfQuantifiableVariable toList(
179: ArrayOfQuantifiableVariable ar) {
180: ListOfQuantifiableVariable res = SLListOfQuantifiableVariable.EMPTY_LIST;
181: for (int i = ar.size() - 1; i >= 0; --i)
182: res = res.prepend(ar.getQuantifiableVariable(i));
183: return res;
184: }
185:
186: /**
187: * Recursively search for equations <tt> x = t </tt> (or similar)
188: *
189: * @return the pair <tt> (x, t) </tt> in case of success (for the first
190: * equation found), <code>null</code> otherwise
191: */
192: private PairOfQuantifiableVariableAndTerm findSimpleEquation(
193: Term formula) {
194: if (formula.op() == Op.EQUALS) {
195: final PairOfQuantifiableVariableAndTerm pair = isSimpleEquation(
196: formula, 0);
197: if (pair != null)
198: return pair;
199:
200: return isSimpleEquation(formula, 1);
201: } else if (formula.op() == Op.AND) {
202: final PairOfQuantifiableVariableAndTerm pair = findSimpleEquation(formula
203: .sub(0));
204: if (pair != null)
205: return pair;
206:
207: return findSimpleEquation(formula.sub(1));
208: }
209:
210: return null;
211: }
212:
213: private PairOfQuantifiableVariableAndTerm isSimpleEquation(
214: Term formula, int varLocation) {
215: if (!isMinimizedVar(formula.sub(varLocation).op()))
216: return null;
217:
218: final QuantifiableVariable var = (QuantifiableVariable) formula
219: .sub(varLocation).op();
220: final Term value = formula.sub(1 - varLocation);
221:
222: if (value.freeVars().contains(var)
223: || !value.sort().extendsTrans(var.sort()))
224: return null;
225:
226: return new PairOfQuantifiableVariableAndTerm(var, value);
227: }
228:
229: private static class PairOfQuantifiableVariableAndTerm {
230: public final QuantifiableVariable variable;
231: public final Term term;
232:
233: public PairOfQuantifiableVariableAndTerm(
234: QuantifiableVariable variable, Term term) {
235: this.variable = variable;
236: this.term = term;
237: }
238: }
239:
240: }
|