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;
012:
013: import de.uka.ilkd.key.logic.*;
014: import de.uka.ilkd.key.proof.Goal;
015: import de.uka.ilkd.key.rule.BuiltInRule;
016: import de.uka.ilkd.key.rule.BuiltInRuleApp;
017: import de.uka.ilkd.key.rule.RuleApp;
018:
019: /**
020: * Instances of this class are immutable
021: */
022: public class BuiltInRuleAppContainer extends RuleAppContainer {
023:
024: BuiltInRuleAppContainer(RuleApp p_app, RuleAppCost p_cost) {
025: super (p_app, p_cost);
026: }
027:
028: /**
029: * Create a list of new RuleAppContainers that are to be
030: * considered for application.
031: */
032: public ListOfRuleAppContainer createFurtherApps(Goal p_goal,
033: Strategy p_strategy) {
034: if (isStillApplicable(p_goal))
035: return createAppContainers((BuiltInRuleApp) getRuleApp(),
036: null, p_goal, p_strategy);
037: return SLListOfRuleAppContainer.EMPTY_LIST;
038: }
039:
040: /**
041: * Create a <code>RuleApp</code> that is suitable to be applied
042: * or <code>null</code>.
043: */
044: public RuleApp completeRuleApp(Goal p_goal, Strategy p_strategy) {
045: if (!isStillApplicable(p_goal))
046: return null;
047:
048: final BuiltInRuleApp app = getBuiltInRuleApp();
049: final BuiltInRule rule = (BuiltInRule) app.rule();
050: final Constraint userConstraint = app.userConstraint();
051: final PosInOccurrence pio = getBuiltInRuleApp()
052: .posInOccurrence();
053:
054: return new BuiltInRuleApp(rule, pio, userConstraint);
055: }
056:
057: /**
058: * @return the BuiltInRuleApp belonging to this container
059: */
060: protected BuiltInRuleApp getBuiltInRuleApp() {
061: return (BuiltInRuleApp) getRuleApp();
062: }
063:
064: /**
065: * @return true iff the stored rule app is applicable for the given sequent,
066: * i.e. if the bound position does still exist (if-formulas are not
067: * considered)
068: */
069: protected boolean isStillApplicable(Goal p_goal) {
070: final BuiltInRuleApp app = getBuiltInRuleApp();
071: final PosInOccurrence pio = app.posInOccurrence();
072: if (pio == null) {
073: return true;
074: }
075: final ConstrainedFormula cfma = pio.constrainedFormula();
076: final boolean antec = pio.isInAntec();
077: final Sequent seq = p_goal.sequent();
078: final Semisequent semiseq = antec ? seq.antecedent() : seq
079: .succedent();
080:
081: if (!semiseq.contains(cfma))
082: return false;
083:
084: return true;
085: }
086:
087: /**
088: * Create containers for RuleApps.
089: * @return list of containers for currently applicable BuiltInRuleApps,
090: * the cost may be an instance of <code>TopRuleAppCost</code>.
091: */
092: static ListOfRuleAppContainer createAppContainers(
093: BuiltInRuleApp p_app, PosInOccurrence p_pio, Goal p_goal,
094: Strategy p_strategy) {
095: ListOfRuleAppContainer result = SLListOfRuleAppContainer.EMPTY_LIST;
096:
097: final RuleAppCost cost = p_strategy.computeCost(p_app, p_pio,
098: p_goal);
099:
100: BuiltInRuleAppContainer container = new BuiltInRuleAppContainer(
101: p_app, cost);
102:
103: result = result.prepend(container);
104:
105: return result;
106: }
107:
108: }
|