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.feature;
012:
013: import de.uka.ilkd.key.java.Services;
014: import de.uka.ilkd.key.logic.PosInOccurrence;
015: import de.uka.ilkd.key.proof.Goal;
016: import de.uka.ilkd.key.rule.TacletApp;
017: import de.uka.ilkd.key.rule.metaconstruct.arith.Monomial;
018: import de.uka.ilkd.key.strategy.termProjection.ProjectionToTerm;
019:
020: /**
021: * Feature that decides whether the multiplication of two inequations (using
022: * rules of set inEqSimp_nonLin_multiply) is allowed. We only do this if the
023: * product of the left sides of the inequations has factors in common with the
024: * left side of some other inequation, similarly to how it is decided in the
025: * Buchberger algorithm.
026: */
027: public abstract class InEquationMultFeature extends
028: BinaryTacletAppFeature {
029:
030: protected final ProjectionToTerm targetCandidate;
031: protected final ProjectionToTerm mult1Candidate;
032: protected final ProjectionToTerm mult2Candidate;
033:
034: /**
035: * Return zero iff the multiplication of mult1 and mult2 is allowed,
036: * because the resulting product is partially covered by target.
037: *
038: * @param mult1Candidate
039: * the left side of the first inequation to be multiplied
040: * @param mult2Candidate
041: * the left side of the second inequation to be multiplied
042: * @param targetCandidate
043: * the left side of the inequation that is supposed to bound the
044: * other two inequations
045: */
046: public static Feature partiallyBounded(
047: ProjectionToTerm mult1Candidate,
048: ProjectionToTerm mult2Candidate,
049: ProjectionToTerm targetCandidate) {
050: return new InEquationMultFeature(mult1Candidate,
051: mult2Candidate, targetCandidate) {
052: protected boolean filter(Monomial targetM, Monomial mult1M,
053: Monomial mult2M) {
054: return !mult2M.reduce(targetM)
055: .variablesDisjoint(mult1M)
056: && !mult1M.reduce(targetM).variablesDisjoint(
057: mult2M);
058: }
059: };
060: }
061:
062: /**
063: * Return zero iff the product of mult1 and mult2 is a factor of target
064: */
065: public static Feature totallyBounded(
066: ProjectionToTerm mult1Candidate,
067: ProjectionToTerm mult2Candidate,
068: ProjectionToTerm targetCandidate) {
069: return new InEquationMultFeature(mult1Candidate,
070: mult2Candidate, targetCandidate) {
071: protected boolean filter(Monomial targetM, Monomial mult1M,
072: Monomial mult2M) {
073: return targetM
074: .variablesSubsume(mult1M.multiply(mult2M));
075: }
076: };
077: }
078:
079: /**
080: * Return zero iff the product of mult1 and mult2 is target
081: */
082: public static Feature exactlyBounded(
083: ProjectionToTerm mult1Candidate,
084: ProjectionToTerm mult2Candidate,
085: ProjectionToTerm targetCandidate) {
086: return new InEquationMultFeature(mult1Candidate,
087: mult2Candidate, targetCandidate) {
088: protected boolean filter(Monomial targetM, Monomial mult1M,
089: Monomial mult2M) {
090: return targetM.variablesEqual(mult1M.multiply(mult2M));
091: }
092: };
093: }
094:
095: protected InEquationMultFeature(ProjectionToTerm mult1Candidate,
096: ProjectionToTerm mult2Candidate,
097: ProjectionToTerm targetCandidate) {
098: this .mult1Candidate = mult1Candidate;
099: this .mult2Candidate = mult2Candidate;
100: this .targetCandidate = targetCandidate;
101: }
102:
103: protected final boolean filter(TacletApp app, PosInOccurrence pos,
104: Goal goal) {
105: final Services services = goal.proof().getServices();
106: final Monomial targetM = Monomial.create(targetCandidate
107: .toTerm(app, pos, goal), services);
108: final Monomial mult1M = Monomial.create(mult1Candidate.toTerm(
109: app, pos, goal), services);
110: final Monomial mult2M = Monomial.create(mult2Candidate.toTerm(
111: app, pos, goal), services);
112:
113: return filter(targetM, mult1M, mult2M);
114: }
115:
116: protected abstract boolean filter(Monomial targetM,
117: Monomial mult1M, Monomial mult2M);
118: }
|