de.uka.ilkd.key.gui.actions

Class CounterExampleAction.NoMainWindowCounterExampleGenerator

java.lang.Object

de.uka.ilkd.key.smt.counterexample.AbstractCounterExampleGenerator

de.uka.ilkd.key.smt.counterexample.AbstractSideProofCounterExampleGenerator

de.uka.ilkd.key.gui.actions.CounterExampleAction.NoMainWindowCounterExampleGenerator

Enclosing class:

CounterExampleAction

public static class CounterExampleAction.NoMainWindowCounterExampleGenerator
extends AbstractSideProofCounterExampleGenerator

Performs the SemanticsBlastingMacro in a side proof hidden to the user and shows the result with help of the SolverListener.

Constructor Summary

Constructors

Constructor and Description
NoMainWindowCounterExampleGenerator()

Method Summary

Modifier and Type	Method and Description
protected SolverLauncherListener	createSolverListener(SMTSettings settings, Proof proof) Creates the SolverLauncherListener which handles the results of the launched SMT solver.

Methods inherited from class de.uka.ilkd.key.smt.counterexample.AbstractSideProofCounterExampleGenerator

createProof

Methods inherited from class de.uka.ilkd.key.smt.counterexample.AbstractCounterExampleGenerator

createNewSequent, isSolverAvailable, searchCounterExample, semanticsBlastingCompleted

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Detail

NoMainWindowCounterExampleGenerator

public NoMainWindowCounterExampleGenerator()

Method Detail

createSolverListener

protected SolverLauncherListener createSolverListener(SMTSettings settings,
                                                      Proof proof)

Creates the SolverLauncherListener which handles the results of the launched SMT solver.

Specified by:

createSolverListener in class AbstractCounterExampleGenerator

Parameters:

settings - The SMTSettings.

proof - The Proof on which the SMT solver will be performed.

Returns:

The SolverLauncherListener to use.