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.rule;
12:
13: import de.uka.ilkd.key.logic.op.SchemaVariable;
14: import de.uka.ilkd.key.logic.sort.Sort;
15:
16: /**
17: * variable condition used if a new variable is introduced
18: */
19: public class NewVarcond {
20:
21: private SchemaVariable sv;
22: private SchemaVariable asSort = null;
23: private Sort sort = null;
24: private boolean elementsort = false;
25:
26: public NewVarcond(SchemaVariable sv, SchemaVariable asSort) {
27: this .sv = sv;
28: this .asSort = asSort;
29: }
30:
31: /*
32: * @param sv the Schemavariable representing a new variable.
33: * @param asSort a Schemavariable defining the sort of the new variable.
34: * @param es true if asSort is an ArraySV and the sort of sv should be
35: * the same as the elementsort of asSort. false otherwise.
36: */
37: public NewVarcond(SchemaVariable sv, SchemaVariable asSort,
38: boolean es) {
39: this .sv = sv;
40: this .asSort = asSort;
41: elementsort = es;
42: }
43:
44: public NewVarcond(SchemaVariable sv, Sort sort) {
45: this .sv = sv;
46: this .sort = sort;
47: }
48:
49: public boolean isDefinedByType() {
50: return asSort == null;
51: }
52:
53: public SchemaVariable getSchemaVariable() {
54: return sv;
55: }
56:
57: public SchemaVariable getPeerSchemaVariable() {
58: return asSort;
59: }
60:
61: public Sort getSort() {
62: return sort;
63: }
64:
65: public boolean isDefinedByElementSort() {
66: return elementsort;
67: }
68:
69: public Object getSortDefiningObject() {
70: return isDefinedByType() ? (Object) getSort()
71: : (Object) getPeerSchemaVariable();
72: }
73:
74: public String toString() {
75: return "\\new("
76: + sv
77: + ", "
78: + (isDefinedByType() ? "" + sort
79: : (isDefinedByElementSort() ? "\\elemTypeof("
80: : "\\typeof(")
81: + getPeerSchemaVariable() + ")") + ")";
82: }
83:
84: }
|