de.uka.ilkd.key.smt

Class SMTSolverImplementation

java.lang.Object

de.uka.ilkd.key.smt.SMTSolverImplementation

All Implemented Interfaces:

SMTSolver, java.lang.Runnable

final class SMTSolverImplementation
extends java.lang.Object
implements SMTSolver, java.lang.Runnable

Nested Class Summary

Nested classes/interfaces inherited from interface de.uka.ilkd.key.smt.SMTSolver

SMTSolver.ReasonOfInterruption, SMTSolver.SolverState

Field Summary

Fields

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 Summary

Constructors

Constructor and Description
SMTSolverImplementation(SMTProblem problem, SolverListener listener, Services services, SolverType myType)

Method Summary

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.

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait

Field Detail

IDCounter

private static int IDCounter

ID

private final int ID

socket

private AbstractSolverSocket socket

query

private ModelExtractor query

problem

private SMTProblem problem

The SMT problem that is related to this solver

listener

private SolverListener listener

It is possible that a solver has a listener.

processLauncher

private ExternalProcessLauncher<SolverCommunication> processLauncher

starts a external process and returns the result

services

private Services services

The services object is stored in order to have the possibility to access it in every method

solverCommunication

private SolverCommunication solverCommunication

The record of the communication between KeY and the given solver. If everything works fine, it also contains the final result.

problemTypeInformation

private ProblemTypeInformation problemTypeInformation

This holds information relevant for retrieving information on a model from an SMT instance. null in the beginning, is created at translation time.

lockStateVariable

private java.util.concurrent.locks.ReentrantLock lockStateVariable

This lock variable is responsible for the state variable sovlerState

lockInterruptionVariable

private java.util.concurrent.locks.ReentrantLock lockInterruptionVariable

This lock variable is responsible for the attribute reasonOfInterruption

thread

private java.lang.Thread thread

The thread that is associated with this solver.

solverTimeout

private SolverTimeout solverTimeout

The timeout that is associated with this solver. Represents the timertask that is started when the solver is started.

reasonOfInterruption

private SMTSolver.ReasonOfInterruption reasonOfInterruption

solverState

private SMTSolver.SolverState solverState

type

private final SolverType type

smtSettings

private SMTSettings smtSettings

Strores the settings that are used for the execution.

problemString

private java.lang.String problemString

Stores the translation of the problem that is associated with this solver

tacletTranslation

private TacletSetTranslation tacletTranslation

Stores the taclet translation that is associated with this solver.

exception

private java.lang.Throwable exception

If there was an exception while executing the solver it is stored in this attribute

exceptionsForTacletTranslation

private java.util.Collection<java.lang.Throwable> exceptionsForTacletTranslation

Constructor Detail

SMTSolverImplementation

SMTSolverImplementation(SMTProblem problem,
                        SolverListener listener,
                        Services services,
                        SolverType myType)

Method Detail

getQuery

public ModelExtractor getQuery()

setQuery

public void setQuery(ModelExtractor query)

start

public void start(SolverTimeout timeout,
                  SMTSettings settings)

Starts a solver process. This method should be accessed only by an instance of SolverLauncher. If you want to start a solver please have a look at SolverLauncher.

Parameters:

timeout -

settings -

getReasonOfInterruption

public SMTSolver.ReasonOfInterruption getReasonOfInterruption()

Description copied from interface: SMTSolver

Returns the reason of the interruption: see ReasonOfInterruption.

Specified by:

getReasonOfInterruption in interface SMTSolver

getException

public java.lang.Throwable getException()

Description copied from interface: SMTSolver

If there has occurred an exception while executing the solver process, the method returns this exceptions, otherwise null

Specified by:

getException in interface SMTSolver

getProblem

public SMTProblem getProblem()

Description copied from interface: SMTSolver

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.

Specified by:

getProblem in interface SMTSolver

setReasonOfInterruption

public void setReasonOfInterruption(SMTSolver.ReasonOfInterruption reasonOfInterruption)

setReasonOfInterruption

private void setReasonOfInterruption(SMTSolver.ReasonOfInterruption reasonOfInterruption,
                                     java.lang.Throwable exc)

getType

public SolverType getType()

Description copied from interface: SMTSolver

Returns the type of the solver process.

Specified by:

getType in interface SMTSolver

getStartTime

public long getStartTime()

Description copied from interface: SMTSolver

Returns the system time when the solver was started. (in ms)

Specified by:

getStartTime in interface SMTSolver

getTimeout

public long getTimeout()

Description copied from interface: SMTSolver

Returns the amount of milliseconds after a timeout occurs. (in ms)

Specified by:

getTimeout in interface SMTSolver

getState

public SMTSolver.SolverState getState()

Description copied from interface: SMTSolver

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.

Specified by:

getState in interface SMTSolver

setSolverState

private void setSolverState(SMTSolver.SolverState value)

wasInterrupted

public boolean wasInterrupted()

Description copied from interface: SMTSolver

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.

Specified by:

wasInterrupted in interface SMTSolver

isRunning

public boolean isRunning()

Description copied from interface: SMTSolver

Returns true if the solver process is running else false.

Specified by:

isRunning in interface SMTSolver

run

public void run()

Specified by:

run in interface java.lang.Runnable

interruptionOccurred

private void interruptionOccurred(java.lang.Throwable e)

name

public java.lang.String name()

Description copied from interface: SMTSolver

Returns the name of the solver.

Specified by:

name in interface SMTSolver

indent

private static java.lang.String indent(java.lang.String string)

translateToCommand

private java.lang.String[] translateToCommand(Term term)
                                       throws IllegalFormulaException,
                                              java.io.IOException

Throws:

IllegalFormulaException

java.io.IOException

interrupt

public void interrupt(SMTSolver.ReasonOfInterruption reason)

Description copied from interface: SMTSolver

Use this method in order to interrupt a running solver process.

Specified by:

interrupt in interface SMTSolver

Parameters:

reason - The reason of interruption. Can only be set to ReasonOfInterruption.Timeout or ReasonOfInterruption.User other wise a IllegalArgumentException is thrown.

getFinalResult

public SMTSolverResult getFinalResult()

Description copied from interface: SMTSolver

Returns the result of the execution. If the solver process is still running the method returns a result object that represents the result 'unknown'.

Specified by:

getFinalResult in interface SMTSolver

getTacletTranslation

public TacletSetTranslation getTacletTranslation()

Description copied from interface: SMTSolver

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.

Specified by:

getTacletTranslation in interface SMTSolver

getTranslation

public java.lang.String getTranslation()

Description copied from interface: SMTSolver

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.

Specified by:

getTranslation in interface SMTSolver

Returns:

String representation of the corresponding problem, if the solver process is not running, otherwise null.

toString

public java.lang.String toString()

Overrides:

toString in class java.lang.Object

getSolverOutput

public java.lang.String getSolverOutput()

Description copied from interface: SMTSolver

Returns the solver output without any change. The format is: " Normal Output: ... Error Output: ... Exit Code: ... "

Specified by:

getSolverOutput in interface SMTSolver

getExceptionsOfTacletTranslation

public java.util.Collection<java.lang.Throwable> getExceptionsOfTacletTranslation()

Description copied from interface: SMTSolver

Returns the exceptions that has been thrown while translating taclets into assumptions.

Specified by:

getExceptionsOfTacletTranslation in interface SMTSolver

getSocket

public AbstractSolverSocket getSocket()

Specified by:

getSocket in interface SMTSolver