de.uka.ilkd.key.testgen

Class ModelGenerator

java.lang.Object

de.uka.ilkd.key.testgen.ModelGenerator

All Implemented Interfaces:

SolverLauncherListener

public class ModelGenerator
extends java.lang.Object
implements SolverLauncherListener

Field Summary

Fields

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 Summary

Constructors

Constructor and Description
ModelGenerator(Goal s, int target, Services services)

Method Summary

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)

Methods inherited from class java.lang.Object

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

Field Detail

services

private final Services services

goal

private Goal goal

count

private int count

models

private final java.util.List<Model> models

target

private final int target

Constructor Detail

ModelGenerator

public ModelGenerator(Goal s,
                      int target,
                      Services services)

Method Detail

launch

public void launch()

Try finding a model for the term with z3.

prepareLauncher

private SolverLauncher prepareLauncher()

Creates a SolverLauncher with the appropriate settings.

Returns:

launcherStopped

public void launcherStopped(SolverLauncher launcher,
                            java.util.Collection<SMTSolver> finishedSolvers)

Specified by:

launcherStopped in interface SolverLauncherListener

addModelToTerm

private boolean addModelToTerm(Model m)

Changes the term such that when evaluated again with z3 another model will be generated. If we have a model (c1=v1 & c2 = v2 & ...) where c1, c2, ... are integer constants we change the term t to the following form: t & !(c1=v1 & c2 = v2 & ...)

Parameters:

m - the model

Returns:

true if the term has been changed

finish

private void finish()

launcherStarted

public void launcherStarted(java.util.Collection<SMTProblem> problems,
                            java.util.Collection<SolverType> solverTypes,
                            SolverLauncher launcher)

Specified by:

launcherStarted in interface SolverLauncherListener

sequentToTerm

public Term sequentToTerm(Sequent s)