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: package de.uka.ilkd.key.rule.metaconstruct.arith;
011:
012: import java.math.BigInteger;
013:
014: import de.uka.ilkd.key.java.Services;
015: import de.uka.ilkd.key.java.expression.literal.IntLiteral;
016: import de.uka.ilkd.key.logic.Name;
017: import de.uka.ilkd.key.logic.Term;
018: import de.uka.ilkd.key.logic.op.AbstractMetaOperator;
019: import de.uka.ilkd.key.logic.op.Function;
020: import de.uka.ilkd.key.logic.op.RigidFunction;
021: import de.uka.ilkd.key.logic.sort.Sort;
022: import de.uka.ilkd.key.rule.inst.SVInstantiations;
023: import de.uka.ilkd.key.util.Debug;
024:
025: /** this class implements the interface for
026: * MetaAdderators. MetaAdderators are used to do complex term
027: * transformation when applying a taclet. Often these transformation
028: * caanot be described with the taclet scheme (or trying to do so would
029: * result in a huge number of rules)
030: */
031: public class MetaDiv extends AbstractMetaOperator {
032:
033: public MetaDiv() {
034: super (new Name("#div"), 2);
035: }
036:
037: /**
038: * checks whether the top level structure of the given @link Term
039: * is syntactically valid, given the assumption that the top level
040: * operator of the term is the same as this Operator. The
041: * assumption that the top level operator and the term are equal
042: * is NOT checked.
043: * @return true iff the top level structure of
044: * the @link Term is valid.
045: */
046: public boolean validTopLevel(Term term) {
047: // a meta operator accepts almost everything
048: return term.op() instanceof MetaDiv && term.arity() == arity();
049: }
050:
051: /**
052: * checks whether the result is consistent with the axiom div_axiom
053: */
054: private boolean checkResult(BigInteger a, BigInteger b,
055: BigInteger result) {
056:
057: // (gt(b,0) -> (leq(0,sub(a,mul(result,b))) & lt(sub(a,mul(result,b)),b)) )
058: if (b.compareTo(BigInteger.ZERO) > 0)
059: return ((BigInteger.ZERO.compareTo(a.subtract(result
060: .multiply(b))) <= 0) && (a.subtract(
061: result.multiply(b)).compareTo(b) < 0));
062:
063: // ( lt(b,0) -> (leq(0,sub(a,mul(result,b))) & lt(sub(a,mul(result,b)),neg(b))) )
064: if (b.compareTo(BigInteger.ZERO) < 0)
065: return ((BigInteger.ZERO.compareTo(a.subtract(result
066: .multiply(b))) <= 0) && (a.subtract(
067: result.multiply(b)).compareTo(b.negate()) < 0));
068:
069: return false;
070: }
071:
072: /** calculates the resulting term. */
073: public Term calculate(Term term, SVInstantiations svInst,
074: Services services) {
075: Term arg1 = term.sub(0);
076: Term arg2 = term.sub(1);
077: BigInteger bigIntArg1 = null;
078: BigInteger bigIntArg2 = null;
079:
080: bigIntArg1 = new BigInteger(convertToDecimalString(arg1,
081: services));
082: bigIntArg2 = new BigInteger(convertToDecimalString(arg2,
083: services));
084: if (bigIntArg2.compareTo(new BigInteger("0")) == 0) {
085: Name undefName = new Name("undef(" + term + ")");
086: Function undef = (Function) (services.getTypeConverter()
087: .getIntegerLDT().functions().lookup(undefName));
088: if (undef == null) {
089: undef = new RigidFunction(undefName, services
090: .getTypeConverter().getIntegerLDT()
091: .targetSort(), new Sort[0]);
092: services.getTypeConverter().getIntegerLDT()
093: .addFunction(undef);
094: }
095: return termFactory.createFunctionTerm(undef);
096: }
097: BigInteger remainder = bigIntArg1.remainder(bigIntArg2);
098: BigInteger bigIntResult = bigIntArg1.divide(bigIntArg2);
099: if (remainder.compareTo(BigInteger.ZERO) != 0) {
100: if (bigIntArg1.compareTo(BigInteger.ZERO) < 0)
101: if (bigIntArg2.compareTo(BigInteger.ZERO) > 0)
102: bigIntResult = bigIntResult
103: .subtract(BigInteger.ONE);
104: else
105: bigIntResult = bigIntResult.add(BigInteger.ONE);
106: }
107: IntLiteral lit = new IntLiteral(bigIntResult.toString());
108: Debug.assertTrue(checkResult(bigIntArg1, bigIntArg2,
109: bigIntResult), bigIntArg1 + "/" + bigIntArg2 + "="
110: + bigIntResult
111: + " is inconsistent with the taclet div_axiom");
112: return services.getTypeConverter().convertToLogicElement(lit);
113:
114: }
115:
116: }
|