public class ModelGenerator extends java.lang.Object implements SolverLauncherListener
Modifier and Type | Field and Description |
---|---|
private int |
count |
private Goal |
goal |
private java.util.List<Model> |
models |
private Services |
services |
private int |
target |
Constructor and Description |
---|
ModelGenerator(Goal s,
int target,
Services services) |
Modifier and Type | Method and Description |
---|---|
private boolean |
addModelToTerm(Model m)
Changes the term such that when evaluated again with z3 another model will be generated.
|
private void |
finish() |
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) |
private SolverLauncher |
prepareLauncher()
Creates a SolverLauncher with the appropriate settings.
|
Term |
sequentToTerm(Sequent s) |
private final Services services
private Goal goal
private int count
private final java.util.List<Model> models
private final int target
public void launch()
private SolverLauncher prepareLauncher()
public void launcherStopped(SolverLauncher launcher, java.util.Collection<SMTSolver> finishedSolvers)
launcherStopped
in interface SolverLauncherListener
private boolean addModelToTerm(Model m)
m
- the modelprivate void finish()
public void launcherStarted(java.util.Collection<SMTProblem> problems, java.util.Collection<SolverType> solverTypes, SolverLauncher launcher)
launcherStarted
in interface SolverLauncherListener