diff --git a/key.core.testgen/src/main/java/de/uka/ilkd/key/smt/counterexample/AbstractCounterExampleGenerator.java b/key.core.testgen/src/main/java/de/uka/ilkd/key/smt/counterexample/AbstractCounterExampleGenerator.java index 36f3689a7ab..61546a95392 100644 --- a/key.core.testgen/src/main/java/de/uka/ilkd/key/smt/counterexample/AbstractCounterExampleGenerator.java +++ b/key.core.testgen/src/main/java/de/uka/ilkd/key/smt/counterexample/AbstractCounterExampleGenerator.java @@ -68,14 +68,12 @@ public void searchCounterExample(UserInterfaceControl ui, Proof oldProof, Sequen throw new IllegalStateException( "Can't find SMT solver " + SolverTypes.Z3_CE_SOLVER.getName()); } - final Proof proof = createProof(ui, oldProof, oldSequent, "Semantics Blasting: " + oldProof.name()); final SemanticsBlastingMacro macro = new SemanticsBlastingMacro(); TaskFinishedInfo info = ProofMacroFinishedInfo.getDefaultInfo(macro, proof); final ProverTaskListener ptl = ui.getProofControl().getDefaultProverTaskListener(); ptl.taskStarted(new DefaultTaskStartedInfo(TaskKind.Macro, macro.getName(), 0)); - try { synchronized (macro) { // TODO: Useless? No other thread has access to macro wait for // macro to terminate @@ -99,8 +97,6 @@ public void searchCounterExample(UserInterfaceControl ui, Proof oldProof, Sequen solvers.add(SolverTypes.Z3_CE_SOLVER); launcher.launch(solvers, SMTProblem.createSMTProblems(proof), proof.getServices()); - - } /** diff --git a/key.core/src/main/java/de/uka/ilkd/key/smt/SMTSolverImplementation.java b/key.core/src/main/java/de/uka/ilkd/key/smt/SMTSolverImplementation.java index d49395a117a..a3394921a9e 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/smt/SMTSolverImplementation.java +++ b/key.core/src/main/java/de/uka/ilkd/key/smt/SMTSolverImplementation.java @@ -255,7 +255,7 @@ public void run() { String[] commands; try { commands = translateToCommand(problem.getSequent()); - } catch (IllegalFormulaException e) { + } catch (Throwable e) { interruptionOccurred(e); listener.processInterrupted(this, problem, e); setSolverState(SolverState.Stopped); diff --git a/key.core/src/main/java/de/uka/ilkd/key/smt/SolverLauncher.java b/key.core/src/main/java/de/uka/ilkd/key/smt/SolverLauncher.java index 03a8b7090fb..6dfacf097f6 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/smt/SolverLauncher.java +++ b/key.core/src/main/java/de/uka/ilkd/key/smt/SolverLauncher.java @@ -286,7 +286,6 @@ private void launchSolvers(Queue solvers, Collection prob // Launch all solvers until the queue is empty or the launcher is // interrupted. launchLoop(solvers); - // at this point either there are no solvers left to start or // the whole launching process was interrupted. waitForRunningSolvers(); @@ -294,7 +293,6 @@ private void launchSolvers(Queue solvers, Collection prob cleanUp(solvers); notifyListenersOfStop(); - } private void notifyListenersOfStart(Collection problems, @@ -320,7 +318,6 @@ private void launchLoop(Queue solvers) { // if there is nothing to do, wait for the next solver // finishing its task. wait.await(); - } catch (InterruptedException e) { launcherInterrupted(e); } @@ -386,8 +383,8 @@ private void notifySolverHasFinished(SMTSolver solver) { lock.lock(); try { session.removeCurrentlyRunning(solver); - wait.signal(); } finally { + wait.signal(); lock.unlock(); } } diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/smt/ProgressDialog.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/smt/ProgressDialog.java index 13a8bb0d6eb..c048e4a057b 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/smt/ProgressDialog.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/smt/ProgressDialog.java @@ -205,7 +205,6 @@ private JButton getStopButton() { if (modus.equals(Modus.SOLVERS_RUNNING)) { listener.stopButtonClicked(); } - }); } return stopButton; diff --git a/keyext.ui.testgen/src/main/java/de/uka/ilkd/key/gui/testgen/CounterExampleAction.java b/keyext.ui.testgen/src/main/java/de/uka/ilkd/key/gui/testgen/CounterExampleAction.java index db480ebfc49..be7ec1c3e2e 100644 --- a/keyext.ui.testgen/src/main/java/de/uka/ilkd/key/gui/testgen/CounterExampleAction.java +++ b/keyext.ui.testgen/src/main/java/de/uka/ilkd/key/gui/testgen/CounterExampleAction.java @@ -9,9 +9,7 @@ import javax.swing.*; import de.uka.ilkd.key.control.AutoModeListener; -import de.uka.ilkd.key.control.UserInterfaceControl; import de.uka.ilkd.key.core.InterruptListener; -import de.uka.ilkd.key.core.KeYMediator; import de.uka.ilkd.key.core.KeYSelectionEvent; import de.uka.ilkd.key.core.KeYSelectionListener; import de.uka.ilkd.key.gui.IssueDialog; @@ -22,8 +20,6 @@ import de.uka.ilkd.key.logic.Sequent; import de.uka.ilkd.key.macros.SemanticsBlastingMacro; import de.uka.ilkd.key.proof.*; -import de.uka.ilkd.key.proof.init.InitConfig; -import de.uka.ilkd.key.proof.mgt.SpecificationRepository; import de.uka.ilkd.key.settings.DefaultSMTSettings; import de.uka.ilkd.key.settings.ProofIndependentSettings; import de.uka.ilkd.key.smt.SolverLauncherListener; @@ -70,15 +66,12 @@ public void init() { @Override public void selectedNodeChanged(KeYSelectionEvent e) { final Proof proof = getMediator().getSelectedProof(); - if (proof == null) { // no proof loaded setEnabled(false); } else { final Node selNode = getMediator().getSelectedNode(); // Can be applied only to root nodes - - setEnabled(haveZ3CE && selNode.childrenCount() == 0 && !selNode.isClosed()); } } @@ -102,7 +95,6 @@ public void autoModeStarted(ProofEvent e) { @Override public void autoModeStopped(ProofEvent e) { getMediator().addKeYSelectionListener(selListener); - selListener.selectedNodeChanged(null); } }); selListener.selectedNodeChanged(new KeYSelectionEvent(getMediator().getSelectionModel())); @@ -112,16 +104,16 @@ public void autoModeStopped(ProofEvent e) { public void actionPerformed(ActionEvent e) { try { // Get required information - Goal goal = getMediator().getSelectedGoal(); - Node node = goal.node(); - Proof oldProof = node.proof(); - Sequent oldSequent = node.sequent(); - // Start SwingWorker (CEWorker) in which counter example search is performed. - getMediator().stopInterface(true); - getMediator().setInteractive(false); - CEWorker worker = new CEWorker(oldProof, oldSequent); - getMediator().addInterruptedListener(worker); - worker.execute(); + final Goal goal = getMediator().getSelectedGoal(); + if (goal != null) { + final Node node = goal.node(); + // Start SwingWorker (CEWorker) in which counter example search is performed. + getMediator().stopInterface(true); + getMediator().setInteractive(false); + CEWorker worker = new CEWorker(node.proof(), node.sequent()); + getMediator().addInterruptedListener(worker); + worker.execute(); + } } catch (Exception exc) { LOGGER.error("", exc); IssueDialog.showExceptionDialog(mainWindow, exc); @@ -165,74 +157,6 @@ protected SolverLauncherListener createSolverListener(DefaultSMTSettings setting } } - /** - * Performs the {@link SemanticsBlastingMacro} in a {@link Proof} registered in the - * {@link MainWindow} and thus visible to the user. Results are shown with help of the - * {@link SolverListener}. - *

- * This class provides only the user interface and no counter example generation logic which - * is implemented by the {@link AbstractCounterExampleGenerator}. - */ - public static class MainWindowCounterExampleGenerator extends AbstractCounterExampleGenerator { - /** - * The {@link KeYMediator} to use. - */ - private final KeYMediator mediator; - - /** - * Constructor. - * - * @param mediator The {@link KeYMediator} to use. - */ - public MainWindowCounterExampleGenerator(KeYMediator mediator) { - this.mediator = mediator; - } - - /** - * {@inheritDoc} - */ - @Override - protected Proof createProof(UserInterfaceControl ui, Proof oldProof, Sequent oldSequent, - String proofName) { - Sequent newSequent = createNewSequent(oldSequent); - InitConfig newInitConfig = oldProof.getInitConfig().deepCopy(); - Proof proof = new Proof(proofName, newSequent, "", newInitConfig.createTacletIndex(), - newInitConfig.createBuiltInRuleIndex(), newInitConfig); - - proof.setEnv(oldProof.getEnv()); - proof.setNamespaces(oldProof.getNamespaces()); - - ProofAggregate pa = new SingleProof(proof, "XXX"); - - ui.registerProofAggregate(pa); - - SpecificationRepository spec = proof.getServices().getSpecificationRepository(); - spec.registerProof(spec.getProofOblInput(oldProof), proof); - - mediator.goalChosen(proof.getOpenGoal(proof.root())); - - return proof; - } - - /** - * {@inheritDoc} - */ - @Override - protected void semanticsBlastingCompleted(UserInterfaceControl ui) { - mediator.setInteractive(true); - mediator.startInterface(true); - } - - /** - * {@inheritDoc} - */ - @Override - protected SolverLauncherListener createSolverListener(DefaultSMTSettings settings, - Proof proof) { - return new SolverListener(settings, proof); - } - } - private class CEWorker extends SwingWorker implements InterruptListener { private final Proof oldProof; private final Sequent oldSequent;