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.rule;
012:
013: import de.uka.ilkd.key.java.Services;
014: import de.uka.ilkd.key.logic.Constraint;
015: import de.uka.ilkd.key.logic.Name;
016: import de.uka.ilkd.key.logic.PosInOccurrence;
017: import de.uka.ilkd.key.proof.Goal;
018: import de.uka.ilkd.key.proof.ListOfGoal;
019: import de.uka.ilkd.key.proof.SLListOfGoal;
020: import de.uka.ilkd.key.proof.decproc.AbstractDecisionProcedure;
021: import de.uka.ilkd.key.proof.decproc.DecisionProcedureResult;
022: import de.uka.ilkd.key.proof.decproc.DecisionProcedureTranslationFactory;
023:
024: /**
025: * Abstract base class for ICS and Simplify built-in rules.
026: */
027: public abstract class AbstractIntegerRule implements BuiltInRule {
028:
029: private final Name name;
030: protected final boolean showResults;
031: protected final DecisionProcedureTranslationFactory dptf;
032:
033: public AbstractIntegerRule(Name p_name,
034: DecisionProcedureTranslationFactory dptf) {
035: this (p_name, true, dptf);
036: }
037:
038: public AbstractIntegerRule(Name p_name, boolean resultWindow,
039: DecisionProcedureTranslationFactory dptf) {
040: name = p_name;
041: showResults = resultWindow;
042: this .dptf = dptf;
043: }
044:
045: /**
046: * returns true iff a rule is applicable at the given
047: * position. This does not necessary mean that a rule application
048: * will change the goal (this decision is made due to performance
049: * reasons)
050: */
051: public boolean isApplicable(Goal goal, PosInOccurrence pio,
052: Constraint userConstraint) {
053: if (pio == null) {
054: return true;
055: }
056: return false;
057: }
058:
059: public ListOfGoal apply(Goal goal, Services services,
060: RuleApp ruleApp) {
061: final BuiltInRuleApp birApp = (BuiltInRuleApp) ruleApp;
062: final Constraint userConstraint = birApp.userConstraint();
063: final AbstractDecisionProcedure dp = getDecisionProcedure(goal,
064: userConstraint, services);
065: final DecisionProcedureResult result = dp.run();
066:
067: ListOfGoal goals = null;
068:
069: if (result.getResult()) {
070: goals = SLListOfGoal.EMPTY_LIST;
071: if (result.getConstraint() != Constraint.BOTTOM) {
072: goals = goal.split(1);
073: goals.head().addClosureConstraint(
074: result.getConstraint());
075: }
076: }
077:
078: return goals;
079: }
080:
081: /**
082: * clones this abstract integer rule and sets its decision procedure translation
083: * factory to the given one
084: * @param dptf the {@link DecisionProcedureTranslationFactory} to be used by the
085: * cloned object
086: * @return the cloned integer rule
087: */
088: public abstract AbstractIntegerRule clone(
089: DecisionProcedureTranslationFactory dptf);
090:
091: /**
092: * Get the decision procedure invoked by this rule.
093: * @param goal the goal on which the decision procedure should operate.
094: * @param userConstraint the user constraint
095: * @return the decision procedure
096: */
097: protected abstract AbstractDecisionProcedure getDecisionProcedure(
098: Goal goal, Constraint userConstraint, Services services);
099:
100: public Name name() {
101: return name;
102: }
103:
104: public String displayName() {
105: return name().toString();
106: }
107:
108: public String toString() {
109: return name().toString();
110: }
111:
112: }
|