Package | Description |
---|---|
de.uka.ilkd.key.gui.smt |
This package contains the graphical user interface of the SMT backend.
|
de.uka.ilkd.key.settings | |
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.communication |
This package contains the classes and interfaces to create the external SMT solver processes and
communicate with them:
ExternalProcessLauncher creates and starts the
external process and connects it to the pipe.
Pipe is responsible for sending and receiving
input/output strings to/from the external process. |
de.uka.ilkd.key.smt.testgen | |
de.uka.ilkd.key.testgen |
Modifier and Type | Method and Description |
---|---|
static java.lang.String |
SolverListener.computeSolverTypeWarningMessage(SolverType type) |
Modifier and Type | Method and Description |
---|---|
void |
SolverListener.launcherStarted(java.util.Collection<SMTProblem> smtproblems,
java.util.Collection<SolverType> solverTypes,
SolverLauncher launcher) |
Modifier and Type | Field and Description |
---|---|
SolverType |
ProofIndependentSMTSettings.SolverData.type |
Modifier and Type | Method and Description |
---|---|
java.util.Collection<SolverType> |
ProofIndependentSMTSettings.getSupportedSolvers() |
Modifier and Type | Method and Description |
---|---|
java.lang.String |
ProofIndependentSMTSettings.getCommand(SolverType type) |
java.lang.String |
ProofIndependentSMTSettings.getParameters(SolverType type) |
void |
ProofIndependentSMTSettings.setCommand(SolverType type,
java.lang.String command) |
void |
ProofIndependentSMTSettings.setParameters(SolverType type,
java.lang.String parameters) |
Constructor and Description |
---|
SolverData(SolverType type) |
Modifier and Type | Field and Description |
---|---|
static SolverType |
SolverType.CVC4_NEW_TL_SOLVER
CVC4 with the new translation
|
static SolverType |
SolverType.CVC4_SOLVER
CVC4 is the successor to CVC3.
|
static SolverType |
SolverType.Z3_CE_SOLVER
Class for the Z3 solver.
|
static SolverType |
SolverType.Z3_NEW_TL_SOLVER
Z3 with new modular translator
|
static SolverType |
SolverType.Z3_SOLVER
Class for the Z3 solver.
|
Modifier and Type | Field and Description |
---|---|
static java.util.List<SolverType> |
SolverType.ALL_SOLVERS |
Modifier and Type | Method and Description |
---|---|
SolverType |
SMTSolver.getType()
Returns the type of the solver process.
|
Modifier and Type | Method and Description |
---|---|
java.util.LinkedList<SolverType> |
SolverTypeCollection.getTypes() |
java.util.Iterator<SolverType> |
SolverTypeCollection.iterator() |
Modifier and Type | Method and Description |
---|---|
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. |
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) |
Constructor and Description |
---|
SolverTypeCollection(java.lang.String name,
int minUsableSolvers,
SolverType type,
SolverType... types) |
SolverTypeCollection(java.lang.String name,
int minUsableSolvers,
SolverType type,
SolverType... types) |
Constructor and Description |
---|
SolverTypeCollection(java.lang.String name,
int minUsableSolvers,
java.util.Collection<SolverType> types)
Instantiates a new solver type collection.
|
Modifier and Type | Method and Description |
---|---|
static AbstractSolverSocket |
AbstractSolverSocket.createSocket(SolverType type,
ModelExtractor query)
Creates a new solver socket that can handle the communication for the given solver type.
|
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.