Package | Description |
---|---|
de.uka.ilkd.key.gui.smt |
This package contains the graphical user interface of the SMT backend.
|
de.uka.ilkd.key.gui.testgen |
This package contains the graphical user interface of the test generation backend.
|
de.uka.ilkd.key.smt |
This package contains the SMT backend of KeY, allowing to translate KeY formulas
to formulas in formats such as SMT-LIB, and allowing to send such formulas to
SMT solvers such as Simplify or Z3.
|
de.uka.ilkd.key.smt.counterexample | |
de.uka.ilkd.key.testgen |
Modifier and Type | Class and Description |
---|---|
class |
SolverListener |
Modifier and Type | Method and Description |
---|---|
protected SolverLauncherListener |
CounterExampleAction.NoMainWindowCounterExampleGenerator.createSolverListener(SMTSettings settings,
Proof proof)
Creates the
SolverLauncherListener which handles the results
of the launched SMT solver. |
protected SolverLauncherListener |
CounterExampleAction.MainWindowCounterExampleGenerator.createSolverListener(SMTSettings settings,
Proof proof)
Creates the
SolverLauncherListener which handles the results
of the launched SMT solver. |
Modifier and Type | Method and Description |
---|---|
void |
SolverLauncher.addListener(SolverLauncherListener listener)
Adds a listener to the launcher object.
|
void |
SolverLauncher.removeListener(SolverLauncherListener listener) |
Modifier and Type | Method and Description |
---|---|
protected abstract SolverLauncherListener |
AbstractCounterExampleGenerator.createSolverListener(SMTSettings settings,
Proof proof)
Creates the
SolverLauncherListener which handles the results
of the launched SMT solver. |
Modifier and Type | Class and Description |
---|---|
class |
ModelGenerator |
Copyright © 2003-2019 The KeY-Project.