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: package de.uka.ilkd.key.strategy.quantifierHeuristics;
018:
019: import de.uka.ilkd.key.logic.SetOfTerm;
020: import de.uka.ilkd.key.logic.Term;
021: import de.uka.ilkd.key.logic.op.EntryOfQuantifiableVariableAndTerm;
022: import de.uka.ilkd.key.logic.op.IteratorOfEntryOfQuantifiableVariableAndTerm;
023: import de.uka.ilkd.key.logic.op.MapAsListFromQuantifiableVariableToTerm;
024: import de.uka.ilkd.key.logic.op.MapFromQuantifiableVariableToTerm;
025: import de.uka.ilkd.key.logic.op.QuantifiableVariable;
026: import de.uka.ilkd.key.logic.op.SetOfQuantifiableVariable;
027:
028: class MultiTrigger extends Trigger {
029:
030: private final SetOfTrigger triggers;
031: private final SetOfQuantifiableVariable qvs;
032: private final Term clause;
033:
034: MultiTrigger(SetOfTrigger triggers, SetOfQuantifiableVariable qvs,
035: Term clause) {
036: this .triggers = triggers;
037: this .qvs = qvs;
038: this .clause = clause;
039: }
040:
041: public SetOfSubstitution getSubstitutionsFromTerms(
042: SetOfTerm targetTerms) {
043: SetOfSubstitution res = SetAsListOfSubstitution.EMPTY_SET;
044: SetOfSubstitution mulsubs = setMultiSubstitution(triggers
045: .toArray(), 0, targetTerms);
046: IteratorOfSubstitution it = mulsubs.iterator();
047: while (it.hasNext()) {
048: Substitution sub = it.next();
049: if (sub.isTotalOn(qvs))
050: res = res.add(sub);
051: }
052:
053: return res;
054: }
055:
056: /**help function for getMultiSubstitution*/
057: private SetOfSubstitution setMultiSubstitution(Trigger[] ts, int i,
058: SetOfTerm terms) {
059: SetOfSubstitution res = SetAsListOfSubstitution.EMPTY_SET;
060: if (i >= ts.length)
061: return res;
062: SetOfSubstitution subi = ts[i].getSubstitutionsFromTerms(terms);
063: SetOfSubstitution nextSubs = setMultiSubstitution(ts, i + 1,
064: terms);
065: if (nextSubs.size() == 0)
066: return res.union(subi);
067: IteratorOfSubstitution it = nextSubs.iterator();
068: while (it.hasNext()) {
069: Substitution sub0 = it.next();
070: IteratorOfSubstitution it1 = subi.iterator();
071: while (it1.hasNext()) {
072: Substitution sub1 = unifySubstitution(sub0, it1.next());
073: if (sub1 != null)
074: res = res.add(sub1);
075: }
076:
077: }
078: return res;
079: }
080:
081: /**unify two substitution, if same variable are bound with same term return
082: * a new substitution with all universal quantifiable variables in two
083: * substituition, otherwise return null*/
084: private Substitution unifySubstitution(Substitution sub0,
085: Substitution sub1) {
086: IteratorOfEntryOfQuantifiableVariableAndTerm it0 = sub0
087: .getVarMap().entryIterator();
088: MapFromQuantifiableVariableToTerm map1 = sub1.getVarMap();
089: MapFromQuantifiableVariableToTerm resMap = MapAsListFromQuantifiableVariableToTerm.EMPTY_MAP;
090:
091: while (it0.hasNext()) {
092: EntryOfQuantifiableVariableAndTerm en = it0.next();
093: QuantifiableVariable key = en.key();
094: Term value = en.value();
095: if (map1.containsKey(key)) {
096: if (!(map1.get(key).equals(value)))
097: return null;
098: }
099: resMap = resMap.put(key, value);
100: }
101: IteratorOfEntryOfQuantifiableVariableAndTerm it1 = map1
102: .entryIterator();
103: while (it1.hasNext()) {
104: EntryOfQuantifiableVariableAndTerm en = it1.next();
105: resMap = resMap.put(en.key(), en.value());
106: }
107:
108: return new Substitution(resMap);
109: }
110:
111: public boolean equals(Object arg0) {
112: if (!(arg0 instanceof MultiTrigger))
113: return false;
114:
115: final MultiTrigger a = (MultiTrigger) arg0;
116: return a.triggers.equals(triggers);
117: }
118:
119: public int hashCode() {
120: return triggers.hashCode();
121: }
122:
123: public String toString() {
124: return "" + triggers;
125: }
126:
127: public Term getTriggerTerm() {
128: return clause;
129: }
130:
131: }
|