001: // This file is part of KeY - Integrated Deductive Software Design
002: // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
003: // Universitaet Koblenz-Landau, Germany
004: // Chalmers University of Technology, Sweden
005: //
006: // The KeY system is protected by the GNU General Public License.
007: // See LICENSE.TXT for details.
008: //
009: //
010:
011: package de.uka.ilkd.key.logic;
012:
013: import de.uka.ilkd.key.java.Services;
014: import de.uka.ilkd.key.logic.op.Metavariable;
015: import de.uka.ilkd.key.logic.op.SetOfMetavariable;
016:
017: /** Abstract constraint interface for constraints offering unification
018: * of terms and joins. There are no public constructors to build up a
019: * new Constraint use the BOTTOM constraint (static final class
020: * variable) and add the needed constraints if a constraint would not
021: * be satisfiable (cycles, unification failed) the Constraint TOP is
022: * returned. TOP is as well as BOTTOM a static final class variable
023: * (means usage of singleton pattern for Constraints BOTTOM and TOP).
024: * Unsatisfiable constrains should only be representated by the TOP
025: * element.
026: */
027:
028: public interface Constraint {
029:
030: /** unsatisfiable Constraint */
031: Constraint TOP = new Top();
032: /** standard constraint class implementing the offered functionality */
033: Constraint BOTTOM = new EqualityConstraint();
034:
035: /**
036: * returns true if Bottom
037: * @return true if Bottom
038: */
039: boolean isBottom();
040:
041: /**
042: * a constraint being instance of this class is satisfiable. If a
043: * method realizes that an unsatisfiable Constraint would be built
044: * because of failed unification, cycle or s.th. similar it
045: * returns the singleton TOP being instance of the subclass Top
046: * @return true always
047: */
048: boolean isSatisfiable();
049:
050: /**
051: * @return Find a term the given metavariable can be instantiated
052: * with which is consistent with every instantiation that
053: * satisfies this constraint (that means, the term such an
054: * instantiation substitutes the metavariable with can always be
055: * unified with the returned term).
056: */
057: Term getInstantiation(Metavariable p_mv);
058:
059: /**
060: * tries to unify the terms t1 and t2
061: * @param t1 Term to be unified
062: * @param t2 Term to be unified
063: * @param services the Services providing access to the type model
064: * the parameter may be <code>null</code> but then the
065: * unification fails (i.e. @link Constraint#TOP is returned) when accessing
066: * the type model (e.g. for introducing intersection sorts) would be necessary).
067: *
068: * @return TOP if not possible, else a new constraint with after
069: * unification of t1 and t2
070: */
071: Constraint unify(Term t1, Term t2, Services services);
072:
073: /**
074: * tries to unify terms t1 and t2.
075: * @param t1 Term to be unfied
076: * @param t2 Term to be unfied
077: * @param services the Services providing access to the type model
078: * @param unchanged true iff the new constraint equals this one
079: * @return TOP if not possible, else a new constraint with after
080: * unification of t1 and t2
081: */
082: Constraint unify(Term t1, Term t2, Services services,
083: BooleanContainer unchanged);
084:
085: /**
086: * @return true iff this constraint is as strong as "co",
087: * i.e. every instantiation satisfying "this" also satisfies "co".
088: */
089: boolean isAsStrongAs(Constraint co);
090:
091: /**
092: * @return true iff this constraint is as weak as "co",
093: * i.e. every instantiation satisfying "co" also satisfies "this".
094: */
095: boolean isAsWeakAs(Constraint co);
096:
097: /** checks equality of constraints
098: */
099: boolean equals(Object obj);
100:
101: /** joins the given constraint with this constraint and returns
102: * the joint new constraint. Every implementing class should
103: * handle the cases co == TOP and ( co instanceof EqualityConstraint ).
104: * @param co Constraint to be joined with this one
105: * @param services the Services providing access to the type model
106: * @return the joined constraint
107: */
108: Constraint join(Constraint co, Services services);
109:
110: /** joins constraint co with this constraint and returns the joint
111: * new constraint. The BooleanContainer is used to wrap a second
112: * return value and indicates a subsumption of co by this
113: * constraint. Every implementing class should handle the cases co
114: * == TOP and ( co instanceof EqualityConstraint ).
115: * @param co Constraint to be joined with this one
116: * @param services the Services providing access to the type model
117: * @param unchanged the BooleanContainers value set true, if this
118: * constraint is as strong as co
119: * @return the joined constraint
120: */
121: Constraint join(Constraint co, Services services,
122: BooleanContainer unchanged);
123:
124: /**
125: * @return a constraint derived from this one by removing all
126: * constraints on the given variable, which may therefore have any
127: * value according to the new constraint (the possible values of
128: * other variables are not modified)
129: */
130: Constraint removeVariables(SetOfMetavariable mvs);
131:
132: /** @return String representation of the constraint */
133: String toString();
134:
135: /** Constraint class for representating the TOP (unsatisfiable) constraint. */
136: class Top implements Constraint {
137:
138: /** creation of TOP */
139: public Top() {
140: }
141:
142: /** is an unsatisfiable Constraint satisfiable? NO.
143: * @return always false
144: */
145: public boolean isSatisfiable() {
146: return false;
147: }
148:
149: public Term getInstantiation(Metavariable p_mv) {
150: // As there is in fact no instantiation satisfying this
151: // constraint, we could return everything
152: return TermFactory.DEFAULT.createFunctionTerm(p_mv);
153: }
154:
155: /** adding new constraints to an unsatisfiable constraint
156: * results in an unsatisfiable constraint so this one is returned
157: *
158: * @return always this
159: */
160: public Constraint unify(Term t1, Term t2, Services services) {
161: return this ;
162: }
163:
164: public Constraint unify(Term t1, Term t2, Services services,
165: BooleanContainer unchanged) {
166: unchanged.setVal(true);
167: return this ;
168: }
169:
170: public boolean equals(Object obj) {
171: return (obj instanceof Top);
172: }
173:
174: public boolean isAsStrongAs(Constraint co) {
175: // Nothing is stronger than this ...
176: return true;
177: }
178:
179: public boolean isAsWeakAs(Constraint co) {
180: // Nothing is stronger than this, except another Top
181: // instance
182: return (co instanceof Top);
183: }
184:
185: /** joint of Top and co is Top
186: * @return this
187: */
188: public Constraint join(Constraint co, Services services) {
189: return this ;
190: }
191:
192: /** joint of Top and co is Top and Top subsumes every constraint
193: * @return this
194: */
195: public Constraint join(Constraint co, Services services,
196: BooleanContainer c) {
197: c.setVal(true);
198: return this ;
199: }
200:
201: /** returns true if Bottom
202: * @return true if Bottom
203: */
204: public boolean isBottom() {
205: return false;
206: }
207:
208: /**
209: * @return a constraint derived from this one by removing all
210: * constraints on the given variable, which may therefore have any
211: * value according to the new constraint (the possible values of
212: * other variables are not modified)
213: */
214: public Constraint removeVariables(SetOfMetavariable mvs) {
215: // the constraint will still be unsatisfiable, as the
216: // other variables have no valid instantiations
217: return this ;
218: }
219:
220: /** @return String representing the TOP constraint
221: */
222: public String toString() {
223: return "TOP";
224: }
225:
226: public int hashCode() {
227: return 12345;
228: }
229: }
230:
231: }
|