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: package de.uka.ilkd.key.unittest.simplify.ast;
09:
10: import de.uka.ilkd.key.util.*;
11:
12: public class FunctionTerm extends Term {
13:
14: protected Function f;
15:
16: public FunctionTerm(Function f, ExtList l) {
17: super (f.name(), l);
18: this .f = f;
19: }
20:
21: public FunctionTerm(Function f) {
22: this (f, new ExtList());
23: }
24:
25: public Function getFunction() {
26: return f;
27: }
28:
29: public boolean isDivision() {
30: return arity() == 2 && f.name().startsWith("div_");
31: }
32:
33: public boolean isArithmetic() {
34: return isDivision() || f == Function.PLUS
35: || f == Function.MINUS || f == Function.MUL;
36: }
37:
38: }
|