public final class IntegerLDT extends LDT
Constructor and Description |
---|
IntegerLDT(Services services) |
Modifier and Type | Method and Description |
---|---|
Function |
getAdd() |
Function |
getArithJavaIntAddition()
returns the function symbol interpreted as the Java addition on
int (or promotabel to int) operators, i.e. this addition performs a modulo
operation wrt. to the range of type
int . |
Function |
getArithModulo()
returns the function symbol used to represent the modulo operation of
the arithmetical integers
|
Function |
getArithModuloByte()
maps an integer back into byte range
|
Function |
getArithModuloChar()
maps an integer back into char range
|
Function |
getArithModuloInt()
maps an integer back into int range
|
Function |
getArithModuloLong()
maps an integer back into long range
|
Function |
getArithModuloShort()
maps an integer back into long range
|
Function |
getBitwiseOrJavaInt()
returns the function symbol representing the bitwise-or for Java int
|
Function |
getBprod() |
Function |
getBsum() |
Function |
getCharSymbol() |
Function |
getDiv() |
Function |
getFunctionFor(Operator op,
Services serv,
ExecutionContext ec)
returns the function symbol for the given operation
null if no function is found for the given operator
|
Function |
getGreaterOrEquals() |
Function |
getGreaterThan() |
Function |
getInBounds(Type t) |
Function |
getIndex()
Placeholder for the loop index variable in an enhanced for loop over arrays.
|
Function |
getJavaAddInt()
the function representing the Java operator when one of the
operators is an or can be promoted to an int
|
Function |
getJavaAddLong()
the function representing the Java operator when one of the
operators is of type long
|
Function |
getJavaBitwiseAndInt()
the function representing the Java operator when one of the
operators is an or can be promoted to int
|
Function |
getJavaBitwiseAndLong()
the function representing the Java operator when one of the
operators is of type long
|
Function |
getJavaBitwiseNegation()
the function representing the Java operator
~ |
Function |
getJavaBitwiseOrInt()
the function representing the Java operator
|
when one of the operands is an or can be promoted to int |
Function |
getJavaBitwiseOrLong()
the function representing the Java operator
|
when one of the operands is of type long |
Function |
getJavaBitwiseXOrInt()
the function representing the Java operator
^
when one of the operands is an or can be promoted to int |
Function |
getJavaBitwiseXOrLong()
the function representing the Java operator
^
when one of the operands is exact of type long |
Function |
getJavaCast(Type t) |
Function |
getJavaCastByte()
the function representing the Java operator
(byte) |
Function |
getJavaCastChar()
the function representing the Java operator
(char) |
Function |
getJavaCastInt()
the function representing the Java operator
(int) |
Function |
getJavaCastLong()
the function representing the Java operator
(long) |
Function |
getJavaCastShort()
the function representing the Java operator
(short) |
Function |
getJavaDivInt()
the function representing the Java operator
/
when one of the operands is an or a subtype of int |
Function |
getJavaDivLong()
the function representing the Java operator
/
when one of the operands is exact of type long |
Function |
getJavaMod()
the function representing the Java operator
%
when one of the operands is an or a subtype of int |
Function |
getJavaMulInt()
the function representing the Java operator
*
when one of the operands is an or a subtype of int |
Function |
getJavaMulLong()
the function representing the Java operator
*
when one of the operands is exact of type long |
Function |
getJavaShiftLeftInt()
the function representing the Java operator
<<
when one of the operands is an or a subtype of int |
Function |
getJavaShiftLeftLong()
the function representing the Java operator
<<
when one of the operands is exact of type long |
Function |
getJavaShiftRightInt()
the function representing the Java operator
>>
when one of the operands is an or a subtype of int |
Function |
getJavaShiftRightLong()
the function representing the Java operator
>>
when one of the operands is exact of type long |
Function |
getJavaSubInt()
the function representing the Java operator
-
when one of the operands is an or a subtype of int |
Function |
getJavaSubLong()
the function representing the Java operator
-
when one of the operands is exact of type long |
Function |
getJavaUnaryMinusInt()
the function representing the Java operator
-expr
when one of the operands is an or a subtype of int |
Function |
getJavaUnaryMinusLong()
the function representing the Java operator
-exprLong
when one of the operands is exact of type long |
Function |
getJavaUnsignedShiftRightInt()
the function representing the Java operator
>>>
when one of the operands is an or a subtype of int |
Function |
getJavaUnsignedShiftRightLong()
the function representing the Java operator
>>>
when one of the operands is exact of type long |
Function |
getJDivision()
returns the function symbol used to represent java-like division of
the arithmetical integers
|
Function |
getJModulo()
returns the function symbol used to represent the java-like modulo operation of
the arithmetical integers
|
Function |
getLessOrEquals() |
Function |
getLessThan() |
Function |
getMod() |
Function |
getModuloLong()
returns a function mapping an arithmetic integer to its Java long representation
|
Function |
getMul() |
Function |
getNeg() |
Function |
getNegativeNumberSign() |
Function |
getNumberLiteralFor(int number) |
Function |
getNumberSymbol() |
Function |
getNumberTerminator() |
Function |
getPow() |
Function |
getSub() |
Type |
getType(Term t) |
boolean |
hasLiteralFunction(Function f) |
private boolean |
isNumberLiteral(Function f) |
boolean |
isResponsible(Operator op,
Term[] subs,
Services services,
ExecutionContext ec)
returns true if the LDT offers an operation for the given java
operator and the logic subterms
|
boolean |
isResponsible(Operator op,
Term sub,
TermServices services,
ExecutionContext ec)
returns true if the LDT offers an operation for the given
unary java operator and the logic subterms
|
boolean |
isResponsible(Operator op,
Term left,
Term right,
Services services,
ExecutionContext ec)
returns true if the LDT offers an operation for the given
binary java operator and the logic subterms
|
private Term |
makeDigit(int digit,
TermBuilder tb) |
Term |
one() |
Term |
translateLiteral(Literal lit,
Services services)
translates a given literal to its logic counterpart
|
Expression |
translateTerm(Term t,
ExtList children,
Services services)
Is called whenever
hasLiteralFunction() returns true. |
Term |
zero() |
addFunction, addFunction, addSortDependingFunction, containsFunction, functions, getNewLDTInstances, name, targetSort, toString
public static final Name NAME
public static final java.lang.String NEGATIVE_LITERAL_STRING
public static final Name NUMBERS_NAME
public static final Name CHAR_ID_NAME
private final Function sharp
private final Function[] numberSymbol
private final Function neglit
private final Function numbers
private final Function charID
private final Function add
private final Function neg
private final Function sub
private final Function mul
private final Function div
private final Function mod
private final Function pow
private final Function bsum
private final Function bprod
private final Function jdiv
private final Function jmod
private final Function unaryMinusJint
private final Function unaryMinusJlong
private final Function addJint
private final Function addJlong
private final Function subJint
private final Function subJlong
private final Function mulJint
private final Function mulJlong
private final Function modJint
private final Function modJlong
private final Function divJint
private final Function divJlong
private final Function shiftright
private final Function shiftleft
private final Function shiftrightJint
private final Function shiftrightJlong
private final Function shiftleftJint
private final Function shiftleftJlong
private final Function unsignedshiftrightJint
private final Function unsignedshiftrightJlong
private final Function binaryOr
private final Function binaryXOr
private final Function binaryAnd
private final Function orJint
private final Function orJlong
private final Function andJint
private final Function andJlong
private final Function xorJint
private final Function xorJlong
private final Function moduloByte
private final Function moduloShort
private final Function moduloInt
private final Function moduloLong
private final Function moduloChar
private final Function javaUnaryMinusInt
private final Function javaUnaryMinusLong
private final Function javaBitwiseNegation
private final Function javaAddInt
private final Function javaAddLong
private final Function javaSubInt
private final Function javaSubLong
private final Function javaMulInt
private final Function javaMulLong
private final Function javaMod
private final Function javaDivInt
private final Function javaDivLong
private final Function javaShiftRightInt
private final Function javaShiftRightLong
private final Function javaShiftLeftInt
private final Function javaShiftLeftLong
private final Function javaUnsignedShiftRightInt
private final Function javaUnsignedShiftRightLong
private final Function javaBitwiseOrInt
private final Function javaBitwiseOrLong
private final Function javaBitwiseAndInt
private final Function javaBitwiseAndLong
private final Function javaBitwiseXOrInt
private final Function javaBitwiseXOrLong
private final Function javaCastByte
private final Function javaCastShort
private final Function javaCastInt
private final Function javaCastLong
private final Function javaCastChar
private final Function lessThan
private final Function greaterThan
private final Function greaterOrEquals
private final Function lessOrEquals
private final Function inByte
private final Function inShort
private final Function inInt
private final Function inLong
private final Function inChar
private final Function index
private final Term one
private final Term zero
public IntegerLDT(Services services)
private boolean isNumberLiteral(Function f)
private Term makeDigit(int digit, TermBuilder tb)
public Function getNumberTerminator()
public Function getNumberLiteralFor(int number)
public Function getNegativeNumberSign()
public Function getNumberSymbol()
public Function getCharSymbol()
public Function getAdd()
public Function getNeg()
public Function getSub()
public Function getMul()
public Function getDiv()
public Function getMod()
public Function getPow()
public Function getBsum()
public Function getBprod()
public Function getLessThan()
public Function getGreaterThan()
public Function getGreaterOrEquals()
public Function getLessOrEquals()
public Function getIndex()
public Function getFunctionFor(Operator op, Services serv, ExecutionContext ec)
getFunctionFor
in class LDT
public boolean isResponsible(Operator op, Term[] subs, Services services, ExecutionContext ec)
LDT
isResponsible
in class LDT
op
- the de.uka.ilkd.key.java.expression.Operator to
translatesubs
- the logic subterms of the java operatorservices
- the Servicesec
- the ExecutionContext in which the expression is evaluatedpublic boolean isResponsible(Operator op, Term left, Term right, Services services, ExecutionContext ec)
LDT
isResponsible
in class LDT
op
- the de.uka.ilkd.key.java.expression.Operator to
translateleft
- the left subterm of the java operatorright
- the right subterm of the java operatorservices
- the Servicesec
- the ExecutionContext in which the expression is evaluatedpublic boolean isResponsible(Operator op, Term sub, TermServices services, ExecutionContext ec)
LDT
isResponsible
in class LDT
op
- the de.uka.ilkd.key.java.expression.Operator to
translatesub
- the logic subterms of the java operatorservices
- the Servicesec
- the ExecutionContext in which the expression is evaluatedpublic Term translateLiteral(Literal lit, Services services)
LDT
translateLiteral
in class LDT
lit
- the Literal to be translatedpublic boolean hasLiteralFunction(Function f)
hasLiteralFunction
in class LDT
public Expression translateTerm(Term t, ExtList children, Services services)
LDT
hasLiteralFunction()
returns true.translateTerm
in class LDT
public Function getJDivision()
public Function getArithModulo()
public Function getJModulo()
public Function getModuloLong()
public Function getArithModuloLong()
public Function getArithModuloInt()
public Function getArithModuloShort()
public Function getArithModuloByte()
public Function getArithModuloChar()
public Function getArithJavaIntAddition()
int
. This function is independent
of the chosen integer semantics.
In case you want to represent the Java addition on operands promotable to int
which shall be interpreted by the chosen integer semantics use
getJavaAddInt()
insteadint
public Function getBitwiseOrJavaInt()
public Function getJavaAddInt()
public Function getJavaAddLong()
public Function getJavaBitwiseAndInt()
public Function getJavaBitwiseAndLong()
public Function getJavaBitwiseNegation()
~
public Function getJavaBitwiseOrInt()
|
when one of the operands is an or can be promoted to intpublic Function getJavaBitwiseOrLong()
|
when one of the operands is of type longpublic Function getJavaBitwiseXOrInt()
^
when one of the operands is an or can be promoted to intpublic Function getJavaBitwiseXOrLong()
^
when one of the operands is exact of type longpublic Function getJavaCastByte()
(byte)
public Function getJavaCastChar()
(char)
public Function getJavaCastInt()
(int)
public Function getJavaCastLong()
(long)
public Function getJavaCastShort()
(short)
public Function getJavaDivInt()
/
when one of the operands is an or a subtype of intpublic Function getJavaDivLong()
/
when one of the operands is exact of type longpublic Function getJavaMod()
%
when one of the operands is an or a subtype of intpublic Function getJavaMulInt()
*
when one of the operands is an or a subtype of intpublic Function getJavaMulLong()
*
when one of the operands is exact of type longpublic Function getJavaShiftLeftInt()
<<
when one of the operands is an or a subtype of intpublic Function getJavaShiftLeftLong()
<<
when one of the operands is exact of type longpublic Function getJavaShiftRightInt()
>>
when one of the operands is an or a subtype of intpublic Function getJavaShiftRightLong()
>>
when one of the operands is exact of type longpublic Function getJavaSubInt()
-
when one of the operands is an or a subtype of intpublic Function getJavaSubLong()
-
when one of the operands is exact of type longpublic Function getJavaUnaryMinusInt()
-expr
when one of the operands is an or a subtype of intpublic Function getJavaUnaryMinusLong()
-exprLong
when one of the operands is exact of type longpublic Function getJavaUnsignedShiftRightInt()
>>>
when one of the operands is an or a subtype of intpublic Function getJavaUnsignedShiftRightLong()
>>>
when one of the operands is exact of type longpublic Term zero()
public Term one()