Package | Description |
---|---|
de.uka.ilkd.key.gui.smt |
This package contains the graphical user interface of the SMT backend.
|
de.uka.ilkd.key.smt |
This package contains the SMT backend of KeY, allowing to translate KeY formulas
to formulas in formats such as SMT-LIB, and allowing to send such formulas to
SMT solvers such as Simplify or Z3.
|
de.uka.ilkd.key.smt.testgen | |
de.uka.ilkd.key.testgen |
Modifier and Type | Method and Description |
---|---|
void |
SolverListener.launcherStopped(SolverLauncher launcher,
java.util.Collection<SMTSolver> problemSolvers) |
Constructor and Description |
---|
InformationWindow(java.awt.Dialog parent,
SMTSolver solver,
java.util.Collection<InformationWindow.Information> information,
java.lang.String title) |
InternSMTProblem(int problemIndex,
int solverIndex,
SMTProblem problem,
SMTSolver solver) |
Modifier and Type | Method and Description |
---|---|
SMTSolver |
SolverType.createSolver(SMTProblem problem,
de.uka.ilkd.key.smt.SolverListener listener,
Services services)
Creates an instance of SMTSolver representing a concrete instance of that solver.
|
Modifier and Type | Method and Description |
---|---|
java.util.Collection<SMTSolver> |
SolverException.getSolvers() |
java.util.Collection<SMTSolver> |
SMTProblem.getSolvers()
Returns the solvers that are related to the problem
|
Modifier and Type | Method and Description |
---|---|
void |
SolverLauncher.processInterrupted(SMTSolver solver,
SMTProblem problem,
java.lang.Throwable e) |
void |
SolverLauncher.processStarted(SMTSolver solver,
SMTProblem problem) |
void |
SolverLauncher.processStopped(SMTSolver solver,
SMTProblem problem) |
void |
SolverLauncher.processTimeout(SMTSolver solver,
SMTProblem problem) |
void |
SolverLauncher.processUser(SMTSolver solver,
SMTProblem problem) |
Modifier and Type | Method and Description |
---|---|
void |
SolverLauncherListener.launcherStopped(SolverLauncher launcher,
java.util.Collection<SMTSolver> finishedSolvers) |
Constructor and Description |
---|
SolverException(java.util.Collection<SMTSolver> solvers) |
Modifier and Type | Method and Description |
---|---|
java.util.Collection<SMTSolver> |
AbstractTestGenerator.filterSolverResultsAndShowSolverStatistics(java.util.Collection<SMTSolver> problemSolvers,
TestGenerationLog log) |
Modifier and Type | Method and Description |
---|---|
java.util.Collection<SMTSolver> |
AbstractTestGenerator.filterSolverResultsAndShowSolverStatistics(java.util.Collection<SMTSolver> problemSolvers,
TestGenerationLog log) |
protected void |
AbstractTestGenerator.generateFiles(java.util.Collection<SMTSolver> problemSolvers,
TestGenerationLog log,
Proof originalProof) |
protected void |
AbstractTestGenerator.handleLauncherStopped(SolverLauncher launcher,
java.util.Collection<SMTSolver> problemSolvers,
TestGenerationLog log) |
protected void |
AbstractTestGenerator.informAboutNoTestResults(SolverLauncher launcher,
java.util.Collection<SMTSolver> problemSolvers,
TestGenerationLog log,
Proof originalProof)
This method is used in the Eclipse world to show a dialog with the log.
|
Modifier and Type | Method and Description |
---|---|
java.lang.StringBuffer |
TestCaseGenerator.createTestCaseCotent(java.util.Collection<SMTSolver> problemSolvers) |
java.lang.String |
TestCaseGenerator.generateJUnitTestSuite(java.util.Collection<SMTSolver> problemSolvers) |
void |
ModelGenerator.launcherStopped(SolverLauncher launcher,
java.util.Collection<SMTSolver> finishedSolvers) |
Copyright © 2003-2019 The KeY-Project.