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: /* Generated by Together */
12:
13: package de.uka.ilkd.key.logic.op;
14:
15: import de.uka.ilkd.key.logic.Name;
16: import de.uka.ilkd.key.logic.Term;
17: import de.uka.ilkd.key.logic.sort.Sort;
18:
19: public class Junctor extends Op {
20:
21: private final int arity;
22:
23: /**
24: * Visibility set to protected as needs to be subclassed in ASMKeY.
25: * Creates a Junctor operator of the given name and arity.
26: */
27: protected Junctor(Name name, int arity) {
28: super (name);
29: this .arity = arity;
30: }
31:
32: public int arity() {
33: return arity;
34: }
35:
36: /** @return true iff all of the subterms of the given subterms
37: * have Sort.FORMULA
38: */
39: public boolean validTopLevel(Term term) {
40: if (arity() != term.arity())
41: return false;
42: for (int i = 0; i < term.arity(); i++) {
43: if (!term.sub(i).sort().equals(Sort.FORMULA))
44: return false;
45: }
46: return true;
47: }
48:
49: /**
50: *
51: * @return Sort.FORMULA
52: */
53: public Sort sort(Term[] term) {
54: return Sort.FORMULA;
55: }
56: }
|