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.
|
java.lang.String |
getRawSolverInput()
Returns the raw solver input.
|
java.lang.String |
getRawSolverOutput()
Returns the raw solver output.
|
SMTSolver.ReasonOfInterruption |
getReasonOfInterruption()
Returns the reason of the interruption: see
ReasonOfInterruption . |
AbstractSolverSocket |
getSocket() |
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.
|
void |
start(de.uka.ilkd.key.smt.SolverTimeout timeout,
SMTSettings settings)
Starts a solver process.
|
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
.void start(de.uka.ilkd.key.smt.SolverTimeout timeout, SMTSettings settings)
SolverLauncher
. If you want to start a
solver please have a look at SolverLauncher
.timeout
- settings
- SMTSolver.ReasonOfInterruption getReasonOfInterruption()
ReasonOfInterruption
.SMTSolverResult getFinalResult()
java.lang.String getRawSolverOutput()
java.lang.String getRawSolverInput()
java.util.Collection<java.lang.Throwable> getExceptionsOfTacletTranslation()
AbstractSolverSocket getSocket()
Copyright © 2003-2019 The KeY-Project.