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 |
private class |
SolverListener.ProgressDialogListenerImpl |
Modifier and Type | Field and Description |
---|---|
private static int |
FILE_ID |
private int |
finishedCounter |
private static java.awt.Color |
GREEN |
private boolean[][] |
problemProcessed |
private java.util.Collection<SolverListener.InternSMTProblem> |
problems |
private ProgressDialog |
progressDialog |
private ProgressModel |
progressModel |
private static java.awt.Color |
RED |
private static int |
RESOLUTION |
private SMTSettings |
settings |
private java.util.Collection<SMTProblem> |
smtProblems |
private Proof |
smtProof |
private java.util.Timer |
timer |
Constructor and Description |
---|
SolverListener(SMTSettings settings,
Proof smtProof) |
Modifier and Type | Method and Description |
---|---|
void |
addWarning(SolverType type) |
private void |
applyEvent(SolverLauncher launcher) |
private void |
applyResults() |
private long |
calculateProgress(SolverListener.InternSMTProblem problem) |
private float |
calculateRemainingTime(SolverListener.InternSMTProblem problem) |
static java.lang.String |
computeSolverTypeWarningMessage(SolverType type) |
static java.lang.String |
computeSolverTypeWarningTitle(SolverType type) |
static boolean |
containsModalityOrQueryOrUpdate(Term term)
Checks if the given
Term contains a modality, query, or update. |
static java.lang.String |
createExceptionTitle(SolverListener.InternSMTProblem problem) |
private void |
discardEvent(SolverLauncher launcher) |
private java.lang.String |
finalizePath(java.lang.String path,
SMTSolver solver,
Goal goal) |
private SolverListener.InternSMTProblem |
getProblem(int col,
int row) |
private java.lang.String |
getTitle(SMTProblem p) |
private void |
interrupted(SolverListener.InternSMTProblem problem) |
void |
launcherStarted(java.util.Collection<SMTProblem> smtproblems,
java.util.Collection<SolverType> solverTypes,
SolverLauncher launcher) |
void |
launcherStopped(SolverLauncher launcher,
java.util.Collection<SMTSolver> problemSolvers) |
private void |
prepareDialog(java.util.Collection<SMTProblem> smtproblems,
java.util.Collection<SolverType> solverTypes,
SolverLauncher launcher) |
private void |
refreshDialog() |
private boolean |
refreshProgessOfProblem(SolverListener.InternSMTProblem problem) |
private void |
running(SolverListener.InternSMTProblem problem) |
private void |
setProgressText(int value) |
private void |
showInformation(SolverListener.InternSMTProblem problem) |
private void |
stopEvent(SolverLauncher launcher) |
private void |
stopped(SolverListener.InternSMTProblem problem) |
private void |
storeInformation() |
private void |
storeInformation(SMTProblem problem) |
private void |
storeSMTTranslation(SMTSolver solver,
Goal goal,
java.lang.String problemString) |
private void |
storeTacletTranslation(SMTSolver solver,
Goal goal,
TacletSetTranslation translation) |
private void |
storeToFile(java.lang.String text,
java.lang.String path) |
private void |
successfullyStopped(SolverListener.InternSMTProblem problem,
int x,
int y) |
private void |
unknownStopped(SolverListener.InternSMTProblem problem,
int x,
int y) |
private void |
unsuccessfullyStopped(SolverListener.InternSMTProblem problem,
int x,
int y) |
private void |
waiting(SolverListener.InternSMTProblem problem) |
private ProgressDialog progressDialog
private ProgressModel progressModel
private java.util.Collection<SolverListener.InternSMTProblem> problems
private java.util.Collection<SMTProblem> smtProblems
private boolean[][] problemProcessed
private int finishedCounter
private java.util.Timer timer
private final SMTSettings settings
private final Proof smtProof
private static final java.awt.Color RED
private static final java.awt.Color GREEN
private static int FILE_ID
private static final int RESOLUTION
public SolverListener(SMTSettings settings, Proof smtProof)
public void launcherStopped(SolverLauncher launcher, java.util.Collection<SMTSolver> problemSolvers)
launcherStopped
in interface SolverLauncherListener
public static java.lang.String createExceptionTitle(SolverListener.InternSMTProblem problem)
private java.lang.String getTitle(SMTProblem p)
private void applyResults()
private void showInformation(SolverListener.InternSMTProblem problem)
private void prepareDialog(java.util.Collection<SMTProblem> smtproblems, java.util.Collection<SolverType> solverTypes, SolverLauncher launcher)
private SolverListener.InternSMTProblem getProblem(int col, int row)
private void stopEvent(SolverLauncher launcher)
private void discardEvent(SolverLauncher launcher)
private void applyEvent(SolverLauncher launcher)
public void launcherStarted(java.util.Collection<SMTProblem> smtproblems, java.util.Collection<SolverType> solverTypes, SolverLauncher launcher)
launcherStarted
in interface SolverLauncherListener
private void refreshDialog()
private long calculateProgress(SolverListener.InternSMTProblem problem)
private float calculateRemainingTime(SolverListener.InternSMTProblem problem)
private boolean refreshProgessOfProblem(SolverListener.InternSMTProblem problem)
private void waiting(SolverListener.InternSMTProblem problem)
private void running(SolverListener.InternSMTProblem problem)
private void setProgressText(int value)
private void stopped(SolverListener.InternSMTProblem problem)
private void interrupted(SolverListener.InternSMTProblem problem)
private void successfullyStopped(SolverListener.InternSMTProblem problem, int x, int y)
private void unsuccessfullyStopped(SolverListener.InternSMTProblem problem, int x, int y)
private void unknownStopped(SolverListener.InternSMTProblem problem, int x, int y)
private void storeInformation()
private void storeInformation(SMTProblem problem)
private void storeTacletTranslation(SMTSolver solver, Goal goal, TacletSetTranslation translation)
private void storeSMTTranslation(SMTSolver solver, Goal goal, java.lang.String problemString)
private void storeToFile(java.lang.String text, java.lang.String path)
private java.lang.String finalizePath(java.lang.String path, SMTSolver solver, Goal goal)
public void addWarning(SolverType type)
public static java.lang.String computeSolverTypeWarningTitle(SolverType type)
public static java.lang.String computeSolverTypeWarningMessage(SolverType type)