Package | Description |
---|---|
de.uka.ilkd.key.gui.smt |
This package contains the graphical user interface of the SMT backend.
|
de.uka.ilkd.key.gui.testgen |
This package contains the graphical user interface of the test generation 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.counterexample | |
de.uka.ilkd.key.smt.model | |
de.uka.ilkd.key.smt.newsmt2 | |
de.uka.ilkd.key.smt.testgen | |
de.uka.ilkd.key.taclettranslation.assumptions | |
de.uka.ilkd.key.testgen | |
org.key_project.ui.interactionlog.model.builtin |
Class and Description |
---|
SMTProblem
Represents a problem that can be passed to a solver.
|
SMTSolver
The SMTSolver interface represents a solver process (e.g.
|
SolverLauncher
IN ORDER TO START THE SOLVERS USE THIS CLASS.
There are two cases how the solvers can be started: 1. |
SolverLauncherListener
This interface can be used to observe a launcher.
|
SolverType
This interface is used for modeling different solvers.
|
SolverTypeCollection
Stores a set of solver types.
|
Class and Description |
---|
SolverLauncherListener
This interface can be used to observe a launcher.
|
Class and Description |
---|
SMTSettings |
SolverType
This interface is used for modeling different solvers.
|
SolverTypeCollection
Stores a set of solver types.
|
Class and Description |
---|
AbstractSMTTranslator
This abstract class provides a stub for translation of KeY-Formulas to other
standards.
|
AbstractSMTTranslator.Configuration |
AbstractSMTTranslator.FunctionWrapper
remember all function declarations
|
IllegalFormulaException |
ModelExtractor
Class for sending queries to the solver and extracting the relevant information regarding the model.
|
ProblemTypeInformation |
RuleAppSMT
The rule application that is used when a goal is closed by means of an external solver.
|
RuleAppSMT.SMTRule |
SMTProblem
Represents a problem that can be passed to a solver.
|
SMTSettings |
SMTSolver
The SMTSolver interface represents a solver process (e.g.
|
SMTSolver.ReasonOfInterruption |
SMTSolver.SolverState
A solver process can have differnt states.
|
SMTSolverResult
Encapsulates the result of a single solver.
|
SMTSolverResult.ThreeValuedTruth
In the context of proving nodes/sequents these values mean the following:
TRUE iff negation of the sequent is unsatisfiable,
FALSIFIABLE iff negation of the sequent is satisfiable (i.e.
|
SMTTranslator
Classes that implement this interface provide a translation of
a KeY-problem into a specific format.
|
SolverLauncher
IN ORDER TO START THE SOLVERS USE THIS CLASS.
There are two cases how the solvers can be started: 1. |
SolverLauncherListener
This interface can be used to observe a launcher.
|
SolverType
This interface is used for modeling different solvers.
|
SolverTypeCollection
Stores a set of solver types.
|
SortHierarchy
The SortHierarchy works as a wrapper class for sorts.
|
VersionChecker
Little helper class that helps to check for the version of a solver.
|
Class and Description |
---|
ModelExtractor
Class for sending queries to the solver and extracting the relevant information regarding the model.
|
SMTSolverResult
Encapsulates the result of a single solver.
|
SolverType
This interface is used for modeling different solvers.
|
Class and Description |
---|
SolverLauncherListener
This interface can be used to observe a launcher.
|
Class and Description |
---|
ProblemTypeInformation |
Class and Description |
---|
SMTSettings |
SMTTranslationException |
SMTTranslator
Classes that implement this interface provide a translation of
a KeY-problem into a specific format.
|
Class and Description |
---|
SMTProblem
Represents a problem that can be passed to a solver.
|
SMTSolver
The SMTSolver interface represents a solver process (e.g.
|
SolverLauncher
IN ORDER TO START THE SOLVERS USE THIS CLASS.
There are two cases how the solvers can be started: 1. |
SolverType
This interface is used for modeling different solvers.
|
Class and Description |
---|
SMTSettings |
Class and Description |
---|
SMTProblem
Represents a problem that can be passed to a solver.
|
SMTSolver
The SMTSolver interface represents a solver process (e.g.
|
SolverLauncher
IN ORDER TO START THE SOLVERS USE THIS CLASS.
There are two cases how the solvers can be started: 1. |
SolverLauncherListener
This interface can be used to observe a launcher.
|
SolverType
This interface is used for modeling different solvers.
|
Class and Description |
---|
RuleAppSMT
The rule application that is used when a goal is closed by means of an external solver.
|
Copyright © 2003-2019 The KeY-Project.