001: // This file is part of KeY - Integrated Deductive Software Design
002: // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
003: // Universitaet Koblenz-Landau, Germany
004: // Chalmers University of Technology, Sweden
005: //
006: // The KeY system is protected by the GNU General Public License.
007: // See LICENSE.TXT for details.
008: //
009: //
010:
011: package de.uka.ilkd.key.rule.soundness;
012:
013: import de.uka.ilkd.key.java.JavaInfo;
014: import de.uka.ilkd.key.java.ProgramElement;
015: import de.uka.ilkd.key.java.Services;
016: import de.uka.ilkd.key.java.abstraction.*;
017: import de.uka.ilkd.key.logic.Name;
018: import de.uka.ilkd.key.logic.ProgramElementName;
019: import de.uka.ilkd.key.logic.Term;
020: import de.uka.ilkd.key.logic.TermFactory;
021: import de.uka.ilkd.key.logic.op.SchemaVariable;
022: import de.uka.ilkd.key.rule.inst.SVInstantiations;
023:
024: /**
025: * Abstract superclass of all skolem builders
026: */
027: public abstract class AbstractSkolemBuilder implements SkolemBuilder {
028:
029: private static int skolemCnt = 0;
030:
031: private final Services services;
032:
033: private final SkolemSet oriSkolemSet;
034: private SVInstantiations svi;
035:
036: public AbstractSkolemBuilder(SkolemSet p_oriSkolemSet,
037: Services p_services) {
038: oriSkolemSet = p_oriSkolemSet;
039: services = p_services;
040: setSVI(getOriginalSkolemSet().getInstantiations());
041: }
042:
043: /**
044: * The formula for which skolem symbols are to be created
045: */
046: protected Term getOriginalFormula() {
047: return getOriginalSkolemSet().getFormula();
048: }
049:
050: private void setSVI(SVInstantiations svi) {
051: this .svi = svi;
052: }
053:
054: protected SVInstantiations getSVI() {
055: return svi;
056: }
057:
058: /**
059: * The object that is to be enriched by further skolem symbols
060: */
061: protected SkolemSet getOriginalSkolemSet() {
062: return oriSkolemSet;
063: }
064:
065: protected IteratorOfSkolemSet toIterator(SkolemSet p) {
066: return SLListOfSkolemSet.EMPTY_LIST.prepend(p).iterator();
067: }
068:
069: protected KeYJavaType getObjectKeYJavaType() {
070: return getJavaInfo().getJavaLangObject();
071: }
072:
073: /**
074: * Add an instantiation to the SVInstantiations object
075: */
076: protected void addInstantiation(SchemaVariable p_sv, Term p_term) {
077: setSVI(getSVI().add(p_sv, p_term));
078: }
079:
080: /**
081: * Add an instantiation to the SVInstantiations object
082: */
083: protected void addInstantiation(SchemaVariable p_sv,
084: ProgramElement p_pe) {
085: setSVI(getSVI().add(p_sv, p_pe));
086: }
087:
088: /**
089: * Add an instantiation to the SVInstantiations object
090: */
091: protected void addInstantiation(SchemaVariable p_sv,
092: ProgramElement p_pe, int p_instantiationType) {
093: setSVI(getSVI().add(p_sv, p_pe, p_instantiationType));
094: }
095:
096: protected boolean isInstantiated(SchemaVariable p_sv) {
097: return getSVI().isInstantiated(p_sv);
098: }
099:
100: protected SVPartitioning getSVPartitioning() {
101: return getOriginalSkolemSet().getSVPartitioning();
102: }
103:
104: protected KeYJavaType getPartitionType(int p_variableNumber) {
105: return getSVPartitioning().getType(p_variableNumber,
106: getOriginalSkolemSet().getSVTypeInfos());
107: }
108:
109: /**
110: * Types that should be considered for untyped schema
111: * variables. Currently only primitive types and the object type
112: * are returned
113: */
114: protected IteratorOfKeYJavaType createTypeCandidates() {
115: final Type[] primitiveTypes = new Type[] {
116: PrimitiveType.JAVA_BYTE, PrimitiveType.JAVA_SHORT,
117: PrimitiveType.JAVA_INT, PrimitiveType.JAVA_CHAR,
118: PrimitiveType.JAVA_LONG,
119: // PrimitiveType.JAVA_FLOAT,
120: // PrimitiveType.JAVA_DOUBLE,
121: PrimitiveType.JAVA_BOOLEAN,
122: // NullType.JAVA_NULL
123: };
124:
125: ListOfKeYJavaType list = SLListOfKeYJavaType.EMPTY_LIST;
126: int i;
127:
128: for (i = 0; i != primitiveTypes.length; ++i)
129: list = list.prepend(getJavaInfo().getKeYJavaType(
130: primitiveTypes[i]));
131:
132: list = list.prepend(getObjectKeYJavaType());
133:
134: return list.iterator();
135: }
136:
137: protected Services getServices() {
138: return services;
139: }
140:
141: protected JavaInfo getJavaInfo() {
142: return getServices().getJavaInfo();
143: }
144:
145: /**
146: * HACK: Create a new and unique identifier
147: */
148: static Name createUniqueName(String baseName) {
149: return new Name(baseName + "_" + skolemCnt++);
150: }
151:
152: /**
153: * HACK: Create a new and unique identifier
154: */
155: static Name createUniqueName(Name baseName) {
156: return createUniqueName("" + baseName);
157: }
158:
159: /**
160: * HACK: Create a new and unique identifier
161: */
162: static ProgramElementName createUniquePEName(String baseName) {
163: return new ProgramElementName(baseName + "_" + skolemCnt++);
164: }
165:
166: /**
167: * HACK: Create a new and unique identifier
168: */
169: static ProgramElementName createUniquePEName(Name baseName) {
170: return createUniquePEName("" + baseName);
171: }
172:
173: protected TermFactory getTF() {
174: return TermFactory.DEFAULT;
175: }
176:
177: }
|