ksmt-core/io.ksmt.expr/KBvSignedRemExpr

KBvSignedRemExpr

class KBvSignedRemExpr<S : KBvSort> : KApp<S, S>

Signed remainder.

It is defined as arg0 - (arg0 /s arg1) * arg1, where \s represents signed division. The most significant bit (sign) of the result is equal to the most significant bit of arg0. If arg1 is zero, then the result is undefined.

Functions

open override fun accept(transformer: KTransformerBase): KExpr<S>

decl

fun ~~decl~~(): KDecl<S>

equals

open operator override fun equals(other: Any?): Boolean

hashCode

open override fun hashCode(): Int

internEquals

open override fun internEquals(other: Any): Boolean

Any.equals analogue for interning purposes.

internHashCode

open override fun internHashCode(): Int

Any.hashCode analogue for interning purposes.

open override fun print(printer: ExpressionPrinter)

open override fun print(builder: StringBuilder)

toString

open override fun toString(): String

Properties

arg0

val arg0: KExpr<S>

arg1

val arg1: KExpr<S>

args

open override val args: List<KExpr<S>>

ctx

val ctx: KContext

decl

open override val decl: KDecl<S>

sort

open override val sort: S

Extensions

asExpr

fun <T : KSort> KExpr<*>.asExpr(sort: T): KExpr<T>

isComplement

fun KExpr<KBoolSort>.isComplement(other: KExpr<KBoolSort>): Boolean

toRealValue

fun <T : KArithSort> KExpr<T>.toRealValue(): ArithUtils.RealValue?