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.ListOfTerm;
014: import de.uka.ilkd.key.logic.Name;
015: import de.uka.ilkd.key.logic.Term;
016: import de.uka.ilkd.key.logic.ldt.IntegerLDT;
017: import de.uka.ilkd.key.logic.op.EntryOfSchemaVariableAndInstantiationEntry;
018: import de.uka.ilkd.key.logic.op.Function;
019: import de.uka.ilkd.key.logic.op.IteratorOfEntryOfSchemaVariableAndInstantiationEntry;
020: import de.uka.ilkd.key.logic.op.Operator;
021: import de.uka.ilkd.key.proof.Goal;
022: import de.uka.ilkd.key.rule.*;
023: import de.uka.ilkd.key.util.LRUCache;
024:
025: public abstract class AbstractMonomialSmallerThanFeature extends
026: SmallerThanFeature {
027:
028: private static final Name newSymRuleSetName = new Name(
029: "polySimp_newSmallSym");
030: private static final LRUCache introductionTimeCache = new LRUCache(
031: 10000);
032: private final Function add, mul, Z;
033:
034: private Goal currentGoal = null;
035:
036: protected AbstractMonomialSmallerThanFeature(IntegerLDT numbers) {
037: this .add = numbers.getArithAddition();
038: this .mul = numbers.getArithMultiplication();
039: this .Z = numbers.getNumberSymbol();
040: }
041:
042: protected int introductionTime(Operator op) {
043: if (op == add || op == mul || op == Z)
044: return -1;
045: Integer res = (Integer) introductionTimeCache.get(op);
046: if (res == null) {
047: res = new Integer(introductionTimeHelp(op));
048: introductionTimeCache.put(op, res);
049: }
050: return res.intValue();
051: }
052:
053: private int introductionTimeHelp(Operator op) {
054: ListOfRuleApp appliedRules = getCurrentGoal().appliedRuleApps();
055: while (!appliedRules.isEmpty()) {
056: final RuleApp app = appliedRules.head();
057: appliedRules = appliedRules.tail();
058:
059: if (app instanceof TacletApp) {
060: final TacletApp tapp = (TacletApp) app;
061: if (!inNewSmallSymRuleSet(tapp))
062: continue;
063:
064: if (introducesSkolemSymbol(tapp, op))
065: return appliedRules.size();
066: }
067: }
068:
069: return -1;
070: }
071:
072: private boolean introducesSkolemSymbol(TacletApp tapp, Operator op) {
073: final IteratorOfEntryOfSchemaVariableAndInstantiationEntry it = tapp
074: .instantiations().pairIterator();
075: while (it.hasNext()) {
076: final EntryOfSchemaVariableAndInstantiationEntry entry = it
077: .next();
078: if (!entry.key().isSkolemTermSV())
079: continue;
080: if (op == ((Term) entry.value().getInstantiation()).op())
081: return true;
082: }
083: return false;
084: }
085:
086: private boolean inNewSmallSymRuleSet(TacletApp tapp) {
087: ListOfRuleSet ruleSets = tapp.taclet().getRuleSets();
088: while (!ruleSets.isEmpty()) {
089: final RuleSet rs = ruleSets.head();
090: ruleSets = ruleSets.tail();
091: if (rs.name().equals(newSymRuleSetName))
092: return true;
093: }
094: return false;
095: }
096:
097: protected ListOfTerm collectAtoms(Term t) {
098: final AtomCollector m = new AtomCollector();
099: m.collect(t);
100: return m.getResult();
101: }
102:
103: private class AtomCollector extends Collector {
104: protected void collect(Term te) {
105: if (te.op() == mul) {
106: collect(te.sub(0));
107: collect(te.sub(1));
108: } else {
109: addTerm(te);
110: }
111: }
112: }
113:
114: /**
115: * @param currentGoal The currentGoal to set.
116: */
117: protected void setCurrentGoal(Goal currentGoal) {
118: this .currentGoal = currentGoal;
119: }
120:
121: /**
122: * @return Returns the currentGoal.
123: */
124: protected Goal getCurrentGoal() {
125: return currentGoal;
126: }
127: }
|