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.strategy.feature;
12:
13: import de.uka.ilkd.key.logic.PosInOccurrence;
14: import de.uka.ilkd.key.logic.Term;
15: import de.uka.ilkd.key.logic.ldt.IntegerLDT;
16: import de.uka.ilkd.key.logic.op.Function;
17: import de.uka.ilkd.key.proof.Goal;
18: import de.uka.ilkd.key.rule.TacletApp;
19: import de.uka.ilkd.key.strategy.termProjection.ProjectionToTerm;
20:
21: /**
22: * Feature that returns zero iff each variable/atom of one monomial is smaller
23: * than all variables of a second monomial
24: */
25: public class AtomsSmallerThanFeature extends
26: AbstractMonomialSmallerThanFeature {
27:
28: private final ProjectionToTerm left, right;
29: private final Function Z;
30:
31: private AtomsSmallerThanFeature(ProjectionToTerm left,
32: ProjectionToTerm right, IntegerLDT numbers) {
33: super (numbers);
34: this .left = left;
35: this .right = right;
36: this .Z = numbers.getNumberSymbol();
37: }
38:
39: public static Feature create(ProjectionToTerm left,
40: ProjectionToTerm right, IntegerLDT numbers) {
41: return new AtomsSmallerThanFeature(left, right, numbers);
42: }
43:
44: protected boolean filter(TacletApp app, PosInOccurrence pos,
45: Goal goal) {
46: setCurrentGoal(goal);
47:
48: final boolean res = lessThan(collectAtoms(left.toTerm(app, pos,
49: goal)), collectAtoms(right.toTerm(app, pos, goal)));
50:
51: setCurrentGoal(null);
52:
53: return res;
54: }
55:
56: /**
57: * this overwrites the method of <code>SmallerThanFeature</code>
58: */
59: protected boolean lessThan(Term t1, Term t2) {
60: if (t1.op() == Z) {
61: if (t2.op() != Z)
62: return true;
63: return super .lessThan(t1, t2);
64: } else {
65: if (t2.op() == Z)
66: return false;
67: }
68:
69: final int v = introductionTime(t2.op())
70: - introductionTime(t1.op());
71: if (v < 0)
72: return true;
73: if (v > 0)
74: return false;
75:
76: return super.lessThan(t1, t2);
77: }
78: }
|