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.Services;
014: import de.uka.ilkd.key.logic.*;
015: import de.uka.ilkd.key.logic.op.IteratorOfSchemaVariable;
016: import de.uka.ilkd.key.logic.op.SchemaVariable;
017: import de.uka.ilkd.key.logic.op.SortedSchemaVariable;
018: import de.uka.ilkd.key.logic.sort.Sort;
019: import de.uka.ilkd.key.rule.Taclet;
020:
021: /**
022: * Create skolem symbols for term and formula schema variables
023: */
024: public class FunctionSkolemBuilder extends
025: AbstractPVPrefixSkolemBuilder {
026:
027: private final Namespace skolemFunctions;
028: private final Taclet taclet;
029:
030: public FunctionSkolemBuilder(Taclet p_taclet,
031: SkolemSet p_oriSkolemSet,
032: ProgramVariablePrefixes p_prefixes, Services p_services) {
033: super (p_oriSkolemSet, p_prefixes, p_services);
034:
035: taclet = p_taclet;
036: skolemFunctions = new Namespace();
037: }
038:
039: public IteratorOfSkolemSet build() {
040: IteratorOfSchemaVariable it = getOriginalSkolemSet()
041: .getMissing().iterator();
042: SchemaVariable sv;
043:
044: while (it.hasNext()) {
045: sv = it.next();
046:
047: if (sv.isTermSV())
048: createSkolemTermSV((SortedSchemaVariable) sv);
049: else if (sv.isFormulaSV())
050: createSkolemFormulaSV((SortedSchemaVariable) sv);
051: }
052:
053: return toIterator(getOriginalSkolemSet().add(getSVI())
054: .addFunctions(skolemFunctions));
055: }
056:
057: private void addVocabulary(SkolemSymbolFactory p_factory) {
058: skolemFunctions.add(p_factory.getFunctions());
059: }
060:
061: private Term createSkolemFunction(SortedSchemaVariable p_sv,
062: Name p_name, Sort p_sort) {
063:
064: final FunctionSkolemSymbolFactory f = new FunctionSkolemSymbolFactory(
065: getServices());
066:
067: final Term t = f.createFunctionSymbol(p_name, p_sort,
068: createLogicArgs(p_sv), getProgramVariablePrefix(p_sv));
069:
070: addVocabulary(f);
071:
072: return t;
073: }
074:
075: // Very inefficient
076: private ListOfTerm createLogicArgs(SortedSchemaVariable p_sv) {
077: IteratorOfSchemaVariable it = taclet.getPrefix(p_sv).iterator();
078: ListOfTerm res = SLListOfTerm.EMPTY_LIST;
079:
080: while (it.hasNext())
081: res = res.append((Term) getSVI()
082: .getInstantiation(it.next()));
083:
084: return res;
085: }
086:
087: private void createSkolemTermSV(SortedSchemaVariable p_sv) {
088:
089: if (!isInstantiated(p_sv)) {
090: final Name name = createUniqueName(p_sv.name());
091: addInstantiation(p_sv, createSkolemFunction(p_sv, name,
092: p_sv.sort()));
093: }
094:
095: }
096:
097: private void createSkolemFormulaSV(SortedSchemaVariable p_sv) {
098: // currently formula skolem symbols are created just
099: // like function skolem symbols
100: createSkolemTermSV(p_sv);
101: }
102:
103: }
|