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.rule;
12:
13: import de.uka.ilkd.key.java.Services;
14: import de.uka.ilkd.key.logic.Constraint;
15: import de.uka.ilkd.key.logic.PosInOccurrence;
16: import de.uka.ilkd.key.proof.Goal;
17: import de.uka.ilkd.key.proof.ListOfGoal;
18:
19: /**
20: * this class represents an application of a built in rule
21: * application
22: */
23: public class BuiltInRuleApp implements RuleApp {
24:
25: private BuiltInRule builtInRule;
26: private PosInOccurrence pio;
27: private Constraint userConstraint;
28:
29: /**
30: *
31: */
32: public BuiltInRuleApp(BuiltInRule builtInRule, PosInOccurrence pio,
33: Constraint userConstraint) {
34: this .builtInRule = builtInRule;
35: this .pio = pio;
36: this .userConstraint = userConstraint;
37: }
38:
39: /**
40: * returns the rule of this rule application
41: */
42: public Rule rule() {
43: return builtInRule;
44: }
45:
46: /**
47: * returns the PositionInOccurrence (representing a ConstrainedFormula and
48: * a position in the corresponding formula) of this rule application
49: */
50: public PosInOccurrence posInOccurrence() {
51: return pio;
52: }
53:
54: /** applies the specified rule at the specified position
55: * if all schema variables have been instantiated
56: * @param goal the Goal where to apply the rule
57: * @param services the Services encapsulating all java information
58: * @return list of new created goals
59: */
60: public ListOfGoal execute(Goal goal, Services services) {
61: goal.addAppliedRuleApp(this );
62: ListOfGoal result = builtInRule.apply(goal, services, this );
63: if (result == null)
64: goal.removeAppliedRuleApp();
65: return result;
66: }
67:
68: /**
69: * returns the constraint under which a rule is applicable
70: */
71: public Constraint constraint() {
72: return Constraint.BOTTOM;
73: }
74:
75: /**
76: * returns the user constraint
77: */
78: public Constraint userConstraint() {
79: return userConstraint;
80: }
81:
82: /** returns true if all variables are instantiated
83: * @return true if all variables are instantiated
84: */
85: public boolean complete() {
86: return true;
87: }
88:
89: /**
90: * toString
91: */
92: public String toString() {
93: return "" + rule().name();
94: }
95:
96: }
|