de.uka.ilkd.key.smt

Class SolverLauncher

java.lang.Object

de.uka.ilkd.key.smt.SolverLauncher

All Implemented Interfaces:

SolverListener

public class SolverLauncher
extends java.lang.Object
implements SolverListener

IN ORDER TO START THE SOLVERS USE THIS CLASS.
There are two cases how the solvers can be started:

1. Case: Starting the solvers synchronously

First Step: Create the SMT problem:
SMTProblem problem = new SMTProblem(g); // g can be either a goal or term

Second Step: Create the launcher object:
SolverLauncher launcher = new SolverLauncher(new SMTSettings(){...});

Third Step: Launch the solvers you want to execute
launcher.launch(problem, services,SolverType.Z3_SOLVER,SolverType.YICES_SOLVER);

Forth Step: Get the final result
return problem.getFinalResult();

In case that you want to access the result of each solver:

 for (SMTSolver solver : problem.getSolvers()) {
     solver.getFinalResult();
 }

2. Case: Starting the solvers asynchronously:

 Thread thread = new Thread(new Runnable() {        
 public void run() {
   SMTProblem final problem = new SMTProblem(...);
   SolverLauncher launcher = new SolverLauncher(new SMTSettings(...));
   launcher.addListener(new SolverLauncherListener(){
          public void launcherStopped(SolverLauncher launcher, Collection problemSolvers){
                // do something with the results here...
                problem.getFinalResult();
                // handling the problems that have occurred:
                for(SMTSolver solver : problemSolvers){
                        solver.getException();
                        ...
                }
          }
          public void launcherStarted(Collection problems,
                                      Collection solverTypes,
                                      SolverLauncher launcher);
                 });
   launcher.launch(problem,services,SolverType.Z3_SOLVER,SolverType.YICES_SOLVER);
              
                }
            });
    thread.start();

NOTE: In case that you add at least one listener to a launcher no exception is thrown when a solver produces an error. The exceptions of the solvers are stored within the solver object and can be accessed by solver.getException.

Field Summary

Fields

Modifier and Type	Field and Description
private boolean	launcherHasBeenUsed Every launcher object should be used only once.
private java.util.LinkedList<SolverLauncherListener>	listeners
private java.util.concurrent.locks.ReentrantLock	lock Used for synchronisation.
private static int	PERIOD Period of a timer task.
private Session	session A sesion encapsulates some attributes that should be accessed only by specified methods (in oder to maintain thread safety)
private SMTSettings	settings The SMT settings that should be used
private java.util.concurrent.Semaphore	stopSemaphore This semaphore is used for stopping the launcher.
private java.util.Timer	timer The timer that is responsible for the timeouts.
private java.util.concurrent.locks.Condition	wait This condition is used in order to make the launcher thread wait.

Constructor Summary

Constructors

Constructor and Description
SolverLauncher(SMTSettings settings) Create for every solver execution a new object.

Method Summary

Modifier and Type	Method and Description
void	addListener(SolverLauncherListener listener) Adds a listener to the launcher object.
private void	checkLaunchCall()
private void	cleanUp(java.util.Collection<SMTSolver> solvers) In case of that the user has interrupted the execution the reason of interruption must be set.
private void	fillRunningList(java.util.LinkedList<SMTSolver> solvers) Takes the next solvers from the queue and starts them.
private boolean	isInterrupted() If all permits of the semaphore are acquired the launcher must be stopped.
void	launch(java.util.Collection<SolverType> solverTypes, java.util.Collection<SMTProblem> problems, Services services) Launches several solvers for the problems that are handed over.
void	launch(SMTProblem problem, Services services, SolverType... solverTypes) Launches several solvers for the problem that is handed over.
private void	launcherInterrupted(java.lang.Exception e) If there is some exception that is caused by the launcher (not by the solvers) just forward it
private void	launchIntern(java.util.Collection<SMTProblem> problems, java.util.Collection<SolverType> factories)
private void	launchIntern(java.util.Collection<SolverType> factories, java.util.Collection<SMTProblem> problems, Services services)
private void	launchIntern(SMTProblem problem, Services services, SolverType[] solverTypes)
private void	launchLoop(java.util.LinkedList<SMTSolver> solvers) Core of the launcher.
private void	launchSolvers(java.util.LinkedList<SMTSolver> solvers, java.util.Collection<SMTProblem> problems, java.util.Collection<SolverType> solverTypes)
private void	notifyListenersOfStart(java.util.Collection<SMTProblem> problems, java.util.Collection<SolverType> solverTypes)
private void	notifyListenersOfStop()
private void	notifySolverHasFinished(SMTSolver solver) Is called when a solver has finished its task (Solver Thread).
private java.util.Collection<SMTProblem>	prepareSolvers(java.util.Collection<SolverType> factories, java.util.Collection<SMTProblem> problems, Services services) Creates the concrete solver objects and distributes them to the SMT problems.
void	processInterrupted(SMTSolver solver, SMTProblem problem, java.lang.Throwable e)
void	processStarted(SMTSolver solver, SMTProblem problem)
void	processStopped(SMTSolver solver, SMTProblem problem)
void	processTimeout(SMTSolver solver, SMTProblem problem)
void	processUser(SMTSolver solver, SMTProblem problem)
void	removeListener(SolverLauncherListener listener)
private boolean	startNextSolvers(java.util.LinkedList<SMTSolver> solvers) Checks whether it is possible to start another solver.
void	stop() Stops the execution of the launcher.
private void	waitForRunningSolvers() The launcher should not be stopped until every solver has stopped.

Methods inherited from class java.lang.Object

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

Field Detail

PERIOD

private static final int PERIOD

Period of a timer task. Sometimes it happens that a timer event got lost. Therefore the timer tasks are called periodly until it is canceld

See Also:

Constant Field Values

lock

private final java.util.concurrent.locks.ReentrantLock lock

Used for synchronisation. This lock is used in the same way as the synchronizestatement.

wait

private final java.util.concurrent.locks.Condition wait

This condition is used in order to make the launcher thread wait. The launcher goes to sleep when no more solvers can be started and some other solvers are still executed. Everytime a solver stops it sends a signal to the wait-condition in order to wake up the launcher.

timer

private final java.util.Timer timer

The timer that is responsible for the timeouts.

session

private final Session session

A sesion encapsulates some attributes that should be accessed only by specified methods (in oder to maintain thread safety)

settings

private final SMTSettings settings

The SMT settings that should be used

stopSemaphore

private final java.util.concurrent.Semaphore stopSemaphore

This semaphore is used for stopping the launcher. If the permit is acquired the launcher stops.

listeners

private java.util.LinkedList<SolverLauncherListener> listeners

launcherHasBeenUsed

private boolean launcherHasBeenUsed

Every launcher object should be used only once.

Constructor Detail

SolverLauncher

public SolverLauncher(SMTSettings settings)

Create for every solver execution a new object. Don't reuse the solver launcher object.

Parameters:

settings - settings for the execution of the SMT Solvers.

Method Detail

addListener

public void addListener(SolverLauncherListener listener)

Adds a listener to the launcher object. The listener can be used to observe the solver execution. If at least one listener was added to the solver launcher, no exception is thrown when a solver produces an error. The error can be read when the method launcherStopped of the listener is called.

removeListener

public void removeListener(SolverLauncherListener listener)

launch

public void launch(SMTProblem problem,
                   Services services,
                   SolverType... solverTypes)

Launches several solvers for the problem that is handed over.
Note: Calling this methods does not create an extra thread, i.e. the calling thread is blocked until the method returns. (Synchronous method call).

Parameters:

problem - The problem that should be translated and passed to the solvers

services - The services object of the current proof.

solverTypes - A list of solver types that should be used for the problem.

launch

public void launch(java.util.Collection<SolverType> solverTypes,
                   java.util.Collection<SMTProblem> problems,
                   Services services)

Launches several solvers for the problems that are handed over. Note: Calling this methods does not create an extra thread, i.e. the calling thread is blocked until the method returns. (Synchronous method call).

Parameters:

problems - The problems that should be translated and passed to the solvers

services - The services object of the current proof.

solverTypes - A list of solver types that should be used for the problem.

stop

public void stop()

Stops the execution of the launcher.

prepareSolvers

private java.util.Collection<SMTProblem> prepareSolvers(java.util.Collection<SolverType> factories,
                                                        java.util.Collection<SMTProblem> problems,
                                                        Services services)

Creates the concrete solver objects and distributes them to the SMT problems.

launchIntern

private void launchIntern(SMTProblem problem,
                          Services services,
                          SolverType[] solverTypes)

launchIntern

private void launchIntern(java.util.Collection<SolverType> factories,
                          java.util.Collection<SMTProblem> problems,
                          Services services)

checkLaunchCall

private void checkLaunchCall()

launchIntern

private void launchIntern(java.util.Collection<SMTProblem> problems,
                          java.util.Collection<SolverType> factories)

fillRunningList

private void fillRunningList(java.util.LinkedList<SMTSolver> solvers)

Takes the next solvers from the queue and starts them. It depends on the settings how many solvers can be executed concurrently.

isInterrupted

private boolean isInterrupted()

If all permits of the semaphore are acquired the launcher must be stopped.

startNextSolvers

private boolean startNextSolvers(java.util.LinkedList<SMTSolver> solvers)

Checks whether it is possible to start another solver.

launchSolvers

private void launchSolvers(java.util.LinkedList<SMTSolver> solvers,
                           java.util.Collection<SMTProblem> problems,
                           java.util.Collection<SolverType> solverTypes)

notifyListenersOfStart

private void notifyListenersOfStart(java.util.Collection<SMTProblem> problems,
                                    java.util.Collection<SolverType> solverTypes)

launchLoop

private void launchLoop(java.util.LinkedList<SMTSolver> solvers)

Core of the launcher. Start all solvers until the queue is empty or the launcher is interrupted.

waitForRunningSolvers

private void waitForRunningSolvers()

The launcher should not be stopped until every solver has stopped.

cleanUp

private void cleanUp(java.util.Collection<SMTSolver> solvers)

In case of that the user has interrupted the execution the reason of interruption must be set.

notifyListenersOfStop

private void notifyListenersOfStop()

notifySolverHasFinished

private void notifySolverHasFinished(SMTSolver solver)

Is called when a solver has finished its task (Solver Thread). It removes the solver from the list of the currently running solvers and tries to wake up the launcher.

launcherInterrupted

private void launcherInterrupted(java.lang.Exception e)

If there is some exception that is caused by the launcher (not by the solvers) just forward it

processStarted

public void processStarted(SMTSolver solver,
                           SMTProblem problem)

Specified by:

processStarted in interface SolverListener

processStopped

public void processStopped(SMTSolver solver,
                           SMTProblem problem)

Specified by:

processStopped in interface SolverListener

processInterrupted

public void processInterrupted(SMTSolver solver,
                               SMTProblem problem,
                               java.lang.Throwable e)

Specified by:

processInterrupted in interface SolverListener

processTimeout

public void processTimeout(SMTSolver solver,
                           SMTProblem problem)

Specified by:

processTimeout in interface SolverListener

processUser

public void processUser(SMTSolver solver,
                        SMTProblem problem)

Specified by:

processUser in interface SolverListener