jmlparser-parent
Toggle table of contents
3.28.2-J8.0-K13.5-SNAPSHOT
jvm
Target filter
jvm
Switch theme
Search in API
Skip to content
jmlparser-parent
smt
/
io.github.jmltoolkit.smt
/
ArithmeticTranslator
Arithmetic
Translator
interface
ArithmeticTranslator
(
source
)
Author
Alexander Weigl
Inheritors
BitVectorArithmeticTranslator
Members
Functions
array
Length
Link copied to clipboard
abstract
fun
arrayLength
(
obj
:
SExpr
)
:
SExpr
binary
Link copied to clipboard
abstract
fun
binary
(
operator
:
BinaryExpr.Operator
,
left
:
SExpr
,
right
:
SExpr
)
:
SExpr
get
Type
Link copied to clipboard
abstract
fun
getType
(
asPrimitive
:
ResolvedType
)
:
SmtType
get
Variable
Link copied to clipboard
open
fun
getVariable
(
variables
:
NodeList
<
Parameter
>
)
:
List
<
SExpr
>
abstract
fun
getVariable
(
jmlBoundVariable
:
Parameter
)
:
SExpr
make
Boolean
Link copied to clipboard
abstract
fun
makeBoolean
(
value
:
Boolean
)
:
SExpr
make
Char
Link copied to clipboard
abstract
fun
makeChar
(
n
:
CharLiteralExpr
)
:
SExpr
make
Int
Link copied to clipboard
abstract
fun
makeInt
(
n
:
IntegerLiteralExpr
)
:
SExpr
abstract
fun
makeInt
(
i
:
BigInteger
)
:
SExpr
abstract
fun
makeInt
(
i
:
Long
)
:
SExpr
make
Int
Var
Link copied to clipboard
abstract
fun
makeIntVar
(
)
:
SExpr
make
Long
Link copied to clipboard
abstract
fun
makeLong
(
n
:
LongLiteralExpr
)
:
SExpr
make
Var
Link copied to clipboard
abstract
fun
makeVar
(
rtype
:
ResolvedType
)
:
SExpr
unary
Link copied to clipboard
abstract
fun
unary
(
operator
:
UnaryExpr.Operator
,
accept
:
SExpr
)
:
SExpr