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: //This file is part of KeY - Integrated Deductive Software Design
09: // Copyright (C) 2001-2005 Universitaet Karlsruhe, Germany
10: // Universitaet Koblenz-Landau, Germany
11: // Chalmers University of Technology, Sweden
12: //
13: // The KeY system is protected by the GNU General Public License.
14: // See LICENSE.TXT for details.
15: //
16: //
17: package de.uka.ilkd.key.rule.metaconstruct.arith;
18:
19: import de.uka.ilkd.key.java.Services;
20: import de.uka.ilkd.key.logic.Name;
21: import de.uka.ilkd.key.logic.Term;
22: import de.uka.ilkd.key.logic.op.AbstractMetaOperator;
23: import de.uka.ilkd.key.rule.inst.SVInstantiations;
24:
25: /**
26: * Metaoperator for computing the result of dividing one monomial by another
27: */
28: public class DivideLCRMonomials extends AbstractMetaOperator {
29:
30: public DivideLCRMonomials() {
31: super (new Name("#divideLCRMonomials"), 2);
32: }
33:
34: /**
35: * checks whether the top level structure of the given
36: *
37: * @link Term is syntactically valid, given the assumption that the top
38: * level operator of the term is the same as this Operator. The
39: * assumption that the top level operator and the term are equal is
40: * NOT checked.
41: * @return true iff the top level structure of the
42: * @link Term is valid.
43: */
44: public boolean validTopLevel(Term term) {
45: // a meta operator accepts almost everything
46: return term.op() instanceof DivideLCRMonomials
47: && term.arity() == arity();
48: }
49:
50: /** calculates the resulting term. */
51: public Term calculate(Term term, SVInstantiations svInst,
52: Services services) {
53: final Term arg1 = term.sub(0);
54: final Term arg2 = term.sub(1);
55:
56: final Monomial m1 = Monomial.create(arg1, services);
57: final Monomial m2 = Monomial.create(arg2, services);
58:
59: final Monomial res = m2.divideLCR(m1);
60: return res.toTerm(services);
61: }
62:
63: }
|