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.PosInOccurrence;
014: import de.uka.ilkd.key.logic.Term;
015: import de.uka.ilkd.key.logic.op.IteratorOfQuantifiableVariable;
016: import de.uka.ilkd.key.logic.op.Op;
017: import de.uka.ilkd.key.logic.op.Operator;
018: import de.uka.ilkd.key.logic.op.QuantifiableVariable;
019:
020: public class QuanEliminationAnalyser {
021:
022: /**
023: *
024: * @param definitionPIO
025: * @return the distance to the quantifier that can be eliminated;
026: * <code>Integer.MAX_VALUE</code> if the subformula is not an
027: * eliminable definition
028: */
029: public int eliminableDefinition(Term definition,
030: PosInOccurrence envPIO) {
031: final PosInOccurrence matrixPIO = walkUpMatrix(envPIO);
032: final Term matrix = matrixPIO.subTerm();
033:
034: if (matrixPIO.isTopLevel())
035: return Integer.MAX_VALUE;
036:
037: PosInOccurrence quantPIO = matrixPIO.up();
038: Term quantTerm = quantPIO.subTerm();
039: final boolean ex;
040: if (quantTerm.op() == Op.EX) {
041: ex = true;
042: } else if (quantTerm.op() == Op.ALL) {
043: ex = false;
044: } else {
045: return Integer.MAX_VALUE;
046: }
047:
048: if (!isDefinitionCandidate(definition, envPIO.subTerm(), ex))
049: return Integer.MAX_VALUE;
050:
051: int distance = 0;
052: while (true) {
053: final QuantifiableVariable var = quantTerm.varsBoundHere(0)
054: .lastQuantifiableVariable();
055:
056: if (isDefinition(definition, var, ex)
057: && isEliminableVariableSomePaths(var, matrix, ex))
058: return distance;
059:
060: if (quantPIO.isTopLevel())
061: return Integer.MAX_VALUE;
062: quantPIO = quantPIO.up();
063: quantTerm = quantPIO.subTerm();
064:
065: if (quantTerm.op() != (ex ? Op.EX : Op.ALL))
066: return Integer.MAX_VALUE;
067:
068: ++distance;
069: }
070: }
071:
072: private boolean isDefinitionCandidate(Term t, Term env, boolean ex) {
073: if (!hasDefinitionShape(t, ex))
074: return false;
075: return !ex || !isBelowOr(t, env);
076: }
077:
078: private boolean isBelowOr(Term t, Term env) {
079: final Operator envOp = env.op();
080: if (envOp == Op.OR && (env.sub(0) == t || env.sub(1) == t))
081: return true;
082: if (envOp == Op.OR || envOp == Op.AND)
083: return isBelowOr(t, env.sub(0)) || isBelowOr(t, env.sub(1));
084: return false;
085: }
086:
087: private boolean hasDefinitionShape(Term t, boolean ex) {
088: final IteratorOfQuantifiableVariable it = t.freeVars()
089: .iterator();
090: while (it.hasNext()) {
091: if (isDefinition(t, it.next(), ex))
092: return true;
093: }
094: return false;
095: }
096:
097: private PosInOccurrence walkUpMatrix(PosInOccurrence pio) {
098: while (!pio.isTopLevel()) {
099: final PosInOccurrence parent = pio.up();
100: final Operator parentOp = parent.subTerm().op();
101: if (parentOp != Op.AND && parentOp != Op.OR)
102: return pio;
103: pio = parent;
104: }
105: return pio;
106: }
107:
108: /**
109: * The variable <code>var</code> is either eliminable or does not occur on
110: * all conjunctive/disjunctive paths through <code>matrix</code>
111: * (depending on whether <code>ex</code> is true/false)
112: */
113: public boolean isEliminableVariableSomePaths(
114: QuantifiableVariable var, Term matrix, boolean ex) {
115: if (!matrix.freeVars().contains(var))
116: return true;
117:
118: final Operator op = matrix.op();
119:
120: if (op == (ex ? Op.OR : Op.AND)) {
121: return isEliminableVariableSomePaths(var, matrix.sub(0), ex)
122: && isEliminableVariableSomePaths(var,
123: matrix.sub(1), ex);
124: } else if (op == (ex ? Op.AND : Op.OR)) {
125: return isEliminableVariableAllPaths(var, matrix.sub(0), ex)
126: || isEliminableVariableAllPaths(var, matrix.sub(1),
127: ex)
128: || (isEliminableVariableSomePaths(var, matrix
129: .sub(0), ex) && isEliminableVariableSomePaths(
130: var, matrix.sub(1), ex));
131: }
132:
133: if (ex)
134: return isDefiningEquationEx(matrix, var);
135: else
136: return isDefiningEquationAll(matrix, var);
137: }
138:
139: /**
140: * The variable <code>var</code> is eliminable on all
141: * conjunctive/disjunctive paths through <code>matrix</code> (depending on
142: * whether <code>ex</code> is true/false)
143: */
144: public boolean isEliminableVariableAllPaths(
145: QuantifiableVariable var, Term matrix, boolean ex) {
146: final Operator op = matrix.op();
147:
148: if (op == (ex ? Op.OR : Op.AND)) {
149: return isEliminableVariableAllPaths(var, matrix.sub(0), ex)
150: && isEliminableVariableAllPaths(var, matrix.sub(1),
151: ex);
152: } else if (op == (ex ? Op.AND : Op.OR)) {
153: return isEliminableVariableAllPaths(var, matrix.sub(0), ex)
154: || isEliminableVariableAllPaths(var, matrix.sub(1),
155: ex);
156: }
157:
158: if (ex)
159: return isDefiningEquationEx(matrix, var);
160: else
161: return isDefiningEquationAll(matrix, var);
162: }
163:
164: private boolean isDefinition(Term t, QuantifiableVariable var,
165: boolean ex) {
166: if (ex)
167: return isDefinitionEx(t, var);
168: else
169: return isDefiningEquationAll(t, var);
170: }
171:
172: private boolean isDefinitionEx(Term t, QuantifiableVariable var) {
173: if (t.op() == Op.OR) {
174: return isDefinitionEx(t.sub(0), var)
175: && isDefinitionEx(t.sub(1), var);
176: }
177: return isDefiningEquationEx(t, var);
178: }
179:
180: private boolean isDefiningEquationAll(Term t,
181: QuantifiableVariable var) {
182: if (t.op() != Op.NOT)
183: return false;
184: return isDefiningEquation(t.sub(0), var);
185: }
186:
187: private boolean isDefiningEquationEx(Term t,
188: QuantifiableVariable var) {
189: return isDefiningEquation(t, var);
190: }
191:
192: private boolean isDefiningEquation(Term t, QuantifiableVariable var) {
193: if (t.op() != Op.EQUALS)
194: return false;
195: final Term left = t.sub(0);
196: final Term right = t.sub(1);
197: final Operator leftOp = left.op();
198: final Operator rightOp = right.op();
199: return leftOp == var && !right.freeVars().contains(var)
200: || rightOp == var && !left.freeVars().contains(var);
201: }
202:
203: }
|