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.*;
14:
15: /**
16: * Abstract superclass for features comparing terms (in particular polynomials
17: * or monomials) using the term ordering
18: */
19: public abstract class SmallerThanFeature extends BinaryTacletAppFeature {
20:
21: private final TermOrdering termOrdering = new LexPathOrdering();
22:
23: protected boolean lessThan(Term t1, Term t2) {
24: return compare(t1, t2) < 0;
25: }
26:
27: protected final int compare(Term t1, Term t2) {
28: return termOrdering.compare(t1, t2);
29: }
30:
31: /**
32: * @return <code>true</code> iff each element of <code>list1</code> is
33: * strictly smaller than all elements of <code>list2</code>
34: */
35: protected final boolean lessThan(ListOfTerm list1, ListOfTerm list2) {
36: if (list2.isEmpty())
37: return false;
38: final IteratorOfTerm it1 = list1.iterator();
39: while (it1.hasNext()) {
40: final Term te1 = it1.next();
41: final IteratorOfTerm it2 = list2.iterator();
42: while (it2.hasNext()) {
43: if (!lessThan(te1, it2.next()))
44: return false;
45: }
46: }
47: return true;
48: }
49:
50: protected abstract static class Collector {
51:
52: private ListOfTerm terms = SLListOfTerm.EMPTY_LIST;
53:
54: protected void addTerm(Term mon) {
55: terms = terms.prepend(mon);
56: }
57:
58: public ListOfTerm getResult() {
59: return terms;
60: }
61:
62: }
63:
64: }
|