Create n-ary array store expression (store array_0 ... indices_n value) without cache. Cache is used to speed up mkArrayNSelect operation simplification but can result in a huge memory consumption.

mkArraySelect

open fun <D : KSort, R : KSort> mkArraySelect(array: KExpr<KArraySort<D, R>>, index: KExpr<D>): KExpr<R>

Create an array select expression (select array).

open fun <D0 : KSort, D1 : KSort, R : KSort> mkArraySelect(array: KExpr<KArray2Sort<D0, D1, R>>, index0: KExpr<D0>, index1: KExpr<D1>): KExpr<R>

open fun <D0 : KSort, D1 : KSort, D2 : KSort, R : KSort> mkArraySelect(array: KExpr<KArray3Sort<D0, D1, D2, R>>, index0: KExpr<D0>, index1: KExpr<D1>, index2: KExpr<D2>): KExpr<R>

Create an array select expression (select array index1).

mkArraySelectDecl

fun <D0 : KSort, D1 : KSort, R : KSort> mkArraySelectDecl(array: KArray2Sort<D0, D1, R>): KArray2SelectDecl<D0, D1, R>

fun <D0 : KSort, D1 : KSort, D2 : KSort, R : KSort> mkArraySelectDecl(array: KArray3Sort<D0, D1, D2, R>): KArray3SelectDecl<D0, D1, D2, R>

fun <D : KSort, R : KSort> mkArraySelectDecl(array: KArraySort<D, R>): KArraySelectDecl<D, R>

mkArraySelectNoSimplify

open fun <D : KSort, R : KSort> mkArraySelectNoSimplify(array: KExpr<KArraySort<D, R>>, index: KExpr<D>): KArraySelect<D, R>

Create an array select expression (select array).

open fun <D0 : KSort, D1 : KSort, R : KSort> mkArraySelectNoSimplify(array: KExpr<KArray2Sort<D0, D1, R>>, index0: KExpr<D0>, index1: KExpr<D1>): KArray2Select<D0, D1, R>

open fun <D0 : KSort, D1 : KSort, D2 : KSort, R : KSort> mkArraySelectNoSimplify(array: KExpr<KArray3Sort<D0, D1, D2, R>>, index0: KExpr<D0>, index1: KExpr<D1>, index2: KExpr<D2>): KArray3Select<D0, D1, D2, R>

Create an array select expression (select array index1).

mkArraySort

fun <D : KSort, R : KSort> mkArraySort(domain: D, range: R): KArraySort<D, R>

Create an array sort (Array domain).

fun <D0 : KSort, D1 : KSort, R : KSort> mkArraySort(domain0: D0, domain1: D1, range: R): KArray2Sort<D0, D1, R>

Create an array sort (Array domain0 range).

fun <D0 : KSort, D1 : KSort, D2 : KSort, R : KSort> mkArraySort(domain0: D0, domain1: D1, domain2: D2, range: R): KArray3Sort<D0, D1, D2, R>

Create an array sort (Array domain0 domain2).

mkArrayStore

open fun <D : KSort, R : KSort> mkArrayStore(array: KExpr<KArraySort<D, R>>, index: KExpr<D>, value: KExpr<R>): KExpr<KArraySort<D, R>>

Create an array store expression (store array value).

open fun <D0 : KSort, D1 : KSort, R : KSort> mkArrayStore(array: KExpr<KArray2Sort<D0, D1, R>>, index0: KExpr<D0>, index1: KExpr<D1>, value: KExpr<R>): KExpr<KArray2Sort<D0, D1, R>>

Create an array store expression (store array index1).

open fun <D0 : KSort, D1 : KSort, D2 : KSort, R : KSort> mkArrayStore(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>>

Create an array store expression (store array index1 value).

mkArrayStoreDecl

fun <D0 : KSort, D1 : KSort, R : KSort> mkArrayStoreDecl(array: KArray2Sort<D0, D1, R>): KArray2StoreDecl<D0, D1, R>

fun <D0 : KSort, D1 : KSort, D2 : KSort, R : KSort> mkArrayStoreDecl(array: KArray3Sort<D0, D1, D2, R>): KArray3StoreDecl<D0, D1, D2, R>

fun <D : KSort, R : KSort> mkArrayStoreDecl(array: KArraySort<D, R>): KArrayStoreDecl<D, R>

mkArrayStoreNoSimplify

open fun <D : KSort, R : KSort> mkArrayStoreNoSimplify(array: KExpr<KArraySort<D, R>>, index: KExpr<D>, value: KExpr<R>): KArrayStore<D, R>

Create an array store expression (store array value).

open fun <D0 : KSort, D1 : KSort, R : KSort> mkArrayStoreNoSimplify(array: KExpr<KArray2Sort<D0, D1, R>>, index0: KExpr<D0>, index1: KExpr<D1>, value: KExpr<R>): KArray2Store<D0, D1, R>

Create an array store expression (store array index1).

open fun <D0 : KSort, D1 : KSort, D2 : KSort, R : KSort> mkArrayStoreNoSimplify(array: KExpr<KArray3Sort<D0, D1, D2, R>>, index0: KExpr<D0>, index1: KExpr<D1>, index2: KExpr<D2>, value: KExpr<R>): KArray3Store<D0, D1, D2, R>

Create an array store expression (store array index1 value).

mkArrayStoreNoSimplifyNoAnalyze

open fun <D : KSort, R : KSort> mkArrayStoreNoSimplifyNoAnalyze(array: KExpr<KArraySort<D, R>>, index: KExpr<D>, value: KExpr<R>): KArrayStore<D, R>

Create an array store expression (store array value) without cache. Cache is used to speed up mkArraySelect operation simplification but can result in a huge memory consumption.

open fun <D0 : KSort, D1 : KSort, R : KSort> mkArrayStoreNoSimplifyNoAnalyze(array: KExpr<KArray2Sort<D0, D1, R>>, index0: KExpr<D0>, index1: KExpr<D1>, value: KExpr<R>): KArray2Store<D0, D1, R>

Create an array store expression (store array index1) without cache. Cache is used to speed up mkArraySelect operation simplification but can result in a huge memory consumption.

open fun <D0 : KSort, D1 : KSort, D2 : KSort, R : KSort> mkArrayStoreNoSimplifyNoAnalyze(array: KExpr<KArray3Sort<D0, D1, D2, R>>, index0: KExpr<D0>, index1: KExpr<D1>, index2: KExpr<D2>, value: KExpr<R>): KArray3Store<D0, D1, D2, R>

Create an array store expression (store array index1 value) without cache. Cache is used to speed up mkArraySelect operation simplification but can result in a huge memory consumption.

mkBool

fun mkBool(value: Boolean): KExpr<KBoolSort>

mkBoolSort

fun mkBoolSort(): KBoolSort

Create a Bool sort.

mkBv

fun mkBv(value: Boolean): KBitVec1Value

Create a BitVec value with 1 bit length.

fun mkBv(value: Byte): KBitVec8Value

Create a BitVec value with 8 bit length.

fun mkBv(value: Int): KBitVec32Value

Create a BitVec value with 32 bit length.

fun mkBv(value: Long): KBitVec64Value

Create a BitVec value with 64 bit length.

fun mkBv(value: Short): KBitVec16Value

Create a BitVec value with 16 bit length.

fun <T : KBvSort> mkBv(value: BigInteger, sort: T): KBitVecValue<T>

fun <T : KBvSort> mkBv(value: Boolean, sort: T): KBitVecValue<T>

fun <T : KBvSort> mkBv(value: Byte, sort: T): KBitVecValue<T>

fun <T : KBvSort> mkBv(value: Int, sort: T): KBitVecValue<T>

fun <T : KBvSort> mkBv(value: Long, sort: T): KBitVecValue<T>

fun <T : KBvSort> mkBv(value: Short, sort: T): KBitVecValue<T>

Create a BitVec value of the BitVec sort.

fun mkBv(value: BigInteger, sizeBits: UInt): KBitVecValue<KBvSort>

fun mkBv(value: Boolean, sizeBits: UInt): KBitVecValue<KBvSort>

fun mkBv(value: Byte, sizeBits: UInt): KBitVecValue<KBvSort>

fun mkBv(value: Int, sizeBits: UInt): KBitVecValue<KBvSort>

fun mkBv(value: Long, sizeBits: UInt): KBitVecValue<KBvSort>

fun mkBv(value: Short, sizeBits: UInt): KBitVecValue<KBvSort>

Create a BitVec value with sizeBits bit length.

fun mkBv(value: String, sizeBits: UInt): KBitVecValue<KBvSort>

Create a BitVec value with sizeBits bit length from the given binary string value.

mkBv16Sort

fun mkBv16Sort(): KBv16Sort

Create a BitVec sort with 16 bits length (_ BitVec 16).

mkBv1Sort

fun mkBv1Sort(): KBv1Sort

Create a BitVec sort with 1 bit length (_ BitVec 1).

mkBv2IntDecl

fun mkBv2IntDecl(value: KBvSort, isSigned: Boolean): KBv2IntDecl

mkBv2IntExpr

open fun <T : KBvSort> mkBv2IntExpr(value: KExpr<T>, isSigned: Boolean): KExpr<KIntSort>

Convert BitVec expressions value to the arithmetic Int expressions. When isSigned is set, the sign (highest, leftmost) bit is treated as the value sign.

mkBv2IntExprNoSimplify

open fun <T : KBvSort> mkBv2IntExprNoSimplify(value: KExpr<T>, isSigned: Boolean): KBv2IntExpr

Convert BitVec expressions value to the arithmetic Int expressions. When isSigned is set, the sign (highest, leftmost) bit is treated as the value sign.

mkBv32Sort

fun mkBv32Sort(): KBv32Sort

Create a BitVec sort with 32 bits length (_ BitVec 32).

mkBv64Sort

fun mkBv64Sort(): KBv64Sort

Create a BitVec sort with 64 bits length (_ BitVec 64).

mkBv8Sort

fun mkBv8Sort(): KBv8Sort

Create a BitVec sort with 8 bits length (_ BitVec 8).

mkBvAddDecl

fun <T : KBvSort> mkBvAddDecl(arg0: T, arg1: T): KBvAddDecl<T>

mkBvAddExpr

open fun <T : KBvSort> mkBvAddExpr(arg0: KExpr<T>, arg1: KExpr<T>): KExpr<T>

Create BitVec arithmetic addition (bvadd) expression.

mkBvAddExprNoSimplify

open fun <T : KBvSort> mkBvAddExprNoSimplify(arg0: KExpr<T>, arg1: KExpr<T>): KBvAddExpr<T>

Create BitVec arithmetic addition (bvadd) expression.

mkBvAddNoOverflowDecl

fun <T : KBvSort> mkBvAddNoOverflowDecl(arg0: T, arg1: T, isSigned: Boolean): KBvAddNoOverflowDecl<T>

mkBvAddNoOverflowExpr

open fun <T : KBvSort> mkBvAddNoOverflowExpr(arg0: KExpr<T>, arg1: KExpr<T>, isSigned: Boolean): KExpr<KBoolSort>

Create BitVec add-no-overflow check expression. Determines that BitVec arithmetic addition does not overflow. An overflow occurs when the addition result value is greater than max supported value.

mkBvAddNoOverflowExprNoSimplify

open fun <T : KBvSort> mkBvAddNoOverflowExprNoSimplify(arg0: KExpr<T>, arg1: KExpr<T>, isSigned: Boolean): KBvAddNoOverflowExpr<T>

Create BitVec add-no-overflow check expression. Determines that BitVec arithmetic addition does not overflow. An overflow occurs when the addition result value is greater than max supported value.

mkBvAddNoUnderflowDecl

fun <T : KBvSort> mkBvAddNoUnderflowDecl(arg0: T, arg1: T): KBvAddNoUnderflowDecl<T>

mkBvAddNoUnderflowExpr

open fun <T : KBvSort> mkBvAddNoUnderflowExpr(arg0: KExpr<T>, arg1: KExpr<T>): KExpr<KBoolSort>

Create BitVec add-no-underflow check expression. Determines that BitVec arithmetic addition does not underflow. An underflow occurs when the addition result value is lower than min supported value.

mkBvAddNoUnderflowExprNoSimplify

open fun <T : KBvSort> mkBvAddNoUnderflowExprNoSimplify(arg0: KExpr<T>, arg1: KExpr<T>): KBvAddNoUnderflowExpr<T>

Create BitVec add-no-underflow check expression. Determines that BitVec arithmetic addition does not underflow. An underflow occurs when the addition result value is lower than min supported value.

mkBvAndDecl

fun <T : KBvSort> mkBvAndDecl(arg0: T, arg1: T): KBvAndDecl<T>

mkBvAndExpr

open fun <T : KBvSort> mkBvAndExpr(arg0: KExpr<T>, arg1: KExpr<T>): KExpr<T>

Create bitwise AND (bvand) expression.

mkBvAndExprNoSimplify

open fun <T : KBvSort> mkBvAndExprNoSimplify(arg0: KExpr<T>, arg1: KExpr<T>): KBvAndExpr<T>

Create bitwise AND (bvand) expression.

mkBvArithShiftRightDecl

fun <T : KBvSort> mkBvArithShiftRightDecl(arg0: T, arg1: T): KBvArithShiftRightDecl<T>

mkBvArithShiftRightExpr

open fun <T : KBvSort> mkBvArithShiftRightExpr(arg: KExpr<T>, shift: KExpr<T>): KExpr<T>

Create BitVec arithmetic shift right (bvashr) expression. The shifted expressions is padded with sign (leftmost, highest) bits.

mkBvArithShiftRightExprNoSimplify

open fun <T : KBvSort> mkBvArithShiftRightExprNoSimplify(arg: KExpr<T>, shift: KExpr<T>): KBvArithShiftRightExpr<T>

Create BitVec arithmetic shift right (bvashr) expression. The shifted expressions is padded with sign (leftmost, highest) bits.

mkBvConcatDecl

fun mkBvConcatDecl(arg0: KBvSort, arg1: KBvSort): KBvConcatDecl

mkBvConcatExpr

open fun <T : KBvSort, S : KBvSort> mkBvConcatExpr(arg0: KExpr<T>, arg1: KExpr<S>): KExpr<KBvSort>

Create BitVec concatenation (concat) expression.

mkBvConcatExprNoSimplify

open fun <T : KBvSort, S : KBvSort> mkBvConcatExprNoSimplify(arg0: KExpr<T>, arg1: KExpr<S>): KBvConcatExpr

Create BitVec concatenation (concat) expression.

mkBvDecl

fun mkBvDecl(value: Boolean): KDecl<KBv1Sort>

fun mkBvDecl(value: Byte): KDecl<KBv8Sort>

fun mkBvDecl(value: Int): KDecl<KBv32Sort>

fun mkBvDecl(value: Long): KDecl<KBv64Sort>

fun mkBvDecl(value: Short): KDecl<KBv16Sort>

fun mkBvDecl(value: BigInteger, size: UInt): KDecl<KBvSort>

fun mkBvDecl(value: String, sizeBits: UInt): KDecl<KBvSort>

mkBvDivNoOverflowDecl

fun <T : KBvSort> mkBvDivNoOverflowDecl(arg0: T, arg1: T): KBvDivNoOverflowDecl<T>

mkBvDivNoOverflowExpr

open fun <T : KBvSort> mkBvDivNoOverflowExpr(arg0: KExpr<T>, arg1: KExpr<T>): KExpr<KBoolSort>

Create BitVec div-no-overflow check expression. Determines that BitVec arithmetic signed division does not overflow.

mkBvDivNoOverflowExprNoSimplify

open fun <T : KBvSort> mkBvDivNoOverflowExprNoSimplify(arg0: KExpr<T>, arg1: KExpr<T>): KBvDivNoOverflowExpr<T>

Create BitVec div-no-overflow check expression. Determines that BitVec arithmetic signed division does not overflow.

mkBvExtractDecl

fun mkBvExtractDecl(high: Int, low: Int, value: KExpr<KBvSort>): KBvExtractDecl

mkBvExtractExpr

open fun <T : KBvSort> mkBvExtractExpr(high: Int, low: Int, value: KExpr<T>): KExpr<KBvSort>

Create BitVec extract (extract) expression. Extract bits from low (including) to high (including) as a new BitVec.

mkBvExtractExprNoSimplify

open fun <T : KBvSort> mkBvExtractExprNoSimplify(high: Int, low: Int, value: KExpr<T>): KBvExtractExpr

Create BitVec extract (extract) expression. Extract bits from low (including) to high (including) as a new BitVec.

mkBvHex

fun mkBvHex(value: String, sizeBits: UInt): KBitVecValue<KBvSort>

Create a BitVec value with sizeBits bit length from the given hex string value.

mkBvHexDecl

fun mkBvHexDecl(value: String, sizeBits: UInt): KDecl<KBvSort>

mkBvLogicalShiftRightDecl

fun <T : KBvSort> mkBvLogicalShiftRightDecl(arg0: T, arg1: T): KBvLogicalShiftRightDecl<T>

mkBvLogicalShiftRightExpr

open fun <T : KBvSort> mkBvLogicalShiftRightExpr(arg: KExpr<T>, shift: KExpr<T>): KExpr<T>

Create BitVec logical shift right (bvlshr) expression. The shifted expressions is padded with zero bits.

mkBvLogicalShiftRightExprNoSimplify

open fun <T : KBvSort> mkBvLogicalShiftRightExprNoSimplify(arg: KExpr<T>, shift: KExpr<T>): KBvLogicalShiftRightExpr<T>

Create BitVec logical shift right (bvlshr) expression. The shifted expressions is padded with zero bits.

mkBvMulDecl

fun <T : KBvSort> mkBvMulDecl(arg0: T, arg1: T): KBvMulDecl<T>

mkBvMulExpr

open fun <T : KBvSort> mkBvMulExpr(arg0: KExpr<T>, arg1: KExpr<T>): KExpr<T>

Create BitVec arithmetic multiplication (bvmul) expression.

mkBvMulExprNoSimplify

open fun <T : KBvSort> mkBvMulExprNoSimplify(arg0: KExpr<T>, arg1: KExpr<T>): KBvMulExpr<T>

Create BitVec arithmetic multiplication (bvmul) expression.

mkBvMulNoOverflowDecl

fun <T : KBvSort> mkBvMulNoOverflowDecl(arg0: T, arg1: T, isSigned: Boolean): KBvMulNoOverflowDecl<T>

mkBvMulNoOverflowExpr

open fun <T : KBvSort> mkBvMulNoOverflowExpr(arg0: KExpr<T>, arg1: KExpr<T>, isSigned: Boolean): KExpr<KBoolSort>

Create BitVec mul-no-overflow check expression. Determines that BitVec arithmetic multiplication does not overflow. An overflow occurs when the multiplication result value is greater than max supported value.

mkBvMulNoOverflowExprNoSimplify

open fun <T : KBvSort> mkBvMulNoOverflowExprNoSimplify(arg0: KExpr<T>, arg1: KExpr<T>, isSigned: Boolean): KBvMulNoOverflowExpr<T>

mkBvMulNoUnderflowDecl

fun <T : KBvSort> mkBvMulNoUnderflowDecl(arg0: T, arg1: T): KBvMulNoUnderflowDecl<T>

mkBvMulNoUnderflowExpr

open fun <T : KBvSort> mkBvMulNoUnderflowExpr(arg0: KExpr<T>, arg1: KExpr<T>): KExpr<KBoolSort>

Create BitVec mul-no-underflow check expression. Determines that BitVec arithmetic multiplication does not underflow. An underflow occurs when the multiplication result value is lower than min supported value.

mkBvMulNoUnderflowExprNoSimplify

open fun <T : KBvSort> mkBvMulNoUnderflowExprNoSimplify(arg0: KExpr<T>, arg1: KExpr<T>): KBvMulNoUnderflowExpr<T>

mkBvNAndDecl

fun <T : KBvSort> mkBvNAndDecl(arg0: T, arg1: T): KBvNAndDecl<T>

mkBvNAndExpr

open fun <T : KBvSort> mkBvNAndExpr(arg0: KExpr<T>, arg1: KExpr<T>): KExpr<T>

Create bitwise NAND (bvnand) expression.

mkBvNAndExprNoSimplify

open fun <T : KBvSort> mkBvNAndExprNoSimplify(arg0: KExpr<T>, arg1: KExpr<T>): KBvNAndExpr<T>

Create bitwise NAND (bvnand) expression.

mkBvNegationDecl

fun <T : KBvSort> mkBvNegationDecl(sort: T): KBvNegationDecl<T>

mkBvNegationExpr

open fun <T : KBvSort> mkBvNegationExpr(value: KExpr<T>): KExpr<T>

Create BitVec arithmetic negation (bvneg) expression.

mkBvNegationExprNoSimplify

open fun <T : KBvSort> mkBvNegationExprNoSimplify(value: KExpr<T>): KBvNegationExpr<T>

Create BitVec arithmetic negation (bvneg) expression.

mkBvNegationNoOverflowDecl

fun <T : KBvSort> mkBvNegationNoOverflowDecl(value: T): KBvNegNoOverflowDecl<T>

mkBvNegationNoOverflowExpr

open fun <T : KBvSort> mkBvNegationNoOverflowExpr(value: KExpr<T>): KExpr<KBoolSort>

Create BitVec neg-no-overflow check expression. Determines that BitVec arithmetic negation does not overflow.

mkBvNegationNoOverflowExprNoSimplify

open fun <T : KBvSort> mkBvNegationNoOverflowExprNoSimplify(value: KExpr<T>): KBvNegNoOverflowExpr<T>

Create BitVec neg-no-overflow check expression. Determines that BitVec arithmetic negation does not overflow.

mkBvNorDecl

fun <T : KBvSort> mkBvNorDecl(arg0: T, arg1: T): KBvNorDecl<T>

mkBvNorExpr

open fun <T : KBvSort> mkBvNorExpr(arg0: KExpr<T>, arg1: KExpr<T>): KExpr<T>

Create bitwise NOR (bvnor) expression.

mkBvNorExprNoSimplify

open fun <T : KBvSort> mkBvNorExprNoSimplify(arg0: KExpr<T>, arg1: KExpr<T>): KBvNorExpr<T>

Create bitwise NOR (bvnor) expression.

mkBvNotDecl

fun <T : KBvSort> mkBvNotDecl(sort: T): KBvNotDecl<T>

mkBvNotExpr

open fun <T : KBvSort> mkBvNotExpr(value: KExpr<T>): KExpr<T>

Create bitwise NOT (bvnot) expression.

mkBvNotExprNoSimplify

open fun <T : KBvSort> mkBvNotExprNoSimplify(value: KExpr<T>): KBvNotExpr<T>

Create bitwise NOT (bvnot) expression.

mkBvOrDecl

fun <T : KBvSort> mkBvOrDecl(arg0: T, arg1: T): KBvOrDecl<T>

mkBvOrExpr

open fun <T : KBvSort> mkBvOrExpr(arg0: KExpr<T>, arg1: KExpr<T>): KExpr<T>

Create bitwise OR (bvor) expression.

mkBvOrExprNoSimplify

open fun <T : KBvSort> mkBvOrExprNoSimplify(arg0: KExpr<T>, arg1: KExpr<T>): KBvOrExpr<T>

Create bitwise OR (bvor) expression.

mkBvReductionAndDecl

fun <T : KBvSort> mkBvReductionAndDecl(sort: T): KBvReductionAndDecl<T>

mkBvReductionAndExpr

open fun <T : KBvSort> mkBvReductionAndExpr(value: KExpr<T>): KExpr<KBv1Sort>

Create bitwise AND reduction (bvredand) expression. Reduce all bits to a single bit with AND operation.

mkBvReductionAndExprNoSimplify

open fun <T : KBvSort> mkBvReductionAndExprNoSimplify(value: KExpr<T>): KBvReductionAndExpr<T>

Create bitwise AND reduction (bvredand) expression. Reduce all bits to a single bit with AND operation.

mkBvReductionOrDecl

fun <T : KBvSort> mkBvReductionOrDecl(sort: T): KBvReductionOrDecl<T>

mkBvReductionOrExpr

open fun <T : KBvSort> mkBvReductionOrExpr(value: KExpr<T>): KExpr<KBv1Sort>

Create bitwise OR reduction (bvredor) expression. Reduce all bits to a single bit with OR operation.

mkBvReductionOrExprNoSimplify

open fun <T : KBvSort> mkBvReductionOrExprNoSimplify(value: KExpr<T>): KBvReductionOrExpr<T>

Create bitwise OR reduction (bvredor) expression. Reduce all bits to a single bit with OR operation.

mkBvRepeatDecl

fun mkBvRepeatDecl(i: Int, value: KBvSort): KBvRepeatDecl

mkBvRepeatExpr

open fun <T : KBvSort> mkBvRepeatExpr(repeatNumber: Int, value: KExpr<T>): KExpr<KBvSort>

mkBvRepeatExprNoSimplify

open fun <T : KBvSort> mkBvRepeatExprNoSimplify(repeatNumber: Int, value: KExpr<T>): KBvRepeatExpr

Create BitVec repeat (repeat) expression. Returns a BitVec expression with repeatNumber concatenated copies of value.

mkBvRotateLeftDecl

fun <T : KBvSort> mkBvRotateLeftDecl(arg0: T, arg1: T): KBvRotateLeftDecl<T>

mkBvRotateLeftExpr

open fun <T : KBvSort> mkBvRotateLeftExpr(arg: KExpr<T>, rotation: KExpr<T>): KExpr<T>

Create BitVec rotate left (rotateleft) expression. The result expression is rotated left rotation times.

mkBvRotateLeftExprNoSimplify

open fun <T : KBvSort> mkBvRotateLeftExprNoSimplify(arg: KExpr<T>, rotation: KExpr<T>): KBvRotateLeftExpr<T>

Create BitVec rotate left (rotateleft) expression. The result expression is rotated left rotation times.

mkBvRotateLeftIndexedDecl

fun <T : KBvSort> mkBvRotateLeftIndexedDecl(i: Int, valueSort: T): KBvRotateLeftIndexedDecl<T>

mkBvRotateLeftIndexedExpr

open fun <T : KBvSort> mkBvRotateLeftIndexedExpr(rotation: Int, value: KExpr<T>): KExpr<T>

Create BitVec rotate left (rotateleft) expression. The result expression is rotated left rotation times.

mkBvRotateLeftIndexedExprNoSimplify

open fun <T : KBvSort> mkBvRotateLeftIndexedExprNoSimplify(rotation: Int, value: KExpr<T>): KBvRotateLeftIndexedExpr<T>

Create BitVec rotate left (rotateleft) expression. The result expression is rotated left rotation times.

mkBvRotateRightDecl

fun <T : KBvSort> mkBvRotateRightDecl(arg0: T, arg1: T): KBvRotateRightDecl<T>

mkBvRotateRightExpr

open fun <T : KBvSort> mkBvRotateRightExpr(arg: KExpr<T>, rotation: KExpr<T>): KExpr<T>

Create BitVec rotate right (rotateright) expression. The result expression is rotated right rotation times.

mkBvRotateRightExprNoSimplify

open fun <T : KBvSort> mkBvRotateRightExprNoSimplify(arg: KExpr<T>, rotation: KExpr<T>): KBvRotateRightExpr<T>

Create BitVec rotate right (rotateright) expression. The result expression is rotated right rotation times.

mkBvRotateRightIndexedDecl

fun <T : KBvSort> mkBvRotateRightIndexedDecl(i: Int, valueSort: T): KBvRotateRightIndexedDecl<T>

mkBvRotateRightIndexedExpr

open fun <T : KBvSort> mkBvRotateRightIndexedExpr(rotation: Int, value: KExpr<T>): KExpr<T>

Create BitVec rotate right (rotateright) expression. The result expression is rotated right rotation times.

mkBvRotateRightIndexedExprNoSimplify

open fun <T : KBvSort> mkBvRotateRightIndexedExprNoSimplify(rotation: Int, value: KExpr<T>): KBvRotateRightIndexedExpr<T>

Create BitVec rotate right (rotateright) expression. The result expression is rotated right rotation times.

mkBvShiftLeftDecl

fun <T : KBvSort> mkBvShiftLeftDecl(arg0: T, arg1: T): KBvShiftLeftDecl<T>

mkBvShiftLeftExpr

open fun <T : KBvSort> mkBvShiftLeftExpr(arg: KExpr<T>, shift: KExpr<T>): KExpr<T>

Create BitVec shift left (bvshl) expression.

mkBvShiftLeftExprNoSimplify

open fun <T : KBvSort> mkBvShiftLeftExprNoSimplify(arg: KExpr<T>, shift: KExpr<T>): KBvShiftLeftExpr<T>

Create BitVec shift left (bvshl) expression.

mkBvSignedDivDecl

fun <T : KBvSort> mkBvSignedDivDecl(arg0: T, arg1: T): KBvSignedDivDecl<T>

mkBvSignedDivExpr

open fun <T : KBvSort> mkBvSignedDivExpr(arg0: KExpr<T>, arg1: KExpr<T>): KExpr<T>

Create BitVec arithmetic signed division (bvsdiv) expression. The division result sign depends on the arguments signs.

mkBvSignedDivExprNoSimplify

open fun <T : KBvSort> mkBvSignedDivExprNoSimplify(arg0: KExpr<T>, arg1: KExpr<T>): KBvSignedDivExpr<T>

Create BitVec arithmetic signed division (bvsdiv) expression. The division result sign depends on the arguments signs.

mkBvSignedGreaterDecl

fun <T : KBvSort> mkBvSignedGreaterDecl(arg0: T, arg1: T): KBvSignedGreaterDecl<T>

mkBvSignedGreaterExpr

open fun <T : KBvSort> mkBvSignedGreaterExpr(arg0: KExpr<T>, arg1: KExpr<T>): KExpr<KBoolSort>

Create BitVec signed greater (bvsgt) expression.

mkBvSignedGreaterExprNoSimplify

open fun <T : KBvSort> mkBvSignedGreaterExprNoSimplify(arg0: KExpr<T>, arg1: KExpr<T>): KBvSignedGreaterExpr<T>

Create BitVec signed greater (bvsgt) expression.

mkBvSignedGreaterOrEqualDecl

fun <T : KBvSort> mkBvSignedGreaterOrEqualDecl(arg0: T, arg1: T): KBvSignedGreaterOrEqualDecl<T>

mkBvSignedGreaterOrEqualExpr

open fun <T : KBvSort> mkBvSignedGreaterOrEqualExpr(arg0: KExpr<T>, arg1: KExpr<T>): KExpr<KBoolSort>

Create BitVec signed greater-or-equal (bvsge) expression.

mkBvSignedGreaterOrEqualExprNoSimplify

open fun <T : KBvSort> mkBvSignedGreaterOrEqualExprNoSimplify(arg0: KExpr<T>, arg1: KExpr<T>): KBvSignedGreaterOrEqualExpr<T>

Create BitVec signed greater-or-equal (bvsge) expression.

mkBvSignedLessDecl

fun <T : KBvSort> mkBvSignedLessDecl(arg0: T, arg1: T): KBvSignedLessDecl<T>

mkBvSignedLessExpr

open fun <T : KBvSort> mkBvSignedLessExpr(arg0: KExpr<T>, arg1: KExpr<T>): KExpr<KBoolSort>

Create BitVec signed less (bvslt) expression.

mkBvSignedLessExprNoSimplify

open fun <T : KBvSort> mkBvSignedLessExprNoSimplify(arg0: KExpr<T>, arg1: KExpr<T>): KBvSignedLessExpr<T>

Create BitVec signed less (bvslt) expression.

mkBvSignedLessOrEqualDecl

fun <T : KBvSort> mkBvSignedLessOrEqualDecl(arg0: T, arg1: T): KBvSignedLessOrEqualDecl<T>

mkBvSignedLessOrEqualExpr

open fun <T : KBvSort> mkBvSignedLessOrEqualExpr(arg0: KExpr<T>, arg1: KExpr<T>): KExpr<KBoolSort>

Create BitVec signed less-or-equal (bvsle) expression.

mkBvSignedLessOrEqualExprNoSimplify

open fun <T : KBvSort> mkBvSignedLessOrEqualExprNoSimplify(arg0: KExpr<T>, arg1: KExpr<T>): KBvSignedLessOrEqualExpr<T>

Create BitVec signed less-or-equal (bvsle) expression.

mkBvSignedModDecl

fun <T : KBvSort> mkBvSignedModDecl(arg0: T, arg1: T): KBvSignedModDecl<T>

mkBvSignedModExpr

open fun <T : KBvSort> mkBvSignedModExpr(arg0: KExpr<T>, arg1: KExpr<T>): KExpr<T>

Create BitVec arithmetic signed mod (bvsmod) expression.

mkBvSignedModExprNoSimplify

open fun <T : KBvSort> mkBvSignedModExprNoSimplify(arg0: KExpr<T>, arg1: KExpr<T>): KBvSignedModExpr<T>

Create BitVec arithmetic signed mod (bvsmod) expression.

mkBvSignedRemDecl

fun <T : KBvSort> mkBvSignedRemDecl(arg0: T, arg1: T): KBvSignedRemDecl<T>

mkBvSignedRemExpr

open fun <T : KBvSort> mkBvSignedRemExpr(arg0: KExpr<T>, arg1: KExpr<T>): KExpr<T>

Create BitVec arithmetic signed reminder (bvsrem) expression.

mkBvSignedRemExprNoSimplify

open fun <T : KBvSort> mkBvSignedRemExprNoSimplify(arg0: KExpr<T>, arg1: KExpr<T>): KBvSignedRemExpr<T>

Create BitVec arithmetic signed reminder (bvsrem) expression.

mkBvSignExtensionDecl

fun mkBvSignExtensionDecl(i: Int, value: KBvSort): KSignExtDecl

mkBvSignExtensionExpr

open fun <T : KBvSort> mkBvSignExtensionExpr(extensionSize: Int, value: KExpr<T>): KExpr<KBvSort>

Create BitVec signed extension (signext) expression. Returns a BitVec expression with extensionSize extra sign (leftmost, highest) bits. The extra bits are prepended to the provided value.

mkBvSignExtensionExprNoSimplify

open fun <T : KBvSort> mkBvSignExtensionExprNoSimplify(extensionSize: Int, value: KExpr<T>): KBvSignExtensionExpr

Create BitVec signed extension (signext) expression. Returns a BitVec expression with extensionSize extra sign (leftmost, highest) bits. The extra bits are prepended to the provided value.

mkBvSort

open fun mkBvSort(sizeBits: UInt): KBvSort

Create a BitVec sort with sizeBits bits length (_ BitVec sizeBits).

mkBvSubDecl

fun <T : KBvSort> mkBvSubDecl(arg0: T, arg1: T): KBvSubDecl<T>

mkBvSubExpr

open fun <T : KBvSort> mkBvSubExpr(arg0: KExpr<T>, arg1: KExpr<T>): KExpr<T>

Create BitVec arithmetic subtraction (bvsub) expression.

mkBvSubExprNoSimplify

open fun <T : KBvSort> mkBvSubExprNoSimplify(arg0: KExpr<T>, arg1: KExpr<T>): KBvSubExpr<T>

Create BitVec arithmetic subtraction (bvsub) expression.

mkBvSubNoOverflowDecl

fun <T : KBvSort> mkBvSubNoOverflowDecl(arg0: T, arg1: T): KBvSubNoOverflowDecl<T>

mkBvSubNoOverflowExpr

open fun <T : KBvSort> mkBvSubNoOverflowExpr(arg0: KExpr<T>, arg1: KExpr<T>): KExpr<KBoolSort>

Create BitVec sub-no-overflow check expression. Determines that BitVec arithmetic subtraction does not overflow. An overflow occurs when the subtraction result value is greater than max supported value.

mkBvSubNoOverflowExprNoSimplify

open fun <T : KBvSort> mkBvSubNoOverflowExprNoSimplify(arg0: KExpr<T>, arg1: KExpr<T>): KBvSubNoOverflowExpr<T>

mkBvSubNoUnderflowDecl

fun <T : KBvSort> mkBvSubNoUnderflowDecl(arg0: T, arg1: T, isSigned: Boolean): KBvSubNoUnderflowDecl<T>

mkBvSubNoUnderflowExpr

open fun <T : KBvSort> mkBvSubNoUnderflowExpr(arg0: KExpr<T>, arg1: KExpr<T>, isSigned: Boolean): KExpr<KBoolSort>

Create BitVec sub-no-underflow check expression. Determines that BitVec arithmetic subtraction does not underflow. An underflow occurs when the subtraction result value is lower than min supported value.

mkBvSubNoUnderflowExprNoSimplify

open fun <T : KBvSort> mkBvSubNoUnderflowExprNoSimplify(arg0: KExpr<T>, arg1: KExpr<T>, isSigned: Boolean): KBvSubNoUnderflowExpr<T>

mkBvToFpDecl

fun <T : KFpSort> mkBvToFpDecl(sort: T, rm: KFpRoundingModeSort, value: KBvSort, signed: Boolean): KBvToFpDecl<T>

mkBvToFpExpr

open fun <T : KFpSort> mkBvToFpExpr(sort: T, roundingMode: KExpr<KFpRoundingModeSort>, value: KExpr<KBvSort>, signed: Boolean): KExpr<T>

Create Fp from BitVec value. Rounding is performed according to the roundingMode.

mkBvToFpExprNoSimplify

open fun <T : KFpSort> mkBvToFpExprNoSimplify(sort: T, roundingMode: KExpr<KFpRoundingModeSort>, value: KExpr<KBvSort>, signed: Boolean): KBvToFpExpr<T>

Create Fp from BitVec value. Rounding is performed according to the roundingMode.

mkBvUnsignedDivDecl

fun <T : KBvSort> mkBvUnsignedDivDecl(arg0: T, arg1: T): KBvUnsignedDivDecl<T>

mkBvUnsignedDivExpr

open fun <T : KBvSort> mkBvUnsignedDivExpr(arg0: KExpr<T>, arg1: KExpr<T>): KExpr<T>

Create BitVec arithmetic unsigned division (bvudiv) expression.

mkBvUnsignedDivExprNoSimplify

open fun <T : KBvSort> mkBvUnsignedDivExprNoSimplify(arg0: KExpr<T>, arg1: KExpr<T>): KBvUnsignedDivExpr<T>

Create BitVec arithmetic unsigned division (bvudiv) expression.

mkBvUnsignedGreaterDecl

fun <T : KBvSort> mkBvUnsignedGreaterDecl(arg0: T, arg1: T): KBvUnsignedGreaterDecl<T>

mkBvUnsignedGreaterExpr

open fun <T : KBvSort> mkBvUnsignedGreaterExpr(arg0: KExpr<T>, arg1: KExpr<T>): KExpr<KBoolSort>

Create BitVec unsigned greater (bvugt) expression.

mkBvUnsignedGreaterExprNoSimplify

open fun <T : KBvSort> mkBvUnsignedGreaterExprNoSimplify(arg0: KExpr<T>, arg1: KExpr<T>): KBvUnsignedGreaterExpr<T>

Create BitVec unsigned greater (bvugt) expression.

mkBvUnsignedGreaterOrEqualDecl

fun <T : KBvSort> mkBvUnsignedGreaterOrEqualDecl(arg0: T, arg1: T): KBvUnsignedGreaterOrEqualDecl<T>

mkBvUnsignedGreaterOrEqualExpr

open fun <T : KBvSort> mkBvUnsignedGreaterOrEqualExpr(arg0: KExpr<T>, arg1: KExpr<T>): KExpr<KBoolSort>

Create BitVec unsigned greater-or-equal (bvuge) expression.

mkBvUnsignedGreaterOrEqualExprNoSimplify

open fun <T : KBvSort> mkBvUnsignedGreaterOrEqualExprNoSimplify(arg0: KExpr<T>, arg1: KExpr<T>): KBvUnsignedGreaterOrEqualExpr<T>

Create BitVec unsigned greater-or-equal (bvuge) expression.

mkBvUnsignedLessDecl

fun <T : KBvSort> mkBvUnsignedLessDecl(arg0: T, arg1: T): KBvUnsignedLessDecl<T>

mkBvUnsignedLessExpr

open fun <T : KBvSort> mkBvUnsignedLessExpr(arg0: KExpr<T>, arg1: KExpr<T>): KExpr<KBoolSort>

Create BitVec unsigned less (bvult) expression.

mkBvUnsignedLessExprNoSimplify

open fun <T : KBvSort> mkBvUnsignedLessExprNoSimplify(arg0: KExpr<T>, arg1: KExpr<T>): KBvUnsignedLessExpr<T>

Create BitVec unsigned less (bvult) expression.

mkBvUnsignedLessOrEqualDecl

fun <T : KBvSort> mkBvUnsignedLessOrEqualDecl(arg0: T, arg1: T): KBvUnsignedLessOrEqualDecl<T>

mkBvUnsignedLessOrEqualExpr

open fun <T : KBvSort> mkBvUnsignedLessOrEqualExpr(arg0: KExpr<T>, arg1: KExpr<T>): KExpr<KBoolSort>

Create BitVec unsigned less-or-equal (bvule) expression.

mkBvUnsignedLessOrEqualExprNoSimplify

open fun <T : KBvSort> mkBvUnsignedLessOrEqualExprNoSimplify(arg0: KExpr<T>, arg1: KExpr<T>): KBvUnsignedLessOrEqualExpr<T>

Create BitVec unsigned less-or-equal (bvule) expression.

mkBvUnsignedRemDecl

fun <T : KBvSort> mkBvUnsignedRemDecl(arg0: T, arg1: T): KBvUnsignedRemDecl<T>

mkBvUnsignedRemExpr

open fun <T : KBvSort> mkBvUnsignedRemExpr(arg0: KExpr<T>, arg1: KExpr<T>): KExpr<T>

Create BitVec arithmetic unsigned reminder (bvurem) expression.

mkBvUnsignedRemExprNoSimplify

open fun <T : KBvSort> mkBvUnsignedRemExprNoSimplify(arg0: KExpr<T>, arg1: KExpr<T>): KBvUnsignedRemExpr<T>

Create BitVec arithmetic unsigned reminder (bvurem) expression.

mkBvXNorDecl

fun <T : KBvSort> mkBvXNorDecl(arg0: T, arg1: T): KBvXNorDecl<T>

mkBvXNorExpr

open fun <T : KBvSort> mkBvXNorExpr(arg0: KExpr<T>, arg1: KExpr<T>): KExpr<T>

Create bitwise XNOR (bvxnor) expression.

mkBvXNorExprNoSimplify

open fun <T : KBvSort> mkBvXNorExprNoSimplify(arg0: KExpr<T>, arg1: KExpr<T>): KBvXNorExpr<T>

Create bitwise XNOR (bvxnor) expression.

mkBvXorDecl

fun <T : KBvSort> mkBvXorDecl(arg0: T, arg1: T): KBvXorDecl<T>

mkBvXorExpr

open fun <T : KBvSort> mkBvXorExpr(arg0: KExpr<T>, arg1: KExpr<T>): KExpr<T>

Create bitwise XOR (bvxor) expression.

mkBvXorExprNoSimplify

open fun <T : KBvSort> mkBvXorExprNoSimplify(arg0: KExpr<T>, arg1: KExpr<T>): KBvXorExpr<T>

Create bitwise XOR (bvxor) expression.

mkBvZeroExtensionDecl

fun mkBvZeroExtensionDecl(i: Int, value: KBvSort): KZeroExtDecl

mkBvZeroExtensionExpr

open fun <T : KBvSort> mkBvZeroExtensionExpr(extensionSize: Int, value: KExpr<T>): KExpr<KBvSort>

Create BitVec zero extension (zeroext) expression. Returns a BitVec expression with extensionSize extra zero bits. The extra bits are prepended to the provided value.

mkBvZeroExtensionExprNoSimplify

open fun <T : KBvSort> mkBvZeroExtensionExprNoSimplify(extensionSize: Int, value: KExpr<T>): KBvZeroExtensionExpr

Create BitVec zero extension (zeroext) expression. Returns a BitVec expression with extensionSize extra zero bits. The extra bits are prepended to the provided value.

mkConst

fun <T : KSort> mkConst(name: String, sort: T): KApp<T, *>

Create a constant named name with sort sort.

mkConstApp

open fun <T : KSort> mkConstApp(decl: KDecl<T>): KConst<T>

Create constant (function without arguments) app expression.

mkConstDecl

fun <T : KSort> mkConstDecl(name: String, sort: T): KUninterpretedConstDecl<T>

mkDefaultValueSampler

open fun mkDefaultValueSampler(): KSortVisitor<KExpr<*>>

mkDistinct

@JvmOverloads

open fun <T : KSort> mkDistinct(args: List<KExpr<T>>, order: Boolean = true): KExpr<KBoolSort>

Create DISTINCT expression.

mkDistinctDecl

fun <T : KSort> mkDistinctDecl(arg: T): KDistinctDecl<T>

mkDistinctNoSimplify

open fun <T : KSort> mkDistinctNoSimplify(args: List<KExpr<T>>): KDistinctExpr<T>

Create DISTINCT expression.

mkEq

@JvmOverloads

open fun <T : KSort> mkEq(lhs: KExpr<T>, rhs: KExpr<T>, order: Boolean = true): KExpr<KBoolSort>

Create EQ expression.

mkEqDecl

fun <T : KSort> mkEqDecl(arg: T): KEqDecl<T>

mkEqNoSimplify

open fun <T : KSort> mkEqNoSimplify(lhs: KExpr<T>, rhs: KExpr<T>): KEqExpr<T>

Create EQ expression.

mkExistentialQuantifier

open fun mkExistentialQuantifier(body: KExpr<KBoolSort>, bounds: List<KDecl<*>>): KExistentialQuantifier

Create existential quantifier (exists).

mkFalse

fun mkFalse(): KFalse

Create boolean False constant.

mkFalseDecl

fun mkFalseDecl(): KFalseDecl

mkFp

fun <T : KFpSort> mkFp(value: Double, sort: T): KFpValue<T>

fun <T : KFpSort> mkFp(value: Float, sort: T): KFpValue<T>

fun <T : KFpSort> mkFp(significand: KBitVecValue<*>, unbiasedExponent: KBitVecValue<*>, signBit: Boolean, sort: T): KFpValue<T>

fun <T : KFpSort> mkFp(significand: Int, unbiasedExponent: Int, signBit: Boolean, sort: T): KFpValue<T>

fun <T : KFpSort> mkFp(significand: Long, unbiasedExponent: Long, signBit: Boolean, sort: T): KFpValue<T>

mkFp128

fun mkFp128(significand: KBitVecValue<*>, unbiasedExponent: KBitVecValue<*>, signBit: Boolean): KFp128Value

fun mkFp128(significand: Long, unbiasedExponent: Long, signBit: Boolean): KFp128Value

Create FP128 from the IEEE binary representation. Note: unbiasedExponent here is unbiased, i.e. signed.

mkFp128Biased

fun mkFp128Biased(significand: KBitVecValue<*>, biasedExponent: KBitVecValue<*>, signBit: Boolean): KFp128Value

Create FP128 from the IEEE binary representation. Note: biasedExponent here is biased, i.e. unsigned.

mkFp128Decl

fun mkFp128Decl(significandBits: KBitVecValue<*>, unbiasedExponent: KBitVecValue<*>, signBit: Boolean): KFp128Decl

mkFp128DeclBiased

fun mkFp128DeclBiased(significandBits: KBitVecValue<*>, biasedExponent: KBitVecValue<*>, signBit: Boolean): KFp128Decl

mkFp128NaN

fun mkFp128NaN(): KFp128Value

Create FP128 NaN value.

mkFp128Sort

fun mkFp128Sort(): KFp128Sort

Create a 128-bit IEEE floating point sort (_ FloatingPoint 15 113).

mkFp16

fun mkFp16(value: Float): KFp16Value

Create FP16 from the value.

mkFp16Decl

fun mkFp16Decl(value: Float): KFp16Decl

mkFp16NaN

fun mkFp16NaN(): KFp16Value

Create FP16 NaN value.

mkFp16Sort

fun mkFp16Sort(): KFp16Sort

Create a 16-bit IEEE floating point sort (_ FloatingPoint 5 11).

mkFp32

fun mkFp32(value: Float): KFp32Value

Create FP32 from the value.

mkFp32Decl

fun mkFp32Decl(value: Float): KFp32Decl

mkFp32NaN

fun mkFp32NaN(): KFp32Value

Create FP32 NaN value.

mkFp32Sort

fun mkFp32Sort(): KFp32Sort

Create a 32-bit IEEE floating point sort (_ FloatingPoint 8 24).

mkFp64

fun mkFp64(value: Double): KFp64Value

Create FP64 from the value.

mkFp64Decl

fun mkFp64Decl(value: Double): KFp64Decl

mkFp64NaN

fun mkFp64NaN(): KFp64Value

Create FP64 NaN value.

mkFp64Sort

fun mkFp64Sort(): KFp64Sort

Create a 64-bit IEEE floating point sort (_ FloatingPoint 11 53).

mkFpAbsDecl

fun <T : KFpSort> mkFpAbsDecl(valueSort: T): KFpAbsDecl<T>

mkFpAbsExpr

open fun <T : KFpSort> mkFpAbsExpr(value: KExpr<T>): KExpr<T>

Create Fp absolute value (fp.abs) expression.

mkFpAbsExprNoSimplify

open fun <T : KFpSort> mkFpAbsExprNoSimplify(value: KExpr<T>): KFpAbsExpr<T>

Create Fp absolute value (fp.abs) expression.

mkFpAddDecl

fun <T : KFpSort> mkFpAddDecl(roundingMode: KFpRoundingModeSort, arg0Sort: T, arg1Sort: T): KFpAddDecl<T>

mkFpAddExpr

open fun <T : KFpSort> mkFpAddExpr(roundingMode: KExpr<KFpRoundingModeSort>, arg0: KExpr<T>, arg1: KExpr<T>): KExpr<T>

Create Fp addition (fp.add) expression. The result is rounded according to the provided roundingMode.

mkFpAddExprNoSimplify

open fun <T : KFpSort> mkFpAddExprNoSimplify(roundingMode: KExpr<KFpRoundingModeSort>, arg0: KExpr<T>, arg1: KExpr<T>): KFpAddExpr<T>

Create Fp addition (fp.add) expression. The result is rounded according to the provided roundingMode.

mkFpBiased

fun <T : KFpSort> mkFpBiased(significand: KBitVecValue<*>, biasedExponent: KBitVecValue<*>, signBit: Boolean, sort: T): KFpValue<T>

fun <T : KFpSort> mkFpBiased(significand: Int, biasedExponent: Int, signBit: Boolean, sort: T): KFpValue<T>

fun <T : KFpSort> mkFpBiased(significand: Long, biasedExponent: Long, signBit: Boolean, sort: T): KFpValue<T>

mkFpCustomSize

fun <T : KFpSort> mkFpCustomSize(unbiasedExponent: KBitVecValue<out KBvSort>, significand: KBitVecValue<out KBvSort>, signBit: Boolean): KFpValue<T>

fun <T : KFpSort> mkFpCustomSize(exponentSize: UInt, significandSize: UInt, unbiasedExponent: KBitVecValue<*>, significand: KBitVecValue<*>, signBit: Boolean): KFpValue<T>

Create FP with a custom size from the IEEE binary representation. Important: unbiasedExponent here is an unbiased value.

mkFpCustomSizeBiased

fun <T : KFpSort> mkFpCustomSizeBiased(significandSize: UInt, exponentSize: UInt, significand: KBitVecValue<*>, biasedExponent: KBitVecValue<*>, signBit: Boolean): KFpValue<T>

Create FP with a custom size from the IEEE binary representation. Important: biasedExponent here is an biased value.

mkFpCustomSizeDecl

fun <T : KFpSort> mkFpCustomSizeDecl(significandSize: UInt, exponentSize: UInt, significand: KBitVecValue<*>, unbiasedExponent: KBitVecValue<*>, signBit: Boolean): KFpDecl<T>

mkFpCustomSizeDeclBiased

fun <T : KFpSort> mkFpCustomSizeDeclBiased(significandSize: UInt, exponentSize: UInt, significand: KBitVecValue<*>, biasedExponent: KBitVecValue<*>, signBit: Boolean): KFpDecl<T>

mkFpDivDecl

fun <T : KFpSort> mkFpDivDecl(roundingMode: KFpRoundingModeSort, arg0Sort: T, arg1Sort: T): KFpDivDecl<T>

mkFpDivExpr

open fun <T : KFpSort> mkFpDivExpr(roundingMode: KExpr<KFpRoundingModeSort>, arg0: KExpr<T>, arg1: KExpr<T>): KExpr<T>

Create Fp division (fp.div) expression. The result is rounded according to the provided roundingMode.

mkFpDivExprNoSimplify

open fun <T : KFpSort> mkFpDivExprNoSimplify(roundingMode: KExpr<KFpRoundingModeSort>, arg0: KExpr<T>, arg1: KExpr<T>): KFpDivExpr<T>

Create Fp division (fp.div) expression. The result is rounded according to the provided roundingMode.

mkFpEqualDecl

fun <T : KFpSort> mkFpEqualDecl(arg0Sort: T, arg1Sort: T): KFpEqualDecl<T>

mkFpEqualExpr

open fun <T : KFpSort> mkFpEqualExpr(arg0: KExpr<T>, arg1: KExpr<T>): KExpr<KBoolSort>

Create Fp equality comparison (fp.eq) expression. Checks arguments equality using IEEE 754-2008 rules.

mkFpEqualExprNoSimplify

open fun <T : KFpSort> mkFpEqualExprNoSimplify(arg0: KExpr<T>, arg1: KExpr<T>): KFpEqualExpr<T>

Create Fp equality comparison (fp.eq) expression. Checks arguments equality using IEEE 754-2008 rules.

mkFpFromBvDecl

fun <T : KFpSort> mkFpFromBvDecl(signSort: KBv1Sort, expSort: KBvSort, significandSort: KBvSort): KFpFromBvDecl<T>

mkFpFromBvExpr

open fun <T : KFpSort> mkFpFromBvExpr(sign: KExpr<KBv1Sort>, biasedExponent: KExpr<out KBvSort>, significand: KExpr<out KBvSort>): KExpr<T>

Create Fp from IEEE BitVec expressions.

mkFpFromBvExprNoSimplify

open fun <T : KFpSort> mkFpFromBvExprNoSimplify(sign: KExpr<KBv1Sort>, biasedExponent: KExpr<out KBvSort>, significand: KExpr<out KBvSort>): KFpFromBvExpr<T>

Create Fp from IEEE BitVec expressions.

mkFpFusedMulAddDecl

fun <T : KFpSort> mkFpFusedMulAddDecl(roundingMode: KFpRoundingModeSort, arg0Sort: T, arg1Sort: T, arg2Sort: T): KFpFusedMulAddDecl<T>

mkFpFusedMulAddExpr

open fun <T : KFpSort> mkFpFusedMulAddExpr(roundingMode: KExpr<KFpRoundingModeSort>, arg0: KExpr<T>, arg1: KExpr<T>, arg2: KExpr<T>): KExpr<T>

Create Fp fused multiplication and addition (fp.fma) expression. Computes (arg0 * arg1) + arg2. The result is rounded according to the provided roundingMode.

mkFpFusedMulAddExprNoSimplify

open fun <T : KFpSort> mkFpFusedMulAddExprNoSimplify(roundingMode: KExpr<KFpRoundingModeSort>, arg0: KExpr<T>, arg1: KExpr<T>, arg2: KExpr<T>): KFpFusedMulAddExpr<T>

Create Fp fused multiplication and addition (fp.fma) expression. Computes (arg0 * arg1) + arg2. The result is rounded according to the provided roundingMode.

mkFpGreaterDecl

fun <T : KFpSort> mkFpGreaterDecl(arg0Sort: T, arg1Sort: T): KFpGreaterDecl<T>

mkFpGreaterExpr

open fun <T : KFpSort> mkFpGreaterExpr(arg0: KExpr<T>, arg1: KExpr<T>): KExpr<KBoolSort>

Create Fp greater comparison (fp.gt) expression.

mkFpGreaterExprNoSimplify

open fun <T : KFpSort> mkFpGreaterExprNoSimplify(arg0: KExpr<T>, arg1: KExpr<T>): KFpGreaterExpr<T>

Create Fp greater comparison (fp.gt) expression.

mkFpGreaterOrEqualDecl

fun <T : KFpSort> mkFpGreaterOrEqualDecl(arg0Sort: T, arg1Sort: T): KFpGreaterOrEqualDecl<T>

mkFpGreaterOrEqualExpr

open fun <T : KFpSort> mkFpGreaterOrEqualExpr(arg0: KExpr<T>, arg1: KExpr<T>): KExpr<KBoolSort>

Create Fp greater-or-equal comparison (fp.geq) expression.

mkFpGreaterOrEqualExprNoSimplify

open fun <T : KFpSort> mkFpGreaterOrEqualExprNoSimplify(arg0: KExpr<T>, arg1: KExpr<T>): KFpGreaterOrEqualExpr<T>

Create Fp greater-or-equal comparison (fp.geq) expression.

mkFpInf

fun <T : KFpSort> mkFpInf(signBit: Boolean, sort: T): KFpValue<T>

Create Fp Inf value with signBit sign.

mkFpIsInfiniteDecl

fun <T : KFpSort> mkFpIsInfiniteDecl(valueSort: T): KFpIsInfiniteDecl<T>

mkFpIsInfiniteExpr

open fun <T : KFpSort> mkFpIsInfiniteExpr(value: KExpr<T>): KExpr<KBoolSort>

Create Fp is-inf check (fp.isInfinite) expression.

mkFpIsInfiniteExprNoSimplify

open fun <T : KFpSort> mkFpIsInfiniteExprNoSimplify(value: KExpr<T>): KFpIsInfiniteExpr<T>

Create Fp is-inf check (fp.isInfinite) expression.

mkFpIsNaNDecl

fun <T : KFpSort> mkFpIsNaNDecl(valueSort: T): KFpIsNaNDecl<T>

mkFpIsNaNExpr

open fun <T : KFpSort> mkFpIsNaNExpr(value: KExpr<T>): KExpr<KBoolSort>

Create Fp is-nan check (fp.isNaN) expression.

mkFpIsNaNExprNoSimplify

open fun <T : KFpSort> mkFpIsNaNExprNoSimplify(value: KExpr<T>): KFpIsNaNExpr<T>

Create Fp is-nan check (fp.isNaN) expression.

mkFpIsNegativeDecl

fun <T : KFpSort> mkFpIsNegativeDecl(valueSort: T): KFpIsNegativeDecl<T>

mkFpIsNegativeExpr

open fun <T : KFpSort> mkFpIsNegativeExpr(value: KExpr<T>): KExpr<KBoolSort>

Create Fp is-negative check (fp.isNegative) expression.

mkFpIsNegativeExprNoSimplify

open fun <T : KFpSort> mkFpIsNegativeExprNoSimplify(value: KExpr<T>): KFpIsNegativeExpr<T>

Create Fp is-negative check (fp.isNegative) expression.

mkFpIsNormalDecl

fun <T : KFpSort> mkFpIsNormalDecl(valueSort: T): KFpIsNormalDecl<T>

mkFpIsNormalExpr

open fun <T : KFpSort> mkFpIsNormalExpr(value: KExpr<T>): KExpr<KBoolSort>

Create Fp is-normal check (fp.isNormal) expression.

mkFpIsNormalExprNoSimplify

open fun <T : KFpSort> mkFpIsNormalExprNoSimplify(value: KExpr<T>): KFpIsNormalExpr<T>

Create Fp is-normal check (fp.isNormal) expression.

mkFpIsPositiveDecl

fun <T : KFpSort> mkFpIsPositiveDecl(valueSort: T): KFpIsPositiveDecl<T>

mkFpIsPositiveExpr

open fun <T : KFpSort> mkFpIsPositiveExpr(value: KExpr<T>): KExpr<KBoolSort>

Create Fp is-positive check (fp.isPositive) expression.

mkFpIsPositiveExprNoSimplify

open fun <T : KFpSort> mkFpIsPositiveExprNoSimplify(value: KExpr<T>): KFpIsPositiveExpr<T>

Create Fp is-positive check (fp.isPositive) expression.

mkFpIsSubnormalDecl

fun <T : KFpSort> mkFpIsSubnormalDecl(valueSort: T): KFpIsSubnormalDecl<T>

mkFpIsSubnormalExpr

open fun <T : KFpSort> mkFpIsSubnormalExpr(value: KExpr<T>): KExpr<KBoolSort>

Create Fp is-subnormal check (fp.isSubnormal) expression.

mkFpIsSubnormalExprNoSimplify

open fun <T : KFpSort> mkFpIsSubnormalExprNoSimplify(value: KExpr<T>): KFpIsSubnormalExpr<T>

Create Fp is-subnormal check (fp.isSubnormal) expression.

mkFpIsZeroDecl

fun <T : KFpSort> mkFpIsZeroDecl(valueSort: T): KFpIsZeroDecl<T>

mkFpIsZeroExpr

open fun <T : KFpSort> mkFpIsZeroExpr(value: KExpr<T>): KExpr<KBoolSort>

Create Fp is-zero check (fp.isZero) expression.

mkFpIsZeroExprNoSimplify

open fun <T : KFpSort> mkFpIsZeroExprNoSimplify(value: KExpr<T>): KFpIsZeroExpr<T>

Create Fp is-zero check (fp.isZero) expression.

mkFpLessDecl

fun <T : KFpSort> mkFpLessDecl(arg0Sort: T, arg1Sort: T): KFpLessDecl<T>

mkFpLessExpr

open fun <T : KFpSort> mkFpLessExpr(arg0: KExpr<T>, arg1: KExpr<T>): KExpr<KBoolSort>

Create Fp less comparison (fp.lt) expression.

mkFpLessExprNoSimplify

open fun <T : KFpSort> mkFpLessExprNoSimplify(arg0: KExpr<T>, arg1: KExpr<T>): KFpLessExpr<T>

Create Fp less comparison (fp.lt) expression.

mkFpLessOrEqualDecl

fun <T : KFpSort> mkFpLessOrEqualDecl(arg0Sort: T, arg1Sort: T): KFpLessOrEqualDecl<T>

mkFpLessOrEqualExpr

open fun <T : KFpSort> mkFpLessOrEqualExpr(arg0: KExpr<T>, arg1: KExpr<T>): KExpr<KBoolSort>

Create Fp less-or-equal comparison (fp.leq) expression.

mkFpLessOrEqualExprNoSimplify

open fun <T : KFpSort> mkFpLessOrEqualExprNoSimplify(arg0: KExpr<T>, arg1: KExpr<T>): KFpLessOrEqualExpr<T>

Create Fp less-or-equal comparison (fp.leq) expression.

mkFpMaxDecl

fun <T : KFpSort> mkFpMaxDecl(arg0Sort: T, arg1Sort: T): KFpMaxDecl<T>

mkFpMaxExpr

open fun <T : KFpSort> mkFpMaxExpr(arg0: KExpr<T>, arg1: KExpr<T>): KExpr<T>

Create Fp maximum (fp.max) expression.

mkFpMaxExprNoSimplify

open fun <T : KFpSort> mkFpMaxExprNoSimplify(arg0: KExpr<T>, arg1: KExpr<T>): KFpMaxExpr<T>

Create Fp maximum (fp.max) expression.

mkFpMinDecl

fun <T : KFpSort> mkFpMinDecl(arg0Sort: T, arg1Sort: T): KFpMinDecl<T>

mkFpMinExpr

open fun <T : KFpSort> mkFpMinExpr(arg0: KExpr<T>, arg1: KExpr<T>): KExpr<T>

Create Fp minimum (fp.min) expression.

mkFpMinExprNoSimplify

open fun <T : KFpSort> mkFpMinExprNoSimplify(arg0: KExpr<T>, arg1: KExpr<T>): KFpMinExpr<T>

Create Fp minimum (fp.min) expression.

mkFpMulDecl

fun <T : KFpSort> mkFpMulDecl(roundingMode: KFpRoundingModeSort, arg0Sort: T, arg1Sort: T): KFpMulDecl<T>

mkFpMulExpr

open fun <T : KFpSort> mkFpMulExpr(roundingMode: KExpr<KFpRoundingModeSort>, arg0: KExpr<T>, arg1: KExpr<T>): KExpr<T>

Create Fp multiplication (fp.mul) expression. The result is rounded according to the provided roundingMode.

mkFpMulExprNoSimplify

open fun <T : KFpSort> mkFpMulExprNoSimplify(roundingMode: KExpr<KFpRoundingModeSort>, arg0: KExpr<T>, arg1: KExpr<T>): KFpMulExpr<T>

Create Fp multiplication (fp.mul) expression. The result is rounded according to the provided roundingMode.

mkFpNaN

fun <T : KFpSort> mkFpNaN(sort: T): KFpValue<T>

Create Fp NaN value.

mkFpNegationDecl

fun <T : KFpSort> mkFpNegationDecl(valueSort: T): KFpNegationDecl<T>

mkFpNegationExpr

open fun <T : KFpSort> mkFpNegationExpr(value: KExpr<T>): KExpr<T>

Create Fp negation (fp.neg) expression.

mkFpNegationExprNoSimplify

open fun <T : KFpSort> mkFpNegationExprNoSimplify(value: KExpr<T>): KFpNegationExpr<T>

Create Fp negation (fp.neg) expression.

mkFpRemDecl

fun <T : KFpSort> mkFpRemDecl(arg0Sort: T, arg1Sort: T): KFpRemDecl<T>

mkFpRemExpr

open fun <T : KFpSort> mkFpRemExpr(arg0: KExpr<T>, arg1: KExpr<T>): KExpr<T>

Create Fp IEEE remainder (fp.IEEERem) expression.

mkFpRemExprNoSimplify

open fun <T : KFpSort> mkFpRemExprNoSimplify(arg0: KExpr<T>, arg1: KExpr<T>): KFpRemExpr<T>

Create Fp IEEE remainder (fp.IEEERem) expression.

mkFpRoundingModeDecl

fun mkFpRoundingModeDecl(value: KFpRoundingMode): KFpRoundingModeDecl

mkFpRoundingModeExpr

fun mkFpRoundingModeExpr(value: KFpRoundingMode): KFpRoundingModeExpr

Create Fp rounding mode.

mkFpRoundingModeSort

fun mkFpRoundingModeSort(): KFpRoundingModeSort

Create a floating point rounding mode sort.

mkFpRoundToIntegralDecl

fun <T : KFpSort> mkFpRoundToIntegralDecl(roundingMode: KFpRoundingModeSort, valueSort: T): KFpRoundToIntegralDecl<T>

mkFpRoundToIntegralExpr

open fun <T : KFpSort> mkFpRoundToIntegralExpr(roundingMode: KExpr<KFpRoundingModeSort>, value: KExpr<T>): KExpr<T>

Create Fp round to integral (fp.roundToIntegral) expression. The rounding is performed according to the provided roundingMode.

mkFpRoundToIntegralExprNoSimplify

open fun <T : KFpSort> mkFpRoundToIntegralExprNoSimplify(roundingMode: KExpr<KFpRoundingModeSort>, value: KExpr<T>): KFpRoundToIntegralExpr<T>

Create Fp round to integral (fp.roundToIntegral) expression. The rounding is performed according to the provided roundingMode.

mkFpSort

open fun mkFpSort(exponentBits: UInt, significandBits: UInt): KFpSort

Create an arbitrary precision IEEE floating point sort (_ FloatingPoint exponentBits).

mkFpSqrtDecl

fun <T : KFpSort> mkFpSqrtDecl(roundingMode: KFpRoundingModeSort, valueSort: T): KFpSqrtDecl<T>

mkFpSqrtExpr

open fun <T : KFpSort> mkFpSqrtExpr(roundingMode: KExpr<KFpRoundingModeSort>, value: KExpr<T>): KExpr<T>

Create Fp square root (fp.sqrt) expression. The result is rounded according to the provided roundingMode.

mkFpSqrtExprNoSimplify

open fun <T : KFpSort> mkFpSqrtExprNoSimplify(roundingMode: KExpr<KFpRoundingModeSort>, value: KExpr<T>): KFpSqrtExpr<T>

Create Fp square root (fp.sqrt) expression. The result is rounded according to the provided roundingMode.

mkFpSubDecl

fun <T : KFpSort> mkFpSubDecl(roundingMode: KFpRoundingModeSort, arg0Sort: T, arg1Sort: T): KFpSubDecl<T>

mkFpSubExpr

open fun <T : KFpSort> mkFpSubExpr(roundingMode: KExpr<KFpRoundingModeSort>, arg0: KExpr<T>, arg1: KExpr<T>): KExpr<T>

Create Fp subtraction (fp.sub) expression. The result is rounded according to the provided roundingMode.

mkFpSubExprNoSimplify

open fun <T : KFpSort> mkFpSubExprNoSimplify(roundingMode: KExpr<KFpRoundingModeSort>, arg0: KExpr<T>, arg1: KExpr<T>): KFpSubExpr<T>

Create Fp subtraction (fp.sub) expression. The result is rounded according to the provided roundingMode.

mkFpToBvDecl

fun <T : KFpSort> mkFpToBvDecl(roundingMode: KFpRoundingModeSort, valueSort: T, bvSize: Int, isSigned: Boolean): KFpToBvDecl<T>

mkFpToBvExpr

open fun <T : KFpSort> mkFpToBvExpr(roundingMode: KExpr<KFpRoundingModeSort>, value: KExpr<T>, bvSize: Int, isSigned: Boolean): KExpr<KBvSort>

Create Fp to BitVec conversion (fp.to_sbv, fp.to_ubv) expression. Provided Fp value is rounded to the nearest integral according to the roundingMode.

mkFpToBvExprNoSimplify

open fun <T : KFpSort> mkFpToBvExprNoSimplify(roundingMode: KExpr<KFpRoundingModeSort>, value: KExpr<T>, bvSize: Int, isSigned: Boolean): KFpToBvExpr<T>

Create Fp to BitVec conversion (fp.to_sbv, fp.to_ubv) expression. Provided Fp value is rounded to the nearest integral according to the roundingMode.

mkFpToFpDecl

fun <T : KFpSort> mkFpToFpDecl(sort: T, rm: KFpRoundingModeSort, value: KFpSort): KFpToFpDecl<T>

mkFpToFpExpr

open fun <T : KFpSort> mkFpToFpExpr(sort: T, roundingMode: KExpr<KFpRoundingModeSort>, value: KExpr<out KFpSort>): KExpr<T>

Create Fp to another Fp. Rounding is performed according to the roundingMode.

mkFpToFpExprNoSimplify

open fun <T : KFpSort> mkFpToFpExprNoSimplify(sort: T, roundingMode: KExpr<KFpRoundingModeSort>, value: KExpr<out KFpSort>): KFpToFpExpr<T>

Create Fp to another Fp. Rounding is performed according to the roundingMode.

mkFpToIEEEBvDecl

fun <T : KFpSort> mkFpToIEEEBvDecl(valueSort: T): KFpToIEEEBvDecl<T>

mkFpToIEEEBvExpr

open fun <T : KFpSort> mkFpToIEEEBvExpr(value: KExpr<T>): KExpr<KBvSort>

Create Fp to IEEE BitVec conversion expression. Converts Fp value to the corresponding IEEE 754-2008 binary format.

mkFpToIEEEBvExprNoSimplify

open fun <T : KFpSort> mkFpToIEEEBvExprNoSimplify(value: KExpr<T>): KFpToIEEEBvExpr<T>

Create Fp to IEEE BitVec conversion expression. Converts Fp value to the corresponding IEEE 754-2008 binary format.

mkFpToRealDecl

fun <T : KFpSort> mkFpToRealDecl(valueSort: T): KFpToRealDecl<T>

mkFpToRealExpr

open fun <T : KFpSort> mkFpToRealExpr(value: KExpr<T>): KExpr<KRealSort>

Create Fp to Real conversion (fp.to_real) expression.

mkFpToRealExprNoSimplify

open fun <T : KFpSort> mkFpToRealExprNoSimplify(value: KExpr<T>): KFpToRealExpr<T>

Create Fp to Real conversion (fp.to_real) expression.

mkFpZero

fun <T : KFpSort> mkFpZero(signBit: Boolean, sort: T): KFpValue<T>

Create Fp zero value with signBit sign.

mkFreshConst

fun <T : KSort> mkFreshConst(name: String, sort: T): KApp<T, *>

Create a fresh constant with name prefix name and sort sort.

mkFreshConstDecl

fun <T : KSort> mkFreshConstDecl(name: String, sort: T): KConstDecl<T>

mkFreshFuncDecl

fun <T : KSort> mkFreshFuncDecl(name: String, sort: T, args: List<KSort>): KFuncDecl<T>

mkFuncDecl

fun <T : KSort> mkFuncDecl(name: String, sort: T, args: List<KSort>): KFuncDecl<T>

mkFunctionAsArray

open fun <A : KArraySortBase<R>, R : KSort> mkFunctionAsArray(sort: A, function: KFuncDecl<R>): KFunctionAsArray<A, R>

Create a function-as-array expression (_ as-array function).

mkImplies

open fun mkImplies(p: KExpr<KBoolSort>, q: KExpr<KBoolSort>): KExpr<KBoolSort>

Create boolean => (implication) expression.

mkImpliesDecl

fun mkImpliesDecl(): KImpliesDecl

mkImpliesNoSimplify

open fun mkImpliesNoSimplify(p: KExpr<KBoolSort>, q: KExpr<KBoolSort>): KImpliesExpr

Create boolean => (implication) expression.

mkIntMod

open fun mkIntMod(lhs: KExpr<KIntSort>, rhs: KExpr<KIntSort>): KExpr<KIntSort>

Create an Int mod expression.

mkIntModDecl

fun mkIntModDecl(): KIntModDecl

mkIntModNoSimplify

open fun mkIntModNoSimplify(lhs: KExpr<KIntSort>, rhs: KExpr<KIntSort>): KModIntExpr

Create an Int mod expression.

mkIntNum

fun mkIntNum(value: BigInteger): KIntNumExpr

fun mkIntNum(value: Int): KIntNumExpr

fun mkIntNum(value: Long): KIntNumExpr

fun mkIntNum(value: String): KIntNumExpr

Create an Int value.

mkIntNumDecl

fun mkIntNumDecl(value: String): KIntNumDecl

mkIntRem

open fun mkIntRem(lhs: KExpr<KIntSort>, rhs: KExpr<KIntSort>): KExpr<KIntSort>

Create an Int rem expression. The result value is either (mod lhs rhs) when rhs >= 0 and (neg (mod lhs rhs)) otherwise. The result sign matches the rhs sign.

mkIntRemDecl

fun mkIntRemDecl(): KIntRemDecl

mkIntRemNoSimplify

open fun mkIntRemNoSimplify(lhs: KExpr<KIntSort>, rhs: KExpr<KIntSort>): KRemIntExpr

Create an Int rem expression.

mkIntSort

fun mkIntSort(): KIntSort

Create an Int sort.

mkIntToReal

open fun mkIntToReal(arg: KExpr<KIntSort>): KExpr<KRealSort>

Convert an Int expression to a corresponding Real expression.

mkIntToRealDecl

fun mkIntToRealDecl(): KIntToRealDecl

mkIntToRealNoSimplify

open fun mkIntToRealNoSimplify(arg: KExpr<KIntSort>): KToRealIntExpr

Convert an Int expression to a corresponding Real expression.

mkIte

open fun <T : KSort> mkIte(condition: KExpr<KBoolSort>, trueBranch: KExpr<T>, falseBranch: KExpr<T>): KExpr<T>

Create ITE (if-then-else) expression.

mkIteDecl

fun <T : KSort> mkIteDecl(arg: T): KIteDecl<T>

mkIteNoSimplify

open fun <T : KSort> mkIteNoSimplify(condition: KExpr<KBoolSort>, trueBranch: KExpr<T>, falseBranch: KExpr<T>): KIteExpr<T>

Create ITE (if-then-else) expression.

mkNot

open fun mkNot(arg: KExpr<KBoolSort>): KExpr<KBoolSort>

Create boolean NOT expression.

mkNotDecl

fun mkNotDecl(): KNotDecl

mkNotNoSimplify

open fun mkNotNoSimplify(arg: KExpr<KBoolSort>): KNotExpr

Create boolean NOT expression.

mkOr

fun mkOr(vararg args: KExpr<KBoolSort>): KExpr<KBoolSort>

@JvmOverloads

open fun mkOr(args: List<KExpr<KBoolSort>>, flat: Boolean = true, order: Boolean = true): KExpr<KBoolSort>

Create boolean OR expression.

@JvmOverloads

open fun mkOr(lhs: KExpr<KBoolSort>, rhs: KExpr<KBoolSort>, flat: Boolean = true, order: Boolean = true): KExpr<KBoolSort>

Create boolean binary OR expression.

mkOrDecl

fun mkOrDecl(): KOrDecl

mkOrNoSimplify

open fun mkOrNoSimplify(args: List<KExpr<KBoolSort>>): KOrExpr

Create boolean OR expression.

open fun mkOrNoSimplify(lhs: KExpr<KBoolSort>, rhs: KExpr<KBoolSort>): KOrBinaryExpr

Create boolean binary OR expression.

mkRealIsInt

open fun mkRealIsInt(arg: KExpr<KRealSort>): KExpr<KBoolSort>

Check whether the given Real expression has an integer value.

mkRealIsIntDecl

fun mkRealIsIntDecl(): KRealIsIntDecl

mkRealIsIntNoSimplify

open fun mkRealIsIntNoSimplify(arg: KExpr<KRealSort>): KIsIntRealExpr

Check whether the given Real expression has an integer value.

mkRealNum

fun mkRealNum(numerator: KIntNumExpr): KRealNumExpr

fun mkRealNum(numerator: Int): KRealNumExpr

fun mkRealNum(numerator: Long): KRealNumExpr

fun mkRealNum(numerator: KIntNumExpr, denominator: KIntNumExpr): KRealNumExpr

fun mkRealNum(numerator: Int, denominator: Int): KRealNumExpr

fun mkRealNum(numerator: Long, denominator: Long): KRealNumExpr

Create a Real value.

fun mkRealNum(value: String): KRealNumExpr

Create a Real value from a string of the form "123/456".

mkRealNumDecl

fun mkRealNumDecl(value: String): KRealNumDecl

mkRealSort

fun mkRealSort(): KRealSort

Create a Real sort.

mkRealToFpDecl

fun <T : KFpSort> mkRealToFpDecl(sort: T, rm: KFpRoundingModeSort, value: KRealSort): KRealToFpDecl<T>

mkRealToFpExpr

open fun <T : KFpSort> mkRealToFpExpr(sort: T, roundingMode: KExpr<KFpRoundingModeSort>, value: KExpr<KRealSort>): KExpr<T>

Create Fp from Real expression. Rounding is performed according to the roundingMode.

mkRealToFpExprNoSimplify

open fun <T : KFpSort> mkRealToFpExprNoSimplify(sort: T, roundingMode: KExpr<KFpRoundingModeSort>, value: KExpr<KRealSort>): KRealToFpExpr<T>

Create Fp from Real expression. Rounding is performed according to the roundingMode.

mkRealToInt

open fun mkRealToInt(arg: KExpr<KRealSort>): KExpr<KIntSort>

Convert Real expression to an Int expression (floor division).

mkRealToIntDecl

fun mkRealToIntDecl(): KRealToIntDecl

mkRealToIntNoSimplify

open fun mkRealToIntNoSimplify(arg: KExpr<KRealSort>): KToIntRealExpr

Convert Real expression to an Int expression (floor division).

mkTrue

fun mkTrue(): KTrue

Create boolean True constant.

mkTrueDecl

fun mkTrueDecl(): KTrueDecl

mkUninterpretedSort

open fun mkUninterpretedSort(name: String): KUninterpretedSort

Create an uninterpreted sort named name.

mkUninterpretedSortValue

open fun mkUninterpretedSortValue(sort: KUninterpretedSort, valueIdx: Int): KUninterpretedSortValue

Create uninterpreted sort value.

mkUninterpretedSortValueDecl

fun mkUninterpretedSortValueDecl(sort: KUninterpretedSort, valueIdx: Int): KUninterpretedSortValueDecl

mkUniversalQuantifier

open fun mkUniversalQuantifier(body: KExpr<KBoolSort>, bounds: List<KDecl<*>>): KUniversalQuantifier

Create universal quantifier (forall).

mkXor

open fun mkXor(a: KExpr<KBoolSort>, b: KExpr<KBoolSort>): KExpr<KBoolSort>

Create boolean XOR expression.

mkXorDecl

fun mkXorDecl(): KXorDecl

mkXorNoSimplify

open fun mkXorNoSimplify(a: KExpr<KBoolSort>, b: KExpr<KBoolSort>): KXorExpr

Create boolean XOR expression.

mod

infix fun KExpr<KIntSort>.mod(rhs: KExpr<KIntSort>): KExpr<KIntSort>

neq

infix fun <T : KSort> KExpr<T>.neq(other: KExpr<T>): KExpr<KBoolSort>

not

operator fun KExpr<KBoolSort>.not(): KExpr<KBoolSort>

infix fun KExpr<KBoolSort>.or(other: KExpr<KBoolSort>): KExpr<KBoolSort>

plus

operator fun <T : KArithSort> KExpr<T>.plus(other: KExpr<T>): KExpr<T>

power

fun <T : KArithSort> KExpr<T>.power(other: KExpr<T>): KExpr<T>

realSortDefaultValue

open fun realSortDefaultValue(): KExpr<KRealSort>

reductionAnd

fun <T : KBvSort> KExpr<T>.reductionAnd(): KExpr<KBv1Sort>

reductionOr

fun <T : KBvSort> KExpr<T>.reductionOr(): KExpr<KBv1Sort>

rem

infix fun KExpr<KIntSort>.rem(rhs: KExpr<KIntSort>): KExpr<KIntSort>

select

fun <D : KSort, R : KSort> KExpr<KArraySort<D, R>>.select(index: KExpr<D>): KExpr<R>

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

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

store

fun <D : KSort, R : KSort> KExpr<KArraySort<D, R>>.store(index: KExpr<D>, value: KExpr<R>): KExpr<KArraySort<D, R>>

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

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

times

operator fun <T : KArithSort> KExpr<T>.times(other: KExpr<T>): KExpr<T>

toBv

fun Boolean.toBv(): KBitVec1Value

fun Byte.toBv(): KBitVec8Value

fun Int.toBv(): KBitVec32Value

fun Long.toBv(): KBitVec64Value

fun Short.toBv(): KBitVec16Value

fun UByte.toBv(): KBitVec8Value

fun UInt.toBv(): KBitVec32Value

fun ULong.toBv(): KBitVec64Value

fun UShort.toBv(): KBitVec16Value

fun <T : KBvSort> Boolean.toBv(sort: T): KBitVecValue<T>

fun Boolean.toBv(sizeBits: UInt): KBitVecValue<KBvSort>

fun <T : KBvSort> Byte.toBv(sort: T): KBitVecValue<T>

fun Byte.toBv(sizeBits: UInt): KBitVecValue<KBvSort>

fun <T : KBvSort> Int.toBv(sort: T): KBitVecValue<T>

fun Int.toBv(sizeBits: UInt): KBitVecValue<KBvSort>

fun <T : KBvSort> Long.toBv(sort: T): KBitVecValue<T>

fun Long.toBv(sizeBits: UInt): KBitVecValue<KBvSort>

fun <T : KBvSort> Short.toBv(sort: T): KBitVecValue<T>

fun Short.toBv(sizeBits: UInt): KBitVecValue<KBvSort>

toFp

fun Double.toFp(sort: KFpSort = mkFp64Sort()): KFpValue<KFpSort>

fun Float.toFp(sort: KFpSort = mkFp32Sort()): KFpValue<KFpSort>

toIntExpr

fun KExpr<KRealSort>.toIntExpr(): KExpr<KIntSort>

toRealExpr

fun KExpr<KIntSort>.toRealExpr(): KExpr<KRealSort>

unaryMinus

operator fun <T : KArithSort> KExpr<T>.unaryMinus(): KExpr<T>

uninterpretedSortDefaultValue

open fun uninterpretedSortDefaultValue(sort: KUninterpretedSort): KUninterpretedSortValue

xor

infix fun KExpr<KBoolSort>.xor(other: KExpr<KBoolSort>): KExpr<KBoolSort>

Properties

astManagementMode

val astManagementMode: KContext.AstManagementMode

boolSort

val boolSort: KBoolSort

bv16Sort

val bv16Sort: KBv16Sort

bv1Sort

val bv1Sort: KBv1Sort

bv32Sort

val bv32Sort: KBv32Sort

bv64Sort

val bv64Sort: KBv64Sort

bv8Sort

val bv8Sort: KBv8Sort

defaultValueSampler

val defaultValueSampler: KSortVisitor<KExpr<*>>

expr

val Boolean.expr: KExpr<KBoolSort>

val Int.expr: KIntNumExpr

val Long.expr: KIntNumExpr

val BigInteger.expr: KIntNumExpr

val Float.expr: KFp32Value

val Double.expr: KFp64Value

falseExpr

val falseExpr: KFalse

fp16Sort

val fp16Sort: KFp16Sort

fp32Sort

val fp32Sort: KFp32Sort

fp64Sort

val fp64Sort: KFp64Sort

intSort

val intSort: KIntSort

isActive

var isActive: Boolean = true

KContext and all created expressions are only valid as long as the context is active (not closed).

operationMode

val operationMode: KContext.OperationMode

printerParams

val printerParams: PrinterParams

realSort

val realSort: KRealSort

simplificationMode

val simplificationMode: KContext.SimplificationMode

stringRepr

val KAst.stringRepr: String

String representations are not cached since it requires a lot of memory. For example, (and a b) will store a full copy of a and b string representations

trueExpr

val trueExpr: KTrue

Extensions

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>

bvMaxValueSigned

@JvmStatic

fun <T : KBvSort> KContext.bvMaxValueSigned(size: UInt): KBitVecValue<T>

bvMaxValueUnsigned

@JvmStatic

fun <T : KBvSort> KContext.bvMaxValueUnsigned(size: UInt): KBitVecValue<T>

bvMinValueSigned

@JvmStatic

fun <T : KBvSort> KContext.bvMinValueSigned(size: UInt): KBitVecValue<T>

bvOne

@JvmStatic

fun <T : KBvSort> KContext.bvOne(size: UInt): KBitVecValue<T>

bvValue

@JvmStatic

fun <T : KBvSort> KContext.bvValue(size: UInt, value: Int): KBitVecValue<T>

bvZero

@JvmStatic

fun <T : KBvSort> KContext.bvZero(size: UInt): KBitVecValue<T>

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>

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>

fpInfExponentBiased

fun KContext.fpInfExponentBiased(sort: KFpSort): KBitVecValue<KBvSort>

fpInfSignificand

fun KContext.fpInfSignificand(sort: KFpSort): KBitVecValue<KBvSort>

fpNaNExponentBiased

fun KContext.fpNaNExponentBiased(sort: KFpSort): KBitVecValue<KBvSort>

fpNaNSignificand

fun KContext.fpNaNSignificand(sort: KFpSort): KBitVecValue<KBvSort>

fpZeroExponentBiased

fun KContext.fpZeroExponentBiased(sort: KFpSort): KBitVecValue<KBvSort>

fpZeroSignificand

fun KContext.fpZeroSignificand(sort: KFpSort): KBitVecValue<KBvSort>

mkFpMaxValue

fun <T : KFpSort> KContext.mkFpMaxValue(sort: T, signBit: Boolean): KFpValue<T>

mkFpOne

fun <T : KFpSort> KContext.mkFpOne(sort: T, signBit: Boolean): KFpValue<T>

numericValue

fun <T : KArithSort> KContext.numericValue(realValue: ArithUtils.RealValue, sort: T): KExpr<T>

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(lhs: KExpr<KBoolSort>, rhs: KExpr<KBoolSort>, flat: Boolean = true, order: Boolean = true): KExpr<KBoolSort>

fun KContext.simplifyAnd(args: List<KExpr<KBoolSort>>, flat: Boolean = true, order: Boolean = true): 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 <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>

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(lhs: KExpr<KBoolSort>, rhs: KExpr<KBoolSort>, flat: Boolean = true, order: Boolean = true): KExpr<KBoolSort>

fun KContext.simplifyOr(args: List<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>

tryMergeBvConcatExtract

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

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>?