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.gui.Main;
021: import de.uka.ilkd.key.logic.Constraint;
022: import de.uka.ilkd.key.logic.Term;
023: import de.uka.ilkd.key.logic.op.IUpdateOperator;
024: import de.uka.ilkd.key.logic.op.IteratorOfQuantifiableVariable;
025: import de.uka.ilkd.key.logic.op.MapAsListFromQuantifiableVariableToTerm;
026: import de.uka.ilkd.key.logic.op.MapFromQuantifiableVariableToTerm;
027: import de.uka.ilkd.key.logic.op.Metavariable;
028: import de.uka.ilkd.key.logic.op.Modality;
029: import de.uka.ilkd.key.logic.op.Operator;
030: import de.uka.ilkd.key.logic.op.QuantifiableVariable;
031:
032: /**
033: * Matching triggers within another quantifier expression. Problems with the
034: * current implementation:
035: *
036: * * the usage of EqualityConstraint for unification implies that a variable is
037: * never instantiated with non-rigid terms
038: *
039: * * it is unclear whether certain instantiations are lost due to too strict type
040: * checks in EqualityConstraint
041: */
042: class TwoSidedMatching {
043:
044: private final UniTrigger trigger;
045: private final Term triggerWithMVs;
046: private final Substitution targetSubstWithMVs;
047: private final Substitution triggerSubstWithMVs;
048: private final Term targetWithMVs;
049:
050: TwoSidedMatching(UniTrigger trigger, Term targetTerm) {
051: this .trigger = trigger;
052: this .targetSubstWithMVs = ReplacerOfQuanVariablesWithMetavariables
053: .createSubstitutionForVars(targetTerm);
054: this .triggerSubstWithMVs = trigger.getTriggerSetThisBelongsTo()
055: .getReplacementWithMVs();
056: this .targetWithMVs = targetSubstWithMVs.apply(TriggerUtils
057: .discardQuantifiers(targetTerm));
058: this .triggerWithMVs = triggerSubstWithMVs.apply(trigger
059: .getTriggerTerm());
060: }
061:
062: SetOfSubstitution getSubstitutions() {
063: return getAllsubstitutions(targetWithMVs);
064: }
065:
066: private SetOfSubstitution getAllsubstitutions(Term target) {
067: SetOfSubstitution allsubs = SetAsListOfSubstitution.EMPTY_SET;
068: Substitution sub = match(triggerWithMVs, target);
069: if (sub != null
070: && (trigger.isElementOfMultitrigger() || sub
071: .isTotalOn(trigger.getUniVariables())
072: // sub.containFreevar(trigger.ts.allTerm.
073: // varsBoundHere(0).getQuantifiableVariable(0))
074: )) {
075: allsubs = allsubs.add(sub);
076: }
077: final Operator op = target.op();
078: if (!(op instanceof Modality || op instanceof IUpdateOperator)) {
079: for (int i = 0; i < target.arity(); i++) {
080: allsubs = allsubs.union(getAllsubstitutions(target
081: .sub(i)));
082: }
083: }
084: return allsubs;
085: }
086:
087: /** find a substitution in a allterm by using unification */
088: private Substitution match(Term triggerTerm, Term targetTerm) {
089: final Constraint c = Constraint.BOTTOM.unify(targetTerm,
090: triggerTerm, Main.getInstance().mediator()
091: .getServices());
092: if (c.isSatisfiable()) {
093: MapFromQuantifiableVariableToTerm sub = MapAsListFromQuantifiableVariableToTerm.EMPTY_MAP;
094: IteratorOfQuantifiableVariable it = trigger
095: .getUniVariables().iterator();
096: while (it.hasNext()) {
097: QuantifiableVariable q = it.next();
098: Term mv = triggerSubstWithMVs.getSubstitutedTerm(q);
099: Term t = c.getInstantiation((Metavariable) (mv.op()));
100: if (t == null || t.op() instanceof Metavariable)
101: return null;
102: if (isGround(t))
103: sub = sub.put(q, t);
104: }
105: if (sub.size() > 0)
106: return new Substitution(sub);
107: }
108: return null;
109: }
110:
111: private boolean isGround(Term t) {
112: return !triggerSubstWithMVs.termContainsValue(t)
113: && !targetSubstWithMVs.termContainsValue(t);
114: }
115: }
|