SMTSolver (KeY API Documentation)

All Known Implementing Classes:

SMTSolverImplementation
```
public interface SMTSolver
```
The SMTSolver interface represents a solver process (e.g. Z3, Simplify,...) on the KeY side. It is used to store information about an instance of a process and its result. A object of SMTSolver is, therefore, related to exactly one object of typ SMTProblem. Each object of SMTSolver has a specific solver type (SolverType), e.g SolverType.Z3Solver.
Note:
A class that implements this interface should be thread safe since there methods are accessed by different threads concurrently.

Nested Class Summary

Nested Classes
Modifier and Type Interface and Description

static class SMTSolver.ReasonOfInterruption

static class SMTSolver.SolverState
A solver process can have differnt states.

Nested Classes
Modifier and Type	Interface and Description
`static class`	`SMTSolver.ReasonOfInterruption`
`static class`	`SMTSolver.SolverState` A solver process can have differnt states.

Method Summary

All Methods Instance Methods Abstract Methods
Modifier and Type	Method and Description
`java.lang.Throwable`	`getException()` If there has occurred an exception while executing the solver process, the method returns this exceptions, otherwise `null`
`java.util.Collection<java.lang.Throwable>`	`getExceptionsOfTacletTranslation()` Returns the exceptions that has been thrown while translating taclets into assumptions.
`SMTSolverResult`	`getFinalResult()` Returns the result of the execution.
`SMTProblem`	`getProblem()` Returns the SMT Problem that is connected to this solver process.
`SMTSolver.ReasonOfInterruption`	`getReasonOfInterruption()` Returns the reason of the interruption: see `ReasonOfInterruption`.
`AbstractSolverSocket`	`getSocket()`
`java.lang.String`	`getSolverOutput()` Returns the solver output without any change.
`long`	`getStartTime()` Returns the system time when the solver was started.
`SMTSolver.SolverState`	`getState()` Returns the current state of the solver.
`TacletSetTranslation`	`getTacletTranslation()` Returns the taclet translation that is used as assumptions.
`long`	`getTimeout()` Returns the amount of milliseconds after a timeout occurs.
`java.lang.String`	`getTranslation()` Returns the translation of the SMTProblem that is handed over to the solver process.
`SolverType`	`getType()` Returns the type of the solver process.
`void`	`interrupt(SMTSolver.ReasonOfInterruption reasonOfInterruption)` Use this method in order to interrupt a running solver process.
`boolean`	`isRunning()` Returns `true` if the solver process is running else `false`.
`java.lang.String`	`name()` Returns the name of the solver.
`boolean`	`wasInterrupted()` Returns `true` if the solver process was interrupted by an user, an exception or a timeout.

- Method Detail
  - name
```
java.lang.String name()
```
    Returns the name of the solver.
  - getTranslation
```
java.lang.String getTranslation()
```
    Returns the translation of the SMTProblem that is handed over to the solver process. If the solver process is still running the method returns null in order to maintain thread safety.
    
    Returns:
    
    String representation of the corresponding problem, if the solver process is not running, otherwise null.
  - getTacletTranslation
```
TacletSetTranslation getTacletTranslation()
```
    Returns the taclet translation that is used as assumptions. If the solver process is still running the method returns null in order to maintain thread safety.
  - getType
```
SolverType getType()
```
    Returns the type of the solver process.
  - getProblem
```
SMTProblem getProblem()
```
    Returns the SMT Problem that is connected to this solver process. If the solver process is still running the method returns null in order to maintain thread safety.
  - getException
```
java.lang.Throwable getException()
```
    If there has occurred an exception while executing the solver process, the method returns this exceptions, otherwise null
  - interrupt
```
void interrupt(SMTSolver.ReasonOfInterruption reasonOfInterruption)
```
    Use this method in order to interrupt a running solver process.
    
    Parameters:
    
    reasonOfInterruption - The reason of interruption. Can only be set to ReasonOfInterruption.Timeout or ReasonOfInterruption.User other wise a IllegalArgumentException is thrown.
  - getStartTime
```
long getStartTime()
```
    Returns the system time when the solver was started. (in ms)
  - getTimeout
```
long getTimeout()
```
    Returns the amount of milliseconds after a timeout occurs. (in ms)
  - getState
```
SMTSolver.SolverState getState()
```
    Returns the current state of the solver. Possible values are
    Waiting<\code>: The solver process is waiting for the start signal Running<\code>: The solver process is running Stopped<\code>: The solver process was stopped. The reason can be a user interruption, an exception, a timeout or a successfull run.
  wasInterrupted boolean wasInterrupted() Returns true if the solver process was interrupted by an user, an exception or a timeout. In all other cases (including that the solver is still running) the method returns true. isRunning boolean isRunning() Returns true if the solver process is running else false. getReasonOfInterruption SMTSolver.ReasonOfInterruption getReasonOfInterruption() Returns the reason of the interruption: see ReasonOfInterruption. getFinalResult SMTSolverResult getFinalResult() Returns the result of the execution. If the solver process is still running the method returns a result object that represents the result 'unknown'. getSolverOutput java.lang.String getSolverOutput() Returns the solver output without any change. The format is: " Normal Output: ... Error Output: ... Exit Code: ... " getExceptionsOfTacletTranslation java.util.Collection<java.lang.Throwable> getExceptionsOfTacletTranslation() Returns the exceptions that has been thrown while translating taclets into assumptions. getSocket AbstractSolverSocket getSocket()

Interface SMTSolver

Nested Class Summary

Method Summary

Method Detail

name

getTranslation

getTacletTranslation

getType

getProblem

getException

interrupt

getStartTime

getTimeout

getState

wasInterrupted

isRunning

getReasonOfInterruption

getFinalResult

getSolverOutput

getExceptionsOfTacletTranslation

getSocket