ksmt-core/io.ksmt.expr.rewrite.simplify

Package-level declarations

Types

ExpressionOrdering

object ExpressionOrdering : Comparator<KExpr<*>>

KArithExprSimplifier

interface KArithExprSimplifier : KExprSimplifierBase

KArrayExprSimplifier

interface KArrayExprSimplifier : KExprSimplifierBase

KBoolExprSimplifier

interface KBoolExprSimplifier : KExprSimplifierBase

KBvExprSimplifier

interface KBvExprSimplifier : KExprSimplifierBase

KExprSimplifier

open class KExprSimplifier(val ctx: KContext) : KNonRecursiveTransformerBase, KExprSimplifierBase, KBoolExprSimplifier, KArithExprSimplifier, KBvExprSimplifier, KFpExprSimplifier, KArrayExprSimplifier

KExprSimplifierBase

interface KExprSimplifierBase : KTransformer

KFpExprSimplifier

interface KFpExprSimplifier : KExprSimplifierBase

Functions

addArithTerm

fun <T : KArithSort> addArithTerm(value: ArithUtils.RealValue, term: KExpr<T>, terms: MutableList<KExpr<T>>): ArithUtils.RealValue

areDefinitelyDistinct

fun KExprSimplifierBase.areDefinitelyDistinct(left: List<KExpr<*>>, right: List<KExpr<*>>): Boolean

left and right are definitely distinct if there is at least one distinct pair of expressions.

bvLessOrEqual

inline fun <T : KBvSort> KContext.bvLessOrEqual(lhs: KExpr<T>, rhs: KExpr<T>, signed: Boolean, rewriteBvEq: KContext.(KExpr<T>, KExpr<T>) -> KExpr<KBoolSort>, cont: (KExpr<T>, KExpr<T>) -> KExpr<KBoolSort>): KExpr<KBoolSort>

castRealValue

fun <T : KArithSort> KContext.castRealValue(value: ArithUtils.RealValue, sort: T): KExpr<T>

distributeExtractOverConcat

inline fun KContext.distributeExtractOverConcat(high: Int, low: Int, concatenation: KBvConcatExpr, rewriteBvExtractExpr: KContext.(Int, Int, KExpr<KBvSort>) -> KExpr<KBvSort>, rewriteFlatBvConcatExpr: KContext.(List<KExpr<KBvSort>>) -> KExpr<KBvSort>): KExpr<KBvSort>

(extract (concat a b)) ==> (concat (extract a) (extract b))

distributeOperationOverConcat

inline fun <T : KBvSort> KContext.distributeOperationOverConcat(args: List<KExpr<T>>, rewriteBvExtractExpr: KContext.(Int, Int, KExpr<KBvSort>) -> KExpr<KBvSort>, rewriteFlatBvOpExpr: KContext.(List<KExpr<KBvSort>>) -> KExpr<KBvSort>, rewriteBvConcatExpr: KContext.(KExpr<KBvSort>, KExpr<KBvSort>) -> KExpr<KBvSort>): KExpr<T>

ensureExpressionsOrder

fun <T : KSort> MutableList<KExpr<T>>.ensureExpressionsOrder()

evalBinaryOp

inline fun <T : KFpSort> evalBinaryOp(roundingMode: KExpr<KFpRoundingModeSort>, lhs: KExpr<T>, rhs: KExpr<T>, operation: (KFpRoundingMode, KFpValue<*>, KFpValue<*>) -> KFpValue<*>, cont: () -> KExpr<T>): KExpr<T>

evalBvOperation

inline fun <T : KBvSort, S : KBvSort, R : KBvSort> evalBvOperation(lhs: KExpr<T>, rhs: KExpr<S>, operation: (KBitVecValue<T>, KBitVecValue<S>) -> KBitVecValue<R>, cont: () -> KExpr<R>): KExpr<R>

evalBvSignedMulNoOverflow

fun <T : KBvSort> KContext.evalBvSignedMulNoOverflow(lhsValue: KBitVecValue<T>, rhsValue: KBitVecValue<T>, isOverflow: Boolean): KExpr<KBoolSort>

evalFpPredicateOr

inline fun <T : KFpSort> KContext.evalFpPredicateOr(value: KExpr<T>, predicate: (KFpValue<T>) -> Boolean, cont: (KExpr<T>) -> KExpr<KBoolSort>): KExpr<KBoolSort>

evalIntDiv

fun evalIntDiv(a: BigInteger, b: BigInteger): BigInteger

Eval integer div wrt Int theory rules.

evalIntMod

fun evalIntMod(a: BigInteger, b: BigInteger): BigInteger

Eval integer mod wrt Int theory rules.

evalIntRem

fun evalIntRem(a: BigInteger, b: BigInteger): BigInteger

Eval integer rem wrt Int theory rules.

executeIfValue

inline fun <T : KBvSort> executeIfValue(lhs: KExpr<T>, rhs: KExpr<T>, body: (KBitVecValue<T>, KExpr<T>) -> Unit)

flatBinaryBvExpr

inline fun <T> flatBinaryBvExpr(initial: KExpr<KBvSort>, getLhs: (T) -> KExpr<KBvSort>, getRhs: (T) -> KExpr<KBvSort>): List<KExpr<KBvSort>>

flatConcatArgs

fun flatConcatArgs(expr: KBvConcatExpr): List<KExpr<KBvSort>>

isComplement

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

isMaxValue

fun KBitVecValue<*>.isMaxValue(signed: Boolean): Boolean

isMinValue

fun KBitVecValue<*>.isMinValue(signed: Boolean): Boolean

mulArithTerm

fun <T : KArithSort> mulArithTerm(value: ArithUtils.RealValue, term: KExpr<T>, terms: MutableList<KExpr<T>>): ArithUtils.RealValue

rewriteArithGe

inline fun <T : KArithSort> KContext.rewriteArithGe(lhs: KExpr<T>, rhs: KExpr<T>, rewriteArithLe: KContext.(KExpr<T>, KExpr<T>) -> KExpr<KBoolSort>): KExpr<KBoolSort>

(>= a b) ==> (<= b a)

rewriteArithGt

inline fun <T : KArithSort> KContext.rewriteArithGt(lhs: KExpr<T>, rhs: KExpr<T>, rewriteArithLt: KContext.(KExpr<T>, KExpr<T>) -> KExpr<KBoolSort>): KExpr<KBoolSort>

(> a b) ==> (< b a)

rewriteArithSub

inline fun <T : KArithSort> KContext.rewriteArithSub(args: List<KExpr<T>>, rewriteArithAdd: KContext.(List<KExpr<T>>) -> KExpr<T>, rewriteArithUnaryMinus: KContext.(KExpr<T>) -> KExpr<T>): KExpr<T>

(- a b) ==> (+ a -b)

rewriteBvAddNoOverflowExpr

inline fun <T : KBvSort> KContext.rewriteBvAddNoOverflowExpr(lhs: KExpr<T>, rhs: KExpr<T>, isSigned: Boolean, rewriteBvSignedLessExpr: KContext.(KExpr<T>, KExpr<T>) -> KExpr<KBoolSort> = KContext::simplifyBvSignedLessExpr, rewriteBvAddExpr: KContext.(KExpr<KBvSort>, KExpr<KBvSort>) -> KExpr<KBvSort> = KContext::simplifyBvAddExpr, rewriteBvZeroExtensionExpr: KContext.(Int, KExpr<T>) -> KExpr<KBvSort> = KContext::simplifyBvZeroExtensionExpr, rewriteBvExtractExpr: KContext.(Int, Int, KExpr<T>) -> KExpr<KBvSort> = KContext::simplifyBvExtractExpr, rewriteBvEq: KContext.(KExpr<KBvSort>, KExpr<KBvSort>) -> KExpr<KBoolSort> = { l, r -> simplifyEq(l, r) }, rewriteAnd: KContext.(KExpr<KBoolSort>, KExpr<KBoolSort>) -> KExpr<KBoolSort> = { l, r -> simplifyAnd(l, r) }, rewriteImplies: KContext.(KExpr<KBoolSort>, KExpr<KBoolSort>) -> KExpr<KBoolSort> = KContext::simplifyImplies): KExpr<KBoolSort>

rewriteBvAddNoUnderflowExpr

inline fun <T : KBvSort> KContext.rewriteBvAddNoUnderflowExpr(lhs: KExpr<T>, rhs: KExpr<T>, rewriteBvSignedLessExpr: KContext.(KExpr<T>, KExpr<T>) -> KExpr<KBoolSort> = KContext::simplifyBvSignedLessExpr, rewriteBvAddExpr: KContext.(KExpr<T>, KExpr<T>) -> KExpr<T> = KContext::simplifyBvAddExpr, rewriteAnd: KContext.(KExpr<KBoolSort>, KExpr<KBoolSort>) -> KExpr<KBoolSort> = { l, r -> simplifyAnd(l, r) }, rewriteImplies: KContext.(KExpr<KBoolSort>, KExpr<KBoolSort>) -> KExpr<KBoolSort> = KContext::simplifyImplies): KExpr<KBoolSort>

rewriteBvConcatEq

inline fun <T : KBvSort> KContext.rewriteBvConcatEq(l: KExpr<T>, r: KExpr<T>, rewriteBvExtractExpr: KContext.(Int, Int, KExpr<KBvSort>) -> KExpr<KBvSort>, rewriteBvEq: KContext.(KExpr<KBvSort>, KExpr<KBvSort>) -> KExpr<KBoolSort>, rewriteFlatAnd: KContext.(List<KExpr<KBoolSort>>) -> KExpr<KBoolSort>): KExpr<KBoolSort>

(= (concat a b) c) ==> (and (= a (extract (0, ) c)) (= b (extract (, + ) c)) )

rewriteBvDivNoOverflowExpr

inline fun <T : KBvSort> KContext.rewriteBvDivNoOverflowExpr(lhs: KExpr<T>, rhs: KExpr<T>, rewriteBvEq: KContext.(KExpr<T>, KExpr<T>) -> KExpr<KBoolSort> = { l, r -> simplifyEq(l, r) }, rewriteAnd: KContext.(KExpr<KBoolSort>, KExpr<KBoolSort>) -> KExpr<KBoolSort> = { l, r -> simplifyAnd(l, r) }, rewriteNot: KContext.(KExpr<KBoolSort>) -> KExpr<KBoolSort> = KContext::simplifyNot): KExpr<KBoolSort>

rewriteBvMulNoOverflowExpr

fun <T : KBvSort> KContext.rewriteBvMulNoOverflowExpr(lhs: KExpr<T>, rhs: KExpr<T>, isSigned: Boolean, rewriteBvZeroExtensionExpr: KContext.(Int, KExpr<T>) -> KExpr<KBvSort> = KContext::mkBvZeroExtensionExpr, rewriteBvExtractExpr: KContext.(Int, Int, KExpr<KBvSort>) -> KExpr<KBvSort> = KContext::mkBvExtractExpr, rewriteBvConcatExpr: KContext.(KExpr<KBvSort>, KExpr<KBvSort>) -> KExpr<KBvSort> = KContext::mkBvConcatExpr, rewriteBvMulExpr: KContext.(KExpr<KBvSort>, KExpr<KBvSort>) -> KExpr<KBvSort> = KContext::mkBvMulExpr, rewriteBvXorExpr: KContext.(KExpr<KBvSort>, KExpr<KBvSort>) -> KExpr<KBvSort> = KContext::mkBvXorExpr, rewriteBvEq: KContext.(KExpr<KBvSort>, KExpr<KBvSort>) -> KExpr<KBoolSort> = { l, r -> mkEq(l, r) }, rewriteBvNotExpr: KContext.(KExpr<T>) -> KExpr<T> = KContext::mkBvNotExpr, rewriteOr: KContext.(KExpr<KBoolSort>, KExpr<KBoolSort>, Boolean, Boolean) -> KExpr<KBoolSort> = KContext::mkOr, rewriteFlatOr: KContext.(List<KExpr<KBoolSort>>) -> KExpr<KBoolSort> = { mkOr(it) }, rewriteAnd: KContext.(KExpr<KBoolSort>, KExpr<KBoolSort>) -> KExpr<KBoolSort> = { l, r -> mkAnd(l, r) }, rewriteNot: KContext.(KExpr<KBoolSort>) -> KExpr<KBoolSort> = KContext::mkNot): KExpr<KBoolSort>

rewriteBvMulNoUnderflowExpr

fun <T : KBvSort> KContext.rewriteBvMulNoUnderflowExpr(lhs: KExpr<T>, rhs: KExpr<T>, rewriteBvExtractExpr: KContext.(Int, Int, KExpr<KBvSort>) -> KExpr<KBvSort> = KContext::mkBvExtractExpr, rewriteBvConcatExpr: KContext.(KExpr<KBvSort>, KExpr<KBvSort>) -> KExpr<KBvSort> = KContext::mkBvConcatExpr, rewriteBvMulExpr: KContext.(KExpr<KBvSort>, KExpr<KBvSort>) -> KExpr<KBvSort> = KContext::mkBvMulExpr, rewriteBvXorExpr: KContext.(KExpr<KBvSort>, KExpr<KBvSort>) -> KExpr<KBvSort> = KContext::mkBvXorExpr, rewriteBvEq: KContext.(KExpr<KBvSort>, KExpr<KBvSort>) -> KExpr<KBoolSort> = { l, r -> mkEq(l, r) }, rewriteBvNotExpr: KContext.(KExpr<T>) -> KExpr<T> = KContext::mkBvNotExpr, rewriteOr: KContext.(KExpr<KBoolSort>, KExpr<KBoolSort>, Boolean, Boolean) -> KExpr<KBoolSort> = KContext::mkOr, rewriteFlatOr: KContext.(List<KExpr<KBoolSort>>) -> KExpr<KBoolSort> = { mkOr(it) }, rewriteAnd: KContext.(KExpr<KBoolSort>, KExpr<KBoolSort>) -> KExpr<KBoolSort> = { l, r -> mkAnd(l, r) }, rewriteNot: KContext.(KExpr<KBoolSort>) -> KExpr<KBoolSort> = KContext::mkNot): KExpr<KBoolSort>

rewriteBvNAndExpr

inline fun <T : KBvSort> KContext.rewriteBvNAndExpr(lhs: KExpr<T>, rhs: KExpr<T>, rewriteBvOrExpr: KContext.(KExpr<T>, KExpr<T>) -> KExpr<T>, rewriteBvNotExpr: KContext.(KExpr<T>) -> KExpr<T>): KExpr<T>

(bvnand a b) ==> (bvor (bvnot a) (bvnot b))

rewriteBvNegNoOverflowExpr

inline fun <T : KBvSort> KContext.rewriteBvNegNoOverflowExpr(arg: KExpr<T>, rewriteBvEq: KContext.(KExpr<T>, KExpr<T>) -> KExpr<KBoolSort> = { l, r -> simplifyEq(l, r) }, rewriteNot: KContext.(KExpr<KBoolSort>) -> KExpr<KBoolSort> = KContext::simplifyNot): KExpr<KBoolSort>

rewriteBvNorExpr

inline fun <T : KBvSort> KContext.rewriteBvNorExpr(lhs: KExpr<T>, rhs: KExpr<T>, rewriteBvOrExpr: KContext.(KExpr<T>, KExpr<T>) -> KExpr<T>, rewriteBvNotExpr: KContext.(KExpr<T>) -> KExpr<T>): KExpr<T>

(bvnor a b) ==> (bvnot (bvor a b))

rewriteBvRepeatExpr

inline fun KContext.rewriteBvRepeatExpr(repeatNumber: Int, value: KExpr<KBvSort>, rewriteFlatBvConcatExpr: KContext.(List<KExpr<KBvSort>>) -> KExpr<KBvSort>): KExpr<KBvSort>

(repeat a x) ==> (concat a a ..x.. a)

rewriteBvRotateLeftIndexedExpr

inline fun <T : KBvSort> KContext.rewriteBvRotateLeftIndexedExpr(rotation: Int, value: KExpr<T>, crossinline rewriteBvExtractExpr: KContext.(Int, Int, KExpr<T>) -> KExpr<KBvSort>, crossinline rewriteBvConcatExpr: KContext.(KExpr<T>, KExpr<KBvSort>) -> KExpr<KBvSort>): KExpr<T>

(rotateLeft a x) ==> (concat (extract size-1-x:0 a) (extract size-1:size-x a))

rewriteBvRotateRightIndexedExpr

inline fun <T : KBvSort> KContext.rewriteBvRotateRightIndexedExpr(rotation: Int, value: KExpr<T>, crossinline rewriteBvExtractExpr: KContext.(Int, Int, KExpr<T>) -> KExpr<KBvSort>, crossinline rewriteBvConcatExpr: KContext.(KExpr<T>, KExpr<KBvSort>) -> KExpr<KBvSort>): KExpr<T>

(rotateRight a x) ==> (rotateLeft a (- size x))

rewriteBvSignedGreaterExpr

inline fun <T : KBvSort> KContext.rewriteBvSignedGreaterExpr(lhs: KExpr<T>, rhs: KExpr<T>, rewriteBvSignedLessOrEqualExpr: KContext.(KExpr<T>, KExpr<T>) -> KExpr<KBoolSort>, rewriteNot: KContext.(KExpr<KBoolSort>) -> KExpr<KBoolSort>): KExpr<KBoolSort>

(sgt a b) ==> (not (sle a b))

rewriteBvSignedGreaterOrEqualExpr

inline fun <T : KBvSort> KContext.rewriteBvSignedGreaterOrEqualExpr(lhs: KExpr<T>, rhs: KExpr<T>, rewriteBvSignedLessOrEqualExpr: KContext.(KExpr<T>, KExpr<T>) -> KExpr<KBoolSort>): KExpr<KBoolSort>

(sge a b) ==> (sle b a)

rewriteBvSignedLessExpr

inline fun <T : KBvSort> KContext.rewriteBvSignedLessExpr(lhs: KExpr<T>, rhs: KExpr<T>, rewriteBvSignedLessOrEqualExpr: KContext.(KExpr<T>, KExpr<T>) -> KExpr<KBoolSort>, rewriteNot: KContext.(KExpr<KBoolSort>) -> KExpr<KBoolSort>): KExpr<KBoolSort>

(slt a b) ==> (not (sle b a))

rewriteBvSubExpr

inline fun <T : KBvSort> KContext.rewriteBvSubExpr(lhs: KExpr<T>, rhs: KExpr<T>, rewriteBvAddExpr: KContext.(KExpr<T>, KExpr<T>) -> KExpr<T>, rewriteBvNegationExpr: KContext.(KExpr<T>) -> KExpr<T>): KExpr<T>

(- a b) ==> (+ a -b)

rewriteBvSubNoOverflowExpr

inline fun <T : KBvSort> KContext.rewriteBvSubNoOverflowExpr(lhs: KExpr<T>, rhs: KExpr<T>, rewriteBvSignedLessExpr: KContext.(KExpr<T>, KExpr<T>) -> KExpr<KBoolSort> = KContext::simplifyBvSignedLessExpr, rewriteBvAddNoOverflowExpr: (KExpr<T>, KExpr<T>, Boolean) -> KExpr<KBoolSort> = { l, r, isSigned -> simplifyBvAddNoOverflowExpr(l, r, isSigned) }, rewriteBvEq: KContext.(KExpr<T>, KExpr<T>) -> KExpr<KBoolSort> = { l, r -> simplifyEq(l, r) }, rewriteBvNegationExpr: KContext.(KExpr<T>) -> KExpr<T> = KContext::simplifyBvNegationExpr, rewriteIte: (KExpr<KBoolSort>, KExpr<KBoolSort>, KExpr<KBoolSort>) -> KExpr<KBoolSort> = { c, t, f -> simplifyIte(c, t, f) }): KExpr<KBoolSort>

rewriteBvSubNoUnderflowExpr

inline fun <T : KBvSort> KContext.rewriteBvSubNoUnderflowExpr(lhs: KExpr<T>, rhs: KExpr<T>, isSigned: Boolean, rewriteBvSignedLessExpr: KContext.(KExpr<T>, KExpr<T>) -> KExpr<KBoolSort> = KContext::simplifyBvSignedLessExpr, rewriteBvUnsignedLessOrEqualExpr: KContext.(KExpr<T>, KExpr<T>) -> KExpr<KBoolSort> = KContext::simplifyBvUnsignedLessOrEqualExpr, createBvAddNoUnderflowExpr: KContext.(KExpr<T>, KExpr<T>) -> KExpr<KBoolSort> = KContext::simplifyBvAddNoUnderflowExpr, rewriteBvNegationExpr: KContext.(KExpr<T>) -> KExpr<T> = KContext::simplifyBvNegationExpr, rewriteImplies: KContext.(KExpr<KBoolSort>, KExpr<KBoolSort>) -> KExpr<KBoolSort> = KContext::simplifyImplies): KExpr<KBoolSort>

rewriteBvUnsignedGreaterExpr

inline fun <T : KBvSort> KContext.rewriteBvUnsignedGreaterExpr(lhs: KExpr<T>, rhs: KExpr<T>, rewriteBvUnsignedLessOrEqualExpr: KContext.(KExpr<T>, KExpr<T>) -> KExpr<KBoolSort>, rewriteNot: KContext.(KExpr<KBoolSort>) -> KExpr<KBoolSort>): KExpr<KBoolSort>

(ugt a b) ==> (not (ule a b))

rewriteBvUnsignedGreaterOrEqualExpr

inline fun <T : KBvSort> KContext.rewriteBvUnsignedGreaterOrEqualExpr(lhs: KExpr<T>, rhs: KExpr<T>, rewriteBvUnsignedLessOrEqualExpr: KContext.(KExpr<T>, KExpr<T>) -> KExpr<KBoolSort>): KExpr<KBoolSort>

(uge a b) ==> (ule b a)

rewriteBvUnsignedLessExpr

inline fun <T : KBvSort> KContext.rewriteBvUnsignedLessExpr(lhs: KExpr<T>, rhs: KExpr<T>, rewriteBvUnsignedLessOrEqualExpr: KContext.(KExpr<T>, KExpr<T>) -> KExpr<KBoolSort>, rewriteNot: KContext.(KExpr<KBoolSort>) -> KExpr<KBoolSort>): KExpr<KBoolSort>

(ult a b) ==> (not (ule b a))

rewriteBvUnsignedLessOrEqualExprLight

inline fun <T : KBvSort> KContext.rewriteBvUnsignedLessOrEqualExprLight(lhs: KExpr<T>, rhs: KExpr<T>, rewriteBvEq: KContext.(KExpr<T>, KExpr<T>) -> KExpr<KBoolSort>, cont: (KExpr<T>, KExpr<T>) -> KExpr<KBoolSort>): KExpr<KBoolSort>

rewriteBvXNorExpr

inline fun <T : KBvSort> KContext.rewriteBvXNorExpr(lhs: KExpr<T>, rhs: KExpr<T>, rewriteBvXorExpr: KContext.(KExpr<T>, KExpr<T>) -> KExpr<T>, rewriteBvNotExpr: KContext.(KExpr<T>) -> KExpr<T>): KExpr<T>

(bvxnor a b) ==> (bvnot (bvxor a b))

rewriteBvZeroExtensionExpr

inline fun <T : KBvSort> KContext.rewriteBvZeroExtensionExpr(extensionSize: Int, value: KExpr<T>, rewriteBvConcatExpr: KContext.(KExpr<KBvSort>, KExpr<KBvSort>) -> KExpr<KBvSort>): KExpr<KBvSort>

(zeroext a) ==> (concat 0 a)

rewriteFpGreaterExpr

inline fun <T : KFpSort> KContext.rewriteFpGreaterExpr(lhs: KExpr<T>, rhs: KExpr<T>, rewriteFpLessExpr: KContext.(KExpr<T>, KExpr<T>) -> KExpr<KBoolSort>): KExpr<KBoolSort>

rewriteFpGreaterOrEqualExpr

inline fun <T : KFpSort> KContext.rewriteFpGreaterOrEqualExpr(lhs: KExpr<T>, rhs: KExpr<T>, rewriteFpLessOrEqualExpr: KContext.(KExpr<T>, KExpr<T>) -> KExpr<KBoolSort>): KExpr<KBoolSort>

rewriteFpSubExpr

inline fun <T : KFpSort> KContext.rewriteFpSubExpr(roundingMode: KExpr<KFpRoundingModeSort>, lhs: KExpr<T>, rhs: KExpr<T>, rewriteFpNegationExpr: KContext.(KExpr<T>) -> KExpr<T>, rewriteFpAddExpr: KContext.(KExpr<KFpRoundingModeSort>, KExpr<T>, KExpr<T>) -> KExpr<T>): KExpr<T>

a - b ==> a + (-b)

rewriteImplies

inline fun KContext.rewriteImplies(p: KExpr<KBoolSort>, q: KExpr<KBoolSort>, rewriteNot: KContext.(KExpr<KBoolSort>) -> KExpr<KBoolSort>, rewriteOr: KContext.(KExpr<KBoolSort>, KExpr<KBoolSort>) -> KExpr<KBoolSort>): KExpr<KBoolSort>

(=> p q) ==> (or (not p) q)

rewriteXor

inline fun KContext.rewriteXor(a: KExpr<KBoolSort>, b: KExpr<KBoolSort>, rewriteNot: KContext.(KExpr<KBoolSort>) -> KExpr<KBoolSort>, rewriteEq: KContext.(KExpr<KBoolSort>, KExpr<KBoolSort>) -> KExpr<KBoolSort>): KExpr<KBoolSort>

(xor a b) ==> (= (not a) b)

rotateLeft

inline fun <T : KBvSort> KContext.rotateLeft(arg: KExpr<T>, size: Int, rotationNumber: Int, rewriteBvExtractExpr: KContext.(Int, Int, KExpr<T>) -> KExpr<KBvSort>, rewriteBvConcatExpr: KContext.(KExpr<T>, KExpr<KBvSort>) -> KExpr<KBvSort>): KExpr<T>

simplifyAnd

fun KContext.simplifyAnd(args: List<KExpr<KBoolSort>>, flat: Boolean = true, order: Boolean = true): KExpr<KBoolSort>

fun KContext.simplifyAnd(lhs: KExpr<KBoolSort>, rhs: KExpr<KBoolSort>, flat: Boolean = true, order: Boolean = true): KExpr<KBoolSort>

simplifyAndOr

inline fun <T : KApp<KBoolSort, KBoolSort>> simplifyAndOr(flat: Boolean, order: Boolean, args: List<KExpr<KBoolSort>>, neutralElement: KExpr<KBoolSort>, zeroElement: KExpr<KBoolSort>, buildResultExpr: (List<KExpr<KBoolSort>>) -> T): KExpr<KBoolSort>

inline fun <T : KApp<KBoolSort, KBoolSort>> simplifyAndOr(flat: Boolean, order: Boolean, args: List<KExpr<KBoolSort>>, neutralElement: KExpr<KBoolSort>, zeroElement: KExpr<KBoolSort>, buildResultBinaryExpr: (KExpr<KBoolSort>, KExpr<KBoolSort>) -> T, buildResultFlatExpr: (List<KExpr<KBoolSort>>) -> T): KExpr<KBoolSort>

inline fun <T : KApp<KBoolSort, KBoolSort>> simplifyAndOr(flat: Boolean, order: Boolean, lhs: KExpr<KBoolSort>, rhs: KExpr<KBoolSort>, neutralElement: KExpr<KBoolSort>, zeroElement: KExpr<KBoolSort>, buildResultBinaryExpr: (KExpr<KBoolSort>, KExpr<KBoolSort>) -> T, buildResultFlatExpr: (List<KExpr<KBoolSort>>) -> T): KExpr<KBoolSort>

simplifyArithAdd

fun <T : KArithSort> KContext.simplifyArithAdd(args: List<KExpr<T>>): KExpr<T>

simplifyArithAddLight

inline fun <T : KArithSort> KContext.simplifyArithAddLight(args: List<KExpr<T>>, cont: (List<KExpr<T>>) -> KExpr<T>): KExpr<T>

simplifyArithDiv

fun <T : KArithSort> KContext.simplifyArithDiv(lhs: KExpr<T>, rhs: KExpr<T>): KExpr<T>

simplifyArithDivLight

inline fun <T : KArithSort> KContext.simplifyArithDivLight(lhs: KExpr<T>, rhs: KExpr<T>, rewriteArithUnaryMinus: KContext.(KExpr<T>) -> KExpr<T>, cont: (KExpr<T>, KExpr<T>) -> KExpr<T>): KExpr<T>

simplifyArithGe

fun <T : KArithSort> KContext.simplifyArithGe(lhs: KExpr<T>, rhs: KExpr<T>): KExpr<KBoolSort>

simplifyArithGt

fun <T : KArithSort> KContext.simplifyArithGt(lhs: KExpr<T>, rhs: KExpr<T>): KExpr<KBoolSort>

simplifyArithLe

fun <T : KArithSort> KContext.simplifyArithLe(lhs: KExpr<T>, rhs: KExpr<T>): KExpr<KBoolSort>

simplifyArithLeLight

inline fun <T : KArithSort> KContext.simplifyArithLeLight(lhs: KExpr<T>, rhs: KExpr<T>, cont: (KExpr<T>, KExpr<T>) -> KExpr<KBoolSort>): KExpr<KBoolSort>

simplifyArithLt

fun <T : KArithSort> KContext.simplifyArithLt(lhs: KExpr<T>, rhs: KExpr<T>): KExpr<KBoolSort>

simplifyArithLtLight

inline fun <T : KArithSort> KContext.simplifyArithLtLight(lhs: KExpr<T>, rhs: KExpr<T>, cont: (KExpr<T>, KExpr<T>) -> KExpr<KBoolSort>): KExpr<KBoolSort>

simplifyArithMul

fun <T : KArithSort> KContext.simplifyArithMul(args: List<KExpr<T>>): KExpr<T>

simplifyArithMulLight

inline fun <T : KArithSort> KContext.simplifyArithMulLight(args: List<KExpr<T>>, cont: (List<KExpr<T>>) -> KExpr<T>): KExpr<T>

simplifyArithPower

fun <T : KArithSort> KContext.simplifyArithPower(lhs: KExpr<T>, rhs: KExpr<T>): KExpr<T>

simplifyArithPowerLight

inline fun <T : KArithSort> KContext.simplifyArithPowerLight(lhs: KExpr<T>, rhs: KExpr<T>, cont: (KExpr<T>, KExpr<T>) -> KExpr<T>): KExpr<T>

simplifyArithSub

fun <T : KArithSort> KContext.simplifyArithSub(args: List<KExpr<T>>): KExpr<T>

simplifyArithUnaryMinus

fun <T : KArithSort> KContext.simplifyArithUnaryMinus(arg: KExpr<T>): KExpr<T>

simplifyArithUnaryMinusLight

inline fun <T : KArithSort> KContext.simplifyArithUnaryMinusLight(arg: KExpr<T>, cont: (KExpr<T>) -> KExpr<T>): KExpr<T>

simplifyArrayNSelect

fun <R : KSort> KContext.simplifyArrayNSelect(array: KExpr<KArrayNSort<R>>, indices: List<KExpr<*>>): KExpr<R>

simplifyArrayNSelectFromArrayStore

inline fun <R : KSort> KContext.simplifyArrayNSelectFromArrayStore(array: KExpr<KArrayNSort<R>>, indices: List<KExpr<*>>, storeIndexMatch: KContext.(KArrayNStore<R>, List<KExpr<*>>) -> Boolean, storeIndexDistinct: KContext.(KArrayNStore<R>, List<KExpr<*>>) -> Boolean, cont: (KExpr<KArrayNSort<R>>, List<KExpr<*>>) -> KExpr<R>): KExpr<R>

simplifyArrayNSelectLambda

inline fun <R : KSort> KContext.simplifyArrayNSelectLambda(array: KExpr<KArrayNSort<R>>, indices: List<KExpr<*>>, rewriteBody: KContext.(KExpr<R>) -> KExpr<R> = { it }, cont: (KExpr<KArrayNSort<R>>, List<KExpr<*>>) -> KExpr<R>): KExpr<R>

simplifyArrayNStore

fun <R : KSort> KContext.simplifyArrayNStore(array: KExpr<KArrayNSort<R>>, indices: List<KExpr<*>>, value: KExpr<R>): KExpr<KArrayNSort<R>>

simplifyArrayNStoreLight

inline fun <R : KSort> KContext.simplifyArrayNStoreLight(array: KExpr<KArrayNSort<R>>, indices: List<KExpr<*>>, value: KExpr<R>, cont: (KExpr<KArrayNSort<R>>, List<KExpr<*>>, KExpr<R>) -> KExpr<KArrayNSort<R>>): KExpr<KArrayNSort<R>>

simplifyArraySelect

fun <D : KSort, R : KSort> KContext.simplifyArraySelect(array: KExpr<KArraySort<D, R>>, index: KExpr<D>): KExpr<R>

fun <D0 : KSort, D1 : KSort, R : KSort> KContext.simplifyArraySelect(array: KExpr<KArray2Sort<D0, D1, R>>, index0: KExpr<D0>, index1: KExpr<D1>): KExpr<R>

fun <D0 : KSort, D1 : KSort, D2 : KSort, R : KSort> KContext.simplifyArraySelect(array: KExpr<KArray3Sort<D0, D1, D2, R>>, index0: KExpr<D0>, index1: KExpr<D1>, index2: KExpr<D2>): KExpr<R>

simplifyArraySelectLambda

inline fun <A : KArraySortBase<R>, R : KSort, L : KArrayLambdaBase<A, R>> KContext.simplifyArraySelectLambda(array: KExpr<A>, mkLambdaSubstitution: KExprSubstitutor.(L) -> Unit, rewriteBody: KContext.(KExpr<R>) -> KExpr<R>, default: (KExpr<A>) -> KExpr<R>): KExpr<R>

inline fun <D : KSort, R : KSort> KContext.simplifyArraySelectLambda(array: KExpr<KArraySort<D, R>>, index: KExpr<D>, rewriteBody: KContext.(KExpr<R>) -> KExpr<R> = { it }, cont: (KExpr<KArraySort<D, R>>, KExpr<D>) -> KExpr<R>): KExpr<R>

inline fun <D0 : KSort, D1 : KSort, R : KSort> KContext.simplifyArraySelectLambda(array: KExpr<KArray2Sort<D0, D1, R>>, index0: KExpr<D0>, index1: KExpr<D1>, rewriteBody: KContext.(KExpr<R>) -> KExpr<R> = { it }, cont: (KExpr<KArray2Sort<D0, D1, R>>, KExpr<D0>, KExpr<D1>) -> KExpr<R>): KExpr<R>

inline fun <D0 : KSort, D1 : KSort, D2 : KSort, R : KSort> KContext.simplifyArraySelectLambda(array: KExpr<KArray3Sort<D0, D1, D2, R>>, index0: KExpr<D0>, index1: KExpr<D1>, index2: KExpr<D2>, rewriteBody: KContext.(KExpr<R>) -> KExpr<R> = { it }, cont: (KExpr<KArray3Sort<D0, D1, D2, R>>, KExpr<D0>, KExpr<D1>, KExpr<D2>) -> KExpr<R>): KExpr<R>

simplifyArrayStore

fun <D : KSort, R : KSort> KContext.simplifyArrayStore(array: KExpr<KArraySort<D, R>>, index: KExpr<D>, value: KExpr<R>): KExpr<KArraySort<D, R>>

fun <D0 : KSort, D1 : KSort, R : KSort> KContext.simplifyArrayStore(array: KExpr<KArray2Sort<D0, D1, R>>, index0: KExpr<D0>, index1: KExpr<D1>, value: KExpr<R>): KExpr<KArray2Sort<D0, D1, R>>

fun <D0 : KSort, D1 : KSort, D2 : KSort, R : KSort> KContext.simplifyArrayStore(array: KExpr<KArray3Sort<D0, D1, D2, R>>, index0: KExpr<D0>, index1: KExpr<D1>, index2: KExpr<D2>, value: KExpr<R>): KExpr<KArray3Sort<D0, D1, D2, R>>

simplifyArrayStoreLight

inline fun <A : KArraySortBase<R>, R : KSort, S : KArraySelectBase<out A, R>> simplifyArrayStoreLight(array: KExpr<A>, value: KExpr<R>, selectIndicesMatch: (S) -> Boolean, default: () -> KExpr<A>): KExpr<A>

inline fun <D : KSort, R : KSort> KContext.simplifyArrayStoreLight(array: KExpr<KArraySort<D, R>>, index: KExpr<D>, value: KExpr<R>, cont: (KExpr<KArraySort<D, R>>, KExpr<D>, KExpr<R>) -> KExpr<KArraySort<D, R>>): KExpr<KArraySort<D, R>>

inline fun <D0 : KSort, D1 : KSort, R : KSort> KContext.simplifyArrayStoreLight(array: KExpr<KArray2Sort<D0, D1, R>>, index0: KExpr<D0>, index1: KExpr<D1>, value: KExpr<R>, cont: (KExpr<KArray2Sort<D0, D1, R>>, KExpr<D0>, KExpr<D1>, KExpr<R>) -> KExpr<KArray2Sort<D0, D1, R>>): KExpr<KArray2Sort<D0, D1, R>>

inline fun <D0 : KSort, D1 : KSort, D2 : KSort, R : KSort> KContext.simplifyArrayStoreLight(array: KExpr<KArray3Sort<D0, D1, D2, R>>, index0: KExpr<D0>, index1: KExpr<D1>, index2: KExpr<D2>, value: KExpr<R>, cont: (KExpr<KArray3Sort<D0, D1, D2, R>>, KExpr<D0>, KExpr<D1>, KExpr<D2>, KExpr<R>) -> KExpr<KArray3Sort<D0, D1, D2, R>>): KExpr<KArray3Sort<D0, D1, D2, R>>

simplifyBoolIteConstBranches

inline fun KContext.simplifyBoolIteConstBranches(condition: KExpr<KBoolSort>, trueBranch: KExpr<KBoolSort>, falseBranch: KExpr<KBoolSort>, rewriteOr: KContext.(KExpr<KBoolSort>, KExpr<KBoolSort>) -> KExpr<KBoolSort>, rewriteAnd: KContext.(KExpr<KBoolSort>, KExpr<KBoolSort>) -> KExpr<KBoolSort>, rewriteNot: KContext.(KExpr<KBoolSort>) -> KExpr<KBoolSort>, cont: (KExpr<KBoolSort>, KExpr<KBoolSort>, KExpr<KBoolSort>) -> KExpr<KBoolSort>): KExpr<KBoolSort>

(ite c true e) ==> (or c e) (ite c false e) ==> (and (not c) e) (ite c t true) ==> (or (not c) t) (ite c t false) ==> (and c t)

simplifyBoolIteSameConditionBranch

inline fun KContext.simplifyBoolIteSameConditionBranch(condition: KExpr<KBoolSort>, trueBranch: KExpr<KBoolSort>, falseBranch: KExpr<KBoolSort>, rewriteAnd: KContext.(KExpr<KBoolSort>, KExpr<KBoolSort>) -> KExpr<KBoolSort>, rewriteOr: KContext.(KExpr<KBoolSort>, KExpr<KBoolSort>) -> KExpr<KBoolSort>, cont: (KExpr<KBoolSort>, KExpr<KBoolSort>, KExpr<KBoolSort>) -> KExpr<KBoolSort>): KExpr<KBoolSort>

(ite c t c) ==> (and c t) (ite c c e) ==> (or c e)

simplifyBv2IntExpr

fun <T : KBvSort> KContext.simplifyBv2IntExpr(value: KExpr<T>, isSigned: Boolean): KExpr<KIntSort>

simplifyBv2IntExprLight

inline fun <T : KBvSort> KContext.simplifyBv2IntExprLight(value: KExpr<T>, isSigned: Boolean, cont: (KExpr<T>, Boolean) -> KExpr<KIntSort>): KExpr<KIntSort>

simplifyBvAddExpr

fun <T : KBvSort> KContext.simplifyBvAddExpr(lhs: KExpr<T>, rhs: KExpr<T>): KExpr<T>

simplifyBvAddExprLight

inline fun <T : KBvSort> KContext.simplifyBvAddExprLight(lhs: KExpr<T>, rhs: KExpr<T>, cont: (KExpr<T>, KExpr<T>) -> KExpr<T>): KExpr<T>

simplifyBvAddExprNestedAdd

inline fun <T : KBvSort> KContext.simplifyBvAddExprNestedAdd(lhs: KExpr<T>, rhs: KExpr<T>, rewriteBvAddExpr: KContext.(KExpr<T>, KExpr<T>) -> KExpr<T>, cont: (KExpr<T>, KExpr<T>) -> KExpr<T>): KExpr<T>

(+ const1 (+ const2 x)) ==> (+ (+ const1 const2) x)

simplifyBvAddNoOverflowExpr

fun <T : KBvSort> KContext.simplifyBvAddNoOverflowExpr(lhs: KExpr<T>, rhs: KExpr<T>, isSigned: Boolean): KExpr<KBoolSort>

simplifyBvAddNoUnderflowExpr

fun <T : KBvSort> KContext.simplifyBvAddNoUnderflowExpr(lhs: KExpr<T>, rhs: KExpr<T>): KExpr<KBoolSort>

simplifyBvAndExpr

fun <T : KBvSort> KContext.simplifyBvAndExpr(lhs: KExpr<T>, rhs: KExpr<T>): KExpr<T>

simplifyBvAndExprLight

inline fun <T : KBvSort> KContext.simplifyBvAndExprLight(lhs: KExpr<T>, rhs: KExpr<T>, cont: (KExpr<T>, KExpr<T>) -> KExpr<T>): KExpr<T>

simplifyBvAndExprNestedAnd

inline fun <T : KBvSort> KContext.simplifyBvAndExprNestedAnd(lhs: KExpr<T>, rhs: KExpr<T>, rewriteBvAndExpr: KContext.(KExpr<T>, KExpr<T>) -> KExpr<T>, cont: (KExpr<T>, KExpr<T>) -> KExpr<T>): KExpr<T>

(bvand const1 (bvand const2 x)) ==> (bvand (bvand const1 const2) x)

simplifyBvAndOr

inline fun <T : KBvSort> KContext.simplifyBvAndOr(args: List<KExpr<T>>, neutralElement: KBitVecValue<T>, isZeroElement: KContext.(KBitVecValue<T>) -> Boolean, buildZeroElement: KContext.() -> KBitVecValue<T>, operation: (KBitVecValue<T>, KBitVecValue<T>) -> KBitVecValue<T>, cont: (List<KExpr<T>>) -> KExpr<T>): KExpr<T>

simplifyBvArithShiftRightExpr

fun <T : KBvSort> KContext.simplifyBvArithShiftRightExpr(lhs: KExpr<T>, shift: KExpr<T>): KExpr<T>

simplifyBvArithShiftRightExprLight

inline fun <T : KBvSort> KContext.simplifyBvArithShiftRightExprLight(lhs: KExpr<T>, shift: KExpr<T>, cont: (KExpr<T>, KExpr<T>) -> KExpr<T>): KExpr<T>

simplifyBvConcatExpr

fun <T : KBvSort, S : KBvSort> KContext.simplifyBvConcatExpr(lhs: KExpr<T>, rhs: KExpr<S>): KExpr<KBvSort>

simplifyBvConcatExprLight

inline fun <T : KBvSort, S : KBvSort> KContext.simplifyBvConcatExprLight(lhs: KExpr<T>, rhs: KExpr<S>, cont: (KExpr<T>, KExpr<S>) -> KExpr<KBvSort>): KExpr<KBvSort>

eval constants

simplifyBvConcatExprNestedConcat

inline fun <T : KBvSort, S : KBvSort> KContext.simplifyBvConcatExprNestedConcat(lhs: KExpr<T>, rhs: KExpr<S>, rewriteBvConcatExpr: KContext.(KExpr<KBvSort>, KExpr<KBvSort>) -> KExpr<KBvSort>, cont: (KExpr<T>, KExpr<S>) -> KExpr<KBvSort>): KExpr<KBvSort>

(concat const1 (concat const2 a)) ==> (concat (concat const1 const2) a) (concat (concat a const1) const2) ==> (concat a (concat const1 const2))

simplifyBvDivNoOverflowExpr

fun <T : KBvSort> KContext.simplifyBvDivNoOverflowExpr(lhs: KExpr<T>, rhs: KExpr<T>): KExpr<KBoolSort>

simplifyBvExtractExpr

fun <T : KBvSort> KContext.simplifyBvExtractExpr(high: Int, low: Int, value: KExpr<T>): KExpr<KBvSort>

simplifyBvExtractExprLight

inline fun <T : KBvSort> KContext.simplifyBvExtractExprLight(high: Int, low: Int, value: KExpr<T>, cont: (Int, Int, KExpr<T>) -> KExpr<KBvSort>): KExpr<KBvSort>

simplifyBvExtractExprNestedExtract

inline fun <T : KBvSort> KContext.simplifyBvExtractExprNestedExtract(high: Int, low: Int, value: KExpr<T>, rewriteBvExtractExpr: KContext.(Int, Int, KExpr<KBvSort>) -> KExpr<KBvSort>, cont: (Int, Int, KExpr<T>) -> KExpr<KBvSort>): KExpr<KBvSort>

(extracthigh:low (extract_:nestedLow x)) ==> (extracthigh+nestedLow : low+nestedLow x)

simplifyBvExtractExprTryRewrite

simplifyBvLogicalShiftRightExpr

fun <T : KBvSort> KContext.simplifyBvLogicalShiftRightExpr(lhs: KExpr<T>, shift: KExpr<T>): KExpr<T>

simplifyBvLogicalShiftRightExprConstShift

inline fun <T : KBvSort> KContext.simplifyBvLogicalShiftRightExprConstShift(arg: KExpr<T>, shift: KExpr<T>, rewriteBvExtractExpr: KContext.(Int, Int, KExpr<KBvSort>) -> KExpr<KBvSort>, rewriteBvConcatExpr: KContext.(KExpr<KBvSort>, KExpr<KBvSort>) -> KExpr<KBvSort>, cont: (KExpr<T>, KExpr<T>) -> KExpr<T>): KExpr<T>

(bvlshr x shift) ==> (concat 0.shift.0 (extract size-1:shift x))

simplifyBvLogicalShiftRightExprLight

inline fun <T : KBvSort> KContext.simplifyBvLogicalShiftRightExprLight(lhs: KExpr<T>, shift: KExpr<T>, cont: (KExpr<T>, KExpr<T>) -> KExpr<T>): KExpr<T>

simplifyBvMulExpr

fun <T : KBvSort> KContext.simplifyBvMulExpr(lhs: KExpr<T>, rhs: KExpr<T>): KExpr<T>

simplifyBvMulExprLight

inline fun <T : KBvSort> KContext.simplifyBvMulExprLight(lhs: KExpr<T>, rhs: KExpr<T>, cont: (KExpr<T>, KExpr<T>) -> KExpr<T>): KExpr<T>

simplifyBvMulExprMinusOneConst

inline fun <T : KBvSort> KContext.simplifyBvMulExprMinusOneConst(lhs: KExpr<T>, rhs: KExpr<T>, rewriteBvNegationExpr: KContext.(KExpr<T>) -> KExpr<T>, cont: (KExpr<T>, KExpr<T>) -> KExpr<T>): KExpr<T>

(* -1 a) ==> -a

simplifyBvMulExprNestedMul

inline fun <T : KBvSort> KContext.simplifyBvMulExprNestedMul(lhs: KExpr<T>, rhs: KExpr<T>, rewriteBvMulExpr: KContext.(KExpr<T>, KExpr<T>) -> KExpr<T>, cont: (KExpr<T>, KExpr<T>) -> KExpr<T>): KExpr<T>

(* const1 (* const2 x)) ==> (* (* const1 const2) x)

simplifyBvMulNoOverflowExpr

fun <T : KBvSort> KContext.simplifyBvMulNoOverflowExpr(lhs: KExpr<T>, rhs: KExpr<T>, isSigned: Boolean): KExpr<KBoolSort>

simplifyBvMulNoUnderflowExpr

fun <T : KBvSort> KContext.simplifyBvMulNoUnderflowExpr(lhs: KExpr<T>, rhs: KExpr<T>): KExpr<KBoolSort>

simplifyBvNAndExpr

fun <T : KBvSort> KContext.simplifyBvNAndExpr(lhs: KExpr<T>, rhs: KExpr<T>): KExpr<T>

simplifyBvNegationExpr

fun <T : KBvSort> KContext.simplifyBvNegationExpr(arg: KExpr<T>): KExpr<T>

simplifyBvNegationExprAdd

inline fun <T : KBvSort> KContext.simplifyBvNegationExprAdd(arg: KExpr<T>, rewriteBvAddExpr: KContext.(KExpr<T>, KExpr<T>) -> KExpr<T>, rewriteBvNegationExpr: KContext.(KExpr<T>) -> KExpr<T>, cont: (KExpr<T>) -> KExpr<T>): KExpr<T>

(bvneg (bvadd a b)) ==> (bvadd (bvneg a) (bvneg b))

simplifyBvNegationExprLight

inline fun <T : KBvSort> KContext.simplifyBvNegationExprLight(arg: KExpr<T>, cont: (KExpr<T>) -> KExpr<T>): KExpr<T>

simplifyBvNegationNoOverflowExpr

fun <T : KBvSort> KContext.simplifyBvNegationNoOverflowExpr(arg: KExpr<T>): KExpr<KBoolSort>

simplifyBvNorExpr

fun <T : KBvSort> KContext.simplifyBvNorExpr(lhs: KExpr<T>, rhs: KExpr<T>): KExpr<T>

simplifyBvNotExpr

fun <T : KBvSort> KContext.simplifyBvNotExpr(arg: KExpr<T>): KExpr<T>

simplifyBvNotExprConcat

inline fun <T : KBvSort> KContext.simplifyBvNotExprConcat(arg: KExpr<T>, rewriteBvNotExpr: KContext.(KExpr<KBvSort>) -> KExpr<KBvSort>, rewriteBvConcatExpr: KContext.(List<KExpr<KBvSort>>) -> KExpr<KBvSort>, cont: (KExpr<T>) -> KExpr<T>): KExpr<T>

(bvnot (concat a b)) ==> (concat (bvnot a) (bvnot b))

simplifyBvNotExprIte

inline fun <T : KBvSort> KContext.simplifyBvNotExprIte(arg: KExpr<T>, rewriteBvNotExpr: KContext.(KExpr<T>) -> KExpr<T>, rewriteBvIte: KContext.(KExpr<KBoolSort>, KExpr<T>, KExpr<T>) -> KExpr<T>, cont: (KExpr<T>) -> KExpr<T>): KExpr<T>

(bvnot (ite c a b)) ==> (ite c (bvnot a) (bvnot b))

simplifyBvNotExprLight

inline fun <T : KBvSort> KContext.simplifyBvNotExprLight(arg: KExpr<T>, cont: (KExpr<T>) -> KExpr<T>): KExpr<T>

simplifyBvOrExpr

fun <T : KBvSort> KContext.simplifyBvOrExpr(lhs: KExpr<T>, rhs: KExpr<T>): KExpr<T>

simplifyBvOrExprLight

inline fun <T : KBvSort> KContext.simplifyBvOrExprLight(lhs: KExpr<T>, rhs: KExpr<T>, cont: (KExpr<T>, KExpr<T>) -> KExpr<T>): KExpr<T>

simplifyBvOrExprNestedOr

inline fun <T : KBvSort> KContext.simplifyBvOrExprNestedOr(lhs: KExpr<T>, rhs: KExpr<T>, rewriteBvOrExpr: KContext.(KExpr<T>, KExpr<T>) -> KExpr<T>, cont: (KExpr<T>, KExpr<T>) -> KExpr<T>): KExpr<T>

(bvor const1 (bvor const2 x)) ==> (bvor (bvor const1 const2) x)

simplifyBvReductionAndExpr

fun <T : KBvSort> KContext.simplifyBvReductionAndExpr(arg: KExpr<T>): KExpr<KBv1Sort>

simplifyBvReductionAndExprLight

inline fun <T : KBvSort> KContext.simplifyBvReductionAndExprLight(arg: KExpr<T>, cont: (KExpr<T>) -> KExpr<KBv1Sort>): KExpr<KBv1Sort>

simplifyBvReductionOrExpr

fun <T : KBvSort> KContext.simplifyBvReductionOrExpr(arg: KExpr<T>): KExpr<KBv1Sort>

simplifyBvReductionOrExprLight

inline fun <T : KBvSort> KContext.simplifyBvReductionOrExprLight(arg: KExpr<T>, cont: (KExpr<T>) -> KExpr<KBv1Sort>): KExpr<KBv1Sort>

simplifyBvRepeatExpr

fun <T : KBvSort> KContext.simplifyBvRepeatExpr(repeatNumber: Int, value: KExpr<T>): KExpr<KBvSort>

simplifyBvRepeatExprLight

inline fun <T : KBvSort> KContext.simplifyBvRepeatExprLight(repeatNumber: Int, value: KExpr<T>, cont: (Int, KExpr<T>) -> KExpr<KBvSort>): KExpr<KBvSort>

(repeat a x) ==> (concat a a ..x.. a)

simplifyBvRotateLeftExpr

fun <T : KBvSort> KContext.simplifyBvRotateLeftExpr(lhs: KExpr<T>, rotation: KExpr<T>): KExpr<T>

simplifyBvRotateLeftExprConstRotation

inline fun <T : KBvSort> KContext.simplifyBvRotateLeftExprConstRotation(lhs: KExpr<T>, rotation: KExpr<T>, rewriteBvRotateLeftIndexedExpr: KContext.(Int, KExpr<T>) -> KExpr<T>, cont: (KExpr<T>, KExpr<T>) -> KExpr<T>): KExpr<T>

simplifyBvRotateLeftIndexedExpr

fun <T : KBvSort> KContext.simplifyBvRotateLeftIndexedExpr(rotation: Int, value: KExpr<T>): KExpr<T>

simplifyBvRotateRightExpr

fun <T : KBvSort> KContext.simplifyBvRotateRightExpr(lhs: KExpr<T>, rotation: KExpr<T>): KExpr<T>

simplifyBvRotateRightExprConstRotation

inline fun <T : KBvSort> KContext.simplifyBvRotateRightExprConstRotation(lhs: KExpr<T>, rotation: KExpr<T>, rewriteBvRotateRightIndexedExpr: KContext.(Int, KExpr<T>) -> KExpr<T>, cont: (KExpr<T>, KExpr<T>) -> KExpr<T>): KExpr<T>

(rotateRight a x) ==> (rotateLeft a (- size x))

simplifyBvRotateRightIndexedExpr

fun <T : KBvSort> KContext.simplifyBvRotateRightIndexedExpr(rotation: Int, value: KExpr<T>): KExpr<T>

simplifyBvShiftLeftExpr

fun <T : KBvSort> KContext.simplifyBvShiftLeftExpr(lhs: KExpr<T>, shift: KExpr<T>): KExpr<T>

simplifyBvShiftLeftExprConstShift

inline fun <T : KBvSort> KContext.simplifyBvShiftLeftExprConstShift(lhs: KExpr<T>, shift: KExpr<T>, rewriteBvExtractExpr: KContext.(Int, Int, KExpr<KBvSort>) -> KExpr<KBvSort>, rewriteBvConcatExpr: KContext.(KExpr<KBvSort>, KExpr<KBvSort>) -> KExpr<KBvSort>, cont: (KExpr<T>, KExpr<T>) -> KExpr<T>): KExpr<T>

(bvshl x shift) ==> (concat (extract size-1-shift:0 x) 0.shift.0)

simplifyBvShiftLeftExprLight

inline fun <T : KBvSort> KContext.simplifyBvShiftLeftExprLight(lhs: KExpr<T>, shift: KExpr<T>, cont: (KExpr<T>, KExpr<T>) -> KExpr<T>): KExpr<T>

simplifyBvShiftLeftExprNestedShiftLeft

inline fun <T : KBvSort> KContext.simplifyBvShiftLeftExprNestedShiftLeft(lhs: KExpr<T>, shift: KExpr<T>, rewriteBvAddExpr: KContext.(KExpr<T>, KExpr<T>) -> KExpr<T>, rewriteBvUnsignedLessOrEqualExpr: KContext.(KExpr<T>, KExpr<T>) -> KExpr<KBoolSort>, rewriteBvShiftLeftExpr: KContext.(KExpr<T>, KExpr<T>) -> KExpr<T>, rewriteIte: (KExpr<KBoolSort>, KExpr<T>, KExpr<T>) -> KExpr<T>, cont: (KExpr<T>, KExpr<T>) -> KExpr<T>): KExpr<T>

(bvshl (bvshl x nestedShift) shift) ==> (ite (bvule nestedShift (+ nestedShift shift)) (bvshl x (+ nestedShift shift)) 0)

simplifyBvSignedDivExpr

fun <T : KBvSort> KContext.simplifyBvSignedDivExpr(lhs: KExpr<T>, rhs: KExpr<T>): KExpr<T>

simplifyBvSignedDivExprLight

inline fun <T : KBvSort> KContext.simplifyBvSignedDivExprLight(lhs: KExpr<T>, rhs: KExpr<T>, cont: (KExpr<T>, KExpr<T>) -> KExpr<T>): KExpr<T>

simplifyBvSignedGreaterExpr

fun <T : KBvSort> KContext.simplifyBvSignedGreaterExpr(lhs: KExpr<T>, rhs: KExpr<T>): KExpr<KBoolSort>

simplifyBvSignedGreaterOrEqualExpr

fun <T : KBvSort> KContext.simplifyBvSignedGreaterOrEqualExpr(lhs: KExpr<T>, rhs: KExpr<T>): KExpr<KBoolSort>

simplifyBvSignedLessExpr

fun <T : KBvSort> KContext.simplifyBvSignedLessExpr(lhs: KExpr<T>, rhs: KExpr<T>): KExpr<KBoolSort>

simplifyBvSignedLessOrEqualExpr

fun <T : KBvSort> KContext.simplifyBvSignedLessOrEqualExpr(lhs: KExpr<T>, rhs: KExpr<T>): KExpr<KBoolSort>

simplifyBvSignedLessOrEqualExprLight

inline fun <T : KBvSort> KContext.simplifyBvSignedLessOrEqualExprLight(lhs: KExpr<T>, rhs: KExpr<T>, rewriteBvEq: KContext.(KExpr<T>, KExpr<T>) -> KExpr<KBoolSort>, cont: (KExpr<T>, KExpr<T>) -> KExpr<KBoolSort>): KExpr<KBoolSort>

simplifyBvSignedModExpr

fun <T : KBvSort> KContext.simplifyBvSignedModExpr(lhs: KExpr<T>, rhs: KExpr<T>): KExpr<T>

simplifyBvSignedModExprLight

inline fun <T : KBvSort> KContext.simplifyBvSignedModExprLight(lhs: KExpr<T>, rhs: KExpr<T>, cont: (KExpr<T>, KExpr<T>) -> KExpr<T>): KExpr<T>

simplifyBvSignedRemExpr

fun <T : KBvSort> KContext.simplifyBvSignedRemExpr(lhs: KExpr<T>, rhs: KExpr<T>): KExpr<T>

simplifyBvSignedRemExprLight

inline fun <T : KBvSort> KContext.simplifyBvSignedRemExprLight(lhs: KExpr<T>, rhs: KExpr<T>, cont: (KExpr<T>, KExpr<T>) -> KExpr<T>): KExpr<T>

simplifyBvSignExtensionExpr

fun <T : KBvSort> KContext.simplifyBvSignExtensionExpr(extensionSize: Int, value: KExpr<T>): KExpr<KBvSort>

simplifyBvSignExtensionExprLight

inline fun <T : KBvSort> KContext.simplifyBvSignExtensionExprLight(extensionSize: Int, value: KExpr<T>, cont: (Int, KExpr<T>) -> KExpr<KBvSort>): KExpr<KBvSort>

simplifyBvSubExpr

fun <T : KBvSort> KContext.simplifyBvSubExpr(lhs: KExpr<T>, rhs: KExpr<T>): KExpr<T>

simplifyBvSubNoOverflowExpr

fun <T : KBvSort> KContext.simplifyBvSubNoOverflowExpr(lhs: KExpr<T>, rhs: KExpr<T>): KExpr<KBoolSort>

simplifyBvSubNoUnderflowExpr

fun <T : KBvSort> KContext.simplifyBvSubNoUnderflowExpr(lhs: KExpr<T>, rhs: KExpr<T>, isSigned: Boolean): KExpr<KBoolSort>

simplifyBvToFpExpr

fun <T : KFpSort> KContext.simplifyBvToFpExpr(sort: T, roundingMode: KExpr<KFpRoundingModeSort>, value: KExpr<KBvSort>, signed: Boolean): KExpr<T>

simplifyBvToFpExprLight

inline fun <T : KFpSort> KContext.simplifyBvToFpExprLight(sort: T, roundingMode: KExpr<KFpRoundingModeSort>, value: KExpr<KBvSort>, signed: Boolean, cont: (T, KExpr<KFpRoundingModeSort>, KExpr<KBvSort>, Boolean) -> KExpr<T>): KExpr<T>

simplifyBvUnsignedDivExpr

fun <T : KBvSort> KContext.simplifyBvUnsignedDivExpr(lhs: KExpr<T>, rhs: KExpr<T>): KExpr<T>

simplifyBvUnsignedDivExprLight

inline fun <T : KBvSort> KContext.simplifyBvUnsignedDivExprLight(lhs: KExpr<T>, rhs: KExpr<T>, cont: (KExpr<T>, KExpr<T>) -> KExpr<T>): KExpr<T>

simplifyBvUnsignedDivExprPowerOfTwoDivisor

inline fun <T : KBvSort> KContext.simplifyBvUnsignedDivExprPowerOfTwoDivisor(lhs: KExpr<T>, rhs: KExpr<T>, rewriteBvLogicalShiftRightExpr: KContext.(KExpr<T>, KExpr<T>) -> KExpr<T>, cont: (KExpr<T>, KExpr<T>) -> KExpr<T>): KExpr<T>

(udiv a x), x == 2^n ==> (lshr a n)

simplifyBvUnsignedGreaterExpr

fun <T : KBvSort> KContext.simplifyBvUnsignedGreaterExpr(lhs: KExpr<T>, rhs: KExpr<T>): KExpr<KBoolSort>

simplifyBvUnsignedGreaterOrEqualExpr

fun <T : KBvSort> KContext.simplifyBvUnsignedGreaterOrEqualExpr(lhs: KExpr<T>, rhs: KExpr<T>): KExpr<KBoolSort>

simplifyBvUnsignedLessExpr

fun <T : KBvSort> KContext.simplifyBvUnsignedLessExpr(lhs: KExpr<T>, rhs: KExpr<T>): KExpr<KBoolSort>

simplifyBvUnsignedLessOrEqualExpr

fun <T : KBvSort> KContext.simplifyBvUnsignedLessOrEqualExpr(lhs: KExpr<T>, rhs: KExpr<T>): KExpr<KBoolSort>

simplifyBvUnsignedRemExpr

fun <T : KBvSort> KContext.simplifyBvUnsignedRemExpr(lhs: KExpr<T>, rhs: KExpr<T>): KExpr<T>

simplifyBvUnsignedRemExprLight

inline fun <T : KBvSort> KContext.simplifyBvUnsignedRemExprLight(lhs: KExpr<T>, rhs: KExpr<T>, cont: (KExpr<T>, KExpr<T>) -> KExpr<T>): KExpr<T>

simplifyBvUnsignedRemExprPowerOfTwoDivisor

inline fun <T : KBvSort> KContext.simplifyBvUnsignedRemExprPowerOfTwoDivisor(lhs: KExpr<T>, rhs: KExpr<T>, rewriteBvExtractExpr: KContext.(Int, Int, KExpr<T>) -> KExpr<KBvSort>, rewriteBvZeroExtensionExpr: KContext.(Int, KExpr<T>) -> KExpr<KBvSort>, cont: (KExpr<T>, KExpr<T>) -> KExpr<T>): KExpr<T>

(urem a x), x == 2^n ==> (concat 0 (extract n-1:0 a))

simplifyBvXNorExpr

fun <T : KBvSort> KContext.simplifyBvXNorExpr(lhs: KExpr<T>, rhs: KExpr<T>): KExpr<T>

simplifyBvXorExpr

fun <T : KBvSort> KContext.simplifyBvXorExpr(lhs: KExpr<T>, rhs: KExpr<T>): KExpr<T>

simplifyBvXorExprLight

inline fun <T : KBvSort> KContext.simplifyBvXorExprLight(lhs: KExpr<T>, rhs: KExpr<T>, cont: (KExpr<T>, KExpr<T>) -> KExpr<T>): KExpr<T>

simplifyBvXorExprMaxConst

inline fun <T : KBvSort> KContext.simplifyBvXorExprMaxConst(lhs: KExpr<T>, rhs: KExpr<T>, rewriteBvNotExpr: KContext.(KExpr<T>) -> KExpr<T>, cont: (KExpr<T>, KExpr<T>) -> KExpr<T>): KExpr<T>

(bvxor 0xFFFF... a) ==> (bvnot a)

simplifyBvXorExprNestedXor

inline fun <T : KBvSort> KContext.simplifyBvXorExprNestedXor(lhs: KExpr<T>, rhs: KExpr<T>, rewriteBvXorExpr: KContext.(KExpr<T>, KExpr<T>) -> KExpr<T>, cont: (KExpr<T>, KExpr<T>) -> KExpr<T>): KExpr<T>

(bvxor const1 (bvxor const2 x)) ==> (bvxor (bvxor const1 const2) x)

simplifyBvZeroExtensionExpr

fun <T : KBvSort> KContext.simplifyBvZeroExtensionExpr(extensionSize: Int, value: KExpr<T>): KExpr<KBvSort>

simplifyBvZeroExtensionExprLight

inline fun <T : KBvSort> KContext.simplifyBvZeroExtensionExprLight(extensionSize: Int, value: KExpr<T>, cont: (Int, KExpr<T>) -> KExpr<KBvSort>): KExpr<KBvSort>

simplifyDistinct

fun <T : KSort> KContext.simplifyDistinct(args: List<KExpr<T>>, order: Boolean = true): KExpr<KBoolSort>

simplifyDistinctLight

inline fun <T : KSort> KContext.simplifyDistinctLight(args: List<KExpr<T>>, rewriteNot: KContext.(KExpr<KBoolSort>) -> KExpr<KBoolSort>, rewriteEq: KContext.(KExpr<T>, KExpr<T>) -> KExpr<KBoolSort>, cont: (List<KExpr<T>>) -> KExpr<KBoolSort>): KExpr<KBoolSort>

simplifyEq

fun <T : KSort> KContext.simplifyEq(lhs: KExpr<T>, rhs: KExpr<T>, order: Boolean = true): KExpr<KBoolSort>

simplifyEqBool

fun KContext.simplifyEqBool(lhs: KExpr<KBoolSort>, rhs: KExpr<KBoolSort>, order: Boolean = true): KExpr<KBoolSort>

inline fun <T : KSort> KContext.simplifyEqBool(lhs: KExpr<T>, rhs: KExpr<T>, rewriteEqBool: KContext.(KExpr<KBoolSort>, KExpr<KBoolSort>) -> KExpr<KBoolSort>, cont: (KExpr<T>, KExpr<T>) -> KExpr<KBoolSort>): KExpr<KBoolSort>

simplifyEqBoolLight

inline fun KContext.simplifyEqBoolLight(lhs: KExpr<KBoolSort>, rhs: KExpr<KBoolSort>, rewriteNot: KContext.(KExpr<KBoolSort>) -> KExpr<KBoolSort>, cont: (KExpr<KBoolSort>, KExpr<KBoolSort>) -> KExpr<KBoolSort>): KExpr<KBoolSort>

simplifyEqBoolNot

inline fun KContext.simplifyEqBoolNot(lhs: KExpr<KBoolSort>, rhs: KExpr<KBoolSort>, rewriteEq: KContext.(KExpr<KBoolSort>, KExpr<KBoolSort>) -> KExpr<KBoolSort>, cont: (KExpr<KBoolSort>, KExpr<KBoolSort>) -> KExpr<KBoolSort>): KExpr<KBoolSort>

(= (not a) (not b)) ==> (= a b)

simplifyEqBvConcat

inline fun <T : KBvSort> KContext.simplifyEqBvConcat(lhs: KExpr<T>, rhs: KExpr<T>, crossinline rewriteBvExtractExpr: KContext.(Int, Int, KExpr<KBvSort>) -> KExpr<KBvSort>, crossinline rewriteBvEq: KContext.(KExpr<KBvSort>, KExpr<KBvSort>) -> KExpr<KBoolSort>, crossinline rewriteFlatAnd: KContext.(List<KExpr<KBoolSort>>) -> KExpr<KBoolSort>, cont: (KExpr<T>, KExpr<T>) -> KExpr<KBoolSort>): KExpr<KBoolSort>

simplifyEqBvLight

inline fun <T : KBvSort> KContext.simplifyEqBvLight(lhs: KExpr<T>, rhs: KExpr<T>, cont: (KExpr<T>, KExpr<T>) -> KExpr<KBoolSort>): KExpr<KBoolSort>

simplifyEqFpLight

inline fun <T : KFpSort> KContext.simplifyEqFpLight(lhs: KExpr<T>, rhs: KExpr<T>, cont: (KExpr<T>, KExpr<T>) -> KExpr<KBoolSort>): KExpr<KBoolSort>

simplifyEqIntLight

inline fun KContext.simplifyEqIntLight(lhs: KExpr<KIntSort>, rhs: KExpr<KIntSort>, cont: (KExpr<KIntSort>, KExpr<KIntSort>) -> KExpr<KBoolSort>): KExpr<KBoolSort>

simplifyEqLight

inline fun <T : KSort> KContext.simplifyEqLight(lhs: KExpr<T>, rhs: KExpr<T>, cont: (KExpr<T>, KExpr<T>) -> KExpr<KBoolSort>): KExpr<KBoolSort>

simplifyEqRealLight

inline fun KContext.simplifyEqRealLight(lhs: KExpr<KRealSort>, rhs: KExpr<KRealSort>, cont: (KExpr<KRealSort>, KExpr<KRealSort>) -> KExpr<KBoolSort>): KExpr<KBoolSort>

simplifyExpr

inline fun <T : KSort, P : KExpr<T>> KExprSimplifierBase.simplifyExpr(expr: P, preprocess: KContext.(P) -> KExpr<T>): KExpr<T>

Specialized version of simplifyExpr for expressions which are always rewritten with another expression on the preprocess stage.

inline fun <T : KSort, P : KExpr<T>, A0 : KSort> KExprSimplifierBase.simplifyExpr(expr: P, a0: KExpr<A0>, preprocess: KContext.(P) -> KExpr<T> = { expr }, crossinline simplifier: KContext.(KExpr<A0>) -> KExpr<T>): KExpr<T>

Specialized version of simplifyExpr for expressions with a single argument.

inline fun <T : KSort, P : KExpr<T>, A : KSort> KExprSimplifierBase.simplifyExpr(expr: P, args: List<KExpr<A>>, preprocess: KContext.(P) -> KExpr<T> = { expr }, crossinline simplifier: KContext.(List<KExpr<A>>) -> KExpr<T>): KExpr<T>

Simplify an expression. preprocess Rewrite an expression before simplification of an args (top-down). simplifier Rewrite an expression after args simplification (bottom-up).

inline fun <T : KSort, P : KExpr<T>, A0 : KSort, A1 : KSort> KExprSimplifierBase.simplifyExpr(expr: P, a0: KExpr<A0>, a1: KExpr<A1>, preprocess: KContext.(P) -> KExpr<T> = { expr }, crossinline simplifier: KContext.(KExpr<A0>, KExpr<A1>) -> KExpr<T>): KExpr<T>

Specialized version of simplifyExpr for expressions with two arguments.

inline fun <T : KSort, P : KExpr<T>, A0 : KSort, A1 : KSort, A2 : KSort> KExprSimplifierBase.simplifyExpr(expr: P, a0: KExpr<A0>, a1: KExpr<A1>, a2: KExpr<A2>, preprocess: KContext.(P) -> KExpr<T> = { expr }, crossinline simplifier: KContext.(KExpr<A0>, KExpr<A1>, KExpr<A2>) -> KExpr<T>): KExpr<T>

Specialized version of simplifyExpr for expressions with three arguments.

inline fun <T : KSort, P : KExpr<T>, A0 : KSort, A1 : KSort, A2 : KSort, A3 : KSort> KExprSimplifierBase.simplifyExpr(expr: P, a0: KExpr<A0>, a1: KExpr<A1>, a2: KExpr<A2>, a3: KExpr<A3>, preprocess: KContext.(P) -> KExpr<T> = { expr }, crossinline simplifier: KContext.(KExpr<A0>, KExpr<A1>, KExpr<A2>, KExpr<A3>) -> KExpr<T>): KExpr<T>

Specialized version of simplifyExpr for expressions with four arguments.

inline fun <T : KSort, P : KExpr<T>, A0 : KSort, A1 : KSort, A2 : KSort, A3 : KSort, A4 : KSort> KExprSimplifierBase.simplifyExpr(expr: P, a0: KExpr<A0>, a1: KExpr<A1>, a2: KExpr<A2>, a3: KExpr<A3>, a4: KExpr<A4>, preprocess: KContext.(P) -> KExpr<T> = { expr }, crossinline simplifier: KContext.(KExpr<A0>, KExpr<A1>, KExpr<A2>, KExpr<A3>, KExpr<A4>) -> KExpr<T>): KExpr<T>

Specialized version of simplifyExpr for expressions with five arguments.

simplifyExprBase

inline fun <T : KSort> KExprSimplifierBase.simplifyExprBase(expr: KExpr<T>, preprocess: KExprSimplifier.() -> KExpr<T>, simplify: KExprSimplifier.() -> KExpr<T>): KExpr<T>

Simplify an expression.

simplifyFlatBvAddExpr

inline fun <T : KBvSort> KContext.simplifyFlatBvAddExpr(args: List<KExpr<T>>, cont: (List<KExpr<T>>) -> KExpr<T>): KExpr<T>

simplifyFlatBvAndExpr

inline fun <T : KBvSort> KContext.simplifyFlatBvAndExpr(args: List<KExpr<T>>, cont: (List<KExpr<T>>) -> KExpr<T>): KExpr<T>

simplifyFlatBvAndExprDistributeOverConcat

inline fun <T : KBvSort> KContext.simplifyFlatBvAndExprDistributeOverConcat(args: List<KExpr<T>>, rewriteBvExtractExpr: KContext.(Int, Int, KExpr<KBvSort>) -> KExpr<KBvSort>, rewriteFlatBvAndExpr: KContext.(List<KExpr<KBvSort>>) -> KExpr<KBvSort>, rewriteBvConcatExpr: KContext.(KExpr<KBvSort>, KExpr<KBvSort>) -> KExpr<KBvSort>, cont: (List<KExpr<T>>) -> KExpr<T>): KExpr<T>

(bvand (concat a b) c) ==> (concat (bvand (extract (0, ) c)) (bvand b (extract (, + ) c)) )

simplifyFlatBvConcatExpr

inline fun KContext.simplifyFlatBvConcatExpr(args: List<KExpr<KBvSort>>, rewriteBvExtractExpr: KContext.(Int, Int, KExpr<KBvSort>) -> KExpr<KBvSort>, rewriteFlatBvConcatExpr: KContext.(List<KExpr<KBvSort>>) -> KExpr<KBvSort>, cont: (List<KExpr<KBvSort>>) -> KExpr<KBvSort>): KExpr<KBvSort>

simplifyFlatBvMulExpr

inline fun <T : KBvSort> KContext.simplifyFlatBvMulExpr(args: List<KExpr<T>>, cont: (negateResult: Boolean, List<KExpr<T>>) -> KExpr<T>): KExpr<T>

simplifyFlatBvOrExpr

inline fun <T : KBvSort> KContext.simplifyFlatBvOrExpr(args: List<KExpr<T>>, cont: (List<KExpr<T>>) -> KExpr<T>): KExpr<T>

simplifyFlatBvOrExprDistributeOverConcat

inline fun <T : KBvSort> KContext.simplifyFlatBvOrExprDistributeOverConcat(args: List<KExpr<T>>, rewriteBvExtractExpr: KContext.(Int, Int, KExpr<KBvSort>) -> KExpr<KBvSort>, rewriteFlatBvOrExpr: KContext.(List<KExpr<KBvSort>>) -> KExpr<KBvSort>, rewriteBvConcatExpr: KContext.(KExpr<KBvSort>, KExpr<KBvSort>) -> KExpr<KBvSort>, cont: (List<KExpr<T>>) -> KExpr<T>): KExpr<T>

(bvor (concat a b) c) ==> (concat (bvor (extract (0, ) c)) (bvor b (extract (, + ) c)) )

simplifyFlatBvXorExpr

inline fun <T : KBvSort> KContext.simplifyFlatBvXorExpr(args: List<KExpr<T>>, cont: (Boolean, List<KExpr<T>>) -> KExpr<T>): KExpr<T>

simplifyFlatBvXorExprDistributeOverConcat

inline fun <T : KBvSort> KContext.simplifyFlatBvXorExprDistributeOverConcat(args: List<KExpr<T>>, rewriteBvExtractExpr: KContext.(Int, Int, KExpr<KBvSort>) -> KExpr<KBvSort>, rewriteFlatBvXorExpr: KContext.(List<KExpr<KBvSort>>) -> KExpr<KBvSort>, rewriteBvConcatExpr: KContext.(KExpr<KBvSort>, KExpr<KBvSort>) -> KExpr<KBvSort>, cont: (List<KExpr<T>>) -> KExpr<T>): KExpr<T>

(bvxor (concat a b) c) ==> (concat (bvxor (extract (0, ) c)) (bvxor b (extract (, + ) c)) )

simplifyFpAbsExpr

fun <T : KFpSort> KContext.simplifyFpAbsExpr(value: KExpr<T>): KExpr<T>

simplifyFpAbsExprLight

inline fun <T : KFpSort> KContext.simplifyFpAbsExprLight(value: KExpr<T>, cont: (KExpr<T>) -> KExpr<T>): KExpr<T>

simplifyFpAddExpr

fun <T : KFpSort> KContext.simplifyFpAddExpr(roundingMode: KExpr<KFpRoundingModeSort>, lhs: KExpr<T>, rhs: KExpr<T>): KExpr<T>

simplifyFpAddExprLight

inline fun <T : KFpSort> KContext.simplifyFpAddExprLight(roundingMode: KExpr<KFpRoundingModeSort>, lhs: KExpr<T>, rhs: KExpr<T>, cont: (KExpr<KFpRoundingModeSort>, KExpr<T>, KExpr<T>) -> KExpr<T>): KExpr<T>

simplifyFpDivExpr

fun <T : KFpSort> KContext.simplifyFpDivExpr(roundingMode: KExpr<KFpRoundingModeSort>, lhs: KExpr<T>, rhs: KExpr<T>): KExpr<T>

simplifyFpDivExprLight

inline fun <T : KFpSort> KContext.simplifyFpDivExprLight(roundingMode: KExpr<KFpRoundingModeSort>, lhs: KExpr<T>, rhs: KExpr<T>, cont: (KExpr<KFpRoundingModeSort>, KExpr<T>, KExpr<T>) -> KExpr<T>): KExpr<T>

simplifyFpEqualExpr

fun <T : KFpSort> KContext.simplifyFpEqualExpr(lhs: KExpr<T>, rhs: KExpr<T>): KExpr<KBoolSort>

simplifyFpEqualExprLight

inline fun <T : KFpSort> KContext.simplifyFpEqualExprLight(lhs: KExpr<T>, rhs: KExpr<T>, cont: (KExpr<T>, KExpr<T>) -> KExpr<KBoolSort>): KExpr<KBoolSort>

simplifyFpFromBvExpr

fun <T : KFpSort> KContext.simplifyFpFromBvExpr(sign: KExpr<KBv1Sort>, biasedExponent: KExpr<out KBvSort>, significand: KExpr<out KBvSort>): KExpr<T>

simplifyFpFromBvExprLight

inline fun <T : KFpSort> KContext.simplifyFpFromBvExprLight(sign: KExpr<KBv1Sort>, biasedExponent: KExpr<out KBvSort>, significand: KExpr<out KBvSort>, cont: (KExpr<KBv1Sort>, KExpr<out KBvSort>, KExpr<out KBvSort>) -> KExpr<T>): KExpr<T>

simplifyFpFusedMulAddExpr

fun <T : KFpSort> KContext.simplifyFpFusedMulAddExpr(roundingMode: KExpr<KFpRoundingModeSort>, arg0: KExpr<T>, arg1: KExpr<T>, arg2: KExpr<T>): KExpr<T>

simplifyFpFusedMulAddExprLight

inline fun <T : KFpSort> KContext.simplifyFpFusedMulAddExprLight(roundingMode: KExpr<KFpRoundingModeSort>, arg0: KExpr<T>, arg1: KExpr<T>, arg2: KExpr<T>, cont: (KExpr<KFpRoundingModeSort>, KExpr<T>, KExpr<T>, KExpr<T>) -> KExpr<T>): KExpr<T>

simplifyFpGreaterExpr

fun <T : KFpSort> KContext.simplifyFpGreaterExpr(lhs: KExpr<T>, rhs: KExpr<T>): KExpr<KBoolSort>

simplifyFpGreaterOrEqualExpr

fun <T : KFpSort> KContext.simplifyFpGreaterOrEqualExpr(lhs: KExpr<T>, rhs: KExpr<T>): KExpr<KBoolSort>

simplifyFpIsInfiniteExpr

fun <T : KFpSort> KContext.simplifyFpIsInfiniteExpr(arg: KExpr<T>): KExpr<KBoolSort>

simplifyFpIsInfiniteExprLight

inline fun <T : KFpSort> KContext.simplifyFpIsInfiniteExprLight(arg: KExpr<T>, cont: (KExpr<T>) -> KExpr<KBoolSort>): KExpr<KBoolSort>

simplifyFpIsNaNExpr

fun <T : KFpSort> KContext.simplifyFpIsNaNExpr(arg: KExpr<T>): KExpr<KBoolSort>

simplifyFpIsNaNExprLight

inline fun <T : KFpSort> KContext.simplifyFpIsNaNExprLight(arg: KExpr<T>, cont: (KExpr<T>) -> KExpr<KBoolSort>): KExpr<KBoolSort>

simplifyFpIsNegativeExpr

fun <T : KFpSort> KContext.simplifyFpIsNegativeExpr(arg: KExpr<T>): KExpr<KBoolSort>

simplifyFpIsNegativeExprLight

inline fun <T : KFpSort> KContext.simplifyFpIsNegativeExprLight(arg: KExpr<T>, cont: (KExpr<T>) -> KExpr<KBoolSort>): KExpr<KBoolSort>

simplifyFpIsNormalExpr

fun <T : KFpSort> KContext.simplifyFpIsNormalExpr(arg: KExpr<T>): KExpr<KBoolSort>

simplifyFpIsNormalExprLight

inline fun <T : KFpSort> KContext.simplifyFpIsNormalExprLight(arg: KExpr<T>, cont: (KExpr<T>) -> KExpr<KBoolSort>): KExpr<KBoolSort>

simplifyFpIsPositiveExpr

fun <T : KFpSort> KContext.simplifyFpIsPositiveExpr(arg: KExpr<T>): KExpr<KBoolSort>

simplifyFpIsPositiveExprLight

inline fun <T : KFpSort> KContext.simplifyFpIsPositiveExprLight(arg: KExpr<T>, cont: (KExpr<T>) -> KExpr<KBoolSort>): KExpr<KBoolSort>

simplifyFpIsSubnormalExpr

fun <T : KFpSort> KContext.simplifyFpIsSubnormalExpr(arg: KExpr<T>): KExpr<KBoolSort>

simplifyFpIsSubnormalExprLight

inline fun <T : KFpSort> KContext.simplifyFpIsSubnormalExprLight(arg: KExpr<T>, cont: (KExpr<T>) -> KExpr<KBoolSort>): KExpr<KBoolSort>

simplifyFpIsZeroExpr

fun <T : KFpSort> KContext.simplifyFpIsZeroExpr(arg: KExpr<T>): KExpr<KBoolSort>

simplifyFpIsZeroExprLight

inline fun <T : KFpSort> KContext.simplifyFpIsZeroExprLight(arg: KExpr<T>, cont: (KExpr<T>) -> KExpr<KBoolSort>): KExpr<KBoolSort>

simplifyFpLessExpr

fun <T : KFpSort> KContext.simplifyFpLessExpr(lhs: KExpr<T>, rhs: KExpr<T>): KExpr<KBoolSort>

simplifyFpLessExprLight

inline fun <T : KFpSort> KContext.simplifyFpLessExprLight(lhs: KExpr<T>, rhs: KExpr<T>, cont: (KExpr<T>, KExpr<T>) -> KExpr<KBoolSort>): KExpr<KBoolSort>

simplifyFpLessOrEqualExpr

fun <T : KFpSort> KContext.simplifyFpLessOrEqualExpr(lhs: KExpr<T>, rhs: KExpr<T>): KExpr<KBoolSort>

simplifyFpLessOrEqualExprLight

inline fun <T : KFpSort> KContext.simplifyFpLessOrEqualExprLight(lhs: KExpr<T>, rhs: KExpr<T>, cont: (KExpr<T>, KExpr<T>) -> KExpr<KBoolSort>): KExpr<KBoolSort>

simplifyFpMaxExpr

fun <T : KFpSort> KContext.simplifyFpMaxExpr(lhs: KExpr<T>, rhs: KExpr<T>): KExpr<T>

simplifyFpMaxExprLight

inline fun <T : KFpSort> KContext.simplifyFpMaxExprLight(lhs: KExpr<T>, rhs: KExpr<T>, cont: (KExpr<T>, KExpr<T>) -> KExpr<T>): KExpr<T>

simplifyFpMinExpr

fun <T : KFpSort> KContext.simplifyFpMinExpr(lhs: KExpr<T>, rhs: KExpr<T>): KExpr<T>

simplifyFpMinExprLight

inline fun <T : KFpSort> KContext.simplifyFpMinExprLight(lhs: KExpr<T>, rhs: KExpr<T>, cont: (KExpr<T>, KExpr<T>) -> KExpr<T>): KExpr<T>

simplifyFpMulExpr

fun <T : KFpSort> KContext.simplifyFpMulExpr(roundingMode: KExpr<KFpRoundingModeSort>, lhs: KExpr<T>, rhs: KExpr<T>): KExpr<T>

simplifyFpMulExprLight

inline fun <T : KFpSort> KContext.simplifyFpMulExprLight(roundingMode: KExpr<KFpRoundingModeSort>, lhs: KExpr<T>, rhs: KExpr<T>, cont: (KExpr<KFpRoundingModeSort>, KExpr<T>, KExpr<T>) -> KExpr<T>): KExpr<T>

simplifyFpNegationExpr

fun <T : KFpSort> KContext.simplifyFpNegationExpr(value: KExpr<T>): KExpr<T>

simplifyFpNegationExprLight

inline fun <T : KFpSort> KContext.simplifyFpNegationExprLight(value: KExpr<T>, cont: (KExpr<T>) -> KExpr<T>): KExpr<T>

simplifyFpRemExpr

fun <T : KFpSort> KContext.simplifyFpRemExpr(lhs: KExpr<T>, rhs: KExpr<T>): KExpr<T>

simplifyFpRemExprLight

inline fun <T : KFpSort> KContext.simplifyFpRemExprLight(lhs: KExpr<T>, rhs: KExpr<T>, cont: (KExpr<T>, KExpr<T>) -> KExpr<T>): KExpr<T>

simplifyFpRoundToIntegralExpr

fun <T : KFpSort> KContext.simplifyFpRoundToIntegralExpr(roundingMode: KExpr<KFpRoundingModeSort>, value: KExpr<T>): KExpr<T>

simplifyFpRoundToIntegralExprLight

inline fun <T : KFpSort> KContext.simplifyFpRoundToIntegralExprLight(roundingMode: KExpr<KFpRoundingModeSort>, value: KExpr<T>, cont: (KExpr<KFpRoundingModeSort>, KExpr<T>) -> KExpr<T>): KExpr<T>

simplifyFpSqrtExpr

fun <T : KFpSort> KContext.simplifyFpSqrtExpr(roundingMode: KExpr<KFpRoundingModeSort>, value: KExpr<T>): KExpr<T>

simplifyFpSqrtExprLight

inline fun <T : KFpSort> KContext.simplifyFpSqrtExprLight(roundingMode: KExpr<KFpRoundingModeSort>, value: KExpr<T>, cont: (KExpr<KFpRoundingModeSort>, KExpr<T>) -> KExpr<T>): KExpr<T>

simplifyFpSubExpr

fun <T : KFpSort> KContext.simplifyFpSubExpr(roundingMode: KExpr<KFpRoundingModeSort>, lhs: KExpr<T>, rhs: KExpr<T>): KExpr<T>

simplifyFpToBvExpr

fun <T : KFpSort> KContext.simplifyFpToBvExpr(roundingMode: KExpr<KFpRoundingModeSort>, value: KExpr<T>, bvSize: Int, isSigned: Boolean): KExpr<KBvSort>

simplifyFpToBvExprLight

inline fun <T : KFpSort> KContext.simplifyFpToBvExprLight(roundingMode: KExpr<KFpRoundingModeSort>, value: KExpr<T>, bvSize: Int, isSigned: Boolean, cont: (KExpr<KFpRoundingModeSort>, KExpr<T>, Int, Boolean) -> KExpr<KBvSort>): KExpr<KBvSort>

simplifyFpToFpExpr

fun <T : KFpSort> KContext.simplifyFpToFpExpr(sort: T, roundingMode: KExpr<KFpRoundingModeSort>, value: KExpr<out KFpSort>): KExpr<T>

simplifyFpToFpExprLight

inline fun <T : KFpSort> KContext.simplifyFpToFpExprLight(sort: T, roundingMode: KExpr<KFpRoundingModeSort>, value: KExpr<out KFpSort>, cont: (T, KExpr<KFpRoundingModeSort>, KExpr<out KFpSort>) -> KExpr<T>): KExpr<T>

simplifyFpToIEEEBvExpr

fun <T : KFpSort> KContext.simplifyFpToIEEEBvExpr(arg: KExpr<T>): KExpr<KBvSort>

simplifyFpToIEEEBvExprLight

inline fun <T : KFpSort> KContext.simplifyFpToIEEEBvExprLight(arg: KExpr<T>, cont: (KExpr<T>) -> KExpr<KBvSort>): KExpr<KBvSort>

simplifyFpToRealExpr

fun <T : KFpSort> KContext.simplifyFpToRealExpr(arg: KExpr<T>): KExpr<KRealSort>

simplifyFpToRealExprLight

inline fun <T : KFpSort> KContext.simplifyFpToRealExprLight(arg: KExpr<T>, cont: (KExpr<T>) -> KExpr<KRealSort>): KExpr<KRealSort>

simplifyImplies

fun KContext.simplifyImplies(p: KExpr<KBoolSort>, q: KExpr<KBoolSort>): KExpr<KBoolSort>

simplifyIntMod

fun KContext.simplifyIntMod(lhs: KExpr<KIntSort>, rhs: KExpr<KIntSort>): KExpr<KIntSort>

simplifyIntModLight

inline fun KContext.simplifyIntModLight(lhs: KExpr<KIntSort>, rhs: KExpr<KIntSort>, cont: (KExpr<KIntSort>, KExpr<KIntSort>) -> KExpr<KIntSort>): KExpr<KIntSort>

simplifyIntRem

fun KContext.simplifyIntRem(lhs: KExpr<KIntSort>, rhs: KExpr<KIntSort>): KExpr<KIntSort>

simplifyIntRemLight

inline fun KContext.simplifyIntRemLight(lhs: KExpr<KIntSort>, rhs: KExpr<KIntSort>, cont: (KExpr<KIntSort>, KExpr<KIntSort>) -> KExpr<KIntSort>): KExpr<KIntSort>

simplifyIntToReal

fun KContext.simplifyIntToReal(arg: KExpr<KIntSort>): KExpr<KRealSort>

simplifyIntToRealLight

inline fun KContext.simplifyIntToRealLight(arg: KExpr<KIntSort>, cont: (KExpr<KIntSort>) -> KExpr<KRealSort>): KExpr<KRealSort>

simplifyIte

fun <T : KSort> KContext.simplifyIte(condition: KExpr<KBoolSort>, trueBranch: KExpr<T>, falseBranch: KExpr<T>): KExpr<T>

simplifyIteBool

inline fun <T : KSort> KContext.simplifyIteBool(condition: KExpr<KBoolSort>, trueBranch: KExpr<T>, falseBranch: KExpr<T>, rewriteBoolIte: KContext.(KExpr<KBoolSort>, KExpr<KBoolSort>, KExpr<KBoolSort>) -> KExpr<KBoolSort>, cont: (KExpr<KBoolSort>, KExpr<T>, KExpr<T>) -> KExpr<T>): KExpr<T>

simplifyIteLight

inline fun <T : KSort> KContext.simplifyIteLight(condition: KExpr<KBoolSort>, trueBranch: KExpr<T>, falseBranch: KExpr<T>, cont: (KExpr<KBoolSort>, KExpr<T>, KExpr<T>) -> KExpr<T>): KExpr<T>

simplifyIteNotCondition

inline fun <T : KSort> KContext.simplifyIteNotCondition(condition: KExpr<KBoolSort>, trueBranch: KExpr<T>, falseBranch: KExpr<T>, cont: (KExpr<KBoolSort>, KExpr<T>, KExpr<T>) -> KExpr<T>): KExpr<T>

(ite (not c) a b) ==> (ite c b a)

simplifyIteSameBranches

inline fun <T : KSort> KContext.simplifyIteSameBranches(condition: KExpr<KBoolSort>, trueBranch: KExpr<T>, falseBranch: KExpr<T>, rewriteIte: KContext.(KExpr<KBoolSort>, KExpr<T>, KExpr<T>) -> KExpr<T>, rewriteOr: KContext.(KExpr<KBoolSort>, KExpr<KBoolSort>) -> KExpr<KBoolSort>, cont: (KExpr<KBoolSort>, KExpr<T>, KExpr<T>) -> KExpr<T>): KExpr<T>

(ite c t1 (ite c2 t1 t2)) ==> (ite (or c c2) t1 t2)

simplifyNot

fun KContext.simplifyNot(arg: KExpr<KBoolSort>): KExpr<KBoolSort>

simplifyNotLight

inline fun KContext.simplifyNotLight(arg: KExpr<KBoolSort>, cont: (KExpr<KBoolSort>) -> KExpr<KBoolSort>): KExpr<KBoolSort>

simplifyOr

fun KContext.simplifyOr(args: List<KExpr<KBoolSort>>, flat: Boolean = true, order: Boolean = true): KExpr<KBoolSort>

fun KContext.simplifyOr(lhs: KExpr<KBoolSort>, rhs: KExpr<KBoolSort>, flat: Boolean = true, order: Boolean = true): KExpr<KBoolSort>

simplifyRealIsInt

fun KContext.simplifyRealIsInt(arg: KExpr<KRealSort>): KExpr<KBoolSort>

simplifyRealIsIntLight

inline fun KContext.simplifyRealIsIntLight(arg: KExpr<KRealSort>, cont: (KExpr<KRealSort>) -> KExpr<KBoolSort>): KExpr<KBoolSort>

simplifyRealToFpExpr

fun <T : KFpSort> KContext.simplifyRealToFpExpr(sort: T, roundingMode: KExpr<KFpRoundingModeSort>, value: KExpr<KRealSort>): KExpr<T>

simplifyRealToFpExprLight

inline fun <T : KFpSort> KContext.simplifyRealToFpExprLight(sort: T, roundingMode: KExpr<KFpRoundingModeSort>, value: KExpr<KRealSort>, cont: (T, KExpr<KFpRoundingModeSort>, KExpr<KRealSort>) -> KExpr<T>): KExpr<T>

simplifyRealToInt

fun KContext.simplifyRealToInt(arg: KExpr<KRealSort>): KExpr<KIntSort>

simplifyRealToIntLight

inline fun KContext.simplifyRealToIntLight(arg: KExpr<KRealSort>, cont: (KExpr<KRealSort>) -> KExpr<KIntSort>): KExpr<KIntSort>

simplifySelectFromArrayStore

inline fun <A : KArraySortBase<R>, R : KSort, S : KArrayStoreBase<A, R>> KContext.simplifySelectFromArrayStore(initialArray: KExpr<A>, storeIndicesMatch: (S) -> Boolean, storeIndicesDistinct: (S) -> Boolean, findArrayToSelectFrom: (S) -> KExpr<A>, default: (KExpr<A>) -> KExpr<R>): KExpr<R>

Simplify select from a chain of array store expressions.

inline fun <D : KSort, R : KSort> KContext.simplifySelectFromArrayStore(array: KExpr<KArraySort<D, R>>, index: KExpr<D>, storeIndexMatch: KContext.(KArrayStore<D, R>, KExpr<D>) -> Boolean, storeIndexDistinct: KContext.(KArrayStore<D, R>, KExpr<D>) -> Boolean, cont: (KExpr<KArraySort<D, R>>, KExpr<D>) -> KExpr<R>): KExpr<R>

inline fun <D0 : KSort, D1 : KSort, R : KSort> KContext.simplifySelectFromArrayStore(array: KExpr<KArray2Sort<D0, D1, R>>, index0: KExpr<D0>, index1: KExpr<D1>, storeIndexMatch: KContext.(KArray2Store<D0, D1, R>, KExpr<D0>, KExpr<D1>) -> Boolean, storeIndexDistinct: KContext.(KArray2Store<D0, D1, R>, KExpr<D0>, KExpr<D1>) -> Boolean, cont: (KExpr<KArray2Sort<D0, D1, R>>, KExpr<D0>, KExpr<D1>) -> KExpr<R>): KExpr<R>

inline fun <D0 : KSort, D1 : KSort, D2 : KSort, R : KSort> KContext.simplifySelectFromArrayStore(array: KExpr<KArray3Sort<D0, D1, D2, R>>, index0: KExpr<D0>, index1: KExpr<D1>, index2: KExpr<D2>, storeIndexMatch: KContext.(KArray3Store<D0, D1, D2, R>, KExpr<D0>, KExpr<D1>, KExpr<D2>) -> Boolean, storeIndexDistinct: KContext.(KArray3Store<D0, D1, D2, R>, KExpr<D0>, KExpr<D1>, KExpr<D2>) -> Boolean, cont: (KExpr<KArray3Sort<D0, D1, D2, R>>, KExpr<D0>, KExpr<D1>, KExpr<D2>) -> KExpr<R>): KExpr<R>

simplifyXor

fun KContext.simplifyXor(a: KExpr<KBoolSort>, b: KExpr<KBoolSort>): KExpr<KBoolSort>

toRealValue

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

tryEvalArithPower

fun tryEvalArithPower(base: ArithUtils.RealValue, power: ArithUtils.RealValue): ArithUtils.RealValue?

tryMergeBvConcatExtract

inline fun KContext.tryMergeBvConcatExtract(lhs: KBvExtractExpr, rhs: KBvExtractExpr, rewriteBvExtractExpr: KContext.(Int, Int, KExpr<KBvSort>) -> KExpr<KBvSort>): KExpr<KBvSort>?

trySimplifyAndOrElement

fun trySimplifyAndOrElement(arg: KExpr<KBoolSort>, neutralElement: KExpr<KBoolSort>, zeroElement: KExpr<KBoolSort>, posLiterals: MutableSet<KExpr<KBoolSort>>, negLiterals: MutableSet<KExpr<KBoolSort>>, resultElements: MutableList<KExpr<KBoolSort>>): KExpr<KBoolSort>?

trySimplifyBvSignedMulNoOverflow

fun <T : KBvSort> KContext.trySimplifyBvSignedMulNoOverflow(lhs: KExpr<T>, rhs: KExpr<T>, isOverflow: Boolean): KExpr<KBoolSort>?

trySimplifyBvUnsignedMulNoOverflow

fun <T : KBvSort> KContext.trySimplifyBvUnsignedMulNoOverflow(lhs: KExpr<T>, rhs: KExpr<T>): KExpr<KBoolSort>?

withExpressionsOrdered

inline fun <T : KSort, R> withExpressionsOrdered(lhs: KExpr<T>, rhs: KExpr<T>, body: (KExpr<T>, KExpr<T>) -> R): R

Properties

SIMPLIFIER_DEFAULT_BOUNDED_REWRITE_DEPTH

const val SIMPLIFIER_DEFAULT_BOUNDED_REWRITE_DEPTH: Int = 3