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.Term;
021: import de.uka.ilkd.key.logic.op.IUpdateOperator;
022: import de.uka.ilkd.key.logic.op.MapAsListFromQuantifiableVariableToTerm;
023: import de.uka.ilkd.key.logic.op.MapFromQuantifiableVariableToTerm;
024: import de.uka.ilkd.key.logic.op.Modality;
025: import de.uka.ilkd.key.logic.op.Operator;
026: import de.uka.ilkd.key.logic.op.QuantifiableVariable;
027: import de.uka.ilkd.key.logic.op.Quantifier;
028:
029: class BasicMatching {
030:
031: private BasicMatching() {
032: }
033:
034: /**
035: * matching <code>trigger</code> to <code>targetTerm</code> recursively
036: * @param trigger a uni-trigger
037: * @param targetTerm a gound term
038: * @return all substitution found from this matching
039: */
040: static SetOfSubstitution getSubstitutions(Term trigger,
041: Term targetTerm) {
042: SetOfSubstitution allsubs = SetAsListOfSubstitution.EMPTY_SET;
043: if (targetTerm.freeVars().size() > 0
044: || targetTerm.op() instanceof Quantifier)
045: return allsubs;
046: final Substitution subst = match(trigger, targetTerm);
047: if (subst != null)
048: allsubs = allsubs.add(subst);
049: final Operator op = targetTerm.op();
050: if (!(op instanceof Modality || op instanceof IUpdateOperator)) {
051: for (int i = 0; i < targetTerm.arity(); i++)
052: allsubs = allsubs.union(getSubstitutions(trigger,
053: targetTerm.sub(i)));
054: }
055: return allsubs;
056: }
057:
058: /**
059: * @param pattern
060: * @param instance
061: * @return all substitution that a given pattern(ex: a term of a uniTrigger)
062: * match in the instance.
063: */
064: private static Substitution match(Term pattern, Term instance) {
065: final MapFromQuantifiableVariableToTerm map = matchRec(
066: MapAsListFromQuantifiableVariableToTerm.EMPTY_MAP,
067: pattern, instance);
068: if (map == null)
069: return null;
070: return new Substitution(map);
071: }
072:
073: /**
074: * match the pattern to instance recursively.
075: */
076: private static MapFromQuantifiableVariableToTerm matchRec(
077: MapFromQuantifiableVariableToTerm varMap, Term pattern,
078: Term instance) {
079: final Operator patternOp = pattern.op();
080:
081: if (patternOp instanceof QuantifiableVariable)
082: return mapVarWithCheck(varMap,
083: (QuantifiableVariable) patternOp, instance);
084:
085: if (patternOp != instance.op())
086: return null;
087: for (int i = 0; i < pattern.arity(); i++) {
088: varMap = matchRec(varMap, pattern.sub(i), instance.sub(i));
089: if (varMap == null)
090: return null;
091: }
092: return varMap;
093: }
094:
095: /**
096: * match a variable to a instance.
097: * @return true if it is a new vaiable or the instance it matched is
098: * the same as that it matched before.
099: */
100: private static MapFromQuantifiableVariableToTerm mapVarWithCheck(
101: MapFromQuantifiableVariableToTerm varMap,
102: QuantifiableVariable var, Term instance) {
103: final Term oldTerm = varMap.get(var);
104: if (oldTerm == null)
105: return varMap.put(var, instance);
106:
107: if (oldTerm.equals(instance))
108: return varMap;
109: return null;
110: }
111:
112: }
|