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.soundness;
12:
13: import de.uka.ilkd.key.java.Services;
14: import de.uka.ilkd.key.logic.Name;
15: import de.uka.ilkd.key.logic.Term;
16: import de.uka.ilkd.key.logic.op.IteratorOfSchemaVariable;
17: import de.uka.ilkd.key.logic.op.LogicVariable;
18: import de.uka.ilkd.key.logic.op.SchemaVariable;
19: import de.uka.ilkd.key.logic.op.SortedSchemaVariable;
20:
21: /**
22: * Create logical variables as skolem symbols for variable schema
23: * variables
24: */
25: public class LogicVariableSkolemBuilder extends AbstractSkolemBuilder {
26:
27: public LogicVariableSkolemBuilder(SkolemSet p_oriSkolemSet,
28: Services p_services) {
29: super (p_oriSkolemSet, p_services);
30: }
31:
32: public IteratorOfSkolemSet build() {
33: IteratorOfSchemaVariable it = getOriginalSkolemSet()
34: .getMissing().iterator();
35: SchemaVariable sv;
36:
37: while (it.hasNext()) {
38: sv = it.next();
39:
40: if (sv.isVariableSV())
41: createSkolemVariableSV((SortedSchemaVariable) sv);
42: }
43:
44: return toIterator(getOriginalSkolemSet().add(getSVI()));
45: }
46:
47: private void createSkolemVariableSV(SortedSchemaVariable p_sv) {
48:
49: if (!isInstantiated(p_sv)) {
50: Name name = createUniqueName(p_sv.name());
51: LogicVariable var = new LogicVariable(name, p_sv.sort());
52: Term term = getTF().createVariableTerm(var);
53:
54: addInstantiation(p_sv, term);
55: }
56:
57: }
58:
59: }
|