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 java.util.HashSet;
014: import java.util.Iterator;
015:
016: import de.uka.ilkd.key.java.Services;
017: import de.uka.ilkd.key.java.abstraction.KeYJavaType;
018: import de.uka.ilkd.key.logic.Named;
019: import de.uka.ilkd.key.logic.Namespace;
020: import de.uka.ilkd.key.logic.op.*;
021: import de.uka.ilkd.key.rule.inst.ProgramSkolemInstantiation;
022: import de.uka.ilkd.key.rule.inst.SVInstantiations;
023: import de.uka.ilkd.key.util.Debug;
024: import de.uka.ilkd.key.util.ExtList;
025:
026: public class ProgramVariableSkolemBuilder extends AbstractSkolemBuilder {
027:
028: private final RawProgramVariablePrefixes rpvp;
029: private ListOfSkolemSet results = SLListOfSkolemSet.EMPTY_LIST;
030:
031: public ProgramVariableSkolemBuilder(SkolemSet p_oriSkolemSet,
032: RawProgramVariablePrefixes p_rpvp, Services p_services) {
033: super (p_oriSkolemSet, p_services);
034: rpvp = p_rpvp;
035: }
036:
037: public IteratorOfSkolemSet build() {
038: build(0, new HashSet(), getOriginalSkolemSet()
039: .getInstantiations());
040: return results.iterator();
041: }
042:
043: private void addResult(SkolemSet p) {
044: results = results.prepend(p);
045: }
046:
047: private void build(int p_variableNumber, HashSet p_usedVariables,
048: SVInstantiations p_currentSVI) {
049: if (p_variableNumber == getSVPartitioning().size()) {
050: addResult(getOriginalSkolemSet().addVariables(
051: toNamespace(p_usedVariables)).add(p_currentSVI));
052: return;
053: }
054:
055: if (getSVPartitioning().isExpressionSV(p_variableNumber)) {
056: // Expression schema variables are instantiated by a
057: // dedicated builder
058: build(p_variableNumber + 1, p_usedVariables, p_currentSVI);
059: return;
060: }
061:
062: PVCandidate[] pvs = createPVCandidates(p_variableNumber,
063: p_currentSVI, p_usedVariables);
064:
065: for (int i = 0; i != pvs.length; ++i) {
066: p_usedVariables.add(pvs[i].pv);
067:
068: build(p_variableNumber + 1, p_usedVariables, pvs[i].svi);
069:
070: p_usedVariables.remove(pvs[i].pv);
071: }
072: }
073:
074: private Namespace toNamespace(HashSet p_usedVariables) {
075: final Namespace vars = new Namespace();
076:
077: final Iterator it = p_usedVariables.iterator();
078: while (it.hasNext())
079: vars.add((Named) it.next());
080:
081: return vars;
082: }
083:
084: private PVCandidate[] createPVCandidates(int p_variableNumber,
085: SVInstantiations p_currentSVI, HashSet p_usedVars) {
086: final ExtList res = new ExtList();
087: final ListOfSchemaVariable svs = getSVPartitioning()
088: .getPartition(p_variableNumber);
089: final KeYJavaType type = getPartitionType(p_variableNumber);
090:
091: Debug.assertFalse(type == null, "Type of schema variables "
092: + svs + " should be determined at this point");
093:
094: if (getSVPartitioning().isNative(p_variableNumber))
095: createNativePVCandidates(svs, type, p_currentSVI,
096: p_usedVars, res);
097: else
098: createNewPVCandidate(svs, type, p_currentSVI, res,
099: ProgramSkolemInstantiation.NEW_BOUND_VARIABLE);
100:
101: return (PVCandidate[]) res.collect(PVCandidate.class);
102: }
103:
104: /**
105: * Instantiate the given set of schema variables with all existing
106: * program variables of type <code>p_type</code>, and add the
107: * resulting entries to the object <code>p_currentSVI</code>. The
108: * program variable as well as the new
109: * <code>SVInstantiations</code> object is added to
110: * <code>p_res</code> within an <code>PVCandidate</code> object.
111: * @param p_type the type the new variable is to be given
112: */
113: private void createNativePVCandidates(ListOfSchemaVariable p_svs,
114: KeYJavaType p_type, SVInstantiations p_currentSVI,
115: HashSet p_usedVars, ExtList p_res) {
116: final IteratorOfIProgramVariable nativeIt = rpvp
117: .getFreeProgramVariables().iterator();
118:
119: while (nativeIt.hasNext()) {
120: final IProgramVariable pv = nativeIt.next();
121:
122: if (p_usedVars.contains(pv)
123: || pv.getKeYJavaType() != p_type)
124: continue;
125:
126: final PVCandidate pvc = performInstantiation(p_currentSVI,
127: p_svs, pv,
128: ProgramSkolemInstantiation.OCCURRING_VARIABLE);
129:
130: p_res.add(pvc);
131: }
132: }
133:
134: /**
135: * Instantiate the given set of schema variables with a new
136: * program variable, and add the resulting entries to the object
137: * <code>p_currentSVI</code>. The created program variable as well
138: * as the new <code>SVInstantiations</code> object is added to
139: * <code>p_res</code> within an <code>PVCandidate</code> object.
140: * @param p_type the type the new variable is to be given
141: */
142: private void createNewPVCandidate(ListOfSchemaVariable p_svs,
143: KeYJavaType p_type, SVInstantiations p_currentSVI,
144: ExtList p_res, int p_instantiationType) {
145: final String baseName = "" + p_svs.head().name() + "_"
146: + p_type.getJavaType().getFullName();
147:
148: final IProgramVariable pv = new LocationVariable(
149: createUniquePEName(baseName), p_type);
150:
151: final PVCandidate pvc = performInstantiation(p_currentSVI,
152: p_svs, pv, p_instantiationType);
153:
154: p_res.add(pvc);
155: }
156:
157: private PVCandidate performInstantiation(
158: SVInstantiations p_currentSVI, ListOfSchemaVariable p_svs,
159: IProgramVariable p_pv, int p_instantiationType) {
160:
161: SVInstantiations svi = StaticCheckerSVI.addInstantiation(
162: p_currentSVI, p_svs, p_pv, p_instantiationType);
163:
164: Debug.assertFalse(svi == null, "Instantiation of " + p_svs
165: + " with program variable " + p_pv + " failed");
166:
167: return new PVCandidate(p_pv, svi);
168: }
169:
170: private static class PVCandidate {
171: public final IProgramVariable pv;
172: public final SVInstantiations svi;
173:
174: public PVCandidate(IProgramVariable p_pv, SVInstantiations p_svi) {
175: pv = p_pv;
176: svi = p_svi;
177: }
178: }
179: }
|