See: Description
| Interface | Description |
|---|---|
| PipeListener<T> | |
| Query |
Represents a query directed to towards the z3 solver.
|
| 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.
|
| SolverListener | |
| SolverType |
This interface is used for modeling different solvers.
|
| Class | Description |
|---|---|
| AbstractQuery | |
| AbstractSMTTranslator |
This abstract class provides a stub for translation of KeY-Formulas to other
standards.
|
| AbstractSMTTranslator.Configuration | |
| AbstractSMTTranslator.FunctionWrapper |
remember all function declarations
|
| AbstractSolverSocket |
The SolverSocket class describes the communication between the KeY and the SMT solver processe.
|
| AbstractSolverType | |
| AccumulatedException | |
| ArrayFieldQuery |
Query for the value of an array field of an object in a heap.
|
| BufferedMessageReader |
Wraps BufferedReader in order to provide different message delimiters.
|
| ConstantQuery |
Query for constant values.
|
| ContextualBlock |
The class
ContextualBlock is used to integrate comments to translations of AbstractSMTtranslator. |
| CVC3Socket | |
| CVC4Socket | |
| ExactInstanceQuery |
Query for finding out if an object is an exact instance of its sort.
|
| ExternalProcessLauncher<T> |
This class is responsible for starting external processes:
1.
|
| FieldQuery |
Query for the value of a named field of an object in a heap.
|
| FunValueQuery |
Query for finding out the value of a function(classinvariant or model field) for an object in a heap.
|
| LocSetQuery |
Query for checking if a location is in a location set.
|
| ModelExtractor |
Class for sending queries to the solver and extracting the relevant information regarding the model.
|
| NumberTranslation |
Translates a number into a string representation.
|
| ObjectLengthQuery |
Query for finding out the length of an object.
|
| ObjectTypeQuery |
Query for finding out if a given object is of a given sort.
|
| OverflowChecker | |
| Pipe<T> |
On each side of the pipe there are sender and receivers:
Receiver ====<=Output======= Sender ******************
KeY* Sender ======Input=>====== Receiver *External Process*
Receiver ====<=Error======== Sender ******************
|
| ProblemTypeInformation | |
| RuleAppSMT |
The rule application that is used when a goal is closed by means of an external solver.
|
| RuleAppSMT.SMTRule | |
| SeqFieldQuery |
Query for the value of a position of a sequence.
|
| SeqLengthQuery |
Query for finding out the length of a sequence.
|
| Session |
The session class encapsulates some attributes that should be only accessed
by specified methods (in order to maintain thread safety)
|
| SimplifySocket | |
| SimplifyTranslator | |
| SmtLib2Translator |
The translation for the SMT2-format.
|
| SmtLibTranslator | |
| SMTObjTranslator | |
| SMTProblem |
Represents a problem that can be passed to a solver.
|
| SMTSolverImplementation | |
| SMTSolverResult |
Encapsulates the result of a single solver.
|
| SolverCommunication |
Stores the communication between KeY and an external solver: Contains a list that stores the messages
that has been sent from the solver to KeY and vice versa.
|
| SolverCommunication.Message | |
| SolverLauncher |
IN ORDER TO START THE SOLVERS USE THIS CLASS.
|
| SolverTimeout |
The class controls the timer that checks for a solver whether it exceeds a pre-defined timeout.
|
| SolverTypeCollection |
Stores a set of solver types.
|
| SortHierarchy |
The SortHierarchy works as a wrapper class for sorts.
|
| SortWrapper | |
| VersionChecker |
Little helper class that helps to check for the version of a solver.
|
| YICESSocket | |
| Z3CESocket | |
| Z3Socket |
| 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. it has a counterexample),
UNKNOWN otherwise (I'm not sure if this holds if an error occurs)
Note: Currently (1.12.'09) the SMT Solvers do not check if a node is FALSE.
|
| SolverCommunication.MessageType |
The message type depends on the channel which was used for sending the message.
|
| Exception | Description |
|---|---|
| IllegalFormulaException | |
| IllegalNumberException | |
| IllegalResultException | |
| SMTTranslationException | |
| SolverException |
Encapsulates all exceptions that have occurred while
executing the solvers.
|