01: // This file is part of KeY - Integrated Deductive Software Design
02: // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
03: // Universitaet Koblenz-Landau, Germany
04: // Chalmers University of Technology, Sweden
05: //
06: // The KeY system is protected by the GNU General Public License.
07: // See LICENSE.TXT for details.
08: //This file is part of KeY - Integrated Deductive Software Design
09: //Copyright (C) 2001-2005 Universitaet Karlsruhe, Germany
10: // Universitaet Koblenz-Landau, Germany
11: // Chalmers University of Technology, Sweden
12: //
13: //The KeY system is protected by the GNU General Public License.
14: //See LICENSE.TXT for details.
15: //
16: //
17: package de.uka.ilkd.key.strategy.quantifierHeuristics;
18:
19: import de.uka.ilkd.key.logic.IteratorOfTerm;
20: import de.uka.ilkd.key.logic.PosInOccurrence;
21: import de.uka.ilkd.key.logic.Term;
22: import de.uka.ilkd.key.logic.TermBuilder;
23: import de.uka.ilkd.key.logic.op.CastFunctionSymbol;
24: import de.uka.ilkd.key.logic.op.QuantifiableVariable;
25: import de.uka.ilkd.key.logic.sort.AbstractSort;
26: import de.uka.ilkd.key.logic.sort.Sort;
27: import de.uka.ilkd.key.proof.Goal;
28: import de.uka.ilkd.key.rule.RuleApp;
29: import de.uka.ilkd.key.strategy.termgenerator.TermGenerator;
30: import de.uka.ilkd.key.util.Debug;
31:
32: public class HeuristicInstantiation implements TermGenerator {
33:
34: public final static TermGenerator INSTANCE = new HeuristicInstantiation();
35:
36: private final TermBuilder tb = TermBuilder.DF;
37:
38: private HeuristicInstantiation() {
39: }
40:
41: public IteratorOfTerm generate(RuleApp app, PosInOccurrence pos,
42: Goal goal) {
43: Debug.assertFalse(pos == null,
44: "Feature is only applicable to rules with find");
45:
46: final Term qf = pos.constrainedFormula().formula();
47: final Instantiation ia = Instantiation.create(qf, goal
48: .sequent());
49: final QuantifiableVariable var = qf.varsBoundHere(0)
50: .lastQuantifiableVariable();
51: return new Iterator(ia.getSubstitution().iterator(), var);
52: }
53:
54: private class Iterator implements IteratorOfTerm {
55: private final IteratorOfTerm instances;
56:
57: private final QuantifiableVariable quantifiedVar;
58:
59: private final Sort quantifiedVarSort;
60: private final CastFunctionSymbol quantifiedVarSortCast;
61:
62: private Term nextInst = null;
63:
64: private Iterator(IteratorOfTerm it, QuantifiableVariable var) {
65: this .instances = it;
66: this .quantifiedVar = var;
67: quantifiedVarSort = quantifiedVar.sort();
68: quantifiedVarSortCast = ((AbstractSort) quantifiedVarSort)
69: .getCastSymbol();
70: findNextInst();
71: }
72:
73: private void findNextInst() {
74: while (nextInst == null && instances.hasNext()) {
75: nextInst = instances.next();
76: if (!nextInst.sort().extendsTrans(quantifiedVarSort)) {
77: if (!quantifiedVarSort
78: .extendsTrans(nextInst.sort())) {
79: nextInst = null;
80: continue;
81: }
82: nextInst = tb.func(quantifiedVarSortCast, nextInst);
83: }
84: }
85: }
86:
87: public boolean hasNext() {
88: return nextInst != null;
89: }
90:
91: public Term next() {
92: final Term res = nextInst;
93: nextInst = null;
94: findNextInst();
95: return res;
96: }
97: }
98:
99: }
|