smt/io.github.jmltoolkit.smt/BitVectorArithmeticTranslator

BitVectorArithmeticTranslator

Alexander Weigl

Constructors

constructor(smtLog: SmtQuery)

open override fun arrayLength(obj: SExpr): SExpr

open override fun binary(operator: BinaryExpr.Operator, left: SExpr, right: SExpr): SExpr

open override fun getType(asPrimitive: ResolvedType): SmtType

open override fun getVariable(jmlBoundVariable: Parameter): SExpr

open override fun makeBoolean(value: Boolean): SExpr

open override fun makeInt(i: BigInteger): SExpr

open override fun makeInt(i: Long): SExpr

open override fun makeIntVar(): SExpr

open override fun makeVar(rtype: ResolvedType): SExpr

open override fun unary(operator: UnaryExpr.Operator, accept: SExpr): SExpr