public interface SMTSolver
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
. Modifier and Type | Interface and Description |
---|---|
static class |
SMTSolver.ReasonOfInterruption |
static class |
SMTSolver.SolverState
A solver process can have differnt states.
|
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. |
java.lang.String name()
java.lang.String getTranslation()
null
in order to maintain thread safety.TacletSetTranslation getTacletTranslation()
null
in order to
maintain thread safety.SolverType getType()
SMTProblem getProblem()
null
in
order to maintain thread safety.java.lang.Throwable getException()
null
void interrupt(SMTSolver.ReasonOfInterruption reasonOfInterruption)
reasonOfInterruption
- The reason of interruption. Can only be set to
ReasonOfInterruption.Timeout
or
ReasonOfInterruption.User
other wise a
IllegalArgumentException
is thrown.long getStartTime()
long getTimeout()
SMTSolver.SolverState getState()
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.
boolean wasInterrupted()
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
.boolean isRunning()
true
if the solver process is running else
false
.SMTSolver.ReasonOfInterruption getReasonOfInterruption()
ReasonOfInterruption
.SMTSolverResult getFinalResult()
java.lang.String getSolverOutput()
java.util.Collection<java.lang.Throwable> getExceptionsOfTacletTranslation()
AbstractSolverSocket getSocket()