public class ModelGenerator extends java.lang.Object implements SolverLauncherListener
Constructor and Description |
---|
ModelGenerator(Goal s,
int target,
Services services) |
Modifier and Type | Method and Description |
---|---|
void |
launch()
Try finding a model for the term with z3.
|
void |
launcherStarted(java.util.Collection<SMTProblem> problems,
java.util.Collection<SolverType> solverTypes,
SolverLauncher launcher) |
void |
launcherStopped(SolverLauncher launcher,
java.util.Collection<SMTSolver> finishedSolvers) |
Term |
sequentToTerm(Sequent s) |
public void launch()
public void launcherStopped(SolverLauncher launcher, java.util.Collection<SMTSolver> finishedSolvers)
launcherStopped
in interface SolverLauncherListener
public void launcherStarted(java.util.Collection<SMTProblem> problems, java.util.Collection<SolverType> solverTypes, SolverLauncher launcher)
launcherStarted
in interface SolverLauncherListener
Copyright © 2003-2019 The KeY-Project.