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.expression.literal.IntLiteral;
017: import de.uka.ilkd.key.logic.*;
018: import de.uka.ilkd.key.logic.ldt.IntegerLDT;
019: import de.uka.ilkd.key.logic.op.AbstractMetaOperator;
020: import de.uka.ilkd.key.logic.op.Operator;
021: import de.uka.ilkd.key.logic.op.TermSymbol;
022: import de.uka.ilkd.key.util.Debug;
023: import de.uka.ilkd.key.util.LRUCache;
024:
025: /**
026: * Class for analysing and modifying monomial expressions over the integers
027: */
028: public class Monomial {
029:
030: private final ListOfTerm parts;
031: private final BigInteger coefficient;
032:
033: private Monomial(final ListOfTerm parts,
034: final BigInteger coefficient) {
035: this .parts = parts;
036: this .coefficient = coefficient;
037: }
038:
039: private static final LRUCache monomialCache = new LRUCache(2000);
040:
041: public static final Monomial ONE = new Monomial(
042: SLListOfTerm.EMPTY_LIST, BigInteger.ONE);
043:
044: public static Monomial create(Term monoTerm, Services services) {
045: Monomial res = (Monomial) monomialCache.get(monoTerm);
046: if (res == null) {
047: res = createHelp(monoTerm, services);
048: monomialCache.put(monoTerm, res);
049: }
050: return res;
051: }
052:
053: private static Monomial createHelp(Term monomial, Services services) {
054: final Analyser a = new Analyser(services);
055: a.analyse(monomial);
056: return new Monomial(a.parts, a.coeff);
057: }
058:
059: public Monomial setCoefficient(BigInteger c) {
060: return new Monomial(parts, c);
061: }
062:
063: public Monomial multiply(BigInteger c) {
064: return new Monomial(parts, coefficient.multiply(c));
065: }
066:
067: public Monomial multiply(Monomial m) {
068: return new Monomial(parts.prepend(m.parts), coefficient
069: .multiply(m.coefficient));
070: }
071:
072: public Monomial addToCoefficient(BigInteger c) {
073: return new Monomial(parts, coefficient.add(c));
074: }
075:
076: /**
077: * @return true iff the monomial <code>this</code> divides the monomial
078: * <code>m</code>
079: */
080: public boolean divides(Monomial m) {
081: if (m.coefficient.signum() == 0)
082: return true;
083: if (this .coefficient.signum() == 0)
084: return false;
085: if (m.coefficient.remainder(this .coefficient).signum() != 0)
086: return false;
087:
088: return difference(this .parts, m.parts).isEmpty();
089: }
090:
091: /**
092: * @return true iff the variables/parts of <code>this</code> subsume the
093: * variables of <code>m</code>, i.e., if each variable that
094: * occurs in <code>m</code> occurs in the same or a higher power
095: * in <code>this</code>
096: */
097: public boolean variablesSubsume(Monomial m) {
098: return this .parts.size() >= m.parts.size()
099: && difference(m.parts, this .parts).isEmpty();
100: }
101:
102: public boolean variablesEqual(Monomial m) {
103: return this .parts.size() == m.parts.size()
104: && this .variablesSubsume(m);
105: }
106:
107: public boolean variablesDisjoint(Monomial m) {
108: return difference(m.parts, this .parts).size() == m.parts.size();
109: }
110:
111: /**
112: * @return true iff the coefficient of <code>m</code> can be made smaller
113: * (absolutely) by subtracting a multiple of <code>this</code>
114: */
115: public boolean reducible(Monomial m) {
116: final BigInteger a = m.coefficient;
117: final BigInteger c = this .coefficient;
118:
119: if (LexPathOrdering.compare(a.add(c), a) >= 0
120: && LexPathOrdering.compare(a.subtract(c), a) >= 0)
121: return false;
122:
123: return difference(this .parts, m.parts).isEmpty();
124: }
125:
126: /**
127: * @return the result of dividing the monomial <code>m</code> by the
128: * monomial <code>this</code>
129: */
130: public Monomial reduce(Monomial m) {
131: final BigInteger a = m.coefficient;
132: final BigInteger c = this .coefficient;
133:
134: if (a.signum() == 0 || c.signum() == 0)
135: return new Monomial(SLListOfTerm.EMPTY_LIST,
136: BigInteger.ZERO);
137:
138: return new Monomial(difference(m.parts, this .parts),
139: LexPathOrdering.divide(a, c));
140: }
141:
142: /**
143: * @return the result of dividing the least common reducible (LCR) of
144: * monomial <code>m</code> and <code>this</code> by the monomial
145: * <code>this</code>
146: */
147: public Monomial divideLCR(Monomial m) {
148: Debug.assertFalse(coefficient.signum() == 0);
149: Debug.assertFalse(m.coefficient.signum() == 0);
150:
151: final ListOfTerm newParts = difference(m.parts, this .parts);
152:
153: final BigInteger gcd = coefficient.abs().gcd(
154: m.coefficient.abs());
155: return new Monomial(newParts, m.coefficient.divide(gcd));
156:
157: /*
158: The code for groebner bases over the integers. We do not use that
159: anymore and instead compute groebner bases over the rationals
160: (using pseudo-reduction)
161:
162: // in case one the coefficient of one of the monomials divides the other
163: // coefficient: simply make sure that the leading terms cancel out each
164: // other. this makes the whole algorithm a bit more robust concerning
165: // signs
166: if ( coefficient.remainder ( m.coefficient ).signum () == 0 )
167: return new Monomial ( newParts, BigInteger.ONE );
168: if ( m.coefficient.remainder ( coefficient ).signum () == 0 )
169: return new Monomial ( newParts, m.coefficient.divide ( coefficient ) );
170:
171: BigInteger cofactor = cofactor ( coefficient, m.coefficient );
172: // (any)one of the two cofactors has to be negated
173: if ( coefficient.compareTo ( m.coefficient ) < 0 )
174: cofactor = cofactor.negate ();
175:
176: return new Monomial ( newParts, cofactor );
177: */
178: }
179:
180: /**
181: * Extended euclidian algorithm for computing cofactors. This satisfies the
182: * equation <code>gcd(a,b)=a*cofactor(a,b)+b*cofactor(b,a)</code>
183: */
184: private BigInteger cofactor(BigInteger v0, BigInteger v1) {
185: final boolean neg = v0.signum() < 0;
186: v0 = v0.abs();
187: v1 = v1.abs();
188: BigInteger c0 = BigInteger.ONE;
189: BigInteger c1 = BigInteger.ZERO;
190: while (v1.signum() != 0) {
191: final BigInteger[] divRem = v0.divideAndRemainder(v1);
192: v0 = v1;
193: v1 = divRem[1];
194: final BigInteger newC = c0.subtract(c1.multiply(divRem[0]));
195: c0 = c1;
196: c1 = newC;
197: }
198: if (neg)
199: return c0.negate();
200: return c0;
201: }
202:
203: public Term toTerm(Services services) {
204: final TermSymbol mul = services.getTypeConverter()
205: .getIntegerLDT().getArithMultiplication();
206: Term res = null;
207:
208: final IteratorOfTerm it = parts.iterator();
209: if (it.hasNext()) {
210: res = it.next();
211: while (it.hasNext())
212: res = TermFactory.DEFAULT.createFunctionTerm(mul, res,
213: it.next());
214: }
215:
216: final IntLiteral lit = new IntLiteral(coefficient.toString());
217: final Term cTerm = services.getTypeConverter()
218: .convertToLogicElement(lit);
219:
220: if (res == null)
221: res = cTerm;
222: else if (!BigInteger.ONE.equals(coefficient))
223: res = TermFactory.DEFAULT.createFunctionTerm(mul, res,
224: cTerm);
225:
226: return res;
227: }
228:
229: public String toString() {
230: final StringBuffer res = new StringBuffer();
231: res.append(coefficient);
232:
233: final IteratorOfTerm it = parts.iterator();
234: while (it.hasNext())
235: res.append(" * " + it.next());
236:
237: return res.toString();
238: }
239:
240: private static class Analyser {
241: public BigInteger coeff = BigInteger.ONE;
242: public ListOfTerm parts = SLListOfTerm.EMPTY_LIST;
243: private final Services services;
244: private final Operator numbers, mul;
245:
246: public Analyser(final Services services) {
247: this .services = services;
248: final IntegerLDT intLDT = services.getTypeConverter()
249: .getIntegerLDT();
250: numbers = intLDT.getNumberSymbol();
251: mul = intLDT.getArithMultiplication();
252: }
253:
254: public void analyse(Term monomial) {
255: if (monomial.op() == mul) {
256: analyse(monomial.sub(0));
257: analyse(monomial.sub(1));
258: } else if (monomial.op() == numbers) {
259: final BigInteger c = new BigInteger(
260: AbstractMetaOperator.convertToDecimalString(
261: monomial, services));
262: coeff = coeff.multiply(c);
263: } else {
264: parts = parts.prepend(monomial);
265: }
266: }
267: }
268:
269: public boolean equals(Object o) {
270: if (o == this )
271: return true;
272:
273: if (!(o instanceof Monomial))
274: return false;
275:
276: final Monomial m = (Monomial) o;
277:
278: if (!coefficient.equals(m.coefficient))
279: return false;
280: if (parts.size() != m.parts.size())
281: return false;
282: return difference(parts, m.parts).isEmpty();
283: }
284:
285: public int hashCode() {
286: int res = coefficient.hashCode();
287: final IteratorOfTerm it = parts.iterator();
288: while (it.hasNext())
289: res += it.next().hashCode();
290: return res;
291: }
292:
293: /**
294: * @return the list of all terms that occur in <code>a</code> but not in
295: * <code>b</code>. multiplicity is treated as well here, so this
296: * is really difference of multisets
297: */
298: private static ListOfTerm difference(ListOfTerm a, ListOfTerm b) {
299: ListOfTerm res = a;
300: final IteratorOfTerm it = b.iterator();
301: while (it.hasNext() && !res.isEmpty())
302: res = res.removeFirst(it.next());
303: return res;
304: }
305:
306: public BigInteger getCoefficient() {
307: return coefficient;
308: }
309:
310: public ListOfTerm getParts() {
311: return parts;
312: }
313:
314: public boolean variablesAreCoprime(Monomial m) {
315: return difference(parts, m.parts).equals(parts);
316: }
317:
318: }
|