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: //
09: //
10:
11: package de.uka.ilkd.key.proof.decproc;
12:
13: import java.math.BigInteger;
14:
15: import de.uka.ilkd.key.logic.Term;
16: import de.uka.ilkd.key.logic.op.Operator;
17: import de.uka.ilkd.key.util.Debug;
18:
19: public final class NumberTranslation {
20:
21: private NumberTranslation() {
22: }
23:
24: /** This methods translates a term with sort "numbers" into a
25: * BigInteger representing the number.
26: *
27: * @param term term with sort "numbers"
28: * @return An instance of BigInteger representing the number
29: */
30: public static BigInteger translate(Term term) {
31: if (!term.sort().name().toString().trim().equals("numbers")) {
32: throw new IllegalArgumentException(
33: "Only terms with sort \"numbers\" may be translated.\n"
34: + "Term " + term + " is of sort "
35: + term.sort().name().toString().trim());
36: }
37: Operator op = term.op();
38: String name = op.name().toString();
39: if (name.length() == 1) {
40: char ch = name.charAt(0);
41: if (ch >= '0' && ch <= '9') {
42: Debug.assertTrue(term.arity() == 1);
43: return translate(term.sub(0)).multiply(smallInts[10])
44: .add(smallInts[ch - '0']);
45: } else if (ch == '#') {
46: Debug.assertTrue(term.arity() == 0);
47: return BigInteger.ZERO;
48: } else {
49: Debug.fail("unknown number literal");
50: return null; // not reached
51: }
52: } else if ("neglit".equals(name)) {
53: Debug.assertTrue(term.arity() == 1);
54: /* Hint: translate operator "neg" at all places
55: * correctly, e.g. neg(1(neg(1(#)))). */
56: return translate(term.sub(0)).negate();
57: } else {
58: Debug.fail("unknown number literal");
59: return null; // not reached
60: }
61: }
62:
63: /* BigInteger instances for values 0..10 */
64: private static final BigInteger[] smallInts;
65:
66: static {
67: /* initialize smallInts */
68: smallInts = new BigInteger[11];
69: for (int i = 0; i < smallInts.length; ++i) {
70: smallInts[i] = new BigInteger("" + i);
71: }
72: }
73:
74: }
|