Package | Description |
---|---|
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. |
Class and Description |
---|
AbstractSolverSocket
The SolverSocket class describes the communication between the KeY and the SMT solver process.
|
Pipe
This interface describes a pipe for sending messages to or receiving them from an external
SMT solver process.
|
Class and Description |
---|
AbstractSolverSocket
The SolverSocket class describes the communication between the KeY and the SMT solver process.
|
Pipe
This interface describes a pipe for sending messages to or receiving them from an external
SMT solver process.
|
SolverCommunication
Stores the communication between KeY and an external solver: Contains a list that stores the
messages that have been sent from the solver to KeY and vice versa.
|
SolverCommunication.Message
Represents a single message sent from or to the solver.
|
SolverCommunication.MessageType
The message type depends on the channel which was used for sending the message.
|
Copyright © 2003-2019 The KeY-Project.