| 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, ... (same for byte, short,
long and char) are translated into a NumberConstantTerm or a
InterpretedFuncTerms if they represent a negative value
-
- TRUE and FALSE as constant Functions of Sort boolean are translated into
TruthValueFormulas
- Function symbols like #, Z, C, NEGLIT and 0..9, which represent number and character
constants in KeY, are parsed and translated into an SMT-LIB NumberConstantTerm
or an InterpretedFuncTerm, if the constants are negative
- All further Functions of Sort INT or OBJECT are translated into SMT-LIB
UninterpretedFuncTerms
- All further Functions of Sort FORMULA or BOOLEAN are translated
into SMT-LIB UninterpretedPredFormulae
All uninterpreted function and predicate names consists of a prefix indicating that they
represent translations of a Function and a suffix allowing to quickly distinguish
between uninterpreted functoins and predicates
author:
akuwertz
version:
1.4, 11/10/2006 (Added type predicates for uninterpreted functions) |
