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: package de.uka.ilkd.key.logic.op;
12:
13: import de.uka.ilkd.key.logic.Name;
14: import de.uka.ilkd.key.logic.Term;
15: import de.uka.ilkd.key.logic.sort.Sort;
16:
17: public class Quantifier extends Op {
18:
19: /** creates a quantifier */
20: Quantifier(Name name) {
21: super (name);
22: }
23:
24: /**
25: * @return Sort.FORMULA
26: */
27: public Sort sort(Term[] term) {
28: return Sort.FORMULA;
29: }
30:
31: /**
32: * for convenience reasons
33: * @return Sort.FORMULA
34: */
35: public Sort sort(Term term) {
36: return Sort.FORMULA;
37: }
38:
39: /** @return true iff the subterm at postion 0 has Sort.FORMULA and the
40: * arity of the term is 1 and at least one variable is bound.
41: */
42: public boolean validTopLevel(Term term) {
43: if (term.arity() == 0)
44: return false;
45: if (term.varsBoundHere(0).size() == 0)
46: return false;
47: return term.sub(0).sort().equals(Sort.FORMULA);
48: }
49:
50: /** @return arity of the Quantifier as int. */
51: public int arity() {
52: return 1;
53: }
54:
55: }
|