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.PosInOccurrence;
14: import de.uka.ilkd.key.logic.Term;
15: import de.uka.ilkd.key.logic.op.Op;
16: import de.uka.ilkd.key.logic.op.Operator;
17: import de.uka.ilkd.key.logic.op.SetAsListOfQuantifiableVariable;
18: import de.uka.ilkd.key.logic.op.SetOfQuantifiableVariable;
19: import de.uka.ilkd.key.proof.Goal;
20: import de.uka.ilkd.key.rule.RuleApp;
21: import de.uka.ilkd.key.strategy.feature.BinaryFeature;
22: import de.uka.ilkd.key.strategy.feature.Feature;
23: import de.uka.ilkd.key.util.Debug;
24:
25: public class SplittableQuantifiedFormulaFeature extends BinaryFeature {
26:
27: private SplittableQuantifiedFormulaFeature() {
28: }
29:
30: public static final Feature INSTANCE = new SplittableQuantifiedFormulaFeature();
31:
32: protected boolean filter(RuleApp app, PosInOccurrence pos, Goal goal) {
33: Debug.assertFalse(pos == null,
34: "Feature is only applicable to rules with find");
35:
36: final Analyser analyser = new Analyser();
37: if (!analyser.analyse(pos.constrainedFormula().formula()))
38: return false;
39:
40: if (analyser.binOp == Op.AND)
41: return TriggerUtils.intersect(
42: TriggerUtils.intersect(analyser.left.freeVars(),
43: analyser.right.freeVars()),
44: analyser.existentialVars).size() == 0;
45: else if (analyser.binOp == Op.OR)
46: return TriggerUtils.intersect(analyser.left.freeVars(),
47: analyser.right.freeVars()).union(
48: analyser.existentialVars).size() == analyser.existentialVars
49: .size();
50:
51: return false;
52: }
53:
54: private static class Analyser {
55: public SetOfQuantifiableVariable existentialVars = SetAsListOfQuantifiableVariable.EMPTY_SET;
56: public Operator binOp;
57: public Term left, right;
58:
59: public boolean analyse(Term formula) {
60: final Operator op = formula.op();
61:
62: if (op == Op.ALL) {
63: // might be that a variable is bound more than once
64: existentialVars = existentialVars.remove(formula
65: .varsBoundHere(0).lastQuantifiableVariable());
66: return analyse(formula.sub(0));
67: }
68:
69: if (op == Op.EX) {
70: existentialVars = existentialVars.add(formula
71: .varsBoundHere(0).lastQuantifiableVariable());
72: return analyse(formula.sub(0));
73: }
74:
75: if (op == Op.AND || op == Op.OR) {
76: binOp = op;
77: left = formula.sub(0);
78: right = formula.sub(1);
79: return true;
80: }
81:
82: return false;
83: }
84: }
85: }
|