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: /**
12: * Generated by the KeY-Tool
13: * created: APRIL 17, 2000
14: */package de.uka.ilkd.key.logic;
15:
16: import de.uka.ilkd.key.logic.op.ArrayOfQuantifiableVariable;
17: import de.uka.ilkd.key.logic.op.Operator;
18: import de.uka.ilkd.key.logic.op.QuantifiableVariable;
19: import de.uka.ilkd.key.logic.op.Quantifier;
20:
21: class QuantifierTerm extends Term {
22:
23: /**
24: * array of quantifiable variables
25: */
26: private final ArrayOfQuantifiableVariable varsBoundHere;
27:
28: /** sub term */
29: private final Term subTerm;
30:
31: /** depth of the term */
32: private final int depth;
33:
34: /**
35: * creates a quantifier term
36: * @param op Operator representing the Quantifier (all, exist) of this term
37: * @param varsBoundHere an array of Variable containing all variables
38: * bound by the quantifier
39: * @param sort the Sort of this Term (is bool)
40: */
41: public QuantifierTerm(Operator op,
42: QuantifiableVariable[] varsBoundHere, Term subTerm) {
43: this (op, new ArrayOfQuantifiableVariable(varsBoundHere),
44: subTerm);
45: }
46:
47: /**
48: * creates a quantifier term
49: * @param op Operator representing the Quantifier (all, exist) of this term
50: * @param varsBoundHere an array of Variable containing all variables
51: * bound by the quantifier
52: * @param sort the Sort of this Term (is bool)
53: */
54: public QuantifierTerm(Operator op,
55: ArrayOfQuantifiableVariable varsBoundHere, Term subTerm) {
56: super (op, ((Quantifier) op).sort(subTerm));
57: this .subTerm = subTerm;
58: this .depth = subTerm.depth() + 1;
59: this .varsBoundHere = varsBoundHere;
60: fillCaches();
61: }
62:
63: /**@return depth of the term */
64: public int depth() {
65: return depth;
66: }
67:
68: /** @return the variables the term bound direct if it is a Quantifier(term)
69: */
70: public ArrayOfQuantifiableVariable varsBoundHere(int n) {
71: return n == 0 ? varsBoundHere : EMPTY_VAR_LIST;
72: }
73:
74: /** @return n-th subterm (always the only one) */
75: public Term sub(int n) {
76: return subTerm;
77: }
78:
79: /** @return arity of the quantifier term 1 as int */
80: public int arity() {
81: return 1;
82: }
83:
84: }
|