smt/io.github.jmltoolkit.smt/SmtTermFactory

SmtTermFactory

object SmtTermFactory(source)

Author

Alexander Weigl

Functions

add

fun add(left: SExpr, right: SExpr): SExpr

and

fun and(seq: List<SExpr>): SExpr

fun and(vararg terms: SExpr): SExpr

arrayType

fun arrayType(from: SExpr, to: SExpr): SExpr

band

fun band(left: SExpr, right: SExpr): SExpr

binder

fun binder(type: SmtType, name: String): SExpr

boolType

fun boolType(): SExpr

bor

fun bor(left: SExpr, right: SExpr): SExpr

bvadd

fun bvadd(left: SExpr, right: SExpr): SExpr

bvand

fun bvand(left: SExpr, right: SExpr): SExpr

bvgreaterOrEquals

fun bvgreaterOrEquals(left: SExpr, right: SExpr): SExpr

bvgreaterThan

fun bvgreaterThan(left: SExpr, right: SExpr): SExpr

bvlessOrEquals

fun bvlessOrEquals(left: SExpr, right: SExpr): SExpr

bvlessThan

fun bvlessThan(left: SExpr, right: SExpr): SExpr

bvnegate

fun bvnegate(sexpr: SExpr): SExpr

bvnot

fun bvnot(expr: SExpr): SExpr

bvor

fun bvor(left: SExpr, right: SExpr): SExpr

bvshiftLeft

fun bvshiftLeft(left: SExpr, right: SExpr): SExpr

bvshiftRight

fun bvshiftRight(left: SExpr, right: SExpr, sign: Boolean): SExpr

bvType

fun bvType(width: Int): SExpr

command

fun command(symbol: String, vararg args: SExpr): SExpr

divide

fun divide(left: SExpr, right: SExpr, b: Boolean): SExpr

equality

fun equality(left: SExpr, right: SExpr): SExpr

equiv

fun equiv(left: SExpr, right: SExpr): SExpr

exists

fun exists(variables: List<SExpr>, formula: SExpr): SExpr

fieldAccess

fun fieldAccess(javaType: ResolvedType?, stype: SmtType, field: String, obj: SExpr): SExpr

fnApply

fun fnApply(javaType: ResolvedType?, smtType: SmtType, fn: String, arg: SExpr): SExpr

forall

fun forall(variables: List<SExpr>, formula: SExpr): SExpr

fpType

fun fpType(width: Int): SExpr

greaterOrEquals

fun greaterOrEquals(left: SExpr, right: SExpr, b: Boolean): SExpr

greaterThan

fun greaterThan(left: SExpr, right: SExpr): SExpr

iadd

fun iadd(left: SExpr, right: SExpr): SExpr

idivide

fun idivide(left: SExpr, right: SExpr): SExpr

igreaterOrEquals

fun igreaterOrEquals(left: SExpr, right: SExpr): SExpr

igreaterThan

fun igreaterThan(left: SExpr, right: SExpr): SExpr

ilessOrEquals

fun ilessOrEquals(left: SExpr, right: SExpr): SExpr

ilessThan

fun ilessThan(left: SExpr, right: SExpr): SExpr

imodulo

fun imodulo(left: SExpr, right: SExpr): SExpr

impl

fun impl(premise: SExpr, concl: SExpr): SExpr

imultiply

fun imultiply(left: SExpr, right: SExpr): SExpr

intType

fun intType(): SExpr

intValue

fun intValue(value: BigInteger): SAtom

fun intValue(value: Long): SAtom

fun intValue(svalue: String): SAtom

isubstract

fun isubstract(left: SExpr, right: SExpr): SExpr

ite

fun ite(cond: SExpr, then: SExpr, otherwise: SExpr): SExpr

javaObjectType

fun javaObjectType(): SExpr

lessOrEquals

fun lessOrEquals(left: SExpr, right: SExpr, sign: Boolean): SExpr

lessThan

fun lessThan(left: SExpr, right: SExpr): SExpr

let

fun let(vars: List<SExpr>, body: SExpr): SExpr

list

fun list(variables: List<SExpr>): SExpr

fun list(javaType: ResolvedType?, stype: SmtType, vararg args: Any): SExpr

fun list(javaType: ResolvedType, smtType: SmtType, symbol: SAtom, args: Array<SExpr>): SExpr

makeBitvector

fun makeBitvector(width: Int, value: BigInteger): SExpr

fun makeBitvector(width: Int, value: Long): SExpr

makeBoolean

fun makeBoolean(value: Boolean): SExpr

makeFalse

fun makeFalse(): SExpr

makeInt

fun makeInt(value: String): SExpr

makeNull

fun makeNull(): SExpr

makeSuper

fun makeSuper(): SExpr

makeThis

fun makeThis(): SExpr

makeTrue

fun makeTrue(): SExpr

modulo

fun modulo(left: SExpr, right: SExpr, b: Boolean): SExpr

multiply

fun multiply(left: SExpr, right: SExpr): SExpr

negate

fun negate(sexpr: SExpr): SExpr

nonNull

fun nonNull(expr: SExpr): SExpr

not

fun not(expr: SExpr): SExpr

fun or(terms: List<SExpr>): SExpr

fun or(vararg terms: SExpr): SExpr

select

fun select(stype: SmtType, javaType: ResolvedType?, array: SExpr, index: SExpr): SExpr

shiftLeft

fun shiftLeft(left: SExpr, right: SExpr): SExpr

shiftRight

fun shiftRight(left: SExpr, right: SExpr, sign: Boolean): SExpr

store

fun store(array: SExpr, index: SExpr, value: SExpr): SExpr

subtract

fun subtract(left: SExpr, right: SExpr): SExpr

symbol

fun symbol(fn: String): SAtom

type

fun type(type: SmtType): SExpr

variable

fun variable(type: SmtType, javaType: ResolvedType?, name: String): SExpr

xor

fun xor(left: SExpr, right: SExpr): SExpr