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 |
---|---|
SMTProblem |
SolverListener.InternSMTProblem.getProblem() |
Modifier and Type | Method and Description |
---|---|
void |
SolverListener.launcherStarted(java.util.Collection<SMTProblem> smtproblems,
java.util.Collection<SolverType> solverTypes,
SolverLauncher launcher) |
Constructor and Description |
---|
InternSMTProblem(int problemIndex,
int solverIndex,
SMTProblem problem,
SMTSolver solver) |
Modifier and Type | Method and Description |
---|---|
SMTProblem |
SMTSolver.getProblem()
Returns the SMT Problem that is connected to this solver process.
|
Modifier and Type | Method and Description |
---|---|
static java.util.Collection<SMTProblem> |
SMTProblem.createSMTProblems(Proof proof)
Creates out of a proof object several SMT problems.
|
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.
|
void |
SolverLauncher.launch(SMTProblem problem,
Services services,
SolverType... solverTypes)
Launches several solvers for the problem that is handed over.
Note: Calling this methods does not create an extra thread, i.e. |
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 |
SolverLauncher.launch(java.util.Collection<SolverType> solverTypes,
java.util.Collection<SMTProblem> problems,
Services services)
Launches several solvers for the problems that are handed over.
|
void |
SolverLauncherListener.launcherStarted(java.util.Collection<SMTProblem> problems,
java.util.Collection<SolverType> solverTypes,
SolverLauncher launcher) |
Modifier and Type | Method and Description |
---|---|
protected void |
AbstractTestGenerator.handleLauncherStarted(java.util.Collection<SMTProblem> problems,
java.util.Collection<SolverType> solverTypes,
SolverLauncher launcher,
TestGenerationLog log) |
Modifier and Type | Method and Description |
---|---|
void |
ModelGenerator.launcherStarted(java.util.Collection<SMTProblem> problems,
java.util.Collection<SolverType> solverTypes,
SolverLauncher launcher) |
Copyright © 2003-2019 The KeY-Project.