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: //This file is part of KeY - Integrated Deductive Software Design
009: //Copyright (C) 2001-2005 Universitaet Karlsruhe, Germany
010: // Universitaet Koblenz-Landau, Germany
011: // Chalmers University of Technology, Sweden
012: //
013: //The KeY system is protected by the GNU General Public License.
014: //See LICENSE.TXT for details.
015: //
016: //
017:
018: package de.uka.ilkd.key.strategy.quantifierHeuristics;
019:
020: import de.uka.ilkd.key.logic.IteratorOfTerm;
021: import de.uka.ilkd.key.logic.ListOfTerm;
022: import de.uka.ilkd.key.logic.SLListOfTerm;
023: import de.uka.ilkd.key.logic.SetOfTerm;
024: import de.uka.ilkd.key.logic.Term;
025: import de.uka.ilkd.key.logic.op.IteratorOfQuantifiableVariable;
026: import de.uka.ilkd.key.logic.op.ListOfQuantifiableVariable;
027: import de.uka.ilkd.key.logic.op.MapFromQuantifiableVariableToTerm;
028: import de.uka.ilkd.key.logic.op.QuantifiableVariable;
029: import de.uka.ilkd.key.logic.op.Quantifier;
030: import de.uka.ilkd.key.logic.op.SLListOfQuantifiableVariable;
031: import de.uka.ilkd.key.logic.op.SetOfQuantifiableVariable;
032: import de.uka.ilkd.key.util.LRUCache;
033:
034: class UniTrigger extends Trigger {
035:
036: private final Term trigger;
037: private final SetOfQuantifiableVariable uqvs;
038:
039: private final TriggersSet triggerSetThisBelongsTo;
040:
041: private final boolean onlyUnify;
042: private final boolean isElementOfMultitrigger;
043:
044: private final LRUCache matchResults = new LRUCache(1000);
045:
046: UniTrigger(Term trigger, SetOfQuantifiableVariable uqvs,
047: boolean isUnify, boolean isElementOfMultitrigger,
048: TriggersSet triggerSetThisBelongsTo) {
049: this .trigger = trigger;
050: this .uqvs = uqvs;
051: this .onlyUnify = isUnify;
052: this .isElementOfMultitrigger = isElementOfMultitrigger;
053: this .triggerSetThisBelongsTo = triggerSetThisBelongsTo;
054: }
055:
056: public SetOfSubstitution getSubstitutionsFromTerms(
057: SetOfTerm targetTerm) {
058: SetOfSubstitution allsubs = SetAsListOfSubstitution.EMPTY_SET;
059: final IteratorOfTerm it = targetTerm.iterator();
060: while (it.hasNext())
061: allsubs = allsubs
062: .union(getSubstitutionsFromTerm(it.next()));
063: return allsubs;
064: }
065:
066: private SetOfSubstitution getSubstitutionsFromTerm(Term t) {
067: SetOfSubstitution res = (SetOfSubstitution) matchResults.get(t);
068: if (res == null) {
069: res = getSubstitutionsFromTermHelp(t);
070: matchResults.put(t, res);
071: }
072: return res;
073: }
074:
075: private SetOfSubstitution getSubstitutionsFromTermHelp(Term t) {
076: SetOfSubstitution newSubs = SetAsListOfSubstitution.EMPTY_SET;
077: if (t.freeVars().size() > 0 || t.op() instanceof Quantifier)
078: newSubs = Matching.twoSidedMatching(this , t);
079: else if (!onlyUnify)
080: newSubs = Matching.basicMatching(this , t);
081: return newSubs;
082: }
083:
084: public Term getTriggerTerm() {
085: return trigger;
086: }
087:
088: public boolean equals(Object arg0) {
089: if (!(arg0 instanceof UniTrigger))
090: return false;
091: final UniTrigger a = (UniTrigger) arg0;
092: return a.trigger.equals(trigger);
093: }
094:
095: public int hashCode() {
096: return trigger.hashCode();
097: }
098:
099: public String toString() {
100: return "" + trigger;
101: }
102:
103: SetOfQuantifiableVariable getUniVariables() {
104: return uqvs;
105: }
106:
107: public TriggersSet getTriggerSetThisBelongsTo() {
108: return triggerSetThisBelongsTo;
109: }
110:
111: /**
112: * use similar algorithm as basic matching to detect loop
113: *
114: * @param candidate
115: * @param searchTerm
116: * @return
117: */
118: public static boolean passedLoopTest(Term candidate, Term searchTerm) {
119: final SetOfSubstitution substs = BasicMatching
120: .getSubstitutions(candidate, searchTerm);
121:
122: final IteratorOfSubstitution it = substs.iterator();
123: while (it.hasNext()) {
124: final Substitution subst = it.next();
125: if (containsLoop(subst))
126: return false;
127: }
128: return true;
129: }
130:
131: /**
132: * Test whether this substitution constains loop.
133: * It is mainly used for unitrigger's loop test.
134: */
135: private static boolean containsLoop(Substitution subst) {
136: final IteratorOfQuantifiableVariable it = subst.getVarMap()
137: .keyIterator();
138: while (it.hasNext()) {
139: if (containsLoop(subst.getVarMap(), it.next()))
140: return true;
141: }
142: return false;
143: }
144:
145: /**
146: * Code copied from logic.EqualityConstraint
147: */
148: private static boolean containsLoop(
149: MapFromQuantifiableVariableToTerm varMap,
150: QuantifiableVariable var) {
151: ListOfQuantifiableVariable body = SLListOfQuantifiableVariable.EMPTY_LIST;
152: ListOfTerm fringe = SLListOfTerm.EMPTY_LIST;
153: Term checkForCycle = varMap.get(var);
154:
155: if (checkForCycle.op() == var)
156: return false;
157:
158: while (true) {
159: final IteratorOfQuantifiableVariable it = checkForCycle
160: .freeVars().iterator();
161: while (it.hasNext()) {
162: final QuantifiableVariable termVar = it.next();
163: if (!body.contains(termVar)) {
164: final Term termVarterm = varMap.get(termVar);
165: if (termVarterm != null) {
166: if (termVarterm.freeVars().contains(var))
167: return true;
168: fringe = fringe.prepend(termVarterm);
169: }
170:
171: if (termVar == var)
172: return true;
173:
174: body = body.prepend(termVar);
175: }
176: }
177:
178: if (fringe == SLListOfTerm.EMPTY_LIST)
179: return false;
180:
181: checkForCycle = fringe.head();
182: fringe = fringe.tail();
183: }
184: }
185:
186: boolean isElementOfMultitrigger() {
187: return isElementOfMultitrigger;
188: }
189:
190: }
|