public static class CounterExampleAction.NoMainWindowCounterExampleGenerator extends AbstractSideProofCounterExampleGenerator
SemanticsBlastingMacro
in a side proof hidden to the
user and shows the result with help of the SolverListener
.Constructor and Description |
---|
NoMainWindowCounterExampleGenerator() |
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. |
createProof
createNewSequent, isSolverAvailable, searchCounterExample, semanticsBlastingCompleted
protected SolverLauncherListener createSolverListener(SMTSettings settings, Proof proof)
SolverLauncherListener
which handles the results
of the launched SMT solver.createSolverListener
in class AbstractCounterExampleGenerator
settings
- The SMTSettings
.proof
- The Proof
on which the SMT solver will be performed.SolverLauncherListener
to use.