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.rule.metaconstruct.arith;
012:
013: import java.math.BigInteger;
014:
015: import de.uka.ilkd.key.java.Services;
016: import de.uka.ilkd.key.java.TypeConverter;
017: import de.uka.ilkd.key.logic.Term;
018: import de.uka.ilkd.key.logic.TermBuilder;
019: import de.uka.ilkd.key.logic.TermFactory;
020: import de.uka.ilkd.key.logic.ldt.IntegerLDT;
021: import de.uka.ilkd.key.logic.op.AbstractMetaOperator;
022: import de.uka.ilkd.key.logic.op.CastFunctionSymbol;
023: import de.uka.ilkd.key.logic.op.Operator;
024: import de.uka.ilkd.key.logic.op.TermSymbol;
025: import de.uka.ilkd.key.util.LRUCache;
026:
027: /**
028: * Class for analysing and modifying polynomial expressions over the integers
029: */
030: public class Polynomial {
031:
032: private final BigInteger constantPart;
033: private final ListOfMonomial parts;
034:
035: private Polynomial(ListOfMonomial parts, BigInteger constantPart) {
036: this .parts = parts;
037: this .constantPart = constantPart;
038: }
039:
040: private static final LRUCache polynomialCache = new LRUCache(2000);
041: private static final BigInteger MINUS_ONE = BigInteger.valueOf(-1);
042:
043: public final static Polynomial ZERO = new Polynomial(
044: SLListOfMonomial.EMPTY_LIST, BigInteger.ZERO);
045: public final static Polynomial ONE = new Polynomial(
046: SLListOfMonomial.EMPTY_LIST, BigInteger.ONE);
047:
048: public static Polynomial create(Term polyTerm, Services services) {
049: Polynomial res = (Polynomial) polynomialCache.get(polyTerm);
050: if (res == null) {
051: res = createHelp(polyTerm, services);
052: polynomialCache.put(polyTerm, res);
053: }
054: return res;
055: }
056:
057: private static Polynomial createHelp(Term polynomial,
058: Services services) {
059: final Analyser a = new Analyser(services);
060: a.analyse(polynomial);
061: return new Polynomial(a.parts, a.constantPart);
062: }
063:
064: public Polynomial multiply(BigInteger c) {
065: if (c.signum() == 0)
066: return new Polynomial(SLListOfMonomial.EMPTY_LIST,
067: BigInteger.ZERO);
068: ListOfMonomial newParts = SLListOfMonomial.EMPTY_LIST;
069: final IteratorOfMonomial it = parts.iterator();
070: while (it.hasNext())
071: newParts = newParts.prepend(it.next().multiply(c));
072:
073: return new Polynomial(newParts, constantPart.multiply(c));
074: }
075:
076: public Polynomial multiply(Monomial m) {
077: if (m.getCoefficient().signum() == 0)
078: return new Polynomial(SLListOfMonomial.EMPTY_LIST,
079: BigInteger.ZERO);
080:
081: ListOfMonomial newParts = SLListOfMonomial.EMPTY_LIST;
082: final IteratorOfMonomial it = parts.iterator();
083: while (it.hasNext())
084: newParts = newParts.prepend(it.next().multiply(m));
085:
086: if (m.getParts().isEmpty())
087: return new Polynomial(newParts, constantPart.multiply(m
088: .getCoefficient()));
089:
090: newParts = addPart(newParts, m.multiply(constantPart));
091: return new Polynomial(newParts, BigInteger.ZERO);
092: }
093:
094: public Polynomial add(BigInteger c) {
095: return new Polynomial(parts, constantPart.add(c));
096: }
097:
098: public Polynomial sub(Polynomial p) {
099: final BigInteger newConst = getConstantTerm().subtract(
100: p.getConstantTerm());
101: ListOfMonomial newParts = parts;
102: final IteratorOfMonomial it = p.getParts().iterator();
103: while (it.hasNext())
104: newParts = addPart(newParts, it.next().multiply(MINUS_ONE));
105: return new Polynomial(newParts, newConst);
106: }
107:
108: public Polynomial add(Monomial m) {
109: if (m.getParts().isEmpty())
110: return new Polynomial(parts, constantPart.add(m
111: .getCoefficient()));
112:
113: return new Polynomial(addPart(parts, m), constantPart);
114: }
115:
116: public Polynomial add(Polynomial p) {
117: final BigInteger newConst = getConstantTerm().add(
118: p.getConstantTerm());
119: ListOfMonomial newParts = parts;
120: final IteratorOfMonomial it = p.getParts().iterator();
121: while (it.hasNext())
122: newParts = addPart(newParts, it.next());
123: return new Polynomial(newParts, newConst);
124: }
125:
126: /**
127: * @return the greatest common divisor of the coefficients of the monomials
128: * of this polynomial. The constant part of the polynomial is not
129: * taken into account. If there are no monomials (apart from the
130: * constant term), the result is <code>BigInteger.ZERO</code>
131: */
132: public BigInteger coeffGcd() {
133: BigInteger res = BigInteger.ZERO;
134: final IteratorOfMonomial it = parts.iterator();
135: while (it.hasNext())
136: res = res.gcd(it.next().getCoefficient());
137: return res;
138: }
139:
140: /**
141: * @return <code>true</code> if the value of <code>this</code> will
142: * always be less than the value of <code>p</code>
143: * (i.e., same monomials, but the constant part is less or equal)
144: */
145: public boolean valueLess(Polynomial p) {
146: if (!sameParts(p))
147: return false;
148: return constantPart.compareTo(p.constantPart) < 0;
149: }
150:
151: /**
152: * @return <code>true</code> if the value of <code>this</code> will
153: * always be equal to the value of <code>p</code>
154: * (i.e., same monomials and same constant part)
155: */
156: public boolean valueEq(Polynomial p) {
157: if (!sameParts(p))
158: return false;
159: return constantPart.equals(p.constantPart);
160: }
161:
162: public boolean valueUneq(Polynomial p) {
163: if (!sameParts(p))
164: return false;
165: return !constantPart.equals(p.constantPart);
166: }
167:
168: public boolean valueEq(BigInteger c) {
169: if (!parts.isEmpty())
170: return false;
171: return constantPart.equals(c);
172: }
173:
174: public boolean valueUneq(BigInteger c) {
175: if (!parts.isEmpty())
176: return false;
177: return !constantPart.equals(c);
178: }
179:
180: /**
181: * @return <code>true</code> if the value of <code>this</code> will
182: * always be less or equal than the value of <code>p</code>
183: * (i.e., same monomials, but the constant part is less or equal)
184: */
185: public boolean valueLeq(Polynomial p) {
186: if (!sameParts(p))
187: return false;
188: return constantPart.compareTo(p.constantPart) <= 0;
189: }
190:
191: public boolean valueLess(BigInteger c) {
192: if (!parts.isEmpty())
193: return false;
194: return constantPart.compareTo(c) < 0;
195: }
196:
197: public boolean valueGeq(BigInteger c) {
198: if (!parts.isEmpty())
199: return false;
200: return constantPart.compareTo(c) >= 0;
201: }
202:
203: public boolean sameParts(Polynomial p) {
204: if (parts.size() != p.parts.size())
205: return false;
206: return difference(parts, p.parts).isEmpty();
207: }
208:
209: public Term toTerm(Services services) {
210: final TermSymbol add = services.getTypeConverter()
211: .getIntegerLDT().getArithAddition();
212: Term res = null;
213:
214: final IteratorOfMonomial it = parts.iterator();
215: if (it.hasNext()) {
216: res = it.next().toTerm(services);
217: while (it.hasNext())
218: res = TermFactory.DEFAULT.createFunctionTerm(add, res,
219: it.next().toTerm(services));
220: }
221:
222: final Term cTerm = TermBuilder.DF.zTerm(services, constantPart
223: .toString());
224:
225: if (res == null)
226: res = cTerm;
227: else if (!BigInteger.ZERO.equals(constantPart))
228: res = TermFactory.DEFAULT.createFunctionTerm(add, cTerm,
229: res);
230:
231: return res;
232: }
233:
234: public String toString() {
235: final StringBuffer res = new StringBuffer();
236: res.append(constantPart);
237:
238: final IteratorOfMonomial it = parts.iterator();
239: while (it.hasNext())
240: res.append(" + " + it.next());
241:
242: return res.toString();
243: }
244:
245: private static class Analyser {
246: public BigInteger constantPart = BigInteger.ZERO;
247: public ListOfMonomial parts = SLListOfMonomial.EMPTY_LIST;
248: private final Services services;
249: private final TypeConverter tc;
250: private final Operator numbers, add;
251:
252: public Analyser(final Services services) {
253: this .services = services;
254: this .tc = services.getTypeConverter();
255: final IntegerLDT intLDT = tc.getIntegerLDT();
256: numbers = intLDT.getNumberSymbol();
257: add = intLDT.getArithAddition();
258: }
259:
260: public void analyse(Term polynomial) {
261: final Operator op = polynomial.op();
262: if (op == add) {
263: analyse(polynomial.sub(0));
264: analyse(polynomial.sub(1));
265: } else if (op == numbers) {
266: final BigInteger c = new BigInteger(
267: AbstractMetaOperator.convertToDecimalString(
268: polynomial, services));
269: constantPart = constantPart.add(c);
270: } else if (op instanceof CastFunctionSymbol
271: && polynomial.sub(0).sort().extendsTrans(
272: tc.getIntegerLDT().targetSort())
273: && (polynomial.sort() == tc.getByteLDT()
274: .targetSort()
275: || polynomial.sort() == tc.getShortLDT()
276: .targetSort()
277: || polynomial.sort() == tc.getCharLDT()
278: .targetSort()
279: || polynomial.sort() == tc.getIntLDT()
280: .targetSort()
281: || polynomial.sort() == tc.getLongLDT()
282: .targetSort() || polynomial.sort() == tc
283: .getIntegerLDT().targetSort())) {
284: // HACK: work around the hackish integer type hierarchy
285: analyse(polynomial.sub(0));
286: } else {
287: parts = addPart(parts, Monomial.create(polynomial,
288: services));
289: }
290: }
291: }
292:
293: /**
294: * @return the list of all monomials that occur in <code>a</code> but not
295: * in <code>b</code>. multiplicity is treated as well here, so
296: * this is really difference of multisets
297: */
298: private static ListOfMonomial difference(ListOfMonomial a,
299: ListOfMonomial b) {
300: ListOfMonomial res = a;
301: final IteratorOfMonomial it = b.iterator();
302: while (it.hasNext() && !res.isEmpty())
303: res = res.removeFirst(it.next());
304: return res;
305: }
306:
307: private static ListOfMonomial addPart(ListOfMonomial oldParts,
308: Monomial m) {
309: if (m.getCoefficient().signum() == 0)
310: return oldParts;
311: final ListOfMonomial newParts = addPartHelp(oldParts, m);
312: if (newParts != null)
313: return newParts;
314: return oldParts.prepend(m);
315: }
316:
317: private static ListOfMonomial addPartHelp(ListOfMonomial oldParts,
318: Monomial m) {
319: if (oldParts.isEmpty())
320: return null;
321: final Monomial head = oldParts.head();
322: final ListOfMonomial tail = oldParts.tail();
323: if (head.variablesEqual(m)) {
324: final Monomial newHead = head.addToCoefficient(m
325: .getCoefficient());
326: if (newHead.getCoefficient().signum() == 0)
327: return tail;
328: return tail.prepend(newHead);
329: }
330: final ListOfMonomial res = addPartHelp(tail, m);
331: if (res == null)
332: return null;
333: return res.prepend(head);
334: }
335:
336: public BigInteger getConstantTerm() {
337: return constantPart;
338: }
339:
340: public ListOfMonomial getParts() {
341: return parts;
342: }
343:
344: }
|