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.gui;
012:
013: import java.util.ArrayList;
014: import java.util.Collections;
015: import java.util.Iterator;
016: import java.util.List;
017:
018: import javax.swing.SwingUtilities;
019:
020: import de.uka.ilkd.key.logic.Constraint;
021: import de.uka.ilkd.key.logic.PIOPathIterator;
022: import de.uka.ilkd.key.logic.PosInOccurrence;
023: import de.uka.ilkd.key.logic.op.IUpdateOperator;
024: import de.uka.ilkd.key.pp.PosInSequent;
025: import de.uka.ilkd.key.proof.*;
026: import de.uka.ilkd.key.rule.*;
027: import de.uka.ilkd.key.strategy.AutomatedRuleApplicationManager;
028: import de.uka.ilkd.key.strategy.FocussedRuleApplicationManager;
029: import de.uka.ilkd.key.util.Debug;
030:
031: public class InteractiveProver {
032:
033: /** the proof the interactive prover works on */
034: private Proof proof;
035:
036: /** the user focused goal */
037: private Goal focusedGoal;
038:
039: /** true iff in interactive mode */
040:
041: private boolean interactive = true;
042:
043: /** the central strategy processor including GUI signalling */
044: private ApplyStrategy applyStrategy;
045: private final ProverTaskListener focussedAutoModeTaskListener = new FocussedAutoModeTaskListener();
046:
047: /** list of proof listeners and interactive proof listeners */
048: private List listenerList = Collections
049: .synchronizedList(new ArrayList(10));
050:
051: /** listens to the current selected proof and node */
052: private KeYSelectionListener selListener;
053:
054: /** the mediator */
055: private KeYMediator mediator;
056:
057: private boolean resumeAutoMode = false;
058:
059: //private static Logger threadLogger = Logger.getLogger("key.threading");
060:
061: /** creates a new interactive prover object
062: */
063: public InteractiveProver(KeYMediator mediator) {
064: selListener = new InteractiveProverKeYSelectionListener();
065: this .mediator = mediator;
066: mediator.addKeYSelectionListener(selListener);
067: applyStrategy = new ApplyStrategy(mediator);
068: applyStrategy.addProverTaskObserver(mediator()
069: .getProverTaskListener());
070: }
071:
072: /** returns the KeYMediator */
073: KeYMediator mediator() {
074: return mediator;
075: }
076:
077: /** sets up a new proof
078: * @param p a Proof that contains the root of the proof tree
079: */
080: public void setProof(Proof p) {
081: proof = p;
082: }
083:
084: public void addAutoModeListener(AutoModeListener p) {
085: synchronized (listenerList) {
086: listenerList.add(p);
087: }
088: }
089:
090: public void removeAutoModeListener(AutoModeListener p) {
091: synchronized (listenerList) {
092: listenerList.remove(p);
093: }
094: }
095:
096: /** fires the event that automatic execution has started */
097: protected void fireAutoModeStarted(ProofEvent e) {
098: synchronized (listenerList) {
099: Iterator it = listenerList.iterator();
100: while (it.hasNext()) {
101: ((AutoModeListener) it.next()).autoModeStarted(e);
102: }
103: }
104: }
105:
106: /** fires the event that automatic execution has stopped */
107: public void fireAutoModeStopped(ProofEvent e) {
108: synchronized (listenerList) {
109: Iterator it = listenerList.iterator();
110: while (it.hasNext()) {
111: ((AutoModeListener) it.next()).autoModeStopped(e);
112: }
113: }
114: }
115:
116: void setResumeAutoMode(boolean b) {
117: resumeAutoMode = b;
118: }
119:
120: public boolean resumeAutoMode() {
121: return resumeAutoMode;
122: }
123:
124: public boolean interactiveMode() {
125: return interactive;
126: }
127:
128: public void setInteractive(boolean interact) {
129: interactive = interact;
130: }
131:
132: /**
133: * Apply a RuleApp and continue with update simplification or strategy
134: * application according to current settings.
135: * @param app
136: * @param goal
137: */
138: public void applyInteractive(RuleApp app, Goal goal) {
139: goal.node().getNodeInfo().setInteractiveRuleApplication(true);
140:
141: ListOfGoal goalList = goal.apply(app);
142:
143: if (!getProof().closed()) {
144: if (resumeAutoMode()) {
145: startAutoMode();
146: } else {
147: ReuseListener rl = mediator().getReuseListener();
148: rl.removeRPConsumedGoal(goal);
149: rl.addRPOldMarkersNewGoals(goalList);
150: if (rl.reusePossible()) {
151: mediator().indicateReuse(rl.getBestReusePoint());
152: } else {
153: mediator().indicateNoReuse();
154: Goal.applyUpdateSimplifier(goalList);
155: }
156: }
157: }
158: }
159:
160: private int getMaxStepCount() {
161: int rv = mediator().getMaxAutomaticSteps();
162:
163: if (Main.batchMode) {
164: //Allow much more steps in batchMode then in regular mode.
165: rv *= 100;
166: }
167:
168: return rv;
169: }
170:
171: private long getTimeout() {
172: return mediator().getAutomaticApplicationTimeout();
173: }
174:
175: /**
176: * returns the proof the interactive prover is working on
177: * @return the proof the interactive prover is working on
178: */
179: public Proof getProof() {
180: return proof;
181: }
182:
183: /**
184: * starts the execution of rules with active strategy
185: */
186: public void startAutoMode() {
187: startAutoMode(proof.openGoals());
188: }
189:
190: /** starts the execution of rules with active strategy. The
191: * strategy will only be applied on the goals of the list that
192: * is handed over and on the new goals an applied rule adds
193: */
194: public void startAutoMode(ListOfGoal goals) {
195: if (goals.isEmpty()) {
196: if (Main.batchMode) {
197: // Everything is already proven.
198: // Nothing to be saved. Exit successfully.
199: System.exit(0);
200: } else {
201: mediator().popupWarning("No (more) goals", "Oops...");
202: return;
203: }
204: }
205:
206: if (Main.batchMode) {
207: interactive = false;
208: }
209:
210: applyStrategy.start(goals, getMaxStepCount(), getTimeout());
211: }
212:
213: /** stops the execution of rules */
214: public void stopAutoMode() {
215: applyStrategy.stop();
216: }
217:
218: /**
219: * starts the execution of rules with active strategy. Restrict the
220: * application of rules to a particular goal and (for
221: * <code>focus!=null</code>) to a particular subterm or subformula of
222: * that goal
223: */
224: public void startFocussedAutoMode(PosInOccurrence focus, Goal goal) {
225: applyStrategy
226: .addProverTaskObserver(focussedAutoModeTaskListener);
227:
228: if (focus != null) {
229: // exchange the rule app manager of that goal to filter rule apps
230:
231: // we also apply rules to directly preceding updates (usually this
232: // makes sense)
233: final PIOPathIterator it = focus.iterator();
234: it.next();
235: focus = it.getPosInOccurrence();
236: while (it.hasNext()) {
237: if (it.getSubTerm().op() instanceof IUpdateOperator) {
238: final IUpdateOperator op = (IUpdateOperator) it
239: .getSubTerm().op();
240: if (it.getChild() == op.targetPos()) {
241: it.next();
242: continue;
243: }
244: }
245:
246: it.next();
247: focus = it.getPosInOccurrence();
248: }
249:
250: final AutomatedRuleApplicationManager realManager = goal
251: .getRuleAppManager();
252: goal.setRuleAppManager(null);
253: final FocussedRuleApplicationManager focusManager = new FocussedRuleApplicationManager(
254: realManager, goal, focus);
255: goal.setRuleAppManager(focusManager);
256: }
257:
258: startAutoMode(SLListOfGoal.EMPTY_LIST.prepend(goal));
259: }
260:
261: private void finishFocussedAutoMode() {
262: applyStrategy
263: .removeProverTaskObserver(focussedAutoModeTaskListener);
264:
265: final IteratorOfGoal it = proof.openGoals().iterator();
266: while (it.hasNext()) {
267: // remove any filtering rule app managers that are left in the proof
268: // goals
269: final Goal goal = it.next();
270: if (goal.getRuleAppManager() instanceof FocussedRuleApplicationManager) {
271: final FocussedRuleApplicationManager focusManager = (FocussedRuleApplicationManager) goal
272: .getRuleAppManager();
273: goal.setRuleAppManager(null);
274: final AutomatedRuleApplicationManager realManager = focusManager
275: .getDelegate();
276: realManager.clearCache();
277: goal.setRuleAppManager(realManager);
278: }
279: }
280: }
281:
282: private final class FocussedAutoModeTaskListener implements
283: ProverTaskListener {
284: public void taskStarted(String message, int size) {
285: }
286:
287: public void taskProgress(int position) {
288: }
289:
290: public void taskFinished() {
291: SwingUtilities.invokeLater(new Runnable() {
292: public void run() {
293: finishFocussedAutoMode();
294: }
295: });
296: }
297: }
298:
299: /**
300: * collects all built-in rules that are applicable at the given sequent
301: * position 'pos'.
302: *
303: * @param pos
304: * the PosInSequent where to look for applicable rules
305: * @param userConstraint
306: * the user defined constraint
307: */
308: public ListOfBuiltInRule getBuiltInRule(PosInOccurrence pos,
309: Constraint userConstraint) {
310: ListOfBuiltInRule rules = SLListOfBuiltInRule.EMPTY_LIST;
311: IteratorOfRuleApp it = getInteractiveRuleAppIndex()
312: .getBuiltInRule(focusedGoal, pos, userConstraint)
313: .iterator();
314:
315: while (it.hasNext()) {
316: BuiltInRule r = (BuiltInRule) it.next().rule();
317: if (!rules.contains(r)) {
318: rules = rules.prepend(r);
319: }
320: }
321: return rules;
322: }
323:
324: /**
325: * @return the <code>RuleAppIndex</code> of the goal currently focussed,
326: * after setting the index to unrestricted (non-automated mode)
327: */
328: private RuleAppIndex getInteractiveRuleAppIndex() {
329: final RuleAppIndex index = focusedGoal.ruleAppIndex();
330: index.autoModeStopped();
331: return index;
332: }
333:
334: /**
335: * collects all built-in rule applications for the given rule that are
336: * applicable at position 'pos' and the current user constraint
337: *
338: * @param rule
339: * the BuiltInRule for which the applications are collected
340: * @param pos
341: * the PosInSequent the position information
342: * @param userConstraint
343: * the user defined constraint
344: * @return a SetOfRuleApp with all possible rule applications
345: */
346: public SetOfRuleApp getBuiltInRuleApp(BuiltInRule rule,
347: PosInOccurrence pos, Constraint userConstraint) {
348:
349: SetOfRuleApp result = SetAsListOfRuleApp.EMPTY_SET;
350: IteratorOfRuleApp it = getInteractiveRuleAppIndex()
351: .getBuiltInRule(focusedGoal, pos, userConstraint)
352: .iterator();
353:
354: while (it.hasNext()) {
355: RuleApp app = it.next();
356: if (app.rule() == rule) {
357: result = result.add(app);
358: }
359: }
360:
361: return result;
362: }
363:
364: /**
365: * collects all applications of a rule given by its name at a give position in the sequent
366: * @param name
367: * the name of the BuiltInRule for which applications are collected.
368: * @param pos
369: * the position in the sequent where the BuiltInRule should be applied
370: * @return
371: * a SetOfRuleApp with all possible applications of the rule
372: */
373: protected SetOfRuleApp getBuiltInRuleAppsForName(String name,
374: PosInOccurrence pos) {
375: SetOfRuleApp result = SetAsListOfRuleApp.EMPTY_SET;
376: ListOfBuiltInRule match = SLListOfBuiltInRule.EMPTY_LIST;
377:
378: final Constraint userConstraint = mediator.getUserConstraint()
379: .getConstraint();
380:
381: //get all possible rules for current position in sequent
382: ListOfBuiltInRule list = getBuiltInRule(pos, userConstraint);
383:
384: IteratorOfBuiltInRule iter = list.iterator();
385:
386: //find all rules that match given name
387: while (iter.hasNext()) {
388: BuiltInRule rule = iter.next();
389: if (rule.name().toString().equals(name))
390: match = match.append(rule);
391: }
392:
393: iter = match.iterator();
394:
395: //find all applications for matched rules
396: while (iter.hasNext()) {
397: result = result.union(getBuiltInRuleApp(iter.next(), pos,
398: userConstraint));
399: }
400:
401: return result;
402: }
403:
404: /**
405: * collects all applicable NoFindTaclets of the current goal (called by the
406: * SequentViewer)
407: *
408: * @return a list of Taclets with all applicable NoFindTaclets
409: */
410: ListOfTacletApp getNoFindTaclet() {
411: return filterTaclet(getInteractiveRuleAppIndex()
412: .getNoFindTaclet(TacletFilter.TRUE,
413: mediator.getServices(),
414: mediator.getUserConstraint().getConstraint()));
415: }
416:
417: /** collects all applicable FindTaclets of the current goal
418: * (called by the SequentViewer)
419: * @return a list of Taclets with all applicable FindTaclets
420: */
421: ListOfTacletApp getFindTaclet(PosInSequent pos) {
422: if (pos != null && !pos.isSequent() && focusedGoal != null) {
423: Debug
424: .out(
425: "NoPosTacletApp: Looking for applicables rule at node",
426: focusedGoal.node().serialNr());
427: return filterTaclet(getInteractiveRuleAppIndex()
428: .getFindTaclet(
429: TacletFilter.TRUE,
430: pos.getPosInOccurrence(),
431: mediator.getServices(),
432: mediator.getUserConstraint()
433: .getConstraint()));
434: }
435: return SLListOfTacletApp.EMPTY_LIST;
436: }
437:
438: /** collects all applicable RewriteTaclets of the current goal
439: * (called by the SequentViewer)
440: * @return a list of Taclets with all applicable RewriteTaclets
441: */
442: ListOfTacletApp getRewriteTaclet(PosInSequent pos) {
443: if (!pos.isSequent()) {
444: return filterTaclet(getInteractiveRuleAppIndex()
445: .getRewriteTaclet(
446: TacletFilter.TRUE,
447: pos.getPosInOccurrence(),
448: mediator.getServices(),
449: mediator.getUserConstraint()
450: .getConstraint()));
451: }
452:
453: return SLListOfTacletApp.EMPTY_LIST;
454: }
455:
456: /**
457: * collects all Taclet applications at the given position of the specified
458: * taclet
459: * @param goal the Goal for which the applications should be returned
460: * @param name the String with the taclet names whose applications are looked for
461: * @param pos the PosInOccurrence describing the position
462: * @return a list of all found rule applications of the given rule at
463: * position pos
464: */
465: protected SetOfTacletApp getAppsForName(Goal goal, String name,
466: PosInOccurrence pos) {
467: return getAppsForName(goal, name, pos, TacletFilter.TRUE);
468: }
469:
470: /**
471: * collects all taclet applications for the given position and taclet
472: * (identified by its name) matching the filter condition
473: * @param goal the Goal for which the applications should be returned
474: * @param name the String with the taclet names whose applications are looked for
475: * @param pos the PosInOccurrence describing the position
476: * @param filter the TacletFilter expressing restrictions
477: * @return a list of all found rule applications of the given rule at
478: * position <tt>pos</tt> passing the filter
479: */
480: protected SetOfTacletApp getAppsForName(Goal goal, String name,
481: PosInOccurrence pos, TacletFilter filter) {
482: SetOfTacletApp result = SetAsListOfTacletApp.EMPTY_SET;
483: ListOfTacletApp fittingApps = SLListOfTacletApp.EMPTY_LIST;
484: final RuleAppIndex index = goal.ruleAppIndex();
485: final Constraint userConstraint = mediator.getUserConstraint()
486: .getConstraint();
487: if (pos == null) {
488: final IteratorOfNoPosTacletApp it = index.getNoFindTaclet(
489: filter, mediator.getServices(), userConstraint)
490: .iterator();
491: while (it.hasNext())
492: fittingApps = fittingApps.prepend(it.next());
493: } else
494: fittingApps = index.getTacletAppAt(filter, pos, mediator
495: .getServices(), userConstraint);
496:
497: IteratorOfTacletApp it = fittingApps.iterator();
498: // filter fitting applications
499: while (it.hasNext()) {
500: TacletApp app = it.next();
501: if (app.rule().name().toString().equals(name)) {
502: result = result.add(app);
503: }
504: }
505: //if (result.size()==0) System.err.println("Available was "+fittingApps);
506: return result;
507: }
508:
509: /** listener to KeYSelection Events in order to be informed if the
510: * current proof changed
511: */
512: private class InteractiveProverKeYSelectionListener implements
513: KeYSelectionListener {
514:
515: /** focused node has changed */
516: public void selectedNodeChanged(KeYSelectionEvent e) {
517: focusedGoal = e.getSource().getSelectedGoal();
518: }
519:
520: /** the selected proof has changed (e.g. a new proof has been
521: * loaded) */
522: public void selectedProofChanged(KeYSelectionEvent e) {
523: Debug.out("InteractiveProver: initialize with new proof");
524: Proof newProof = e.getSource().getSelectedProof();
525: setProof(newProof); // this is null-safe
526: if (newProof != null) {
527: focusedGoal = e.getSource().getSelectedGoal();
528: } else {
529: focusedGoal = null;
530: }
531: }
532:
533: }
534:
535: /**
536: * takes NoPosTacletApps as arguments and returns a duplicate free list of
537: * the contained TacletApps
538: */
539: private ListOfTacletApp filterTaclet(
540: ListOfNoPosTacletApp tacletInstances) {
541: java.util.HashSet applicableRules = new java.util.HashSet();
542: ListOfTacletApp result = SLListOfTacletApp.EMPTY_LIST;
543: IteratorOfNoPosTacletApp it = tacletInstances.iterator();
544: while (it.hasNext()) {
545: TacletApp app = it.next();
546: if (mediator().stupidMode()) {
547: ListOfTacletApp ifCandidates = app
548: .findIfFormulaInstantiations(mediator()
549: .getSelectedGoal().sequent(),
550: mediator().getServices(), mediator()
551: .getUserConstraint()
552: .getConstraint());
553: if (ifCandidates.size() == 0)
554: continue; // skip this app
555: }
556:
557: // for the moment, just remove taclets which are
558: // inconsistent with user constraint
559: // (introduction of new sorts not allowed)
560: if (mediator().getUserConstraint().getConstraint().join(
561: app.constraint(), null).isSatisfiable()) {
562: Taclet taclet = app.taclet();
563: if (!applicableRules.contains(taclet)) {
564: applicableRules.add(taclet);
565: result = result.prepend(app);
566: }
567: }
568: }
569: return result;
570: }
571:
572: }
|