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.logic.op;
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.sort.Sort;
17: import de.uka.ilkd.key.rule.MatchConditions;
18:
19: class SkolemTermSV extends SortedSchemaVariable {
20:
21: /**
22: * creates a new SchemaVariable. That is used as placeholder for
23: * skolem terms.
24: * @param name the Name of the SchemaVariable
25: * @param sort the Sort of the SchemaVariable and the matched type
26: * @param listSV a boolean which is true iff the schemavariable is
27: * allowed to match a list of program constructs
28: * @param strictSV boolean indicating if the schemavariable is declared as strict
29: * forcing exact type match
30: */
31: SkolemTermSV(Name name, Sort sort, boolean listSV) {
32: super (name, Term.class, sort, listSV);
33: if (sort == Sort.FORMULA) {
34: throw new RuntimeException(
35: "A SkolemTermSV is not allowed to"
36: + " have the sort " + sort);
37: }
38:
39: }
40:
41: /** returns true iff this SchemaVariable is used to match
42: * a term but not a formula
43: * @return true iff this SchemaVariable is used to match
44: * a term but not a formula
45: */
46: public boolean isSkolemTermSV() {
47: return true;
48: }
49:
50: public boolean isRigid() {
51: return true;
52: }
53:
54: /** toString */
55: public String toString() {
56: return toString(sort().toString() + " skolem term");
57: }
58:
59: /*
60: * @see de.uka.ilkd.key.logic.op.SortedSchemaVariable#match(de.uka.ilkd.key.logic.op.SVSubstitute, de.uka.ilkd.key.rule.MatchConditions, de.uka.ilkd.key.java.Services)
61: */
62: public MatchConditions match(SVSubstitute subst,
63: MatchConditions mc, Services services) {
64: return null;
65: }
66:
67: }
|