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.IteratorOfTerm;
15: import de.uka.ilkd.key.logic.ListOfTerm;
16: import de.uka.ilkd.key.logic.Name;
17: import de.uka.ilkd.key.logic.Term;
18: import de.uka.ilkd.key.logic.op.IteratorOfIProgramVariable;
19: import de.uka.ilkd.key.logic.op.ListOfIProgramVariable;
20: import de.uka.ilkd.key.logic.op.ProgramVariable;
21: import de.uka.ilkd.key.logic.sort.ArrayOfSort;
22: import de.uka.ilkd.key.logic.sort.Sort;
23: import de.uka.ilkd.key.util.ExtList;
24:
25: /**
26: * Factory to create skolem symbols for terms
27: */
28: public class FunctionSkolemSymbolFactory extends SkolemSymbolFactory {
29:
30: public FunctionSkolemSymbolFactory(Services p_services) {
31: super (p_services);
32: }
33:
34: public Term createFunctionSymbol(Name p_name, Sort p_sort,
35: ListOfTerm p_logicArgs,
36: ListOfIProgramVariable p_influencingPVs) {
37: Term[] logicArgs = toArray(p_logicArgs);
38: Term[] pvArgs = createPVArgs(p_influencingPVs);
39:
40: Term[] realArgs = new Term[logicArgs.length + pvArgs.length];
41:
42: System.arraycopy(logicArgs, 0, realArgs, 0, logicArgs.length);
43: System.arraycopy(pvArgs, 0, realArgs, logicArgs.length,
44: pvArgs.length);
45:
46: SVSkolemFunction f = new SVSkolemFunction(p_name, p_sort,
47: new ArrayOfSort(sortsOf(logicArgs)),
48: getProgramVariableTypes(p_influencingPVs));
49: addFunction(f);
50:
51: return getTF().createFunctionTerm(f, realArgs);
52: }
53:
54: // Very inefficient
55: private Term[] createPVArgs(ListOfIProgramVariable pvp) {
56: IteratorOfIProgramVariable it = pvp.iterator();
57: ExtList res = new ExtList();
58:
59: while (it.hasNext())
60: res.add(getTF().createVariableTerm(
61: (ProgramVariable) it.next()));
62:
63: return (Term[]) res.collect(Term.class);
64: }
65:
66: // Very inefficient
67: private Term[] toArray(ListOfTerm p_list) {
68: IteratorOfTerm it = p_list.iterator();
69: ExtList res = new ExtList();
70:
71: while (it.hasNext())
72: res.add(it.next());
73:
74: return (Term[]) res.collect(Term.class);
75: }
76:
77: private Sort[] sortsOf(Term[] p_terms) {
78: Sort[] res = new Sort[p_terms.length];
79:
80: int j;
81: for (j = 0; j != p_terms.length; ++j)
82: res[j] = p_terms[j].sort();
83:
84: return res;
85: }
86:
87: }
|