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: // Copyright (C) 2001-2005 Universitaet Karlsruhe, Germany
09: // Universitaet Koblenz-Landau, Germany
10: // Chalmers University of Technology, Sweden
11: //
12: // The KeY system is protected by the GNU General Public License.
13: // See LICENSE.TXT for details.
14: //
15: //
16:
17: package de.uka.ilkd.key.logic;
18:
19: import de.uka.ilkd.key.logic.op.Location;
20: import de.uka.ilkd.key.logic.op.Op;
21: import de.uka.ilkd.key.logic.sort.Sort;
22:
23: public class BasicLocationDescriptor implements LocationDescriptor {
24:
25: private final Term fma;
26: private final Term locTerm;
27: private final static Term trueTerm = TermFactory.DEFAULT
28: .createJunctorTerm(Op.TRUE);
29:
30: public BasicLocationDescriptor(Term fma, Term locTerm) {
31: assert fma != null && fma.sort() == Sort.FORMULA
32: && locTerm != null;
33: if (!(locTerm.op() instanceof Location)) {
34: throw new IllegalArgumentException(
35: "Expected a location, but " + locTerm + " is a "
36: + locTerm.op().getClass().getName());
37: }
38: this .fma = fma;
39: this .locTerm = locTerm;
40: }
41:
42: public BasicLocationDescriptor(Term locTerm) {
43: this (trueTerm, locTerm);
44: }
45:
46: public Term getFormula() {
47: return fma;
48: }
49:
50: public Term getLocTerm() {
51: return locTerm;
52: }
53:
54: public boolean equals(Object o) {
55: if (!(o instanceof BasicLocationDescriptor)) {
56: return false;
57: }
58: BasicLocationDescriptor ld = (BasicLocationDescriptor) o;
59: return fma.equals(ld.fma) && locTerm.equals(ld.locTerm);
60: }
61:
62: public int hashCode() {
63: return fma.hashCode() + locTerm.hashCode();
64: }
65:
66: public String toString() {
67: return (fma.equals(trueTerm) ? locTerm.toString() : "(" + fma
68: + "," + locTerm + ")");
69: }
70: }
|