SMTSolver.ReasonOfInterruption, SMTSolver.SolverState
Modifier and Type | Field and Description |
---|---|
private java.lang.Throwable |
exception
If there was an exception while executing the solver it is stored in
this attribute
|
private java.util.Collection<java.lang.Throwable> |
exceptionsForTacletTranslation |
private int |
ID |
private static int |
IDCounter |
private SolverListener |
listener
It is possible that a solver has a listener.
|
private java.util.concurrent.locks.ReentrantLock |
lockInterruptionVariable
This lock variable is responsible for the attribute
reasonOfInterruption |
private java.util.concurrent.locks.ReentrantLock |
lockStateVariable
This lock variable is responsible for the state variable
sovlerState |
private SMTProblem |
problem
The SMT problem that is related to this solver
|
private java.lang.String |
problemString
Stores the translation of the problem that is associated with this
solver
|
private ProblemTypeInformation |
problemTypeInformation
This holds information relevant for retrieving information on a model
from an SMT instance.
|
private ExternalProcessLauncher<SolverCommunication> |
processLauncher
starts a external process and returns the result
|
private ModelExtractor |
query |
private SMTSolver.ReasonOfInterruption |
reasonOfInterruption |
private Services |
services
The services object is stored in order to have the possibility to
access it in every method
|
private SMTSettings |
smtSettings
Strores the settings that are used for the execution.
|
private AbstractSolverSocket |
socket |
private SolverCommunication |
solverCommunication
The record of the communication between KeY and the given solver.
|
private SMTSolver.SolverState |
solverState |
private SolverTimeout |
solverTimeout
The timeout that is associated with this solver.
|
private TacletSetTranslation |
tacletTranslation
Stores the taclet translation that is associated with this solver.
|
private java.lang.Thread |
thread
The thread that is associated with this solver.
|
private SolverType |
type |
Constructor and Description |
---|
SMTSolverImplementation(SMTProblem problem,
SolverListener listener,
Services services,
SolverType myType) |
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.
|
ModelExtractor |
getQuery() |
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.
|
private static java.lang.String |
indent(java.lang.String string) |
void |
interrupt(SMTSolver.ReasonOfInterruption reason)
Use this method in order to interrupt a running solver process.
|
private void |
interruptionOccurred(java.lang.Throwable e) |
boolean |
isRunning()
Returns
true if the solver process is running else
false . |
java.lang.String |
name()
Returns the name of the solver.
|
void |
run() |
void |
setQuery(ModelExtractor query) |
void |
setReasonOfInterruption(SMTSolver.ReasonOfInterruption reasonOfInterruption) |
private void |
setReasonOfInterruption(SMTSolver.ReasonOfInterruption reasonOfInterruption,
java.lang.Throwable exc) |
private void |
setSolverState(SMTSolver.SolverState value) |
void |
start(SolverTimeout timeout,
SMTSettings settings)
Starts a solver process.
|
java.lang.String |
toString() |
private java.lang.String[] |
translateToCommand(Term term) |
boolean |
wasInterrupted()
Returns
true if the solver process was interrupted by an
user, an exception or a timeout. |
private static int IDCounter
private final int ID
private AbstractSolverSocket socket
private ModelExtractor query
private SMTProblem problem
private SolverListener listener
private ExternalProcessLauncher<SolverCommunication> processLauncher
private Services services
private SolverCommunication solverCommunication
private ProblemTypeInformation problemTypeInformation
private java.util.concurrent.locks.ReentrantLock lockStateVariable
sovlerState
private java.util.concurrent.locks.ReentrantLock lockInterruptionVariable
reasonOfInterruption
private java.lang.Thread thread
private SolverTimeout solverTimeout
private SMTSolver.ReasonOfInterruption reasonOfInterruption
private SMTSolver.SolverState solverState
private final SolverType type
private SMTSettings smtSettings
private java.lang.String problemString
private TacletSetTranslation tacletTranslation
private java.lang.Throwable exception
private java.util.Collection<java.lang.Throwable> exceptionsForTacletTranslation
SMTSolverImplementation(SMTProblem problem, SolverListener listener, Services services, SolverType myType)
public ModelExtractor getQuery()
public void setQuery(ModelExtractor query)
public void start(SolverTimeout timeout, SMTSettings settings)
SolverLauncher
. If you want to start a
solver please have a look at SolverLauncher
.timeout
- settings
- public SMTSolver.ReasonOfInterruption getReasonOfInterruption()
SMTSolver
ReasonOfInterruption
.getReasonOfInterruption
in interface SMTSolver
public java.lang.Throwable getException()
SMTSolver
null
getException
in interface SMTSolver
public SMTProblem getProblem()
SMTSolver
null
in
order to maintain thread safety.getProblem
in interface SMTSolver
public void setReasonOfInterruption(SMTSolver.ReasonOfInterruption reasonOfInterruption)
private void setReasonOfInterruption(SMTSolver.ReasonOfInterruption reasonOfInterruption, java.lang.Throwable exc)
public SolverType getType()
SMTSolver
public long getStartTime()
SMTSolver
getStartTime
in interface SMTSolver
public long getTimeout()
SMTSolver
getTimeout
in interface SMTSolver
public SMTSolver.SolverState getState()
SMTSolver
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.
private void setSolverState(SMTSolver.SolverState value)
public boolean wasInterrupted()
SMTSolver
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
.wasInterrupted
in interface SMTSolver
public boolean isRunning()
SMTSolver
true
if the solver process is running else
false
.public void run()
run
in interface java.lang.Runnable
private void interruptionOccurred(java.lang.Throwable e)
public java.lang.String name()
SMTSolver
private static java.lang.String indent(java.lang.String string)
private java.lang.String[] translateToCommand(Term term) throws IllegalFormulaException, java.io.IOException
IllegalFormulaException
java.io.IOException
public void interrupt(SMTSolver.ReasonOfInterruption reason)
SMTSolver
public SMTSolverResult getFinalResult()
SMTSolver
getFinalResult
in interface SMTSolver
public TacletSetTranslation getTacletTranslation()
SMTSolver
null
in order to
maintain thread safety.getTacletTranslation
in interface SMTSolver
public java.lang.String getTranslation()
SMTSolver
null
in order to maintain thread safety.getTranslation
in interface SMTSolver
public java.lang.String toString()
toString
in class java.lang.Object
public java.lang.String getSolverOutput()
SMTSolver
getSolverOutput
in interface SMTSolver
public java.util.Collection<java.lang.Throwable> getExceptionsOfTacletTranslation()
SMTSolver
getExceptionsOfTacletTranslation
in interface SMTSolver
public AbstractSolverSocket getSocket()