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: package de.uka.ilkd.key.strategy.termProjection;
09:
10: import java.math.BigInteger;
11:
12: import de.uka.ilkd.key.java.Services;
13: import de.uka.ilkd.key.logic.PosInOccurrence;
14: import de.uka.ilkd.key.logic.Term;
15: import de.uka.ilkd.key.logic.TermBuilder;
16: import de.uka.ilkd.key.logic.op.AbstractMetaOperator;
17: import de.uka.ilkd.key.logic.op.TermSymbol;
18: import de.uka.ilkd.key.proof.Goal;
19: import de.uka.ilkd.key.rule.RuleApp;
20: import de.uka.ilkd.key.rule.metaconstruct.arith.Monomial;
21:
22: public abstract class AbstractDividePolynomialsProjection implements
23: ProjectionToTerm {
24:
25: private final ProjectionToTerm leftCoefficient, polynomial;
26:
27: protected AbstractDividePolynomialsProjection(
28: ProjectionToTerm leftCoefficient,
29: ProjectionToTerm polynomial) {
30: this .leftCoefficient = leftCoefficient;
31: this .polynomial = polynomial;
32: }
33:
34: public Term toTerm(RuleApp app, PosInOccurrence pos, Goal goal) {
35: final Term coeffT = leftCoefficient.toTerm(app, pos, goal);
36: final Term polyT = polynomial.toTerm(app, pos, goal);
37:
38: final Services services = goal.proof().getServices();
39: final BigInteger coeff = new BigInteger(AbstractMetaOperator
40: .convertToDecimalString(coeffT, services));
41:
42: return quotient(coeff, polyT, services);
43: }
44:
45: protected abstract Term divide(Monomial numerator,
46: BigInteger denominator, Services services);
47:
48: private Term quotient(BigInteger monoCoeff, Term rightPoly,
49: Services services) {
50: final TermSymbol add = services.getTypeConverter()
51: .getIntegerLDT().getArithAddition();
52: if (rightPoly.op() == add) {
53: final Term left = quotient(monoCoeff, rightPoly.sub(0),
54: services);
55: final Term right = quotient(monoCoeff, rightPoly.sub(1),
56: services);
57: return TermBuilder.DF.func(add, left, right);
58: }
59:
60: final Monomial rightMono = Monomial.create(rightPoly, services);
61: return divide(rightMono, monoCoeff, services);
62: }
63:
64: }
|