01: // This file is part of KeY - Integrated Deductive Software Design
02: // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
03: // Universitaet Koblenz-Landau, Germany
04: // Chalmers University of Technology, Sweden
05: //
06: // The KeY system is protected by the GNU General Public License.
07: // See LICENSE.TXT for details.
08: //
09: //
10:
11: package de.uka.ilkd.key.strategy.quantifierHeuristics;
12:
13: import de.uka.ilkd.key.logic.Term;
14: import de.uka.ilkd.key.logic.op.Op;
15: import de.uka.ilkd.key.logic.op.Operator;
16: import de.uka.ilkd.key.logic.op.QuantifiableVariable;
17: import de.uka.ilkd.key.strategy.termfeature.BinaryTermFeature;
18: import de.uka.ilkd.key.strategy.termfeature.TermFeature;
19:
20: public class EliminableQuantifierTF extends BinaryTermFeature {
21:
22: public static final TermFeature INSTANCE = new EliminableQuantifierTF();
23:
24: private final QuanEliminationAnalyser quanAnalyser = new QuanEliminationAnalyser();
25:
26: private EliminableQuantifierTF() {
27: }
28:
29: protected boolean filter(Term term) {
30: final Operator op = term.op();
31: assert op == Op.ALL || op == Op.EX;
32:
33: Term matrix = term;
34: do {
35: matrix = matrix.sub(0);
36: } while (matrix.op() == term.op());
37:
38: if (matrix.op() == Op.ALL || matrix.op() == Op.EX)
39: return false;
40:
41: final QuantifiableVariable var = term.varsBoundHere(0)
42: .lastQuantifiableVariable();
43:
44: return quanAnalyser.isEliminableVariableAllPaths(var, matrix,
45: op == Op.EX);
46: }
47:
48: }
|