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: package de.uka.ilkd.key.rule.metaconstruct.arith;
11:
12: import de.uka.ilkd.key.java.Services;
13: import de.uka.ilkd.key.logic.Name;
14: import de.uka.ilkd.key.logic.Term;
15: import de.uka.ilkd.key.logic.op.AbstractMetaOperator;
16: import de.uka.ilkd.key.rule.inst.SVInstantiations;
17:
18: /**
19: * Metaoperator for computing the result of dividing one monomial by another
20: */
21: public class DivideMonomials extends AbstractMetaOperator {
22:
23: public DivideMonomials() {
24: super (new Name("#divideMonomials"), 2);
25: }
26:
27: /**
28: * checks whether the top level structure of the given @link Term
29: * is syntactically valid, given the assumption that the top level
30: * operator of the term is the same as this Operator. The
31: * assumption that the top level operator and the term are equal
32: * is NOT checked.
33: * @return true iff the top level structure of
34: * the @link Term is valid.
35: */
36: public boolean validTopLevel(Term term) {
37: // a meta operator accepts almost everything
38: return term.op() instanceof DivideMonomials
39: && term.arity() == arity();
40: }
41:
42: /** calculates the resulting term. */
43: public Term calculate(Term term, SVInstantiations svInst,
44: Services services) {
45: final Term arg1 = term.sub(0);
46: final Term arg2 = term.sub(1);
47:
48: final Monomial m1 = Monomial.create(arg1, services);
49: final Monomial m2 = Monomial.create(arg2, services);
50:
51: final Monomial res = m2.reduce(m1);
52: return res.toTerm(services);
53: }
54:
55: }
|