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.strategy.feature;
012:
013: import de.uka.ilkd.key.logic.ConstrainedFormula;
014: import de.uka.ilkd.key.logic.PosInOccurrence;
015: import de.uka.ilkd.key.logic.Semisequent;
016: import de.uka.ilkd.key.logic.Sequent;
017: import de.uka.ilkd.key.logic.op.EntryOfSchemaVariableAndInstantiationEntry;
018: import de.uka.ilkd.key.logic.op.IteratorOfEntryOfSchemaVariableAndInstantiationEntry;
019: import de.uka.ilkd.key.logic.op.MapFromSchemaVariableToInstantiationEntry;
020: import de.uka.ilkd.key.proof.Goal;
021: import de.uka.ilkd.key.proof.Node;
022: import de.uka.ilkd.key.rule.IteratorOfIfFormulaInstantiation;
023: import de.uka.ilkd.key.rule.PosTacletApp;
024: import de.uka.ilkd.key.rule.RuleApp;
025: import de.uka.ilkd.key.rule.TacletApp;
026: import de.uka.ilkd.key.rule.inst.InstantiationEntry;
027: import de.uka.ilkd.key.rule.inst.SVInstantiations;
028:
029: public abstract class AbstractNonDuplicateAppFeature extends
030: BinaryTacletAppFeature {
031:
032: protected AbstractNonDuplicateAppFeature() {
033: }
034:
035: /**
036: * Compare whether two <code>PosInOccurrence</code>s are equal. This can be
037: * done using <code>equals</code> or <code>eqEquals</code> (checking for
038: * same or equal formulas), which has to be decided by the subclasses
039: */
040: protected abstract boolean comparePio(TacletApp newApp,
041: TacletApp oldApp, PosInOccurrence newPio,
042: PosInOccurrence oldPio);
043:
044: /**
045: * Check whether a semisequent contains a formula. Again, one can either
046: * search for the same or an equal formula
047: */
048: protected abstract boolean semiSequentContains(
049: Semisequent semisequent, ConstrainedFormula cfma);
050:
051: /**
052: * Check whether the old rule application <code>ruleCmp</code> is a
053: * duplicate of the new application <code>newApp</code> at position
054: * <code>newPio</code>.<code>newPio</code> can be <code>null</code>
055: */
056: protected boolean sameApplication(RuleApp ruleCmp,
057: TacletApp newApp, PosInOccurrence newPio) {
058: // compare the rules
059: if (newApp.rule() != ruleCmp.rule()) {
060: return false;
061: }
062:
063: final TacletApp cmp = (TacletApp) ruleCmp;
064:
065: // compare the position of application
066: if (newPio != null) {
067: if (!(cmp instanceof PosTacletApp))
068: return false;
069: final PosInOccurrence oldPio = ((PosTacletApp) cmp)
070: .posInOccurrence();
071: if (!comparePio(newApp, cmp, newPio, oldPio))
072: return false;
073: }
074:
075: if (!newApp.constraint().equals(cmp.constraint()))
076: return false;
077:
078: // compare the if-sequent instantiations
079: if (newApp.ifFormulaInstantiations() == null
080: || cmp.ifFormulaInstantiations() == null) {
081: if (newApp.ifFormulaInstantiations() != null
082: || cmp.ifFormulaInstantiations() != null) {
083: return false;
084: }
085: } else {
086:
087: final IteratorOfIfFormulaInstantiation it0 = newApp
088: .ifFormulaInstantiations().iterator();
089: final IteratorOfIfFormulaInstantiation it1 = cmp
090: .ifFormulaInstantiations().iterator();
091:
092: while (it0.hasNext()) {
093: // this test should be improved
094: if (it0.next().getConstrainedFormula() != it1.next()
095: .getConstrainedFormula())
096: return false;
097: }
098: }
099:
100: return equalInterestingInsts(newApp.instantiations(), cmp
101: .instantiations());
102: }
103:
104: private boolean equalInterestingInsts(SVInstantiations inst0,
105: SVInstantiations inst1) {
106: if (!inst0.getUpdateContext().equals(inst1.getUpdateContext()))
107: return false;
108:
109: final MapFromSchemaVariableToInstantiationEntry interesting0 = inst0
110: .interesting();
111: final MapFromSchemaVariableToInstantiationEntry interesting1 = inst1
112: .interesting();
113: return subset(interesting0, interesting1)
114: && subset(interesting1, interesting0);
115: }
116:
117: private boolean subset(
118: MapFromSchemaVariableToInstantiationEntry insts0,
119: MapFromSchemaVariableToInstantiationEntry insts1) {
120: final IteratorOfEntryOfSchemaVariableAndInstantiationEntry it = insts0
121: .entryIterator();
122:
123: while (it.hasNext()) {
124: final EntryOfSchemaVariableAndInstantiationEntry entry0 = it
125: .next();
126:
127: if (entry0.key().isNameSV()
128: || entry0.key().isSkolemTermSV())
129: continue;
130:
131: final InstantiationEntry instEntry1 = insts1.get(entry0
132: .key());
133:
134: if (instEntry1 == null
135: || !entry0.value().getInstantiation().equals(
136: instEntry1.getInstantiation()))
137: return false;
138: }
139:
140: return true;
141: }
142:
143: /**
144: * Search for a duplicate of the application <code>app</code> by walking
145: * upwards in the proof tree. Here, we assume that <code>pos</code> is
146: * non-null, and as an optimisation we stop as soon as we have reached a
147: * point where the formula containing the focus no longer occurs in the
148: * sequent
149: */
150: protected boolean noDuplicateFindTaclet(TacletApp app,
151: PosInOccurrence pos, Goal goal) {
152: final ConstrainedFormula focusFor = pos.constrainedFormula();
153: final boolean antec = pos.isInAntec();
154:
155: Node node = goal.node();
156:
157: int i = 0;
158: while (!node.root()) {
159: final Node par = node.parent();
160:
161: ++i;
162: if (i > 100) {
163: i = 0;
164:
165: final Sequent pseq = par.sequent();
166: if (antec) {
167: if (!semiSequentContains(pseq.antecedent(),
168: focusFor))
169: return true;
170: } else {
171: if (!semiSequentContains(pseq.succedent(), focusFor))
172: return true;
173: }
174: }
175:
176: if (sameApplication(par.getAppliedRuleApp(), app, pos))
177: return false;
178:
179: node = par;
180: }
181:
182: return true;
183: }
184:
185: }
|