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 java.util.HashMap;
014: import java.util.Iterator;
015: import java.util.Map;
016:
017: import de.uka.ilkd.key.java.NameAbstractionTable;
018: import de.uka.ilkd.key.java.Services;
019: import de.uka.ilkd.key.logic.op.*;
020: import de.uka.ilkd.key.logic.sort.IntersectionSort;
021: import de.uka.ilkd.key.logic.sort.SetAsListOfSort;
022: import de.uka.ilkd.key.logic.sort.SetOfSort;
023: import de.uka.ilkd.key.logic.sort.Sort;
024: import de.uka.ilkd.key.rule.SyntacticalReplaceVisitor;
025:
026: /**
027: * This class implements a persistent constraint. The constraint
028: * contains pairs of Metavariables X and Terms t meaning X=t. It
029: * offers services like joining two Constraint objects, adding new
030: * constraints to this one by unfying two terms and creating all
031: * necessary Metavariable - Term pairs. There are no public
032: * constructors to build up a new Constraint use the BOTTOM constraint
033: * of the Constraint interface (static final class variable) and add
034: * the needed constraints. If a constraint would not be satisfiable
035: * (cycles, unification failed) the Constraint TOP of interface
036: * Constraint is returned.
037: */
038:
039: public class EqualityConstraint implements Constraint {
040:
041: /** contains a boolean value */
042: private static final BooleanContainer CONSTRAINTBOOLEANCONTAINER = new BooleanContainer();
043:
044: /** stores constraint content as a mapping from Metavariable to
045: * Term */
046: private HashMap map;
047:
048: /** cache for return values of getInstantiation */
049: private HashMap instantiationCache = null;
050:
051: private Integer hashCode = null;
052:
053: /** static meta variable counter */
054: private static long MV_COUNTER;
055:
056: /** Don't use this constructor, use Constraint.BOTTOM instead */
057: public EqualityConstraint() {
058: this (new HashMap());
059: }
060:
061: private EqualityConstraint(HashMap map) {
062: this .map = map;
063: }
064:
065: protected synchronized Object clone() {
066: EqualityConstraint res = new EqualityConstraint((HashMap) map
067: .clone());
068: res.instantiationCache = instantiationCache == null ? null
069: : (HashMap) instantiationCache.clone();
070: return res;
071: }
072:
073: /** returns true if Bottom
074: * @return true if Bottom
075: */
076: final public boolean isBottom() {
077: return map.isEmpty();
078: }
079:
080: /** a constraint being instance of this class is satisfiable. If a
081: * method realizes that an unsatisfiable Constraint would be built
082: * because of failed unification, cycle or s.th. similar it
083: * returns the singleton TOP being instance of the subclass Top
084: * @return true always
085: */
086: final public boolean isSatisfiable() {
087: return true;
088: }
089:
090: /**
091: * @return list of metavariables, instantiations of which may
092: * restricted by this constraint
093: */
094: public IteratorOfMetavariable restrictedMetavariables() {
095: return new MVIterator(map.keySet().iterator());
096: }
097:
098: private static class MVIterator implements IteratorOfMetavariable {
099: private Iterator it;
100:
101: public MVIterator(Iterator p_it) {
102: it = p_it;
103: }
104:
105: public boolean hasNext() {
106: return it.hasNext();
107: }
108:
109: public Metavariable next() {
110: return (Metavariable) it.next();
111: }
112: }
113:
114: /**
115: * @return The most general known term that is more defining than
116: * p_mv itself by which p_mv can be replaced if the constraint is
117: * valid (or null if the constraint allows arbitrary
118: * instantiations of p_mv). This is just the entry of map.
119: */
120: public Term getDirectInstantiation(Metavariable p_mv) {
121: return (Term) map.get(p_mv);
122: }
123:
124: /**
125: * @return the term by which p_mv is instantiated by the most
126: * general substitution satisfying the constraint
127: */
128: public synchronized Term getInstantiation(Metavariable p_mv) {
129: Term t = null;
130: if (instantiationCache == null)
131: instantiationCache = new HashMap();
132: else
133: t = (Term) instantiationCache.get(p_mv);
134:
135: if (t == null) {
136: t = (Term) map.get(p_mv);
137: if (t == null)
138: t = TermFactory.DEFAULT.createFunctionTerm(p_mv);
139: else
140: t = instantiate(t);
141:
142: instantiationCache.put(p_mv, t);
143: }
144:
145: return t;
146: }
147:
148: private synchronized Term getInstantiationIfExisting(
149: Metavariable p_mv) {
150: if (instantiationCache == null)
151: return null;
152: return (Term) instantiationCache.get(p_mv);
153: }
154:
155: /**
156: * instantiatiates term <code>p</code> according to the instantiations
157: * of the metavariables described by this constraint.
158: * @param p the Term p to be instantiated
159: * @return the instantiated term
160: */
161: private Term instantiate(Term p) {
162: SyntacticalReplaceVisitor srVisitor = new SyntacticalReplaceVisitor(
163: this );
164: p.execPostOrder(srVisitor);
165: return srVisitor.getTerm();
166: }
167:
168: /**
169: * unifies terms t1 and t2
170: * @param t1 Term to be unified
171: * @param t2 term to be unified
172: * @param services the Services providing access to the type model
173: * (e.g. necessary when introducing intersection sorts)
174: * @return TOP if not possible, else a new constraint with after
175: * unification of t1 and t2
176: */
177: public Constraint unify(Term t1, Term t2, Services services) {
178: return unify(t1, t2, services, CONSTRAINTBOOLEANCONTAINER);
179: }
180:
181: /** executes unification for terms t1 and t2.
182: * @param t1 Term to be unfied
183: * @param t2 Term to be unfied
184: * @param services the Services providing access to the type model
185: * (e.g. necessary when introducing intersection sorts)
186: * @param unchanged true iff the new constraint equals this one
187: * @return TOP if not possible, else a new constraint unifying t1
188: * and t2 ( == this iff this subsumes the unification )
189: */
190: public Constraint unify(Term t1, Term t2, Services services,
191: BooleanContainer unchanged) {
192: final Constraint newConstraint = unifyHelp(t1, t2, false,
193: services);
194:
195: if (!newConstraint.isSatisfiable()) {
196: unchanged.setVal(false);
197: return Constraint.TOP;
198: }
199:
200: if (newConstraint == this ) {
201: unchanged.setVal(true);
202: return this ;
203: }
204:
205: unchanged.setVal(false);
206: return newConstraint;
207: }
208:
209: /**
210: * compare two quantifiable variables if they are equal modulo renaming
211: * @param ownVar first QuantifiableVariable to be compared
212: * @param cmpVar second QuantifiableVariable to be compared
213: * @param ownBoundVars variables bound above the current position
214: * @param cmpBoundVars variables bound above the current position
215: */
216: private static boolean compareBoundVariables(
217: QuantifiableVariable ownVar, QuantifiableVariable cmpVar,
218: ListOfQuantifiableVariable ownBoundVars,
219: ListOfQuantifiableVariable cmpBoundVars) {
220:
221: final int ownNum = indexOf(ownVar, ownBoundVars);
222: final int cmpNum = indexOf(cmpVar, cmpBoundVars);
223:
224: if (ownNum == -1 && cmpNum == -1)
225: // if both variables are not bound the variables have to be the
226: // same object
227: return ownVar == cmpVar;
228:
229: // otherwise the variables have to be bound at the same point (and both
230: // be bound)
231: return ownNum == cmpNum;
232: }
233:
234: /**
235: * @return the index of the first occurrence of <code>var</code> in
236: * <code>list</code>, or <code>-1</code> if the variable is not
237: * an element of the list
238: */
239: private static int indexOf(QuantifiableVariable var,
240: ListOfQuantifiableVariable list) {
241: int res = 0;
242: while (!list.isEmpty()) {
243: if (list.head() == var)
244: return res;
245: ++res;
246: list = list.tail();
247: }
248: return -1;
249: }
250:
251: /**
252: * Compares two terms modulo bound renaming and return a (possibly new)
253: * constraint object that holds the instantiations necessary to make the two
254: * terms equal.
255: *
256: * @param t0
257: * the first term
258: * @param t1
259: * the second term
260: * @param ownBoundVars variables bound above the current position
261: * @param cmpBoundVars variables bound above the current position
262: * @param modifyThis
263: * <code>this</code> is an object that has just been created
264: * during this unification process
265: * @param services the Services providing access to the type model
266: * (e.g. necessary when introducing intersection sorts). Value
267: * <code>null</code> is allowed, but unification fails
268: * (i.e. @link Constraint#TOP is returned), if e.g. intersection sorts are required.
269: * @return a constraint under which t0, t1 are equal modulo bound renaming.
270: * <code>this</code> is returned iff the terms are equal modulo
271: * bound renaming under <code>this</code>, or
272: * <code>modifyThis==true</code> and the terms are unifiable. For
273: * <code>!modifyThis</code> a new object is created, and
274: * <code>this</code> is never modified.
275: * <code>Constraint.TOP</code> is always returned for ununifiable
276: * terms
277: */
278: private Constraint unifyHelp(Term t0, Term t1,
279: ListOfQuantifiableVariable ownBoundVars,
280: ListOfQuantifiableVariable cmpBoundVars,
281: NameAbstractionTable nat, boolean modifyThis,
282: Services services) {
283:
284: if (t0 == t1 && ownBoundVars.equals(cmpBoundVars))
285: return this ;
286:
287: final Operator op0 = t0.op();
288:
289: if (op0 instanceof QuantifiableVariable)
290: return handleQuantifiableVariable(t0, t1, ownBoundVars,
291: cmpBoundVars);
292:
293: final Operator op1 = t1.op();
294:
295: if (op1 instanceof Metavariable) {
296: if (op0 == op1)
297: return this ;
298:
299: if (op0 instanceof Metavariable)
300: return handleTwoMetavariables(t0, t1, modifyThis,
301: services);
302:
303: if (t0.sort().extendsTrans(t1.sort()))
304: return normalize((Metavariable) op1, t0, modifyThis,
305: services);
306:
307: return Constraint.TOP;
308: } else if (op0 instanceof Metavariable) {
309: if (t1.sort().extendsTrans(t0.sort()))
310: return normalize((Metavariable) op0, t1, modifyThis,
311: services);
312:
313: return Constraint.TOP;
314: }
315:
316: if (!(op0 instanceof ProgramVariable) && op0 != op1)
317: return Constraint.TOP;
318:
319: if (t0.sort() != t1.sort() || t0.arity() != t1.arity())
320: return Constraint.TOP;
321:
322: nat = handleJava(t0, t1, nat);
323: if (nat == FAILED)
324: return Constraint.TOP;
325:
326: return descendRecursively(t0, t1, ownBoundVars, cmpBoundVars,
327: nat, modifyThis, services);
328: }
329:
330: /**
331: * Resolve an equation <tt>X=Y</tt> (concerning two metavariables) by
332: * introducing a third variable <tt>Z</tt> whose sort is the intersection
333: * of the sorts of <tt>X</tt>,<tt>Y</tt> and adding equations
334: * <tt>X=Z</tt>,<tt>Y=Z</tt>. NB: This method must only be called if
335: * none of the sorts of <code>t0</code>,<code>t1</code> is subsort of
336: * the other one. Otherwise the resulting equation might get commuted,
337: * <tt>Z</tt> might occur on the left side of the new equations and
338: * horrible things will happen.
339: *
340: * @param t0
341: * @param t1
342: * @param services
343: * @return
344: */
345: private Constraint introduceNewMV(Term t0, Term t1,
346: boolean modifyThis, Services services) {
347: if (services == null)
348: return Constraint.TOP;
349:
350: final SetOfSort set = SetAsListOfSort.EMPTY_SET.add(t0.sort())
351: .add(t1.sort());
352:
353: final Sort intersectionSort = IntersectionSort
354: .getIntersectionSort(set, services);
355:
356: if (intersectionSort instanceof IntersectionSort
357: && ((IntersectionSort) intersectionSort)
358: .hasEmptyDomain()) {
359: return Constraint.TOP;
360: }
361:
362: // I think these MV will never occur in saved proofs, or?
363:
364: final Metavariable newMV = new Metavariable(new Name("#MV"
365: + (MV_COUNTER++)), intersectionSort);
366: final Term newMVTerm = TermFactory.DEFAULT
367: .createFunctionTerm(newMV);
368:
369: final Constraint addFirst = normalize((Metavariable) t0.op(),
370: newMVTerm, modifyThis, services);
371: if (!addFirst.isSatisfiable())
372: return Constraint.TOP;
373: return ((EqualityConstraint) addFirst).normalize(
374: (Metavariable) t1.op(), newMVTerm, modifyThis
375: || addFirst != this , services);
376: }
377:
378: /**
379: * used to encode that <tt>handleJava</tt> results in an unsatisfiable constraint
380: * (faster than using exceptions)
381: */
382: private static NameAbstractionTable FAILED = new NameAbstractionTable();
383:
384: private static NameAbstractionTable handleJava(Term t0, Term t1,
385: NameAbstractionTable nat) {
386:
387: if (t0.javaBlock() != JavaBlock.EMPTY_JAVABLOCK
388: || t1.javaBlock() != JavaBlock.EMPTY_JAVABLOCK) {
389: nat = checkNat(nat);
390: if (!t0.javaBlock().equalsModRenaming(t1.javaBlock(), nat)) {
391: return FAILED;
392: }
393: }
394:
395: if (!(t0.op() instanceof SchemaVariable)
396: && t0.op() instanceof ProgramVariable) {
397: if (!(t1.op() instanceof ProgramVariable)) {
398: return FAILED;
399: }
400: nat = checkNat(nat);
401: if (!((ProgramVariable) t0.op()).equalsModRenaming(
402: (ProgramVariable) t1.op(), nat)) {
403: return FAILED;
404: }
405: }
406:
407: return nat;
408: }
409:
410: private Constraint descendRecursively(Term t0, Term t1,
411: ListOfQuantifiableVariable ownBoundVars,
412: ListOfQuantifiableVariable cmpBoundVars,
413: NameAbstractionTable nat, boolean modifyThis,
414: Services services) {
415: Constraint newConstraint = this ;
416:
417: for (int i = 0; i < t0.arity(); i++) {
418: ListOfQuantifiableVariable subOwnBoundVars = ownBoundVars;
419: ListOfQuantifiableVariable subCmpBoundVars = cmpBoundVars;
420:
421: if (t0.varsBoundHere(i).size() != t1.varsBoundHere(i)
422: .size())
423: return Constraint.TOP;
424: for (int j = 0; j < t0.varsBoundHere(i).size(); j++) {
425: final QuantifiableVariable ownVar = t0.varsBoundHere(i)
426: .getQuantifiableVariable(j);
427: final QuantifiableVariable cmpVar = t1.varsBoundHere(i)
428: .getQuantifiableVariable(j);
429: if (ownVar.sort() != cmpVar.sort())
430: return Constraint.TOP;
431:
432: subOwnBoundVars = subOwnBoundVars.prepend(ownVar);
433: subCmpBoundVars = subCmpBoundVars.prepend(cmpVar);
434: }
435:
436: newConstraint = ((EqualityConstraint) newConstraint)
437: .unifyHelp(t0.sub(i), t1.sub(i), subOwnBoundVars,
438: subCmpBoundVars, nat, modifyThis, services);
439:
440: if (!newConstraint.isSatisfiable())
441: return Constraint.TOP;
442: modifyThis = modifyThis || newConstraint != this ;
443: }
444:
445: return newConstraint;
446: }
447:
448: private static NameAbstractionTable checkNat(
449: NameAbstractionTable nat) {
450: if (nat == null)
451: return new NameAbstractionTable();
452: return nat;
453: }
454:
455: private Constraint handleTwoMetavariables(Term t0, Term t1,
456: boolean modifyThis, Services services) {
457: final Metavariable mv0 = (Metavariable) t0.op();
458: final Metavariable mv1 = (Metavariable) t1.op();
459: final Sort mv0S = mv0.sort();
460: final Sort mv1S = mv1.sort();
461: if (mv1S.extendsTrans(mv0S)) {
462: if (mv0S == mv1S) {
463: // sorts are equal use Metavariable-order to choose the left MV
464: if (mv0.compareTo(mv1) >= 0)
465: return normalize(mv0, t1, modifyThis, services);
466: return normalize(mv1, t0, modifyThis, services);
467: }
468: return normalize(mv0, t1, modifyThis, services);
469: } else if (mv0S.extendsTrans(mv1S)) {
470: return normalize(mv1, t0, modifyThis, services);
471: }
472:
473: // The sorts are incompatible. This is resolved by creating a new
474: // metavariable and by splitting the equation into two
475: return introduceNewMV(t0, t1, modifyThis, services);
476: }
477:
478: private Constraint handleQuantifiableVariable(Term t0, Term t1,
479: ListOfQuantifiableVariable ownBoundVars,
480: ListOfQuantifiableVariable cmpBoundVars) {
481: if (!((t1.op() instanceof QuantifiableVariable) && compareBoundVariables(
482: (QuantifiableVariable) t0.op(),
483: (QuantifiableVariable) t1.op(), ownBoundVars,
484: cmpBoundVars)))
485: return Constraint.TOP;
486: return this ;
487: }
488:
489: /**
490: * Unify t1 and t2
491: * @param modifyThis
492: * <code>this</code> is an object that has just been created
493: * during this unification process
494: * @param services the Services providing access to the type model
495: *
496: * @return a constraint under which t0, t1 are equal modulo bound renaming.
497: * <code>this</code> is returned iff the terms are equal modulo
498: * bound renaming under <code>this</code>, or
499: * <code>modifyThis==true</code> and the terms are unifiable. For
500: * <code>!modifyThis</code> a new object is created, and
501: * <code>this</code> is never modified.
502: * <code>Constraint.TOP</code> is always returned for ununifiable
503: * terms
504: */
505: private Constraint unifyHelp(Term t1, Term t2, boolean modifyThis,
506: Services services) {
507: return unifyHelp(t1, t2,
508: SLListOfQuantifiableVariable.EMPTY_LIST,
509: SLListOfQuantifiableVariable.EMPTY_LIST, null,
510: modifyThis, services);
511: }
512:
513: /**
514: * checks for cycles and adds additional constraints if necessary
515: *
516: * PRECONDITION: the sorts of mv and t match; if t is also a
517: * metavariable with same sort as mv, the order of mv and t is
518: * correct (using Metavariable.compareTo)
519: *
520: * @param mv Metavariable asked to be mapped to the term t
521: * @param t the Term the metavariable should be mapped to (if there
522: * are no cycles )
523: * @param services the Services providing access to the type model
524: * @return the resulting Constraint ( == this iff this subsumes
525: * the new constraint )
526: */
527: private Constraint normalize(Metavariable mv, Term t,
528: boolean modifyThis, Services services) {
529: // MV cycles are impossible if the orders of MV pairs are
530: // correct
531:
532: if (!t.isRigid())
533: return Constraint.TOP;
534:
535: // metavariable instantiations must not contain free variables
536: if (t.freeVars().size() != 0
537: || (modifyThis ? hasCycle(mv, t)
538: : hasCycleByInst(mv, t))) // cycle
539: return Constraint.TOP;
540: else if (map.containsKey(mv))
541: return unifyHelp(valueOf(mv), t, modifyThis, services);
542:
543: final EqualityConstraint newConstraint = getMutableConstraint(modifyThis);
544: newConstraint.map.put(mv, t);
545:
546: return newConstraint;
547: }
548:
549: private EqualityConstraint getMutableConstraint(boolean modifyThis) {
550: if (modifyThis)
551: return this ;
552: return new EqualityConstraint((HashMap) map.clone());
553: }
554:
555: /**
556: * checks equality of constraints by subsuming relation (only equal if no
557: * new sorts need to be introduced for subsumption)
558: */
559: public boolean equals(Object obj) {
560: if (this == obj)
561: return true;
562: if (obj instanceof Constraint) {
563: Constraint c = (Constraint) obj;
564: if (c instanceof EqualityConstraint)
565: return map.keySet().equals(
566: ((EqualityConstraint) c).map.keySet())
567: && join(c, null) == this
568: && c.join(this , null) == c;
569: return isAsStrongAs(c) && isAsWeakAs(c);
570: }
571: return false;
572: }
573:
574: /**
575: * @return true iff this constraint is as strong as "co",
576: * i.e. every instantiation satisfying "this" also satisfies "co".
577: */
578: public boolean isAsStrongAs(Constraint co) {
579: if (this == co)
580: return true;
581: if (co instanceof EqualityConstraint)
582: // use necessary condition for this relation: key set of
583: // this is superset of key set of co
584: return map.keySet().containsAll(
585: ((EqualityConstraint) co).map.keySet())
586: && join(co, null) == this ;
587: return co.isAsWeakAs(this );
588: }
589:
590: /**
591: * @return true iff this constraint is as weak as "co",
592: * i.e. every instantiation satisfying "co" also satisfies "this".
593: */
594: public boolean isAsWeakAs(Constraint co) {
595: if (this == co)
596: return true;
597: if (co instanceof EqualityConstraint)
598: // use necessary condition for this relation: key set of
599: // co is superset of key set of this
600: return ((EqualityConstraint) co).map.keySet().containsAll(
601: map.keySet())
602: && co.join(this , null) == co;
603: return co.isAsStrongAs(this );
604: }
605:
606: /** joins the given constraint with this constraint
607: * and returns the joint new constraint.
608: * @param co Constraint to be joined with this one
609: * @return the joined constraint
610: */
611: public Constraint join(Constraint co, Services services) {
612: return join(co, services, CONSTRAINTBOOLEANCONTAINER);
613: }
614:
615: /** joins constraint co with this constraint
616: * and returns the joint new constraint. The BooleanContainer is
617: * used to wrap a second return value and indicates a subsumption
618: * of co by this constraint.
619: * @param co Constraint to be joined with this one
620: * @param services the Services providing access to the type model
621: * @param unchanged the BooleanContainers value set true, if this
622: * constraint is as strong as co
623: * @return the joined constraint
624: */
625: public synchronized Constraint join(Constraint co,
626: Services services, BooleanContainer unchanged) {
627: if (co.isBottom() || co == this ) {
628: unchanged.setVal(true);
629: return this ;
630: } else if (isBottom()) {
631: unchanged.setVal(false);
632: return co;
633: }
634:
635: if (!(co instanceof EqualityConstraint)) {
636: // BUG: Don't know how to set p_subsumed (at least not
637: // efficiently)
638: unchanged.setVal(false);
639: return co.join(this , services);
640: }
641:
642: final ECPair cacheKey;
643:
644: lookup: synchronized (joinCacheMonitor) {
645: ecPair0.set(this , co);
646: Constraint res = (Constraint) joinCache.get(ecPair0);
647:
648: if (res == null) {
649: cacheKey = ecPair0.copy();
650: res = (Constraint) joinCacheOld.get(cacheKey);
651: if (res == null)
652: break lookup;
653: joinCache.put(cacheKey, res);
654: }
655:
656: unchanged.setVal(this == res);
657: return res;
658: }
659:
660: final Constraint res = joinHelp((EqualityConstraint) co,
661: services);
662:
663: unchanged.setVal(res == this );
664:
665: synchronized (joinCacheMonitor) {
666: if (joinCache.size() > 1000) {
667: joinCacheOld.clear();
668: final HashMap t = joinCacheOld;
669: joinCacheOld = joinCache;
670: joinCache = t;
671: }
672:
673: joinCache.put(cacheKey, res);
674: return res;
675: }
676: }
677:
678: private Constraint joinHelp(EqualityConstraint co, Services services) {
679: Iterator it = co.map.entrySet().iterator();
680: Constraint newConstraint = this ;
681: boolean newCIsNew = false;
682: Map.Entry entry;
683:
684: while (it.hasNext()) {
685: entry = (Map.Entry) it.next();
686: newConstraint = ((EqualityConstraint) newConstraint)
687: .normalize((Metavariable) entry.getKey(),
688: (Term) entry.getValue(), newCIsNew,
689: services);
690: if (!newConstraint.isSatisfiable())
691: return Constraint.TOP;
692: newCIsNew = newCIsNew || newConstraint != this ;
693: }
694:
695: if (newConstraint == this )
696: return this ;
697:
698: return newConstraint;
699: }
700:
701: /**
702: * @return a constraint derived from this one by removing all
703: * constraints on the given variable, which may therefore have any
704: * value according to the new constraint (the possible values of
705: * other variables are not modified)
706: */
707: public Constraint removeVariables(SetOfMetavariable mvs) {
708: if (mvs != SetAsListOfMetavariable.EMPTY_SET && !isBottom()) {
709: Iterator it = map.entrySet().iterator();
710: Map.Entry entry;
711: EqualityConstraint removeConstraint = new EqualityConstraint();
712: EqualityConstraint newConstraint = new EqualityConstraint();
713:
714: // Find equalities with removed metavariable as left side
715: while (it.hasNext()) {
716: entry = (Map.Entry) it.next();
717: if (mvs.contains((Metavariable) entry.getKey()))
718: removeConstraint.map.put(entry.getKey(), entry
719: .getValue());
720: else
721: newConstraint.map.put(entry.getKey(), entry
722: .getValue());
723: }
724:
725: // Find equalities with removed metavariable as right side
726: it = newConstraint.map.entrySet().iterator();
727: while (it.hasNext()) {
728: entry = (Map.Entry) it.next();
729: if (((Term) entry.getValue()).op() instanceof Metavariable
730: && (((Metavariable) entry.getKey()).sort() == ((Term) entry
731: .getValue()).sort())
732: && (mvs.contains((Metavariable) ((Term) entry
733: .getValue()).op()))
734: && !(removeConstraint.map
735: .containsKey(((Term) entry.getValue())
736: .op()))) {
737: removeConstraint.map.put(((Term) entry.getValue())
738: .op(), TermFactory.DEFAULT
739: .createFunctionTerm((Metavariable) entry
740: .getKey()));
741: it.remove();
742: }
743: }
744:
745: if (!removeConstraint.map.isEmpty()) {
746: // Substitute removed variables occurring within right
747: // sides of the remaining equalities
748:
749: // Usually at this point removeConstraint is not a
750: // well-formed constraint, as the order of MV may be
751: // wrong. However, "SyntacticalReplaceVisitor" doesn't
752: // care about that.
753: if (newConstraint.map.isEmpty())
754: return Constraint.BOTTOM;
755:
756: it = newConstraint.map.entrySet().iterator();
757: newConstraint = new EqualityConstraint();
758:
759: while (it.hasNext()) {
760: entry = (Map.Entry) it.next();
761: newConstraint.map.put(entry.getKey(),
762: removeConstraint.instantiate((Term) entry
763: .getValue()));
764: }
765:
766: return newConstraint;
767: }
768: }
769:
770: return this ;
771: }
772:
773: /** checks if there is a cycle if the metavariable mv and Term
774: * term would be added to this constraint e.g. X=g(Y), Y=f(X)
775: * @param mv the Metavariable
776: * @param term The Term
777: * @return a boolean that is true iff. adding a mapping (mv,term)
778: * would cause a cycle
779: */
780: private boolean hasCycle(Metavariable mv, Term term) {
781: ListOfMetavariable body = SLListOfMetavariable.EMPTY_LIST;
782: ListOfTerm fringe = SLListOfTerm.EMPTY_LIST;
783: Term checkForCycle = term;
784:
785: while (true) {
786: final IteratorOfMetavariable it = checkForCycle.metaVars()
787: .iterator();
788: while (it.hasNext()) {
789: final Metavariable termMV = it.next();
790: if (!body.contains(termMV)) {
791: final Term termMVterm = getInstantiationIfExisting(termMV);
792: if (termMVterm != null) {
793: if (termMVterm.metaVars().contains(mv))
794: return true;
795: } else {
796: if (map.containsKey(termMV))
797: fringe = fringe.prepend((Term) map
798: .get(termMV));
799: }
800:
801: if (termMV == mv)
802: return true;
803:
804: body = body.prepend(termMV);
805: }
806: }
807:
808: if (fringe == SLListOfTerm.EMPTY_LIST)
809: return false;
810:
811: checkForCycle = fringe.head();
812: fringe = fringe.tail();
813: }
814: }
815:
816: private boolean hasCycleByInst(Metavariable mv, Term term) {
817: final IteratorOfMetavariable it = term.metaVars().iterator();
818:
819: while (it.hasNext()) {
820: final Metavariable termMV = it.next();
821: if (termMV == mv)
822: return true;
823: final Term termMVterm = getInstantiationIfExisting(termMV);
824: if (termMVterm != null) {
825: if (termMVterm.metaVars().contains(mv))
826: return true;
827: } else {
828: if (map.containsKey(termMV)
829: && hasCycle(mv, getDirectInstantiation(termMV)))
830: return true;
831: }
832: }
833:
834: return false;
835: }
836:
837: /**
838: * ONLY FOR TESTS DONT USE THEM IN ANOTHER WAY
839: *
840: * @return true if metavar is contained as key
841: */
842: boolean isDefined(Metavariable mv) {
843: return map.containsKey(mv);
844: }
845:
846: /** ONLY FOR TESTS DONT USE THEM IN ANOTHER WAY
847: * @return mapping to mv */
848: Term valueOf(Metavariable mv) {
849: return (Term) map.get(mv);
850: }
851:
852: /** @return String representation of the constraint */
853: public String toString() {
854: return map.toString();
855: }
856:
857: private static final class ECPair {
858: private Constraint first;
859: private Constraint second;
860: private int hash;
861:
862: public boolean equals(Object o) {
863: if (!(o instanceof ECPair))
864: return false;
865: final ECPair e = (ECPair) o;
866: return first == e.first && second == e.second;
867: }
868:
869: public void set(Constraint first, Constraint second) {
870: this .first = first;
871: this .second = second;
872: this .hash = first.hashCode() + second.hashCode();
873: }
874:
875: public int hashCode() {
876: return hash;
877: }
878:
879: public ECPair copy() {
880: return new ECPair(first, second, hash);
881: }
882:
883: public ECPair(Constraint first, Constraint second) {
884: set(first, second);
885: }
886:
887: public ECPair(Constraint first, Constraint second, int hash) {
888: this .first = first;
889: this .second = second;
890: this .hash = hash;
891: }
892: }
893:
894: private static final Boolean joinCacheMonitor = Boolean.FALSE;
895:
896: private static HashMap joinCache = new HashMap();
897: private static HashMap joinCacheOld = new HashMap();
898:
899: private static final ECPair ecPair0 = new ECPair(null, null, 0);
900:
901: public int hashCode() {
902: if (hashCode == null) {
903: int h = 0;
904: final IteratorOfMetavariable it = restrictedMetavariables();
905: while (it.hasNext()) {
906: final Metavariable mv = it.next();
907: h += mv.hashCode();
908: h += getInstantiation(mv).hashCode();
909: }
910:
911: hashCode = new Integer(h);
912: }
913:
914: return hashCode.intValue();
915: }
916: }
|