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 java.util.HashMap;
020: import java.util.Iterator;
021: import java.util.Map;
022:
023: import de.uka.ilkd.key.gui.Main;
024: import de.uka.ilkd.key.java.Services;
025: import de.uka.ilkd.key.logic.IteratorOfConstrainedFormula;
026: import de.uka.ilkd.key.logic.Sequent;
027: import de.uka.ilkd.key.logic.SetAsListOfTerm;
028: import de.uka.ilkd.key.logic.SetOfTerm;
029: import de.uka.ilkd.key.logic.Term;
030: import de.uka.ilkd.key.logic.TermBuilder;
031: import de.uka.ilkd.key.logic.op.CastFunctionSymbol;
032: import de.uka.ilkd.key.logic.op.IteratorOfQuantifiableVariable;
033: import de.uka.ilkd.key.logic.op.MapAsListFromQuantifiableVariableToTerm;
034: import de.uka.ilkd.key.logic.op.MapFromQuantifiableVariableToTerm;
035: import de.uka.ilkd.key.logic.op.Op;
036: import de.uka.ilkd.key.logic.op.Operator;
037: import de.uka.ilkd.key.logic.op.QuantifiableVariable;
038: import de.uka.ilkd.key.logic.sort.AbstractSort;
039: import de.uka.ilkd.key.strategy.LongRuleAppCost;
040: import de.uka.ilkd.key.strategy.RuleAppCost;
041: import de.uka.ilkd.key.strategy.TopRuleAppCost;
042:
043: class Instantiation {
044:
045: private final static TermBuilder tb = TermBuilder.DF;
046:
047: /**universally quatifiable variable bound in<code>allTerm</code> */
048: private final QuantifiableVariable firstVar;
049:
050: private final Term matrix;
051:
052: /** Literals occurring in the sequent at hand. This is used for branch
053: * prediction */
054: private SetOfTerm assumedLiterals = SetAsListOfTerm.EMPTY_SET;
055:
056: /** HashMap from instance(<code>Term</code>) to cost <code>Long</code> */
057: private final Map instancesWithCosts = new HashMap();
058:
059: /**the <code>TriggersSet</code> of this <code>allTerm</code>*/
060: private final TriggersSet triggersSet;
061:
062: /**Terms bound in every formula on <code>goal</code>*/
063: private final SetOfTerm matchedTerms;
064:
065: private Instantiation(Term allterm, Sequent seq) {
066: firstVar = allterm.varsBoundHere(0).getQuantifiableVariable(0);
067: matrix = TriggerUtils.discardQuantifiers(allterm);
068: matchedTerms = sequentToTerms(seq);
069: triggersSet = TriggersSet.create(allterm);
070: assumedLiterals = initAssertLiterals(seq);
071: addInstances(matchedTerms);
072: }
073:
074: private static Term lastQuantifiedFormula = null;
075: private static Sequent lastSequent = null;
076: private static Instantiation lastResult = null;
077:
078: static Instantiation create(Term qf, Sequent seq) {
079: if (qf == lastQuantifiedFormula && seq == lastSequent)
080: return lastResult;
081:
082: lastQuantifiedFormula = qf;
083: lastSequent = seq;
084: lastResult = new Instantiation(qf, seq);
085:
086: return lastResult;
087: }
088:
089: private static SetOfTerm sequentToTerms(Sequent seq) {
090: SetOfTerm res = SetAsListOfTerm.EMPTY_SET;
091: IteratorOfConstrainedFormula it = seq.iterator();
092: while (it.hasNext())
093: res = res.add(it.next().formula());
094: return res;
095: }
096:
097: /**
098: * @param terms
099: * on which trigger are doning matching search every
100: * <code>Substitution</code> s by matching
101: * <code>triggers</code> from <code>triggersSet</code> to
102: * <code>terms</code> compute their cost and store the pair of
103: * instance (Term) and cost(Long) in
104: * <code>instancesCostCache</code>
105: */
106: private void addInstances(SetOfTerm terms) {
107: final IteratorOfTrigger trs = triggersSet.getAllTriggers()
108: .iterator();
109: while (trs.hasNext()) {
110: final SetOfSubstitution subs = trs.next()
111: .getSubstitutionsFromTerms(terms);
112: final IteratorOfSubstitution it = subs.iterator();
113: while (it.hasNext())
114: addInstance(it.next());
115: }
116:
117: // if ( instancesWithCosts.isEmpty () )
118: // ensure that there is always at least one instantiation
119: // addArbitraryInstance ();
120: }
121:
122: private void addArbitraryInstance() {
123: MapFromQuantifiableVariableToTerm varMap = MapAsListFromQuantifiableVariableToTerm.EMPTY_MAP;
124:
125: final IteratorOfQuantifiableVariable it = triggersSet
126: .getUniQuantifiedVariables().iterator();
127: while (it.hasNext()) {
128: final QuantifiableVariable v = it.next();
129: final Term inst = createArbitraryInstantiation(v, Main
130: .getInstance().mediator().getServices());
131: varMap = varMap.put(v, inst);
132: }
133:
134: addInstance(new Substitution(varMap));
135: }
136:
137: private Term createArbitraryInstantiation(QuantifiableVariable var,
138: Services services) {
139: return tb.func(((AbstractSort) var.sort()).getCastSymbol(), tb
140: .zTerm(services, "0"));
141: }
142:
143: private void addInstance(Substitution sub) {
144: final long cost = PredictCostProver.computerInstanceCost(sub,
145: getMatrix(), assumedLiterals);
146: if (cost != -1)
147: addInstance(sub, cost);
148: }
149:
150: /**
151: * add instance of <code>var</code> in <code>sub</code> with
152: * <code>cost</code> to <code>instancesCostCache</code> if this instance
153: * is exist, compare thire cost and store the less one.
154: *
155: * @param sub
156: * @param cost
157: */
158: private void addInstance(Substitution sub, long cost) {
159: final Term inst = sub.getSubstitutedTerm(firstVar);
160: final Long oldCost = (Long) instancesWithCosts.get(inst);
161: if (oldCost == null || oldCost.longValue() >= cost)
162: instancesWithCosts.put(inst, new Long(cost));
163: }
164:
165: /**
166: * @param seq
167: * @return all literals in antesequent, and all negation of literal in
168: * succedent
169: */
170: private SetOfTerm initAssertLiterals(Sequent seq) {
171: SetOfTerm assertLits = SetAsListOfTerm.EMPTY_SET;
172: final IteratorOfConstrainedFormula anteIt = seq.antecedent()
173: .iterator();
174: while (anteIt.hasNext()) {
175: final Term atom = anteIt.next().formula();
176: final Operator op = atom.op();
177: if (!(op == Op.ALL || op == Op.EX))
178: assertLits = assertLits.add(atom);
179: }
180: final IteratorOfConstrainedFormula succIt = seq.succedent()
181: .iterator();
182: while (succIt.hasNext()) {
183: final Term atom = succIt.next().formula();
184: final Operator op = atom.op();
185: if (!(op == Op.ALL || op == Op.EX))
186: assertLits = assertLits.add(tb.not(atom));
187: }
188: return assertLits;
189: }
190:
191: /**
192: * Try to find the cost of an instance(inst) according its quantified
193: * formula and current goal.
194: */
195: static RuleAppCost computeCost(Term inst, Term form, Sequent seq) {
196: return Instantiation.create(form, seq).computeCostHelp(inst);
197: }
198:
199: private RuleAppCost computeCostHelp(Term inst) {
200: Long cost = (Long) instancesWithCosts.get(inst);
201: if (cost == null && (inst.op() instanceof CastFunctionSymbol))
202: cost = (Long) instancesWithCosts.get(inst.sub(0));
203:
204: if (cost == null) {
205: // if (triggersSet)
206: return TopRuleAppCost.INSTANCE;
207: }
208: if (cost.longValue() == -1)
209: return TopRuleAppCost.INSTANCE;
210:
211: return LongRuleAppCost.create(cost.longValue());
212: }
213:
214: /**get all instances from instancesCostCache subsCache*/
215: SetOfTerm getSubstitution() {
216: SetOfTerm res = SetAsListOfTerm.EMPTY_SET;
217: final Iterator it = instancesWithCosts.keySet().iterator();
218: while (it.hasNext())
219: res = res.add((Term) it.next());
220: return res;
221: }
222:
223: private Term getMatrix() {
224: return matrix;
225: }
226:
227: }
|