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.quantifierHeuristics;
012:
013: import de.uka.ilkd.key.java.Services;
014: import de.uka.ilkd.key.logic.IteratorOfTerm;
015: import de.uka.ilkd.key.logic.PosInOccurrence;
016: import de.uka.ilkd.key.logic.Term;
017: import de.uka.ilkd.key.logic.ldt.IntegerLDT;
018: import de.uka.ilkd.key.logic.op.Op;
019: import de.uka.ilkd.key.logic.op.Operator;
020: import de.uka.ilkd.key.proof.Goal;
021: import de.uka.ilkd.key.rule.TacletApp;
022: import de.uka.ilkd.key.rule.metaconstruct.arith.Polynomial;
023: import de.uka.ilkd.key.strategy.feature.Feature;
024: import de.uka.ilkd.key.strategy.feature.SmallerThanFeature;
025: import de.uka.ilkd.key.strategy.termProjection.ProjectionToTerm;
026:
027: public class LiteralsSmallerThanFeature extends SmallerThanFeature {
028:
029: private final ProjectionToTerm left, right;
030: private final IntegerLDT numbers;
031:
032: private final QuanEliminationAnalyser quanAnalyser = new QuanEliminationAnalyser();
033:
034: // ugly, but we need some services
035: private Services services = null;
036: private PosInOccurrence focus = null;
037:
038: private LiteralsSmallerThanFeature(ProjectionToTerm left,
039: ProjectionToTerm right, IntegerLDT numbers) {
040: this .left = left;
041: this .right = right;
042: this .numbers = numbers;
043: }
044:
045: public static Feature create(ProjectionToTerm left,
046: ProjectionToTerm right, IntegerLDT numbers) {
047: return new LiteralsSmallerThanFeature(left, right, numbers);
048: }
049:
050: protected boolean filter(TacletApp app, PosInOccurrence pos,
051: Goal goal) {
052: final Term leftTerm = left.toTerm(app, pos, goal);
053: final Term rightTerm = right.toTerm(app, pos, goal);
054:
055: return compareTerms(leftTerm, rightTerm, pos, goal.proof()
056: .getServices());
057: }
058:
059: protected boolean compareTerms(Term leftTerm, Term rightTerm,
060: PosInOccurrence pos, Services p_services) {
061: services = p_services;
062: focus = pos;
063:
064: final LiteralCollector m1 = new LiteralCollector();
065: m1.collect(leftTerm);
066: final LiteralCollector m2 = new LiteralCollector();
067: m2.collect(rightTerm);
068:
069: final boolean res = lessThan(m1.getResult(), m2.getResult());
070:
071: services = null;
072: focus = null;
073:
074: return res;
075: }
076:
077: /**
078: * this overwrites the method of <code>SmallerThanFeature</code>
079: */
080: protected boolean lessThan(Term t1, Term t2) {
081:
082: final int t1Def = quanAnalyser.eliminableDefinition(t1, focus);
083: final int t2Def = quanAnalyser.eliminableDefinition(t2, focus);
084:
085: if (t1Def > t2Def)
086: return true;
087: if (t1Def < t2Def)
088: return false;
089:
090: // HACK: we move literals that do not contain any variables to the left,
091: // so that they can be moved out of the scope of the quantifiers
092: if (t1.freeVars().size() == 0) {
093: if (t2.freeVars().size() > 0)
094: return false;
095: } else {
096: if (t2.freeVars().size() == 0)
097: return true;
098: }
099:
100: t1 = discardNegation(t1);
101: t2 = discardNegation(t2);
102:
103: if (isBinaryIntRelation(t2)) {
104: if (!isBinaryIntRelation(t1))
105: return true;
106:
107: int c = compare(t1.sub(0), t2.sub(0));
108: if (c < 0)
109: return true;
110: if (c > 0)
111: return false;
112:
113: c = comparePolynomials(t1.sub(1), t2.sub(1));
114: if (c < 0)
115: return true;
116: if (c > 0)
117: return false;
118:
119: final Polynomial t1RHS = Polynomial.create(t1.sub(1),
120: services);
121: final Polynomial t2RHS = Polynomial.create(t2.sub(1),
122: services);
123: if (t1RHS.valueLess(t2RHS))
124: return true;
125: if (t2RHS.valueLess(t1RHS))
126: return false;
127:
128: c = formulaKind(t1) - formulaKind(t2);
129: if (c < 0)
130: return true;
131: if (c > 0)
132: return false;
133: } else {
134: if (isBinaryIntRelation(t1))
135: return false;
136: }
137:
138: return super .lessThan(t1, t2);
139: }
140:
141: private int comparePolynomials(Term t1, Term t2) {
142: final IteratorOfTerm it1 = new MonomialIterator(t1);
143: final IteratorOfTerm it2 = new MonomialIterator(t2);
144:
145: while (true) {
146: if (it1.hasNext()) {
147: if (!it2.hasNext())
148: return 1;
149: } else {
150: if (it2.hasNext())
151: return -1;
152: else
153: return 0;
154: }
155:
156: final int c = compare(it1.next(), it2.next());
157: if (c != 0)
158: return c;
159: }
160: }
161:
162: private Term discardNegation(Term t) {
163: while (t.op() == Op.NOT)
164: t = t.sub(0);
165: return t;
166: }
167:
168: private boolean isBinaryIntRelation(Term t) {
169: return formulaKind(t) >= 0;
170: }
171:
172: private int formulaKind(Term t) {
173: final Operator op = t.op();
174: if (op == numbers.getLessOrEquals())
175: return 1;
176: if (op == numbers.getGreaterOrEquals())
177: return 2;
178: if (op == Op.EQUALS)
179: return 3;
180: return -1;
181: }
182:
183: private class MonomialIterator implements IteratorOfTerm {
184: private Term polynomial;
185: private Term nextMonomial = null;
186:
187: private MonomialIterator(Term polynomial) {
188: this .polynomial = polynomial;
189: findNextMonomial();
190: }
191:
192: private void findNextMonomial() {
193: while (nextMonomial == null && polynomial != null) {
194: if (polynomial.op() == numbers.getArithAddition()) {
195: nextMonomial = polynomial.sub(1);
196: polynomial = polynomial.sub(0);
197: } else {
198: nextMonomial = polynomial;
199: polynomial = null;
200: }
201:
202: if (nextMonomial.op() == numbers.getNumberSymbol())
203: nextMonomial = null;
204: }
205: }
206:
207: public boolean hasNext() {
208: return nextMonomial != null;
209: }
210:
211: public Term next() {
212: final Term res = nextMonomial;
213: nextMonomial = null;
214: findNextMonomial();
215: return res;
216: }
217: }
218:
219: private class LiteralCollector extends Collector {
220: protected void collect(Term te) {
221: final Operator op = te.op();
222: if (op == Op.OR) {
223: collect(te.sub(0));
224: collect(te.sub(1));
225: } else {
226: addTerm(te);
227: }
228: }
229: }
230:
231: }
|