Skip to content

Commit

Permalink
Bugfix: A decision procedure is applied only on the selected goal, wh…
Browse files Browse the repository at this point in the history 
…en it is run from the taclet menu of that specific goal.
  • Loading branch information
Christoph Gladisch committed Nov 30, 2009
1 parent e0030dc commit 4593a8a
Show file tree
Hide file tree
Showing 3 changed files with 148 additions and 99 deletions.
1 change: 1 addition & 0 deletions system/de/uka/ilkd/key/gui/nodeviews/SequentViewListener.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -140,6 +140,7 @@ public void mouseClicked(MouseEvent me) {
} else {

menu = new TacletMenu(seqView,
mediator.getSelectedGoal(),
mediator.getFindTaclet(mousePos),
mediator.getRewriteTaclet(mousePos),
mediator.getNoFindTaclet(),
Expand Down
10 changes: 8 additions & 2 deletions system/de/uka/ilkd/key/gui/nodeviews/TacletMenu.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand All @@ -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
Expand All @@ -68,13 +72,15 @@ class TacletMenu extends JMenu {
* @param pos the PosInSequent
*/
TacletMenu(SequentView sequentView,
final Goal selectedGoal,
ImmutableList<TacletApp> findList, ImmutableList<TacletApp> rewriteList,
ImmutableList<TacletApp> noFindList, ImmutableList<BuiltInRule> builtInList,
PosInSequent pos) {
super();
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),
Expand Down Expand Up @@ -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 {
Expand Down
236 changes: 139 additions & 97 deletions system/de/uka/ilkd/key/smt/DecProcRunner.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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();
Expand All @@ -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)) {
Expand Down Expand Up @@ -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<Goal> 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<Goal> 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();
Expand Down

0 comments on commit 4593a8a

Please sign in to comment.