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.termgenerator;
012:
013: import java.math.BigInteger;
014: import java.util.ArrayList;
015: import java.util.Iterator;
016: import java.util.List;
017:
018: import de.uka.ilkd.key.java.Services;
019: import de.uka.ilkd.key.logic.ConstrainedFormula;
020: import de.uka.ilkd.key.logic.IteratorOfConstrainedFormula;
021: import de.uka.ilkd.key.logic.IteratorOfTerm;
022: import de.uka.ilkd.key.logic.ListOfTerm;
023: import de.uka.ilkd.key.logic.PosInOccurrence;
024: import de.uka.ilkd.key.logic.SLListOfTerm;
025: import de.uka.ilkd.key.logic.Term;
026: import de.uka.ilkd.key.logic.ldt.IntegerLDT;
027: import de.uka.ilkd.key.logic.op.Op;
028: import de.uka.ilkd.key.proof.Goal;
029: import de.uka.ilkd.key.rule.RuleApp;
030: import de.uka.ilkd.key.rule.metaconstruct.arith.IteratorOfMonomial;
031: import de.uka.ilkd.key.rule.metaconstruct.arith.Monomial;
032: import de.uka.ilkd.key.rule.metaconstruct.arith.Polynomial;
033: import de.uka.ilkd.key.strategy.termProjection.ProjectionToTerm;
034:
035: /**
036: * Try to rewrite a monomial (term) <code>source</code> so that it becomes a
037: * multiple of another monomial <code>target</code>, using the integer
038: * equations of the antecedent. The output of the term generator is a list of
039: * polynomials <code>x</code> such that
040: * <code>x * target = source (modulo ...)</code>. This is done using the
041: * method introduced in "Automating elementary number-theoretic proofs using
042: * Groebner bases", 2007, John Harrison. Compared to the paper, we only perform
043: * a simplified Groebner basis computation, basically only consisting of
044: * reduction steps with polynomials that have a single monomial. This is already
045: * enough to handle many practical cases and to significantly improve polynomial
046: * division modulo equations.
047: *
048: * In the future, this class should also be used for instantiating explicit
049: * quantifiers over the integers.
050: */
051: public class MultiplesModEquationsGenerator implements TermGenerator {
052:
053: private final ProjectionToTerm source;
054: private final ProjectionToTerm target;
055:
056: private MultiplesModEquationsGenerator(ProjectionToTerm source,
057: ProjectionToTerm target) {
058: this .source = source;
059: this .target = target;
060: }
061:
062: public static TermGenerator create(ProjectionToTerm source,
063: ProjectionToTerm target) {
064: return new MultiplesModEquationsGenerator(source, target);
065: }
066:
067: public IteratorOfTerm generate(RuleApp app, PosInOccurrence pos,
068: Goal goal) {
069: final Services services = goal.proof().getServices();
070:
071: final Monomial sourceM = Monomial.create(source.toTerm(app,
072: pos, goal), services);
073: final Monomial targetM = Monomial.create(target.toTerm(app,
074: pos, goal), services);
075:
076: if (targetM.divides(sourceM))
077: return toIterator(targetM.reduce(sourceM).toTerm(services));
078:
079: final List cofactorPolys = extractPolys(goal, services);
080:
081: if (cofactorPolys.isEmpty())
082: return SLListOfTerm.EMPTY_LIST.iterator();
083:
084: return computeMultiples(sourceM, targetM, cofactorPolys,
085: services).iterator();
086: }
087:
088: private IteratorOfTerm toIterator(Term quotient) {
089: return SLListOfTerm.EMPTY_LIST.prepend(quotient).iterator();
090: }
091:
092: /**
093: * Compute multiples of <code>targetM</code> that are congruent to
094: * <code>sourceM</code> modulo the polynomials in
095: * <code>cofactorPolys</code>. The result is a list of terms x with the
096: * property <code>x * targetM = sourceM (modulo ...)</code>.
097: *
098: * This method will change the object <code>cofactorPolys</code>.
099: */
100: private ListOfTerm computeMultiples(Monomial sourceM,
101: Monomial targetM, List cofactorPolys, Services services) {
102: ListOfTerm res = SLListOfTerm.EMPTY_LIST;
103:
104: final List cofactorMonos = new ArrayList();
105: cofactorMonos
106: .add(new CofactorMonomial(targetM, Polynomial.ONE));
107:
108: boolean changed = true;
109: while (changed) {
110: changed = false;
111:
112: final Iterator polyIt = cofactorPolys.iterator();
113: while (polyIt.hasNext()) {
114: CofactorPolynomial poly = (CofactorPolynomial) polyIt
115: .next();
116:
117: final Iterator monoIt = cofactorMonos.iterator();
118: while (monoIt.hasNext()) {
119: final CofactorMonomial mono = (CofactorMonomial) monoIt
120: .next();
121: final CofactorItem reduced = poly.reduce(mono);
122: if (reduced instanceof CofactorMonomial) {
123: polyIt.remove();
124: cofactorMonos.add(reduced);
125: res = addRes((CofactorMonomial) reduced,
126: sourceM, res, services);
127: changed = true;
128: break;
129: } else {
130: poly = (CofactorPolynomial) reduced;
131: }
132: }
133: }
134: }
135:
136: return res;
137: }
138:
139: private ListOfTerm addRes(CofactorMonomial newMono,
140: Monomial sourceM, ListOfTerm res, Services services) {
141: final Monomial mono = newMono.mono;
142: final Polynomial cofactor = newMono.cofactor;
143:
144: if (mono.divides(sourceM)) {
145: final Polynomial quotient = cofactor.multiply(mono
146: .reduce(sourceM));
147:
148: // do not return zero, that's too easy
149: if (!quotient.getParts().isEmpty()
150: || quotient.getConstantTerm().signum() != 0)
151: return res.prepend(quotient.toTerm(services));
152: }
153: return res;
154: }
155:
156: /**
157: * Extract all integer equations of the antecedent and convert them into
158: * <code>Polynomial</code>s.
159: *
160: * @returns a list of polynomials, stored in objects of
161: * <code>CofactorPolynomial</code>. The initial cofactor is set
162: * to zero.
163: */
164: private List extractPolys(Goal goal, Services services) {
165: final IntegerLDT numbers = services.getTypeConverter()
166: .getIntegerLDT();
167:
168: final List res = new ArrayList();
169:
170: final IteratorOfConstrainedFormula it = goal.sequent()
171: .antecedent().iterator();
172: while (it.hasNext()) {
173: final ConstrainedFormula cfm = it.next();
174: if (!cfm.constraint().isBottom())
175: continue;
176:
177: final Term t = cfm.formula();
178: if (t.op() != Op.EQUALS
179: || !t.sub(0).sort().extendsTrans(
180: numbers.targetSort())
181: || !t.sub(1).sort().extendsTrans(
182: numbers.targetSort()))
183: continue;
184:
185: final Polynomial left = Polynomial.create(t.sub(0),
186: services);
187: final Polynomial right = Polynomial.create(t.sub(1),
188: services);
189:
190: res.add(new CofactorPolynomial(left.sub(right),
191: Polynomial.ZERO));
192: }
193:
194: return res;
195: }
196:
197: // Some classes to hold pairs of monomials/polynomials and cofactors (again
198: // polynomials).
199:
200: private static abstract class CofactorItem {
201: public final Polynomial cofactor;
202:
203: public CofactorItem(Polynomial cofactor) {
204: this .cofactor = cofactor;
205: }
206: }
207:
208: private static class CofactorMonomial extends CofactorItem {
209: public final Monomial mono;
210:
211: public CofactorMonomial(Monomial mono, Polynomial cofactor) {
212: super (cofactor);
213: this .mono = mono;
214: }
215: }
216:
217: private static class CofactorPolynomial extends CofactorItem {
218: public final Polynomial poly;
219:
220: public CofactorPolynomial(Polynomial poly, Polynomial cofactor) {
221: super (cofactor);
222: this .poly = poly;
223: }
224:
225: /**
226: * Add <code>coeff</code> times <code>mono</code> to this
227: * polynomial, adjusting the cofactor accordingly
228: */
229: public CofactorPolynomial add(CofactorMonomial mono,
230: Monomial coeff) {
231: return new CofactorPolynomial(poly.add(mono.mono
232: .multiply(coeff)), cofactor.add(mono.cofactor
233: .multiply(coeff)));
234: }
235:
236: /**
237: * Reduce the polynomial by adding a multiple of the monomial
238: * <code>mono</code>. The result is either
239: * <code>CofactorPolynomial</code> or <code>CofactorMonomial</code>,
240: * depending on whether the resulting polynomial has one or multiple
241: * monomials
242: */
243: public CofactorItem reduce(CofactorMonomial mono) {
244: CofactorPolynomial res = this ;
245: final IteratorOfMonomial it = poly.getParts().iterator();
246: while (it.hasNext()) {
247: final Monomial part = it.next();
248: if (mono.mono.divides(part)) {
249: final Monomial coeff = mono.mono.reduce(part);
250: res = res.add(mono, coeff.multiply(BigInteger
251: .valueOf(-1)));
252: }
253: }
254: if (res.poly.getParts().size() == 1
255: && res.poly.getConstantTerm().signum() == 0)
256: return new CofactorMonomial(res.poly.getParts().head(),
257: res.cofactor);
258: if (res.poly.getParts().size() == 0
259: && res.poly.getConstantTerm().signum() != 0)
260: return new CofactorMonomial(Monomial.ONE
261: .multiply(res.poly.getConstantTerm()),
262: res.cofactor);
263: return res;
264: }
265: }
266:
267: }
|