public class SolverLauncher
extends java.lang.Object
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
.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.
|
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.
Note: Calling this methods does not create an extra thread, i.e. |
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) |
void |
stop()
Stops the execution of the launcher.
|
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()
public void processStarted(SMTSolver solver, SMTProblem problem)
public void processStopped(SMTSolver solver, SMTProblem problem)
public void processInterrupted(SMTSolver solver, SMTProblem problem, java.lang.Throwable e)
public void processTimeout(SMTSolver solver, SMTProblem problem)
public void processUser(SMTSolver solver, SMTProblem problem)
Copyright © 2003-2019 The KeY-Project.