public class SolverListener extends java.lang.Object implements SolverLauncherListener
Modifier and Type | Class and Description |
---|---|
protected static class |
SolverListener.ContainsModalityOrQueryVisitor
Utility class used to check whether a term contains constructs that are not handled by the SMT translation.
|
static class |
SolverListener.InternSMTProblem |
Constructor and Description |
---|
SolverListener(SMTSettings settings,
Proof smtProof) |
Modifier and Type | Method and Description |
---|---|
static java.lang.String |
computeSolverTypeWarningMessage(SolverType type) |
static boolean |
containsModalityOrQuery(Term term)
Checks if the given
Term contains a modality, query, or update. |
void |
launcherStarted(java.util.Collection<SMTProblem> smtproblems,
java.util.Collection<SolverType> solverTypes,
SolverLauncher launcher) |
void |
launcherStopped(SolverLauncher launcher,
java.util.Collection<SMTSolver> problemSolvers) |
public SolverListener(SMTSettings settings, Proof smtProof)
public void launcherStopped(SolverLauncher launcher, java.util.Collection<SMTSolver> problemSolvers)
launcherStopped
in interface SolverLauncherListener
public void launcherStarted(java.util.Collection<SMTProblem> smtproblems, java.util.Collection<SolverType> solverTypes, SolverLauncher launcher)
launcherStarted
in interface SolverLauncherListener
public static java.lang.String computeSolverTypeWarningMessage(SolverType type)
Copyright © 2003-2019 The KeY-Project.