public class SolverLauncher extends java.lang.Object implements SolverListener
SMTProblem problem = new SMTProblem(g); // g can be either a goal or term
SolverLauncher launcher = new SolverLauncher(new SMTSettings(){...});
launcher.launch(problem, services,SolverType.Z3_SOLVER,SolverType.YICES_SOLVER);
return problem.getFinalResult();
for (SMTSolver solver : problem.getSolvers()) { solver.getFinalResult(); }
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, CollectionproblemSolvers){ // 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();
solver.getException
.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 and Description |
---|
SolverLauncher(SMTSettings settings)
Create for every solver execution a new object.
|
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.
|
private static final int PERIOD
private final java.util.concurrent.locks.ReentrantLock lock
synchronizestatement.
private final java.util.concurrent.locks.Condition wait
wait
-condition in order to wake up the launcher.private final java.util.Timer timer
private final Session session
private final SMTSettings settings
private final java.util.concurrent.Semaphore stopSemaphore
private java.util.LinkedList<SolverLauncherListener> listeners
private boolean launcherHasBeenUsed
public SolverLauncher(SMTSettings settings)
settings
- settings for the execution of the SMT Solvers.public void addListener(SolverLauncherListener listener)
launcherStopped
of the
listener is called.public void removeListener(SolverLauncherListener listener)
public void launch(SMTProblem problem, Services services, SolverType... solverTypes)
problem
- The problem that should be translated and passed to the
solversservices
- The services object of the current proof.solverTypes
- A list of solver types that should be used for the problem.public void launch(java.util.Collection<SolverType> solverTypes, java.util.Collection<SMTProblem> problems, Services services)
problems
- The problems that should be translated and passed to the
solversservices
- The services object of the current proof.solverTypes
- A list of solver types that should be used for the problem.public void stop()
private java.util.Collection<SMTProblem> prepareSolvers(java.util.Collection<SolverType> factories, java.util.Collection<SMTProblem> problems, Services services)
private void launchIntern(SMTProblem problem, Services services, SolverType[] solverTypes)
private void launchIntern(java.util.Collection<SolverType> factories, java.util.Collection<SMTProblem> problems, Services services)
private void checkLaunchCall()
private void launchIntern(java.util.Collection<SMTProblem> problems, java.util.Collection<SolverType> factories)
private void fillRunningList(java.util.LinkedList<SMTSolver> solvers)
private boolean isInterrupted()
private boolean startNextSolvers(java.util.LinkedList<SMTSolver> solvers)
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 launchLoop(java.util.LinkedList<SMTSolver> solvers)
private void waitForRunningSolvers()
private void cleanUp(java.util.Collection<SMTSolver> solvers)
private void notifyListenersOfStop()
private void notifySolverHasFinished(SMTSolver solver)
private void launcherInterrupted(java.lang.Exception e)
public void processStarted(SMTSolver solver, SMTProblem problem)
processStarted
in interface SolverListener
public void processStopped(SMTSolver solver, SMTProblem problem)
processStopped
in interface SolverListener
public void processInterrupted(SMTSolver solver, SMTProblem problem, java.lang.Throwable e)
processInterrupted
in interface SolverListener
public void processTimeout(SMTSolver solver, SMTProblem problem)
processTimeout
in interface SolverListener
public void processUser(SMTSolver solver, SMTProblem problem)
processUser
in interface SolverListener