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;
12:
13: import de.uka.ilkd.key.logic.sort.Sort;
14:
15: /** This class contains a term of type bool with the constraints it
16: * has to satisfy. In opposition to terms a ConstrainedFormula is not
17: * persistent.
18: */
19: public class ConstrainedFormula implements java.io.Serializable {
20:
21: private final Term term;
22: private final Constraint constraint;
23:
24: private final int hashCode;
25:
26: /** creates a new ConstrainedFormula
27: * @param term a Term of sort Sort.FORMULA
28: * @param constraint the Contraint that has to be satisfied
29: */
30: public ConstrainedFormula(Term term, Constraint constraint) {
31: if (term.sort() != Sort.FORMULA) {
32: throw new RuntimeException("A Term instead of a Formula");
33: }
34: this .term = term;
35: this .constraint = constraint;
36: this .hashCode = term.hashCode() * 13 + constraint.hashCode();
37: }
38:
39: /** creates a new ConstrainedFormula with the `empty' constraint
40: * BOTTOM.
41: * @param term a Term of sort Sort.FORMULA
42: */
43: public ConstrainedFormula(Term term) {
44: this (term, Constraint.BOTTOM);
45: }
46:
47: /** @return the stored Term */
48: public Term formula() {
49: return term;
50: }
51:
52: /** @return the stored Constraint */
53: public Constraint constraint() {
54: return constraint;
55: }
56:
57: /** equal if terms and constraints are equal */
58: public boolean equals(Object obj) {
59: if (this == obj) {
60: return true;
61: }
62: if (obj instanceof ConstrainedFormula) {
63: ConstrainedFormula cmp = (ConstrainedFormula) obj;
64: if (term.equals(cmp.formula())
65: && constraint.equals(cmp.constraint())) {
66: return true;
67: }
68: }
69: return false;
70: }
71:
72: /** String representation */
73: public String toString() {
74: return term + (constraint.isBottom() ? "" : "<<" + constraint);
75: }
76:
77: public int hashCode() {
78: return hashCode;
79: }
80: }
|