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.conditions;
12:
13: import de.uka.ilkd.key.java.Services;
14: import de.uka.ilkd.key.logic.op.SVSubstitute;
15: import de.uka.ilkd.key.logic.op.SchemaVariable;
16: import de.uka.ilkd.key.logic.sort.ObjectSort;
17: import de.uka.ilkd.key.logic.sort.Sort;
18: import de.uka.ilkd.key.rule.VariableConditionAdapter;
19: import de.uka.ilkd.key.rule.inst.SVInstantiations;
20:
21: /**
22: * This variable condition checks if a schemavariable is instantiated
23: * with a reference or primitive type
24: */
25: public class TypeCondition extends VariableConditionAdapter {
26:
27: private final TypeResolver resolver;
28:
29: private final boolean nonNull;
30:
31: private final boolean isReference;
32:
33: /**
34: * create a type condition
35: * @param var the TypeResolver for the type to be checked
36: * @param isReference check for reference or primitive type
37: * @param nonNull if Sort null should be allowed (only important when
38: * isReference is set to true)
39: */
40: public TypeCondition(TypeResolver tr, boolean isReference,
41: boolean nonNull) {
42: this .resolver = tr;
43: this .isReference = isReference;
44: this .nonNull = nonNull;
45: }
46:
47: /**
48: * checks if the condition for a correct instantiation is fulfilled
49: * @param p_var the template Variable to be instantiated
50: * @param candidate the SVSubstitute which is a candidate for an
51: * instantiation of var
52: * @param svInst the SVInstantiations that are already known to be needed
53: * @return true iff condition is fulfilled
54: */
55: public boolean check(SchemaVariable p_var, SVSubstitute candidate,
56: SVInstantiations svInst, Services services) {
57:
58: if (!resolver.isComplete(p_var, candidate, svInst, services)) {
59: // instantiation not yet complete
60: return true;
61: }
62: final Sort s = resolver.resolveSort(p_var, candidate, svInst,
63: services);
64:
65: if (isReference) {
66: return (s instanceof ObjectSort && (!nonNull || s != Sort.NULL));
67: } else {
68: return !(s instanceof ObjectSort);
69: }
70: }
71:
72: public String toString() {
73: String prefix = "\\isReference";
74: if (isReference && nonNull) {
75: prefix += "[non_null]";
76: }
77: return (isReference ? "" : "\\not") + prefix + "( " + resolver
78: + " )";
79: }
80:
81: }
|