From 4593a8ab394d874fee59296dcc507dcbea2ab89a Mon Sep 17 00:00:00 2001 From: Christoph Gladisch Date: Mon, 30 Nov 2009 16:52:21 +0100 Subject: [PATCH] Bugfix: A decision procedure is applied only on the selected goal, when it is run from the taclet menu of that specific goal. --- .../gui/nodeviews/SequentViewListener.java | 1 + .../ilkd/key/gui/nodeviews/TacletMenu.java | 10 +- system/de/uka/ilkd/key/smt/DecProcRunner.java | 236 +++++++++++------- 3 files changed, 148 insertions(+), 99 deletions(-) diff --git a/system/de/uka/ilkd/key/gui/nodeviews/SequentViewListener.java b/system/de/uka/ilkd/key/gui/nodeviews/SequentViewListener.java index 6aa6c427ccc..d65750ce156 100644 --- a/system/de/uka/ilkd/key/gui/nodeviews/SequentViewListener.java +++ b/system/de/uka/ilkd/key/gui/nodeviews/SequentViewListener.java @@ -140,6 +140,7 @@ public void mouseClicked(MouseEvent me) { } else { menu = new TacletMenu(seqView, + mediator.getSelectedGoal(), mediator.getFindTaclet(mousePos), mediator.getRewriteTaclet(mousePos), mediator.getNoFindTaclet(), diff --git a/system/de/uka/ilkd/key/gui/nodeviews/TacletMenu.java b/system/de/uka/ilkd/key/gui/nodeviews/TacletMenu.java index 484bca44bbd..32e64ccc28a 100644 --- a/system/de/uka/ilkd/key/gui/nodeviews/TacletMenu.java +++ b/system/de/uka/ilkd/key/gui/nodeviews/TacletMenu.java @@ -31,6 +31,7 @@ import de.uka.ilkd.key.pp.AbbrevException; import de.uka.ilkd.key.pp.AbbrevMap; import de.uka.ilkd.key.pp.PosInSequent; +import de.uka.ilkd.key.proof.Goal; import de.uka.ilkd.key.rule.*; import de.uka.ilkd.key.smt.DecProcRunner; import de.uka.ilkd.key.smt.SMTRule; @@ -51,11 +52,14 @@ class TacletMenu extends JMenu { private TacletAppComparator comp = new TacletAppComparator(); static Logger logger = Logger.getLogger(TacletMenu.class.getName()); + private final Goal selectedGoal; /** * creates empty menu */ - TacletMenu() {} + TacletMenu() { + selectedGoal = null; + } /** creates a new menu that displays all applicable rules at the given @@ -68,6 +72,7 @@ class TacletMenu extends JMenu { * @param pos the PosInSequent */ TacletMenu(SequentView sequentView, + final Goal selectedGoal, ImmutableList findList, ImmutableList rewriteList, ImmutableList noFindList, ImmutableList builtInList, PosInSequent pos) { @@ -75,6 +80,7 @@ class TacletMenu extends JMenu { this.sequentView = sequentView; this.mediator = sequentView.mediator(); this.pos = pos; + this.selectedGoal = selectedGoal; // delete RewriteTaclet from findList because they will be in // the rewrite list and concatenate both lists createTacletMenu(removeRewrites(findList).prepend(rewriteList), @@ -350,7 +356,7 @@ public void actionPerformed(ActionEvent e) { if (((BuiltInRuleMenuItem) e.getSource()).connectedTo() instanceof SMTRule || ((BuiltInRuleMenuItem) e.getSource()).connectedTo() instanceof SMTRuleMulti) { new DecProcRunner(Main.getInstance() - , Main.getInstance().mediator().getProof() + , selectedGoal//Main.getInstance().mediator().getProof() , Main.getInstance().mediator().getProof().getUserConstraint().getConstraint() , ((BuiltInRuleMenuItem) e.getSource()).connectedTo()).start(); } else { diff --git a/system/de/uka/ilkd/key/smt/DecProcRunner.java b/system/de/uka/ilkd/key/smt/DecProcRunner.java index 560d8fc3ad5..a8189e42dcc 100644 --- a/system/de/uka/ilkd/key/smt/DecProcRunner.java +++ b/system/de/uka/ilkd/key/smt/DecProcRunner.java @@ -46,25 +46,53 @@ public class DecProcRunner extends SwingWorker { private final IMain main; + private final KeYMediator mediator; private final Proof proof; + /** This field is set only, when this runner is applied to the specific goal. + * If this field is null, then the runner is applied to all open goals of the proof tree*/ + private final Goal selectedGoal; private int totalGoals = 0; private final KeYExceptionHandler exceptionHandler; private final Constraint userConstraint; private final BuiltInRule simpRule; - private Object construcResult = null; + /**Warning: After analysing where the data for this field comes from, it seems that it is not really used.*/ + private Object construcResult = null; + + + + /**Use this constructor if you want apply the dec. proc. to all open goals. */ public DecProcRunner(IMain main, Proof proof, Constraint userConstraint) { //instantiate this DecProcRunner with the currently selected standard SMT solver this(main, proof, userConstraint, null); } + + /**Use this constructor if you want apply the dec. proc. only to the goal given as parameter. */ + public DecProcRunner(IMain main, Goal goal, Constraint userConstraint) { + //instantiate this DecProcRunner with the currently selected standard SMT solver + this(main, goal, userConstraint, null); + } + + /**Use this constructor if you want apply the dec. proc. to all open goals. */ public DecProcRunner(IMain main, Proof proof, Constraint userConstraint, BuiltInRule r) { + this(main, proof, null, userConstraint, r); + } + + /**Use this constructor if you want to apply the dec. proc. only to the goal given as parameter */ + public DecProcRunner(IMain main, Goal goal, Constraint userConstraint, BuiltInRule r) { + this(main, goal.proof(), goal, userConstraint, r); + } + + public DecProcRunner(IMain main, Proof proof, Goal goal, Constraint userConstraint, BuiltInRule r) { this.main = main; + this.mediator = main.mediator(); this.proof = proof; this.userConstraint = userConstraint; + this.selectedGoal = goal; if (r == null) { this.simpRule = getIntegerDecisionProcedure(); @@ -76,8 +104,9 @@ public DecProcRunner(IMain main, Proof proof, Constraint userConstraint, BuiltIn } + + public void finished() { - final KeYMediator mediator = main.mediator(); mediator.startInterface(true); String msg = (String) this.construcResult; if(!"".equals(msg)) { @@ -106,112 +135,125 @@ public void finished() { } public Object construct() { - this.construcResult = this.doWork(); - return this.construcResult; + this.construcResult = this.doWork(); + return this.construcResult; } + /**@return the return value is probably meaningless */ private Object doWork() { - String status = ""; + String status = "";//Warning status is not used main.mediator().stopInterface(true); - final KeYMediator mediator = main.mediator(); + mediator.resetNrGoalsClosedByHeuristics(); + + proof.env().registerRule(simpRule, + de.uka.ilkd.key.proof.mgt.AxiomJustification.INSTANCE); + + if(selectedGoal!=null){ + main.setStatusLine("Running external decision procedure: " + simpRule.displayName(), 99); + workOnGoal( selectedGoal,0); + }else{ + totalGoals = proof.openGoals().size(); + main.setStatusLine("Running external decision procedure: " + + simpRule.displayName(), 99*totalGoals); + workOnAllOpenGoals(); + } + return status; + } + + private void workOnAllOpenGoals(){ + + int cnt = 0; + + + final Iterator goals = proof.openGoals().iterator(); + + while (goals.hasNext()) { + workOnGoal(goals.next(), ++cnt); + } + } + + /**Applies decision procedure rule on the goal g. + * @param temp is just a counter for user feedback*/ + private void workOnGoal(Goal g, final int temp){ InterruptListener il = null; - try { - try { - totalGoals = proof.openGoals().size(); - int cnt = 0; - - proof.env().registerRule(simpRule, - de.uka.ilkd.key.proof.mgt.AxiomJustification.INSTANCE); - - main.setStatusLine("Running external decision procedure: " + - simpRule.displayName(), 99*totalGoals); - - final Iterator goals = proof.openGoals().iterator(); - - while (goals.hasNext()) { - BuiltInRuleApp birApp = new BuiltInRuleApp(simpRule, null, - userConstraint); - - Goal g = goals.next(); - - cnt++; - final int temp = cnt; - - //start a task to update the progressbar according to the timeprogress. - BaseProgressMonitor pm = null; - - //add a progress monitor to disply up to date progress. - if (simpRule instanceof SMTRule || simpRule instanceof SMTRuleMulti) { - final MakesProgress prog = (MakesProgress) simpRule; - //final SMTRule rule = (SMTRule) simpRule; - il = new InterruptListener() { - public void interruptionPerformed(ActionEvent e) { - prog.interrupt(); - //rule.interrupt(); - if (temp == totalGoals) { - main.setStatusLine("Goal " + temp + " interrupted by user."); - } else { - main.setStatusLine("Goal " + temp + " interrupted by user. Processing goal " + (temp+1) ); - } - } - }; - main.mediator().addinterruptListener(il); - int step = 99; - int base = (cnt-1) * step; - pm = new BaseProgressMonitor(base, main.getProgressMonitor()); - prog.addProgressMonitor(pm); - //rule.addProgressMonitor(pm); - } - ProofTreeListener ptl = new ProofTreeListener() { - - public void proofGoalRemoved(ProofTreeEvent e) { - int step = 99; - main.getProgressMonitor().setProgress(step*temp); - } - - public void proofIsBeingPruned(ProofTreeEvent e) {} - public void proofPruned(ProofTreeEvent e) {} - public void proofClosed(ProofTreeEvent e) {} - public void proofStructureChanged(ProofTreeEvent e) {} - public void proofGoalsAdded(ProofTreeEvent e) {} - public void proofGoalsChanged(ProofTreeEvent e) {} - public void proofExpanded(ProofTreeEvent e) {} - }; - proof.addProofTreeListener(ptl); - g.apply(birApp); - if (il != null) { - mediator.removeInterruptListener(il); - il = null; - } - //remove the progress monitor again - if (pm != null) { - - ((MakesProgress)simpRule).removeProgressMonitor(pm); - } + try { + try { - proof.removeProofTreeListener(ptl); - + BuiltInRuleApp birApp = new BuiltInRuleApp(simpRule, null, + userConstraint); + + + //start a task to update the progressbar according to the timeprogress. + BaseProgressMonitor pm = null; + + //add a progress monitor to disply up to date progress. + if (simpRule instanceof SMTRule || simpRule instanceof SMTRuleMulti) { + final MakesProgress prog = (MakesProgress) simpRule; + //final SMTRule rule = (SMTRule) simpRule; + il = new InterruptListener() { + public void interruptionPerformed(ActionEvent e) { + prog.interrupt(); + //rule.interrupt(); + if (temp == totalGoals) { + main.setStatusLine("Goal " + temp + " interrupted by user."); + } else { + main.setStatusLine("Goal " + temp + " interrupted by user. Processing goal " + (temp+1) ); + } } - } catch (ExceptionHandlerException e) { - throw e; - } catch (Throwable thr) { - exceptionHandler.reportException(thr); - } - } catch (ExceptionHandlerException ex){ - main.setStatusLine("Running external decision procedure failed"); - throw(ex); - } finally { - if (il != null) { - mediator.removeInterruptListener(il); - il = null; - } - mediator.startInterface(true); + }; + main.mediator().addinterruptListener(il); + int step = 99; + int base = (temp-1) * step; + pm = new BaseProgressMonitor(base, main.getProgressMonitor()); + prog.addProgressMonitor(pm); + //rule.addProgressMonitor(pm); + } + ProofTreeListener ptl = new ProofTreeListener() { + + public void proofGoalRemoved(ProofTreeEvent e) { + int step = 99; + main.getProgressMonitor().setProgress(step*temp); + } + + public void proofIsBeingPruned(ProofTreeEvent e) {} + public void proofPruned(ProofTreeEvent e) {} + public void proofClosed(ProofTreeEvent e) {} + public void proofStructureChanged(ProofTreeEvent e) {} + public void proofGoalsAdded(ProofTreeEvent e) {} + public void proofGoalsChanged(ProofTreeEvent e) {} + public void proofExpanded(ProofTreeEvent e) {} + }; + proof.addProofTreeListener(ptl); + g.apply(birApp); + if (il != null) { + mediator.removeInterruptListener(il); + il = null; + } + //remove the progress monitor again + if (pm != null) { + + ((MakesProgress)simpRule).removeProgressMonitor(pm); } - return status; + proof.removeProofTreeListener(ptl); + + } catch (ExceptionHandlerException e) { + throw e; + } catch (Throwable thr) { + exceptionHandler.reportException(thr); + } + } catch (ExceptionHandlerException ex){ + main.setStatusLine("Running external decision procedure failed"); + throw(ex); + } finally { + if (il != null) { + mediator.removeInterruptListener(il); + il = null; + } + mediator.startInterface(true); + } } - private BuiltInRule getIntegerDecisionProcedure() { final Name simpRuleName = proof.getSettings().getDecisionProcedureSettings().getActiveRule().getRuleName();