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.logic.ListOfTerm;
014: import de.uka.ilkd.key.logic.PosInOccurrence;
015: import de.uka.ilkd.key.logic.Term;
016: import de.uka.ilkd.key.logic.ldt.IntegerLDT;
017: import de.uka.ilkd.key.logic.op.Function;
018: import de.uka.ilkd.key.proof.Goal;
019: import de.uka.ilkd.key.rule.TacletApp;
020: import de.uka.ilkd.key.strategy.LongRuleAppCost;
021: import de.uka.ilkd.key.strategy.TopRuleAppCost;
022: import de.uka.ilkd.key.strategy.termProjection.ProjectionToTerm;
023: import de.uka.ilkd.key.strategy.termfeature.*;
024:
025: /**
026: * Feature that returns zero iff each monomial of one polynomial is smaller than
027: * all monomials of a second polynomial
028: */
029: public class MonomialsSmallerThanFeature extends
030: AbstractMonomialSmallerThanFeature {
031:
032: private final TermFeature hasCoeff;
033:
034: private final ProjectionToTerm left, right;
035: private final Function Z, mul, add;
036:
037: private MonomialsSmallerThanFeature(ProjectionToTerm left,
038: ProjectionToTerm right, IntegerLDT numbers) {
039: super (numbers);
040: this .left = left;
041: this .right = right;
042: this .add = numbers.getArithAddition();
043: this .mul = numbers.getArithMultiplication();
044: this .Z = numbers.getNumberSymbol();
045:
046: hasCoeff = createHasCoeffTermFeature(numbers);
047: }
048:
049: static TermFeature createHasCoeffTermFeature(
050: final IntegerLDT numbers) {
051: return BinarySumTermFeature
052: .createSum(
053: OperatorTF.create(numbers
054: .getArithMultiplication()),
055: SubTermFeature
056: .create(new TermFeature[] {
057: ConstTermFeature
058: .createConst(LongRuleAppCost.ZERO_COST),
059: OperatorTF.create(numbers
060: .getNumberSymbol()) }));
061: }
062:
063: public static Feature create(ProjectionToTerm left,
064: ProjectionToTerm right, IntegerLDT numbers) {
065: return new MonomialsSmallerThanFeature(left, right, numbers);
066: }
067:
068: protected boolean filter(TacletApp app, PosInOccurrence pos,
069: Goal goal) {
070: final MonomialCollector m1 = new MonomialCollector();
071: m1.collect(left.toTerm(app, pos, goal));
072: final MonomialCollector m2 = new MonomialCollector();
073: m2.collect(right.toTerm(app, pos, goal));
074:
075: setCurrentGoal(goal);
076:
077: final boolean res = lessThan(m1.getResult(), m2.getResult());
078:
079: setCurrentGoal(null);
080:
081: return res;
082: }
083:
084: /**
085: * this overwrites the method of <code>SmallerThanFeature</code>
086: */
087: protected boolean lessThan(Term t1, Term t2) {
088:
089: // here, the ordering is graded concerning multiplication on integers
090: final int t1Deg = degree(t1);
091: final int t2Deg = degree(t2);
092: if (t1Deg < t2Deg)
093: return true;
094: if (t1Deg > t2Deg)
095: return false;
096:
097: if (t1Deg == 0) {
098: // check whether the symbol was introduced as part of a basis
099: // transformation; such symbols are smaller than other symbols (and
100: // the smaller the later they were introduced)
101:
102: final int v = introductionTime(t2.op())
103: - introductionTime(t1.op());
104: if (v < 0)
105: return true;
106: if (v > 0)
107: return false;
108: } else {
109: final ListOfTerm atoms1 = collectAtoms(t1);
110: final ListOfTerm atoms2 = collectAtoms(t2);
111:
112: if (atoms1.size() < atoms2.size())
113: return false;
114: if (atoms1.size() > atoms2.size())
115: return true;
116:
117: final int v = compareLexNewSyms(atoms1, atoms2);
118: if (v < 0)
119: return true;
120: if (v > 0)
121: return false;
122: }
123:
124: return super .lessThan(t1, t2);
125: }
126:
127: private int compareLexNewSyms(ListOfTerm atoms1, ListOfTerm atoms2) {
128: while (!atoms1.isEmpty()) {
129: final Term t1 = atoms1.head();
130: final Term t2 = atoms2.head();
131: atoms1 = atoms1.tail();
132: atoms2 = atoms2.tail();
133:
134: final int c = introductionTime(t2.op())
135: - introductionTime(t1.op());
136: if (c != 0)
137: return c;
138: }
139:
140: return 0;
141: }
142:
143: /**
144: * @return the degree of a monomial (number of terms that are connected
145: * multiplicatively) -1. To ensure that also cases like
146: * <tt>f(a*b)=a*b</tt> are handled properly, we simply count the
147: * total number of multiplication operators in the term.
148: */
149: private int degree(Term t) {
150: int res = 0;
151:
152: if (t.op() == mul && t.sub(0).op() != Z && t.sub(1).op() != Z)
153: ++res;
154:
155: for (int i = 0; i != t.arity(); ++i)
156: res += degree(t.sub(i));
157:
158: return res;
159: }
160:
161: private class MonomialCollector extends Collector {
162: protected void collect(Term te) {
163: if (te.op() == add) {
164: collect(te.sub(0));
165: collect(te.sub(1));
166: } else if (te.op() == Z) {
167: // nothing
168: } else {
169: addTerm(stripOffLiteral(te));
170: }
171: }
172:
173: private Term stripOffLiteral(Term te) {
174: if (!(hasCoeff.compute(te) instanceof TopRuleAppCost))
175: // we leave out literals/coefficients on the right, because we
176: // do not want to compare these literals
177: return te.sub(0);
178: return te;
179: }
180: }
181: }
|