| de.uka.ilkd.key.proof.decproc.translation |
|
| Java Source File Name | Type | Comment |
| CreateTypePred.java | Class | This class is responsible for creating and managing type (guard) predicates
Type predicates are needed to support the SMT logic AUFLIA (quanitifier support). |
| IOperatorTranslation.java | Interface | This interface represents a rule for translating KeY Terms into SMT-LIB
Terms and Formulae. |
| PreTranslationVisitor.java | Class | This class implements a visitor used to determine the translatability of KeY Terms
into SMT-LIB Formulae.
This implementation is intended for KeY Terms of Sort Formula. |
| TermTranslationVisitor.java | Class | This class implements a visitor used to translate Terms in KeY into Formulae
in SMT-LIB.
This implementation is intended for KeY Terms of Sort Formula. |
| TranslateArrayOp.java | Class | This class represents the translation rule for ArrayOps.
Thereby the array access represented by the ArrayOp is translated into an SMT-LIB
UninterpretedFuncTerm, if the array is of Sort INT or OBJECT. |
| TranslateAttributeOp.java | Class | This class represents the translation rule for AttributeOps.
Thereby the attribute represented by the AttributeOp has to be a
ProgramVariable. |
| TranslateEquality.java | Class | This class represents the translation rule for an Equality.
Three different types of an Equality are currently translated:
If the target Sort of an Equality is FORMULA, it is translated
into an SMT-LIB ConnectiveFormula as equivalence. |
| TranslateFunction.java | Class | This class represents the translation rule for Functions.
There are several classes of KeY Functions that are translated diffenently:
- ADD, SUB, NEG and the linear MUL are translated into SMT-LIB InterpretedFunctions
- GT, GEQ, LT and LEQ are translated into SMT-LIB PredicateFormulae
- inBYTE, inSHORT, inINT, inLONG and inCHAR are translated into a ConnectiveFormula
consisting of two LT-PredicateFormula
- Type boundaries like int_MIN, int_MAX, int_RANGE, int_HALFRANGE, ...
|
| TranslateIfThenElse.java | Class | This class represents the translation rule for the general IfThenElse operator.
An IfThenElse operator is translated into an SMT-LIB ConnectiveFormula,
if it represents a choice between two Terms of Sort FORMULA. |
| TranslateIUpdateOperator.java | Class | This class represents the translation rule for IUpdateOperators. |
| TranslateJunctor.java | Class | This class represents the translation rule for Junctors.
The following Junctor instances are translated currently:
- NOT
- AND
- OR
- IMP
- TRUE
- FALSE
Each of the first four Junctors mentioned above is translated into a corresponding
SMT-LIB ConnectiveFormula. |
| TranslateLogicVariable.java | Class | This class represents the translation rule for LogicVariables.
A LogicVariable is translated into a TermVariable, if it is of Sort INT or
OBJECT. |
| TranslateMetavariable.java | Class | This class represents the translation rule for MetaVariables. |
| TranslateModality.java | Class | This class represents the translation rule for Modality. |
| TranslateProgramMethod.java | Class | This class represents the translation rule for Program Methods. |
| TranslateProgramVariable.java | Class | This class represents the translation rule for ProgramVariables.
A ProgramVariable is translated into a constant. |
| TranslateQuantifier.java | Class | This class represents the translation rule for Quantifiers.
They are supported only in AUFLIA, not in QF_AUFLIA. |
| TranslateUnknownOp.java | Class | This class represents the translation rule for Operators of unknown or unexpected classes. |
| TranslationVisitor.java | Class | This class representing a visitor intended to be used for the translation of KeY Terms.
The translate a Term, a TranslationVisitor instance will be passed to either
the execPostOrder or the execPreOrder method of the given Term. |