See: Description
Interface | Description |
---|---|
SMTSettings | |
SMTSolver |
The SMTSolver interface represents a solver process (e.g.
|
SMTTranslator |
Classes that implement this interface provide a translation of
a KeY-problem into a specific format.
|
SolverLauncherListener |
This interface can be used to observe a launcher.
|
SolverType |
This interface is used for modeling different solvers.
|
Class | Description |
---|---|
AbstractSMTTranslator |
This abstract class provides a stub for translation of KeY-Formulas to other
standards.
|
AbstractSMTTranslator.Configuration | |
AbstractSMTTranslator.FunctionWrapper |
remember all function declarations
|
AccumulatedException | |
ModelExtractor |
Class for sending queries to the solver and extracting the relevant information regarding the model.
|
NumberTranslation |
Translates a number into a string representation.
|
OverflowChecker | |
ProblemTypeInformation | |
RuleAppSMT |
The rule application that is used when a goal is closed by means of an external solver.
|
RuleAppSMT.SMTRule | |
SimplifyTranslator | |
SMTBeautifier |
Simple routine to prettyprint an SMT2 input.
|
SmtLib2Translator |
The translation for the SMT2-format.
|
SmtLibTranslator | |
SMTObjTranslator | |
SMTProblem |
Represents a problem that can be passed to a solver.
|
SMTSolverResult |
Encapsulates the result of a single solver.
|
SolverLauncher |
IN ORDER TO START THE SOLVERS USE THIS CLASS.
There are two cases how the solvers can be started: 1. |
SolverTypeCollection |
Stores a set of solver types.
|
SortHierarchy |
The SortHierarchy works as a wrapper class for sorts.
|
VersionChecker |
Little helper class that helps to check for the version of a solver.
|
Enum | Description |
---|---|
SMTSolver.ReasonOfInterruption | |
SMTSolver.SolverState |
A solver process can have differnt states.
|
SMTSolverResult.ThreeValuedTruth |
In the context of proving nodes/sequents these values mean the following:
TRUE iff negation of the sequent is unsatisfiable,
FALSIFIABLE iff negation of the sequent is satisfiable (i.e.
|
Exception | Description |
---|---|
IllegalFormulaException | |
IllegalNumberException | |
IllegalResultException | |
SMTTranslationException | |
SolverException |
Encapsulates all exceptions that have occurred while
executing the solvers.
|
Copyright © 2003-2019 The KeY-Project.