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: /** Class representing the intersection of a set of constraints
018: * (i.e. of arbitrary objects implementing the
019: * "Constraint"-interface). Intersection means the constraint allowing
020: * an instantiation of metavariables iff there exists a constraint
021: * within the set allowing this instantiation.
022: */
023:
024: public class IntersectionConstraint implements Constraint {
025:
026: /**
027: * Elements of the set this constraint is the intersection of;
028: * objects having "subConstraints" with less than two elements are
029: * not well-formed, and the list must not contain two different
030: * elements from which one is stronger than the other.
031: */
032: private ListOfConstraint subConstraints = SLListOfConstraint.EMPTY_LIST;
033:
034: /**
035: * Use the static attributes of "Constraint" for new constraints
036: */
037: protected IntersectionConstraint() {
038: }
039:
040: /** returns true if Bottom
041: * @return true if Bottom
042: */
043: public boolean isBottom() {
044: // There is only one bottom element which is an
045: // EqualityConstraint
046: return false;
047: }
048:
049: /** a constraint being instance of this class is satisfiable. If a
050: * method realizes that an unsatisfiable Constraint would be built
051: * because of failed unification, cycle or s.th. similar it
052: * returns the singleton TOP being instance of the subclass Top
053: * @return true always
054: */
055: public boolean isSatisfiable() {
056: return true;
057: }
058:
059: /**
060: * Currently not needed, should return something more specific
061: */
062: public Term getInstantiation(Metavariable p_mv) {
063: return TermFactory.DEFAULT.createFunctionTerm(p_mv);
064: }
065:
066: /**
067: * Intersects p_c0 with p_c1, returning a constraint weaker or as
068: * strong as both p_c0 and p_c1.
069: * @param p_diff a constraint which is as strong (-> simple) as possible
070: * satisfying
071: * intersect ( p_c0, p_diff.val () ) == intersect ( p_c0, p_c1 )
072: */
073: public static Constraint intersect(Constraint p_c0,
074: Constraint p_c1, ConstraintContainer p_diff) {
075: if (p_c0 instanceof IntersectionConstraint)
076: return ((IntersectionConstraint) p_c0).intersectHelp(p_c1,
077: p_diff);
078:
079: IntersectionConstraint res = new IntersectionConstraint();
080: res.subConstraints = res.subConstraints.prepend(p_c0);
081: return res.intersectHelp(p_c1, p_diff);
082: }
083:
084: public static Constraint intersect(Constraint p_c0, Constraint p_c1) {
085: ConstraintContainer cc = new ConstraintContainer();
086: return intersect(p_c0, p_c1, cc);
087: }
088:
089: /**
090: * Intersects this constraint with p_co.
091: * @param p_diff a constraint which is as strong as possible
092: * satisfying
093: * this.intersectHelp ( p_diff.val () ) == this.intersectHelp ( p_co )
094: * @return A constraint representing the intersection of this and
095: * p_co
096: */
097: protected Constraint intersectHelp(Constraint p_co,
098: ConstraintContainer p_diff) {
099:
100: IntersectionConstraint res = new IntersectionConstraint();
101: BooleanContainer bc = new BooleanContainer();
102: IteratorOfConstraint it;
103: IntersectionConstraint diff = new IntersectionConstraint();
104: Constraint c;
105:
106: res.subConstraints = subConstraints;
107:
108: if (p_co instanceof IntersectionConstraint)
109: it = ((IntersectionConstraint) p_co).subConstraints
110: .iterator();
111: else
112: it = SLListOfConstraint.EMPTY_LIST.prepend(p_co).iterator();
113:
114: while (it.hasNext()) {
115: c = it.next();
116: res = res.intersectHelp2(c, bc);
117: if (!bc.val())
118: diff.subConstraints = diff.subConstraints.prepend(c);
119: }
120:
121: p_diff.setVal(diff.intersectSimplify());
122:
123: if (diff.subConstraints == SLListOfConstraint.EMPTY_LIST)
124: return intersectSimplify();
125:
126: res.subConstraints = res.subConstraints
127: .prepend(diff.subConstraints);
128: return res.intersectSimplify();
129:
130: }
131:
132: /**
133: * Removes all elements from "this.subConstraints" that are
134: * stronger than "p_co". Iff "p_co" is stronger than any element
135: * of "this.subConstraints", "p_stronger" is set to true (and
136: * "this" is returned). The return value may in fact be a not
137: * well-formed object of this class ("subConstraints" may be empty
138: * or contain only one element), that can be made correct by
139: * calling "intersectSimplify".
140: */
141: protected IntersectionConstraint intersectHelp2(Constraint p_co,
142: BooleanContainer p_stronger) {
143:
144: IntersectionConstraint res;
145: IteratorOfConstraint it;
146: Constraint c;
147:
148: res = new IntersectionConstraint();
149: it = subConstraints.iterator();
150:
151: while (it.hasNext()) {
152: c = it.next();
153:
154: // Constraint to add is stronger than an existing
155: // element (-> can be ignored)
156: if (p_co.isAsStrongAs(c)) {
157: p_stronger.setVal(true);
158: return this ;
159: }
160:
161: // Constraint to add is weaker than an existing
162: // element (-> this element can be removed)
163: if (!p_co.isAsWeakAs(c)) // otherwise keep the element
164: res.subConstraints = res.subConstraints.prepend(c);
165: }
166:
167: p_stronger.setVal(false);
168:
169: return res;
170:
171: }
172:
173: /**
174: * Make an "IntersectionConstraint" well-formed
175: */
176: protected Constraint intersectSimplify() {
177: if (subConstraints == SLListOfConstraint.EMPTY_LIST)
178: return Constraint.TOP;
179:
180: if (subConstraints.tail() == SLListOfConstraint.EMPTY_LIST)
181: return subConstraints.head();
182:
183: return this ;
184: }
185:
186: /** executes unification for terms t1 and t2
187: * @param t1 Term to be unified
188: * @param t2 term to be unified
189: * @param services a Namespace where new sorts that may be created when
190: * unifying are added. If the value is null unifying will fail if new sorts
191: * are required for a succesfull unification
192: * @return TOP if not possible, else a new constraint with after
193: * unification of t1 and t2
194: */
195: public Constraint unify(Term t1, Term t2, Services services) {
196: return join(Constraint.BOTTOM.unify(t1, t2, services), services);
197: }
198:
199: /** executes unification for terms t1 and t2.
200: * @param t1 Term to be unfied
201: * @param t2 Term to be unfied
202: * @param services a Namespace where new sorts that may be created when
203: * unifying are added. If the value is null unifying will fail if new sorts
204: * are required for a succesfull unification
205: * @param unchanged true iff the new constraint is subsumed by
206: * this one
207: * @return TOP if not possible, else a new constraint with after
208: * unification of t1 and t2
209: */
210: // TODO
211: public Constraint unify(Term t1, Term t2, Services services,
212: BooleanContainer unchanged) {
213: unchanged.setVal(false);
214: return unify(t1, t2, services);
215: }
216:
217: /** joins the given constraint with this constraint and returns
218: * the joint new constraint. Every implementing class should
219: * handle the cases co == TOP and ( co instanceof EqualityConstraint ).
220: * @param co Constraint to be joined with this one
221: * @para, sort_ns a Namespace where new sorts that may be created when
222: * unifying are added. If the value is null unifying and therewith joining
223: * will fail if new sorts are required
224: * @return the joined constraint
225: */
226: public Constraint join(Constraint co, Services services) {
227: IteratorOfConstraint it = subConstraints.iterator();
228: Constraint res = Constraint.TOP;
229:
230: while (it.hasNext())
231: res = IntersectionConstraint.intersect(res, co.join(it
232: .next(), services));
233:
234: return res;
235: }
236:
237: /** joins constraint co with this constraint and returns the joint
238: * new constraint. The BooleanContainer is used to wrap a second
239: * return value and indicates a subsumption of co by this
240: * constraint. Every implementing class should handle the cases co
241: * == TOP and ( co instanceof EqualityConstraint ).
242: * @param co Constraint to be joined with this one
243: * @param services a Namespace where new sorts that may be created when
244: * unifying are added. If the value is null unifying will fail if new sorts
245: * are required for a succesfull unification
246: * @param unchanged the BooleanContainers value set true, if this
247: * constraint is stronger than co (false may stand for "don't
248: * know")
249: * @return the joined constraint
250: */
251: // TODO
252: public Constraint join(Constraint co, Services services,
253: BooleanContainer unchanged) {
254: unchanged.setVal(false);
255: return join(co, services);
256: }
257:
258: /**
259: * @return a constraint derived from this one by removing all
260: * constraints on the given variable, which may therefore have any
261: * value according to the new constraint (the possible values of
262: * other variables are not modified)
263: */
264: public Constraint removeVariables(SetOfMetavariable mvs) {
265: if (mvs.iterator().hasNext()) {
266: Constraint res = Constraint.TOP;
267: IteratorOfConstraint it = subConstraints.iterator();
268:
269: while (it.hasNext())
270: res = intersect(res, it.next().removeVariables(mvs));
271:
272: return res;
273: }
274:
275: return this ;
276: }
277:
278: /** @return String representation of the constraint */
279: public String toString() {
280: return subConstraints.toString();
281: }
282:
283: /** checks equality of constraints by subsuming relation
284: */
285: public boolean equals(Object obj) {
286: if (obj instanceof Constraint) {
287: Constraint c = (Constraint) obj;
288: return isAsStrongAs(c) && isAsWeakAs(c);
289: }
290: return false;
291: }
292:
293: /**
294: * @return true iff this constraint is as strong as "co",
295: * i.e. every instantiation satisfying "this" also satisfies "co".
296: */
297: public boolean isAsStrongAs(Constraint co) {
298: IteratorOfConstraint it = subConstraints.iterator();
299: while (it.hasNext()) {
300: if (!it.next().isAsStrongAs(co))
301: return false;
302: }
303: return true;
304: }
305:
306: /**
307: * @return true iff this constraint is as weak as "co",
308: * i.e. every instantiation satisfying "co" also satisfies "this".
309: */
310: public boolean isAsWeakAs(Constraint co) {
311: if (co instanceof IntersectionConstraint) {
312: IteratorOfConstraint it = ((IntersectionConstraint) co).subConstraints
313: .iterator();
314: while (it.hasNext()) {
315: if (!isAsWeakAs(it.next()))
316: return false;
317: }
318: return true;
319: } else
320: return isAsWeakAsInteger(co);
321: }
322:
323: /**
324: * Same as "isAsWeakAs" for "co" not an IntersectionConstraint
325: */
326: protected boolean isAsWeakAsInteger(Constraint co) {
327: // Under some assumptions this can be reduced to: one element
328: // of this intersection is weaker than "co"
329: IteratorOfConstraint it = subConstraints.iterator();
330: while (it.hasNext()) {
331: if (it.next().isAsWeakAs(co))
332: return true;
333: }
334: return false;
335: }
336:
337: public int hashCode() {
338: //%% HACK
339: return 0;
340: }
341: }
|