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: /** this class represents a logical variable */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.sort.Sort;
16: import de.uka.ilkd.key.rule.MatchConditions;
17:
18: public class LogicVariable extends TermSymbol implements
19: QuantifiableVariable, ParsableVariable {
20:
21: public LogicVariable(Name name, Sort sort) {
22: super (name, sort);
23: if (sort == Sort.FORMULA) {
24: throw new RuntimeException(
25: "Attempt to create logic variable of type formula");
26: }
27: }
28:
29: /**
30: * a match between two logic variables is possible if they have been assigned
31: * they are same or have been assigned to the same abstract name and the sorts
32: * are equal.
33: */
34: public MatchConditions match(SVSubstitute subst,
35: MatchConditions mc, Services services) {
36:
37: if (subst == this ) {
38: return mc;
39: }
40: if (subst instanceof LogicVariable) {
41: final LogicVariable lv = (LogicVariable) subst;
42: if (lv.sort() == sort()
43: && mc.renameTable().sameAbstractName(this , lv)) {
44: return mc;
45: }
46: }
47: return null;
48: }
49:
50: /** @return arity of the Variable as int */
51: public int arity() {
52: return 0;
53: }
54:
55: /** toString */
56: public String toString() {
57: return "" + name() + ":" + sort();
58: }
59:
60: }
|