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.proof.Goal;
15: import de.uka.ilkd.key.rule.TacletApp;
16: import de.uka.ilkd.key.strategy.feature.BinaryTacletAppFeature;
17: import de.uka.ilkd.key.strategy.feature.Feature;
18: import de.uka.ilkd.key.strategy.termProjection.ProjectionToTerm;
19: import de.uka.ilkd.key.util.Debug;
20:
21: /**
22: * Binary feature that return zero if two given projection term is CS-Releated.
23: */
24: public class ExistentiallyConnectedFormulasFeature extends
25: BinaryTacletAppFeature {
26:
27: private final ProjectionToTerm for0, for1;
28:
29: private ExistentiallyConnectedFormulasFeature(
30: ProjectionToTerm for0, ProjectionToTerm for1) {
31: this .for0 = for0;
32: this .for1 = for1;
33: }
34:
35: public static Feature create(ProjectionToTerm for0,
36: ProjectionToTerm for1) {
37: return new ExistentiallyConnectedFormulasFeature(for0, for1);
38: }
39:
40: protected boolean filter(TacletApp app, PosInOccurrence pos,
41: Goal goal) {
42: Debug.assertFalse(pos == null,
43: "Feature is only applicable to rules with find");
44:
45: final ClausesGraph graph = ClausesGraph.create(pos
46: .constrainedFormula().formula());
47:
48: return graph.connected(for0.toTerm(app, pos, goal), for1
49: .toTerm(app, pos, goal));
50: }
51:
52: }
|