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:
015: import de.uka.ilkd.key.java.Services;
016: import de.uka.ilkd.key.logic.IteratorOfTerm;
017: import de.uka.ilkd.key.logic.PosInOccurrence;
018: import de.uka.ilkd.key.logic.SLListOfTerm;
019: import de.uka.ilkd.key.logic.Term;
020: import de.uka.ilkd.key.logic.TermBuilder;
021: import de.uka.ilkd.key.logic.ldt.IntegerLDT;
022: import de.uka.ilkd.key.logic.op.AbstractMetaOperator;
023: import de.uka.ilkd.key.logic.op.Op;
024: import de.uka.ilkd.key.logic.op.Operator;
025: import de.uka.ilkd.key.proof.Goal;
026: import de.uka.ilkd.key.rule.RuleApp;
027: import de.uka.ilkd.key.rule.metaconstruct.arith.Monomial;
028: import de.uka.ilkd.key.strategy.termProjection.ProjectionToTerm;
029:
030: /**
031: * Term generator for infering the range of values that a variable can have from
032: * a given non-linear (in)equation. The generator may only be called on formulas
033: * of the form
034: * <tt>v^n = l</code>, <tt>v^n <= l</code>, <tt>v^n >= l</code>,
035: * where <tt>v</tt> is an atomic term (does not start with
036: * addition or multiplication) and <tt>l</tt> is a literal. The generator will
037: * then produce at most one formula that describes the solutions of the formula
038: * using linear (in)equations.
039: */
040: public class RootsGenerator implements TermGenerator {
041:
042: private final ProjectionToTerm powerRelation;
043:
044: final TermBuilder tb = TermBuilder.DF;
045: private final BigInteger one = BigInteger.ONE;
046: private final BigInteger two = BigInteger.valueOf(2);
047:
048: public static TermGenerator create(ProjectionToTerm powerRelation) {
049: return new RootsGenerator(powerRelation);
050: }
051:
052: private RootsGenerator(ProjectionToTerm powerRelation) {
053: this .powerRelation = powerRelation;
054: }
055:
056: public IteratorOfTerm generate(RuleApp app, PosInOccurrence pos,
057: Goal goal) {
058: final Services services = goal.proof().getServices();
059: final IntegerLDT numbers = services.getTypeConverter()
060: .getIntegerLDT();
061:
062: final Term powerRel = powerRelation.toTerm(app, pos, goal);
063:
064: final Operator op = powerRel.op();
065:
066: assert op.arity() == 2;
067:
068: final BigInteger lit = new BigInteger(AbstractMetaOperator
069: .convertToDecimalString(powerRel.sub(1), services));
070:
071: final Monomial mon = Monomial.create(powerRel.sub(0), services);
072: final int pow = mon.getParts().size();
073: if (pow <= 1 || !mon.getCoefficient().equals(one))
074: return emptyIterator();
075:
076: final Term var = mon.getParts().head();
077: if (!mon.getParts().removeAll(var).isEmpty())
078: return emptyIterator();
079:
080: if (op == numbers.getLessOrEquals()) {
081: return toIterator(breakDownLeq(var, lit, pow, services));
082: } else if (op == numbers.getGreaterOrEquals()) {
083: return toIterator(breakDownGeq(var, lit, pow, services));
084: } else if (op == Op.EQUALS) {
085: return toIterator(breakDownEq(var, lit, pow, services));
086: }
087:
088: return emptyIterator();
089: }
090:
091: private IteratorOfTerm emptyIterator() {
092: return SLListOfTerm.EMPTY_LIST.iterator();
093: }
094:
095: private IteratorOfTerm toIterator(Term res) {
096: if (res.equals(tb.ff()))
097: return emptyIterator();
098: return SLListOfTerm.EMPTY_LIST.prepend(res).iterator();
099: }
100:
101: private Term breakDownEq(Term var, BigInteger lit, int pow,
102: Services services) {
103: final Term zero = tb.zTerm(services, "0");
104:
105: if ((pow % 2 == 0)) {
106: // the even case
107:
108: switch (lit.signum()) {
109: case -1:
110: // no solutions
111: return tb.ff();
112: case 0:
113: // exactly one solution
114: return tb.equals(var, zero);
115: case 1:
116: final BigInteger r = root(lit, pow);
117: if (power(r, pow).equals(lit)) {
118: // two solutions
119: final Term rTerm = tb.zTerm(services, r.toString());
120: final Term rNegTerm = tb.zTerm(services, r.negate()
121: .toString());
122: return tb.or(tb.or(tb.lt(var, rNegTerm, services),
123: tb.gt(var, rTerm, services)), tb.and(tb.gt(
124: var, rNegTerm, services), tb.lt(var, rTerm,
125: services)));
126: } else {
127: // no solution
128: return tb.ff();
129: }
130: }
131: } else {
132: // the odd case
133:
134: final BigInteger r = root(lit, pow);
135: if (power(r, pow).equals(lit)) {
136: // one solution
137: final Term rTerm = tb.zTerm(services, r.toString());
138: return tb.equals(var, rTerm);
139: } else {
140: // no solution
141: return tb.ff();
142: }
143: }
144:
145: assert false; // unreachable
146: return null;
147: }
148:
149: private Term breakDownGeq(Term var, BigInteger lit, int pow,
150: Services services) {
151: if ((pow % 2 == 0)) {
152: // the even case
153:
154: switch (lit.signum()) {
155: case -1:
156: case 0:
157: // the inequation is no restriction
158: return tb.ff();
159: case 1:
160: final BigInteger r = rootRoundingUpwards(lit, pow);
161: final Term rTerm = tb.zTerm(services, r.toString());
162: final Term rNegTerm = tb.zTerm(services, r.negate()
163: .toString());
164: return tb.or(tb.leq(var, rNegTerm, services), tb.geq(
165: var, rTerm, services));
166: }
167: } else {
168: // the odd case
169:
170: return tb.geq(var, tb.zTerm(services, rootRoundingUpwards(
171: lit, pow).toString()), services);
172: }
173:
174: assert false; // unreachable
175: return null;
176: }
177:
178: private Term breakDownLeq(Term var, BigInteger lit, int pow,
179: Services services) {
180: if ((pow % 2 == 0)) {
181: // the even case
182:
183: switch (lit.signum()) {
184: case -1:
185: // no solutions
186: return tb.ff();
187: case 0:
188: return tb.equals(var, tb.zTerm(services, "0"));
189: case 1:
190: final BigInteger r = root(lit, pow);
191: final Term rTerm = tb.zTerm(services, r.toString());
192: final Term rNegTerm = tb.zTerm(services, r.negate()
193: .toString());
194: return tb.and(tb.geq(var, rNegTerm, services), tb.leq(
195: var, rTerm, services));
196: }
197: } else {
198: // the odd case
199:
200: return tb.leq(var, tb.zTerm(services, root(lit, pow)
201: .toString()), services);
202: }
203:
204: assert false; // unreachable
205: return null;
206: }
207:
208: /**
209: * @return a number <tt>res</tt> with the property
210: * <tt>prod in ((res-1)^exp, res^exp]</tt>
211: */
212: private BigInteger rootRoundingUpwards(BigInteger prod, int exp) {
213: final BigInteger res = root(prod, exp);
214: if (power(res, exp).compareTo(prod) < 0)
215: return res.add(one);
216: return res;
217: }
218:
219: /**
220: * @return a number <tt>res</tt> with the property
221: * <tt>prod in [res^exp, (res+1)^exp)</tt>
222: */
223: private BigInteger root(BigInteger prod, int exp) {
224: assert exp > 0;
225:
226: if (prod.signum() >= 0) {
227: return posRoot(prod, exp);
228: } else {
229: assert exp % 2 != 0;
230:
231: BigInteger res = posRoot(prod.abs(), exp).negate();
232: while (power(res, exp).compareTo(prod) > 0)
233: res = res.subtract(one);
234:
235: return res;
236: }
237: }
238:
239: private BigInteger posRoot(BigInteger prod, int exp) {
240: assert exp > 0;
241: assert prod.signum() >= 0;
242:
243: // binary search for finding the root
244:
245: BigInteger lb = BigInteger.ZERO;
246: BigInteger ub = prod;
247: while (!power(lb, exp).equals(prod)
248: && ub.subtract(lb).compareTo(one) > 0) {
249: final BigInteger mid = ub.add(lb).divide(two);
250: if (power(mid, exp).compareTo(prod) <= 0) {
251: lb = mid;
252: } else {
253: ub = mid;
254: }
255: }
256: return lb;
257: }
258:
259: private BigInteger power(BigInteger base, int exp) {
260: assert exp >= 0;
261:
262: // shift-multiplier
263:
264: BigInteger res = BigInteger.ONE;
265: while (true) {
266: if (exp % 2 != 0)
267: res = res.multiply(base);
268:
269: exp >>= 1;
270: if (exp == 0)
271: return res;
272:
273: base = base.multiply(base);
274: }
275: }
276: }
|