From 5f9b78011f6a1562aa2ccda41e34090493d4660b Mon Sep 17 00:00:00 2001 From: saloed Date: Tue, 6 Jun 2023 01:29:12 +0300 Subject: [PATCH 1/6] KContext comments --- ksmt-core/src/main/kotlin/io/ksmt/KContext.kt | 388 +++++++++++++++++- 1 file changed, 382 insertions(+), 6 deletions(-) diff --git a/ksmt-core/src/main/kotlin/io/ksmt/KContext.kt b/ksmt-core/src/main/kotlin/io/ksmt/KContext.kt index 147c987a2..6d1d8b261 100644 --- a/ksmt-core/src/main/kotlin/io/ksmt/KContext.kt +++ b/ksmt-core/src/main/kotlin/io/ksmt/KContext.kt @@ -518,6 +518,9 @@ open class KContext( val boolSort: KBoolSort = KBoolSort(this) + /** + * Create a Bool sort. + * */ fun mkBoolSort(): KBoolSort = boolSort private val arraySortCache = mkCache, KArraySort<*, *>>(operationMode) @@ -525,6 +528,9 @@ open class KContext( private val array3SortCache = mkCache, KArray3Sort<*, *, *, *>>(operationMode) private val arrayNSortCache = mkCache, KArrayNSort<*>>(operationMode) + /** + * Create an array sort (Array [domain] [range]). + * */ fun mkArraySort(domain: D, range: R): KArraySort = ensureContextActive { ensureContextMatch(domain, range) @@ -532,6 +538,9 @@ open class KContext( (arraySortCache.putIfAbsent(sort, sort) ?: sort).uncheckedCast() } + /** + * Create an array sort (Array [domain0] [domain1] [range]). + * */ fun mkArraySort(domain0: D0, domain1: D1, range: R): KArray2Sort = ensureContextActive { ensureContextMatch(domain0, domain1, range) @@ -539,6 +548,9 @@ open class KContext( (array2SortCache.putIfAbsent(sort, sort) ?: sort).uncheckedCast() } + /** + * Create an array sort (Array [domain0] [domain1] [domain2] [range]). + * */ fun mkArraySort( domain0: D0, domain1: D1, domain2: D2, range: R ): KArray3Sort = @@ -548,6 +560,10 @@ open class KContext( (array3SortCache.putIfAbsent(sort, sort) ?: sort).uncheckedCast() } + + /** + * Create a n-ary array sort (Array [domain]_0 ... [domain]_n [range]). + * */ fun mkArrayNSort(domain: List, range: R): KArrayNSort = ensureContextActive { ensureContextMatch(range) @@ -561,12 +577,18 @@ open class KContext( ensureContextActive { KIntSort(this) } } + /** + * Create an Int sort. + * */ fun mkIntSort(): KIntSort = intSortCache private val realSortCache by lazy { ensureContextActive { KRealSort(this) } } + /** + * Create a Real sort. + * */ fun mkRealSort(): KRealSort = realSortCache // bit-vec @@ -577,12 +599,34 @@ open class KContext( private val bv64SortCache: KBv64Sort by lazy { KBv64Sort(this) } private val bvCustomSizeSortCache = mkCache(operationMode) + /** + * Create a BitVec sort with 1 bit length (_ BitVec 1). + * */ fun mkBv1Sort(): KBv1Sort = bv1SortCache + + /** + * Create a BitVec sort with 8 bits length (_ BitVec 8). + * */ fun mkBv8Sort(): KBv8Sort = bv8SortCache + + /** + * Create a BitVec sort with 16 bits length (_ BitVec 16). + * */ fun mkBv16Sort(): KBv16Sort = bv16SortCache + + /** + * Create a BitVec sort with 32 bits length (_ BitVec 32). + * */ fun mkBv32Sort(): KBv32Sort = bv32SortCache + + /** + * Create a BitVec sort with 64 bits length (_ BitVec 64). + * */ fun mkBv64Sort(): KBv64Sort = bv64SortCache + /** + * Create a BitVec sort with [sizeBits] bits length (_ BitVec [sizeBits]). + * */ fun mkBvSort(sizeBits: UInt): KBvSort = ensureContextActive { when (sizeBits.toInt()) { 1 -> mkBv1Sort() @@ -596,6 +640,9 @@ open class KContext( } } + /** + * Create an uninterpreted sort named [name]. + * */ fun mkUninterpretedSort(name: String): KUninterpretedSort = ensureContextActive { KUninterpretedSort(name, this) @@ -608,11 +655,29 @@ open class KContext( private val fp128SortCache: KFp128Sort by lazy { KFp128Sort(this) } private val fpCustomSizeSortCache = mkCache, KFpSort>(operationMode) + /** + * Create a 16-bit IEEE floating point sort (_ FloatingPoint 5 11). + * */ fun mkFp16Sort(): KFp16Sort = fp16SortCache + + /** + * Create a 32-bit IEEE floating point sort (_ FloatingPoint 8 24). + * */ fun mkFp32Sort(): KFp32Sort = fp32SortCache + + /** + * Create a 64-bit IEEE floating point sort (_ FloatingPoint 11 53). + * */ fun mkFp64Sort(): KFp64Sort = fp64SortCache + + /** + * Create a 128-bit IEEE floating point sort (_ FloatingPoint 15 113). + * */ fun mkFp128Sort(): KFp128Sort = fp128SortCache + /** + * Create an arbitrary precision IEEE floating point sort (_ FloatingPoint [exponentBits] [significandBits]). + * */ fun mkFpSort(exponentBits: UInt, significandBits: UInt): KFpSort = ensureContextActive { val eb = exponentBits @@ -632,6 +697,9 @@ open class KContext( ensureContextActive { KFpRoundingModeSort(this) } } + /** + * Create a floating point rounding mode sort. + * */ fun mkFpRoundingModeSort(): KFpRoundingModeSort = roundingModeSortCache // utils @@ -707,6 +775,9 @@ open class KContext( createNoSimplify = ::mkAndNoSimplify ) + /** + * Create boolean AND expression. + * */ open fun mkAndNoSimplify(args: List>): KAndExpr = if (args.size == 2) { mkAndNoSimplify(args.first(), args.last()) @@ -717,6 +788,9 @@ open class KContext( } } + /** + * Create boolean binary AND expression. + * */ open fun mkAndNoSimplify(lhs: KExpr, rhs: KExpr): KAndBinaryExpr = andBinaryCache.createIfContextActive { ensureContextMatch(lhs, rhs) @@ -761,6 +835,9 @@ open class KContext( createNoSimplify = ::mkOrNoSimplify ) + /** + * Create boolean OR expression. + * */ open fun mkOrNoSimplify(args: List>): KOrExpr = if (args.size == 2) { mkOrNoSimplify(args.first(), args.last()) @@ -771,6 +848,9 @@ open class KContext( } } + /** + * Create boolean binary OR expression. + * */ open fun mkOrNoSimplify(lhs: KExpr, rhs: KExpr): KOrBinaryExpr = orBinaryCache.createIfContextActive { ensureContextMatch(lhs, rhs) @@ -779,9 +859,15 @@ open class KContext( private val notCache = mkAstInterner() + /** + * Create boolean NOT expression. + * */ open fun mkNot(arg: KExpr): KExpr = mkSimplified(arg, KContext::simplifyNot, ::mkNotNoSimplify) + /** + * Create boolean NOT expression. + * */ open fun mkNotNoSimplify(arg: KExpr): KNotExpr = notCache.createIfContextActive { ensureContextMatch(arg) KNotExpr(this, arg) @@ -789,9 +875,15 @@ open class KContext( private val impliesCache = mkAstInterner() + /** + * Create boolean `=>` (implication) expression. + * */ open fun mkImplies(p: KExpr, q: KExpr): KExpr = mkSimplified(p, q, KContext::simplifyImplies, ::mkImpliesNoSimplify) + /** + * Create boolean `=>` (implication) expression. + * */ open fun mkImpliesNoSimplify( p: KExpr, q: KExpr @@ -802,9 +894,15 @@ open class KContext( private val xorCache = mkAstInterner() + /** + * Create boolean XOR expression. + * */ open fun mkXor(a: KExpr, b: KExpr): KExpr = mkSimplified(a, b, KContext::simplifyXor, ::mkXorNoSimplify) + /** + * Create boolean XOR expression. + * */ open fun mkXorNoSimplify(a: KExpr, b: KExpr): KXorExpr = xorCache.createIfContextActive { ensureContextMatch(a, b) @@ -814,7 +912,14 @@ open class KContext( val trueExpr: KTrue = KTrue(this) val falseExpr: KFalse = KFalse(this) + /** + * Create boolean True constant. + * */ fun mkTrue(): KTrue = trueExpr + + /** + * Create boolean False constant. + * */ fun mkFalse(): KFalse = falseExpr private val eqCache = mkAstInterner>() @@ -835,6 +940,9 @@ open class KContext( createNoSimplify = ::mkEqNoSimplify ) + /** + * Create EQ expression. + * */ open fun mkEqNoSimplify(lhs: KExpr, rhs: KExpr): KEqExpr = eqCache.createIfContextActive { ensureContextMatch(lhs, rhs) @@ -858,6 +966,9 @@ open class KContext( createNoSimplify = ::mkDistinctNoSimplify ) + /** + * Create DISTINCT expression. + * */ open fun mkDistinctNoSimplify(args: List>): KDistinctExpr = distinctCache.createIfContextActive { ensureContextMatch(args) @@ -866,12 +977,18 @@ open class KContext( private val iteCache = mkAstInterner>() + /** + * Create ITE (if-then-else) expression. + * */ open fun mkIte( condition: KExpr, trueBranch: KExpr, falseBranch: KExpr ): KExpr = mkSimplified(condition, trueBranch, falseBranch, KContext::simplifyIte, ::mkIteNoSimplify) + /** + * Create ITE (if-then-else) expression. + * */ open fun mkIteNoSimplify( condition: KExpr, trueBranch: KExpr, @@ -899,11 +1016,14 @@ open class KContext( get() = mkBool(this) // functions - /* - * For builtin declarations e.g. KAndDecl, mkApp must return the same object as a corresponding builder. - * For example, mkApp(KAndDecl, a, b) and mkAnd(a, b) must end up with the same KAndExpr object. - * To achieve such behaviour we override apply for all builtin declarations. - */ + + /** + * Create function app expression. + * + * For builtin declarations e.g. KAndDecl, mkApp must return the same object as a corresponding builder. + * For example, mkApp(KAndDecl, a, b) and mkAnd(a, b) must end up with the same KAndExpr object. + * To achieve such behaviour we override apply for all builtin declarations. + */ open fun mkApp(decl: KDecl, args: List>) = with(decl) { apply(args) } private val functionAppCache = mkAstInterner>() @@ -921,13 +1041,26 @@ open class KContext( private val constAppCache = mkAstInterner>() + /** + * Create constant (function without arguments) app expression. + * + * @see [mkApp] + * */ open fun mkConstApp(decl: KDecl): KConst = constAppCache.createIfContextActive { ensureContextMatch(decl) KConst(this, decl) }.cast() + /** + * Create a constant named [name] with sort [sort]. + * */ fun mkConst(name: String, sort: T): KApp = with(mkConstDecl(name, sort)) { apply() } + /** + * Create a fresh constant with name prefix [name] and sort [sort]. + * + * It is guaranteed that a fresh constant is not equal by `==` to any other constant. + * */ fun mkFreshConst(name: String, sort: T): KApp = with(mkFreshConstDecl(name, sort)) { apply() } // array @@ -936,6 +1069,9 @@ open class KContext( private val array3StoreCache = mkAstInterner>() private val arrayNStoreCache = mkAstInterner>() + /** + * Create an array store expression (store [array] [index] [value]). + * */ open fun mkArrayStore( array: KExpr>, index: KExpr, @@ -943,6 +1079,9 @@ open class KContext( ): KExpr> = mkSimplified(array, index, value, KContext::simplifyArrayStore, ::mkArrayStoreNoSimplify) + /** + * Create an array store expression (store [array] [index0] [index1] [value]). + * */ open fun mkArrayStore( array: KExpr>, index0: KExpr, @@ -951,6 +1090,9 @@ open class KContext( ): KExpr> = mkSimplified(array, index0, index1, value, KContext::simplifyArrayStore, ::mkArrayStoreNoSimplify) + /** + * Create an array store expression (store [array] [index0] [index1] [index2] [value]). + * */ open fun mkArrayStore( array: KExpr>, index0: KExpr, @@ -960,6 +1102,9 @@ open class KContext( ): KExpr> = mkSimplified(array, index0, index1, index2, value, KContext::simplifyArrayStore, ::mkArrayStoreNoSimplify) + /** + * Create n-ary array store expression (store [array] [indices]_0 ... [indices]_n [value]). + * */ open fun mkArrayNStore( array: KExpr>, indices: List>, @@ -967,6 +1112,9 @@ open class KContext( ): KExpr> = mkSimplified(array, indices, value, KContext::simplifyArrayNStore, ::mkArrayNStoreNoSimplify) + /** + * Create an array store expression (store [array] [index] [value]). + * */ open fun mkArrayStoreNoSimplify( array: KExpr>, index: KExpr, @@ -975,6 +1123,9 @@ open class KContext( mkArrayStoreNoSimplifyNoAnalyze(array, index, value) .analyzeIfSimplificationEnabled() + /** + * Create an array store expression (store [array] [index0] [index1] [value]). + * */ open fun mkArrayStoreNoSimplify( array: KExpr>, index0: KExpr, @@ -984,6 +1135,9 @@ open class KContext( mkArrayStoreNoSimplifyNoAnalyze(array, index0, index1, value) .analyzeIfSimplificationEnabled() + /** + * Create an array store expression (store [array] [index0] [index1] [index2] [value]). + * */ open fun mkArrayStoreNoSimplify( array: KExpr>, index0: KExpr, @@ -994,6 +1148,9 @@ open class KContext( mkArrayStoreNoSimplifyNoAnalyze(array, index0, index1, index2, value) .analyzeIfSimplificationEnabled() + /** + * Create n-ary array store expression (store [array] [indices]_0 ... [indices]_n [value]). + * */ open fun mkArrayNStoreNoSimplify( array: KExpr>, indices: List>, @@ -1002,6 +1159,11 @@ open class KContext( mkArrayNStoreNoSimplifyNoAnalyze(array, indices, value) .analyzeIfSimplificationEnabled() + /** + * Create an array store expression (store [array] [index] [value]) without cache. + * + * @see [KArrayStoreBase] + * */ open fun mkArrayStoreNoSimplifyNoAnalyze( array: KExpr>, index: KExpr, @@ -1011,6 +1173,11 @@ open class KContext( KArrayStore(this, array, index, value) }.cast() + /** + * Create an array store expression (store [array] [index0] [index1] [value]). + * + * @see [KArrayStoreBase] + * */ open fun mkArrayStoreNoSimplifyNoAnalyze( array: KExpr>, index0: KExpr, @@ -1021,6 +1188,11 @@ open class KContext( KArray2Store(this, array, index0, index1, value) }.cast() + /** + * Create an array store expression (store [array] [index0] [index1] [index2] [value]). + * + * @see [KArrayStoreBase] + * */ open fun mkArrayStoreNoSimplifyNoAnalyze( array: KExpr>, index0: KExpr, @@ -1032,6 +1204,11 @@ open class KContext( KArray3Store(this, array, index0, index1, index2, value) }.cast() + /** + * Create n-ary array store expression (store [array] [indices]_0 ... [indices]_n [value]) without cache. + * + * @see [KArrayStoreBase] + * */ open fun mkArrayNStoreNoSimplifyNoAnalyze( array: KExpr>, indices: List>, @@ -1060,17 +1237,26 @@ open class KContext( private val array3SelectCache = mkAstInterner>() private val arrayNSelectCache = mkAstInterner>() + /** + * Create an array select expression (select [array] [index]). + * */ open fun mkArraySelect( array: KExpr>, index: KExpr ): KExpr = mkSimplified(array, index, KContext::simplifyArraySelect, ::mkArraySelectNoSimplify) + /** + * Create an array select expression (select [array] [index0] [index1]). + * */ open fun mkArraySelect( array: KExpr>, index0: KExpr, index1: KExpr ): KExpr = mkSimplified(array, index0, index1, KContext::simplifyArraySelect, ::mkArraySelectNoSimplify) + /** + * Create an array select expression (select [array] [index0] [index1] [index2]). + * */ open fun mkArraySelect( array: KExpr>, index0: KExpr, @@ -1078,11 +1264,17 @@ open class KContext( index2: KExpr ): KExpr = mkSimplified(array, index0, index1, index2, KContext::simplifyArraySelect, ::mkArraySelectNoSimplify) + /** + * Create n-ary array select expression (select [array] [indices]_0 ... [indices]_n). + * */ open fun mkArrayNSelect( array: KExpr>, indices: List> ): KExpr = mkSimplified(array, indices, KContext::simplifyArrayNSelect, ::mkArrayNSelectNoSimplify) + /** + * Create an array select expression (select [array] [index]). + * */ open fun mkArraySelectNoSimplify( array: KExpr>, index: KExpr @@ -1091,6 +1283,9 @@ open class KContext( KArraySelect(this, array, index) }.cast() + /** + * Create an array select expression (select [array] [index0] [index1]). + * */ open fun mkArraySelectNoSimplify( array: KExpr>, index0: KExpr, @@ -1100,6 +1295,9 @@ open class KContext( KArray2Select(this, array, index0, index1) }.cast() + /** + * Create an array select expression (select [array] [index0] [index1] [index2]). + * */ open fun mkArraySelectNoSimplify( array: KExpr>, index0: KExpr, @@ -1110,6 +1308,9 @@ open class KContext( KArray3Select(this, array, index0, index1, index2) }.cast() + /** + * Create n-ary array select expression (select [array] [indices]_0 ... [indices]_n). + * */ open fun mkArrayNSelectNoSimplify( array: KExpr>, indices: List> @@ -1122,6 +1323,13 @@ open class KContext( private val arrayConstCache = mkAstInterner, out KSort>>() + /** + * Create a constant array expression ((as const [arraySort]) [value]). + * + * Maps all indices to some fixed [value]. + * If `(= C ((as const (Array D R)) value))` + * then `(forall (i D) (= (select C i) value))`. + * */ open fun , R : KSort> mkArrayConst( arraySort: A, value: KExpr @@ -1132,6 +1340,13 @@ open class KContext( private val functionAsArrayCache = mkAstInterner, out KSort>>() + /** + * Create a function-as-array expression (_ as-array [function]). + * + * Maps all array indices to the corresponding value of [function]. + * If `(= A (_ as-array f))` + * then `(forall (i (domain f)) (= (select A i) (f i)))` + * */ open fun , R : KSort> mkFunctionAsArray( sort: A, function: KFuncDecl ): KFunctionAsArray = @@ -1145,6 +1360,16 @@ open class KContext( private val array3LambdaCache = mkAstInterner>() private val arrayNLambdaCache = mkAstInterner>() + /** + * Create an array lambda expression (lambda ([indexVar]) [body]). + * + * The sort of the lambda expression is an array + * where the domain is the array are the [indexVar] sort and + * the range is the sort of the [body] of the lambda expression. + * + * If `(= L (lambda (i D)) (body i))` + * then `(forall (i D) (= (select L i) (body i)))`. + * */ open fun mkArrayLambda( indexVar: KDecl, body: KExpr ): KArrayLambda = arrayLambdaCache.createIfContextActive { @@ -1152,6 +1377,11 @@ open class KContext( KArrayLambda(this, indexVar, body) }.cast() + /** + * Create an array lambda expression (lambda ([indexVar0] [indexVar1]) [body]). + * + * @see [mkArrayLambda] + * */ open fun mkArrayLambda( indexVar0: KDecl, indexVar1: KDecl, body: KExpr ): KArray2Lambda = array2LambdaCache.createIfContextActive { @@ -1159,6 +1389,11 @@ open class KContext( KArray2Lambda(this, indexVar0, indexVar1, body) }.cast() + /** + * Create an array lambda expression (lambda ([indexVar0] [indexVar1] [indexVar2]) [body]). + * + * @see [mkArrayLambda] + * */ open fun mkArrayLambda( indexVar0: KDecl, indexVar1: KDecl, indexVar2: KDecl, body: KExpr ): KArray3Lambda = array3LambdaCache.createIfContextActive { @@ -1166,6 +1401,11 @@ open class KContext( KArray3Lambda(this, indexVar0, indexVar1, indexVar2, body) }.cast() + /** + * Create n-ary array lambda expression (lambda ([indices]_0 ... [indices]_n) [body]). + * + * @see [mkArrayLambda] + * */ open fun mkArrayNLambda( indices: List>, body: KExpr ): KArrayNLambda = arrayNLambdaCache.createIfContextActive { @@ -1202,9 +1442,15 @@ open class KContext( // arith private val arithAddCache = mkAstInterner>() + /** + * Create an Int/Real arithmetic addition expression. + * */ open fun mkArithAdd(args: List>): KExpr = mkSimplified(args, KContext::simplifyArithAdd, ::mkArithAddNoSimplify) + /** + * Create an Int/Real arithmetic addition expression. + * */ open fun mkArithAddNoSimplify(args: List>): KAddArithExpr = arithAddCache.createIfContextActive { ensureContextMatch(args) @@ -1213,9 +1459,15 @@ open class KContext( private val arithMulCache = mkAstInterner>() + /** + * Create an Int/Real arithmetic multiplication expression. + * */ open fun mkArithMul(args: List>): KExpr = mkSimplified(args, KContext::simplifyArithMul, ::mkArithMulNoSimplify) + /** + * Create an Int/Real arithmetic multiplication expression. + * */ open fun mkArithMulNoSimplify(args: List>): KMulArithExpr = arithMulCache.createIfContextActive { ensureContextMatch(args) @@ -1224,9 +1476,15 @@ open class KContext( private val arithSubCache = mkAstInterner>() + /** + * Create an Int/Real arithmetic subtraction expression. + * */ open fun mkArithSub(args: List>): KExpr = mkSimplified(args, KContext::simplifyArithSub, ::mkArithSubNoSimplify) + /** + * Create an Int/Real arithmetic subtraction expression. + * */ open fun mkArithSubNoSimplify(args: List>): KSubArithExpr = arithSubCache.createIfContextActive { ensureContextMatch(args) @@ -1244,9 +1502,15 @@ open class KContext( private val arithUnaryMinusCache = mkAstInterner>() + /** + * Create an Int/Real arithmetic negation expression. + * */ open fun mkArithUnaryMinus(arg: KExpr): KExpr = mkSimplified(arg, KContext::simplifyArithUnaryMinus, ::mkArithUnaryMinusNoSimplify) + /** + * Create an Int/Real arithmetic negation expression. + * */ open fun mkArithUnaryMinusNoSimplify(arg: KExpr): KUnaryMinusArithExpr = arithUnaryMinusCache.createIfContextActive { ensureContextMatch(arg) @@ -1255,9 +1519,15 @@ open class KContext( private val arithDivCache = mkAstInterner>() + /** + * Create an Int/Real arithmetic division expression. + * */ open fun mkArithDiv(lhs: KExpr, rhs: KExpr): KExpr = mkSimplified(lhs, rhs, KContext::simplifyArithDiv, ::mkArithDivNoSimplify) + /** + * Create an Int/Real arithmetic division expression. + * */ open fun mkArithDivNoSimplify(lhs: KExpr, rhs: KExpr): KDivArithExpr = arithDivCache.createIfContextActive { ensureContextMatch(lhs, rhs) @@ -1266,9 +1536,15 @@ open class KContext( private val arithPowerCache = mkAstInterner>() + /** + * Create an Int/Real arithmetic power expression. + * */ open fun mkArithPower(lhs: KExpr, rhs: KExpr): KExpr = mkSimplified(lhs, rhs, KContext::simplifyArithPower, ::mkArithPowerNoSimplify) + /** + * Create an Int/Real arithmetic power expression. + * */ open fun mkArithPowerNoSimplify(lhs: KExpr, rhs: KExpr): KPowerArithExpr = arithPowerCache.createIfContextActive { ensureContextMatch(lhs, rhs) @@ -1277,9 +1553,15 @@ open class KContext( private val arithLtCache = mkAstInterner>() + /** + * Create an Int/Real arithmetic `<` (less) expression. + * */ open fun mkArithLt(lhs: KExpr, rhs: KExpr): KExpr = mkSimplified(lhs, rhs, KContext::simplifyArithLt, ::mkArithLtNoSimplify) + /** + * Create an Int/Real arithmetic `<` (less) expression. + * */ open fun mkArithLtNoSimplify(lhs: KExpr, rhs: KExpr): KLtArithExpr = arithLtCache.createIfContextActive { ensureContextMatch(lhs, rhs) @@ -1288,9 +1570,15 @@ open class KContext( private val arithLeCache = mkAstInterner>() + /** + * Create an Int/Real arithmetic `<=` (less-or-equal) expression. + * */ open fun mkArithLe(lhs: KExpr, rhs: KExpr): KExpr = mkSimplified(lhs, rhs, KContext::simplifyArithLe, ::mkArithLeNoSimplify) + /** + * Create an Int/Real arithmetic `<=` (less-or-equal) expression. + * */ open fun mkArithLeNoSimplify(lhs: KExpr, rhs: KExpr): KLeArithExpr = arithLeCache.createIfContextActive { ensureContextMatch(lhs, rhs) @@ -1299,9 +1587,15 @@ open class KContext( private val arithGtCache = mkAstInterner>() + /** + * Create an Int/Real arithmetic `>` (greater) expression. + * */ open fun mkArithGt(lhs: KExpr, rhs: KExpr): KExpr = mkSimplified(lhs, rhs, KContext::simplifyArithGt, ::mkArithGtNoSimplify) + /** + * Create an Int/Real arithmetic `>` (greater) expression. + * */ open fun mkArithGtNoSimplify(lhs: KExpr, rhs: KExpr): KGtArithExpr = arithGtCache.createIfContextActive { ensureContextMatch(lhs, rhs) @@ -1310,9 +1604,15 @@ open class KContext( private val arithGeCache = mkAstInterner>() + /** + * Create an Int/Real arithmetic `>=` (greater-or-equal) expression. + * */ open fun mkArithGe(lhs: KExpr, rhs: KExpr): KExpr = mkSimplified(lhs, rhs, KContext::simplifyArithGe, ::mkArithGeNoSimplify) + /** + * Create an Int/Real arithmetic `>=` (greater-or-equal) expression. + * */ open fun mkArithGeNoSimplify(lhs: KExpr, rhs: KExpr): KGeArithExpr = arithGeCache.createIfContextActive { ensureContextMatch(lhs, rhs) @@ -1334,9 +1634,19 @@ open class KContext( // integer private val intModCache = mkAstInterner() + /** + * Create an Int mod expression. + * + * todo: clarify + * */ open fun mkIntMod(lhs: KExpr, rhs: KExpr): KExpr = mkSimplified(lhs, rhs, KContext::simplifyIntMod, ::mkIntModNoSimplify) + /** + * Create an Int mod expression. + * + * @see mkIntMod + * */ open fun mkIntModNoSimplify( lhs: KExpr, rhs: KExpr @@ -1347,9 +1657,19 @@ open class KContext( private val intRemCache = mkAstInterner() + /** + * Create an Int rem expression. + * + * todo: clarify + * */ open fun mkIntRem(lhs: KExpr, rhs: KExpr): KExpr = mkSimplified(lhs, rhs, KContext::simplifyIntRem, ::mkIntRemNoSimplify) + /** + * Create an Int rem expression. + * + * @see mkIntRem + * */ open fun mkIntRemNoSimplify( lhs: KExpr, rhs: KExpr @@ -1360,9 +1680,15 @@ open class KContext( private val intToRealCache = mkAstInterner() + /** + * Convert an Int expression to a corresponding Real expression. + * */ open fun mkIntToReal(arg: KExpr): KExpr = mkSimplified(arg, KContext::simplifyIntToReal, ::mkIntToRealNoSimplify) + /** + * Convert an Int expression to a corresponding Real expression. + * */ open fun mkIntToRealNoSimplify(arg: KExpr): KToRealIntExpr = intToRealCache.createIfContextActive { ensureContextMatch(arg) KToRealIntExpr(this, arg) @@ -1372,10 +1698,16 @@ open class KContext( private val int64NumCache = mkAstInterner() private val intBigNumCache = mkAstInterner() + /** + * Create an Int value. + * */ fun mkIntNum(value: Int): KIntNumExpr = int32NumCache.createIfContextActive { KInt32NumExpr(this, value) } + /** + * Create an Int value. + * */ fun mkIntNum(value: Long): KIntNumExpr = if (value.toInt().toLong() == value) { mkIntNum(value.toInt()) } else { @@ -1384,6 +1716,9 @@ open class KContext( } } + /** + * Create an Int value. + * */ fun mkIntNum(value: BigInteger): KIntNumExpr = if (value.toLong().toBigInteger() == value) { mkIntNum(value.toLong()) } else { @@ -1392,6 +1727,9 @@ open class KContext( } } + /** + * Create an Int value. + * */ fun mkIntNum(value: String): KIntNumExpr = mkIntNum(value.toBigInteger()) @@ -1409,9 +1747,15 @@ open class KContext( // real private val realToIntCache = mkAstInterner() + /** + * Convert Real expression to an Int expression (floor division). + * */ open fun mkRealToInt(arg: KExpr): KExpr = mkSimplified(arg, KContext::simplifyRealToInt, ::mkRealToIntNoSimplify) + /** + * Convert Real expression to an Int expression (floor division). + * */ open fun mkRealToIntNoSimplify(arg: KExpr): KToIntRealExpr = realToIntCache.createIfContextActive { ensureContextMatch(arg) KToIntRealExpr(this, arg) @@ -1419,9 +1763,15 @@ open class KContext( private val realIsIntCache = mkAstInterner() + /** + * Check whether the given Real expression has an integer value. + * */ open fun mkRealIsInt(arg: KExpr): KExpr = mkSimplified(arg, KContext::simplifyRealIsInt, ::mkRealIsIntNoSimplify) + /** + * Check whether the given Real expression has an integer value. + * */ open fun mkRealIsIntNoSimplify(arg: KExpr): KIsIntRealExpr = realIsIntCache.createIfContextActive { ensureContextMatch(arg) KIsIntRealExpr(this, arg) @@ -1429,18 +1779,43 @@ open class KContext( private val realNumCache = mkAstInterner() + /** + * Create a Real value. + * */ fun mkRealNum(numerator: KIntNumExpr, denominator: KIntNumExpr): KRealNumExpr = realNumCache.createIfContextActive { ensureContextMatch(numerator, denominator) KRealNumExpr(this, numerator, denominator) } - @Suppress("MemberVisibilityCanBePrivate") + /** + * Create a Real value. + * */ fun mkRealNum(numerator: KIntNumExpr) = mkRealNum(numerator, 1.expr) + + /** + * Create a Real value. + * */ fun mkRealNum(numerator: Int) = mkRealNum(mkIntNum(numerator)) + + /** + * Create a Real value. + * */ fun mkRealNum(numerator: Int, denominator: Int) = mkRealNum(mkIntNum(numerator), mkIntNum(denominator)) + + /** + * Create a Real value. + * */ fun mkRealNum(numerator: Long) = mkRealNum(mkIntNum(numerator)) + + /** + * Create a Real value. + * */ fun mkRealNum(numerator: Long, denominator: Long) = mkRealNum(mkIntNum(numerator), mkIntNum(denominator)) + + /** + * Create a Real value from a string of the form `"123/456"`. + * */ fun mkRealNum(value: String): KRealNumExpr { val parts = value.split('/') @@ -1462,6 +1837,7 @@ open class KContext( private val bv64Cache = mkAstInterner() private val bvCache = mkAstInterner() + fun mkBv(value: Boolean): KBitVec1Value = bv1Cache.createIfContextActive { KBitVec1Value(this, value) } fun mkBv(value: Boolean, sizeBits: UInt): KBitVecValue { val intValue = (if (value) 1 else 0) as Number From 81c614232a45194b1e4b88c22c18f14ffd58047b Mon Sep 17 00:00:00 2001 From: Saloed Date: Tue, 6 Jun 2023 12:46:10 +0300 Subject: [PATCH 2/6] Bv docs --- ksmt-core/src/main/kotlin/io/ksmt/KContext.kt | 518 ++++++++++++++++++ 1 file changed, 518 insertions(+) diff --git a/ksmt-core/src/main/kotlin/io/ksmt/KContext.kt b/ksmt-core/src/main/kotlin/io/ksmt/KContext.kt index 6d1d8b261..0111ac106 100644 --- a/ksmt-core/src/main/kotlin/io/ksmt/KContext.kt +++ b/ksmt-core/src/main/kotlin/io/ksmt/KContext.kt @@ -1838,12 +1838,26 @@ open class KContext( private val bvCache = mkAstInterner() + /** + * Create a BitVec value with 1 bit length. + * */ fun mkBv(value: Boolean): KBitVec1Value = bv1Cache.createIfContextActive { KBitVec1Value(this, value) } + + /** + * Create a BitVec value with [sizeBits] bit length. + * + * Note: if [sizeBits] is greater than 1, the [value] bit will be repeated. + * */ fun mkBv(value: Boolean, sizeBits: UInt): KBitVecValue { val intValue = (if (value) 1 else 0) as Number return mkBv(intValue, sizeBits) } + /** + * Create a BitVec value of the BitVec [sort]. + * + * Note: if [sort] size is greater than 1, the [value] bit will be repeated. + * */ fun mkBv(value: Boolean, sort: T): KBitVecValue = mkBv(value, sort.sizeBits).cast() @@ -1851,39 +1865,142 @@ open class KContext( fun Boolean.toBv(sizeBits: UInt): KBitVecValue = mkBv(this, sizeBits) fun Boolean.toBv(sort: T): KBitVecValue = mkBv(this, sort) + /** + * Create a BitVec value with 8 bit length. + * */ fun mkBv(value: Byte): KBitVec8Value = bv8Cache.createIfContextActive { KBitVec8Value(this, value) } + + /** + * Create a BitVec value with [sizeBits] bit length. + * + * Note: if [sizeBits] is less than 8, + * the last [sizeBits] bits of the [value] will be taken. + * + * At the same time, if [sizeBits] is greater than 8, + * binary representation of the [value] will be padded from the start with its sign bit. + * */ fun mkBv(value: Byte, sizeBits: UInt): KBitVecValue = mkBv(value as Number, sizeBits) + + /** + * Create a BitVec value of the BitVec [sort]. + * + * Note: if [sort] size is less than 8, + * the last [sort] size bits of the [value] will be taken. + * + * At the same time, if [sort] size is greater than 8, + * binary representation of the [value] will be padded from the start with its sign bit. + * */ fun mkBv(value: Byte, sort: T): KBitVecValue = mkBv(value as Number, sort) + fun Byte.toBv(): KBitVec8Value = mkBv(this) fun Byte.toBv(sizeBits: UInt): KBitVecValue = mkBv(this, sizeBits) fun Byte.toBv(sort: T): KBitVecValue = mkBv(this, sort) fun UByte.toBv(): KBitVec8Value = mkBv(toByte()) + /** + * Create a BitVec value with 16 bit length. + * */ fun mkBv(value: Short): KBitVec16Value = bv16Cache.createIfContextActive { KBitVec16Value(this, value) } + + /** + * Create a BitVec value with [sizeBits] bit length. + * + * Note: if [sizeBits] is less than 16, + * the last [sizeBits] bits of the [value] will be taken. + * + * At the same time, if [sizeBits] is greater than 16, + * binary representation of the [value] will be padded from the start with its sign bit. + * */ fun mkBv(value: Short, sizeBits: UInt): KBitVecValue = mkBv(value as Number, sizeBits) + + /** + * Create a BitVec value of the BitVec [sort]. + * + * Note: if [sort] size is less than 16, + * the last [sort] size bits of the [value] will be taken. + * + * At the same time, if [sort] size is greater than 16, + * binary representation of the [value] will be padded from the start with its sign bit. + * */ fun mkBv(value: Short, sort: T): KBitVecValue = mkBv(value as Number, sort) + fun Short.toBv(): KBitVec16Value = mkBv(this) fun Short.toBv(sizeBits: UInt): KBitVecValue = mkBv(this, sizeBits) fun Short.toBv(sort: T): KBitVecValue = mkBv(this, sort) fun UShort.toBv(): KBitVec16Value = mkBv(toShort()) + /** + * Create a BitVec value with 32 bit length. + * */ fun mkBv(value: Int): KBitVec32Value = bv32Cache.createIfContextActive { KBitVec32Value(this, value) } + + /** + * Create a BitVec value with [sizeBits] bit length. + * + * Note: if [sizeBits] is less than 32, + * the last [sizeBits] bits of the [value] will be taken. + * + * At the same time, if [sizeBits] is greater than 32, + * binary representation of the [value] will be padded from the start with its sign bit. + * */ fun mkBv(value: Int, sizeBits: UInt): KBitVecValue = mkBv(value as Number, sizeBits) + + /** + * Create a BitVec value of the BitVec [sort]. + * + * Note: if [sort] size is less than 32, + * the last [sort] size bits of the [value] will be taken. + * + * At the same time, if [sort] size is greater than 32, + * binary representation of the [value] will be padded from the start with its sign bit. + * */ fun mkBv(value: Int, sort: T): KBitVecValue = mkBv(value as Number, sort) + fun Int.toBv(): KBitVec32Value = mkBv(this) fun Int.toBv(sizeBits: UInt): KBitVecValue = mkBv(this, sizeBits) fun Int.toBv(sort: T): KBitVecValue = mkBv(this, sort) fun UInt.toBv(): KBitVec32Value = mkBv(toInt()) + /** + * Create a BitVec value with 64 bit length. + * */ fun mkBv(value: Long): KBitVec64Value = bv64Cache.createIfContextActive { KBitVec64Value(this, value) } + + /** + * Create a BitVec value with [sizeBits] bit length. + * + * Note: if [sizeBits] is less than 32, + * the last [sizeBits] bits of the [value] will be taken. + * + * At the same time, if [sizeBits] is greater than 32, + * binary representation of the [value] will be padded from the start with its sign bit. + * */ fun mkBv(value: Long, sizeBits: UInt): KBitVecValue = mkBv(value as Number, sizeBits) + + /** + * Create a BitVec value of the BitVec [sort]. + * + * Note: if [sort] size is less than 64, + * the last [sort] size bits of the [value] will be taken. + * + * At the same time, if [sort] size is greater than 64, + * binary representation of the [value] will be padded from the start with its sign bit. + * */ fun mkBv(value: Long, sort: T): KBitVecValue = mkBv(value as Number, sort) + fun Long.toBv(): KBitVec64Value = mkBv(this) fun Long.toBv(sizeBits: UInt): KBitVecValue = mkBv(this, sizeBits) fun Long.toBv(sort: T): KBitVecValue = mkBv(this, sort) fun ULong.toBv(): KBitVec64Value = mkBv(toLong()) + /** + * Create a BitVec value with [sizeBits] bit length. + * */ fun mkBv(value: BigInteger, sizeBits: UInt): KBitVecValue = mkBv(value as Number, sizeBits) + + /** + * Create a BitVec value of the BitVec [sort]. + * */ fun mkBv(value: BigInteger, sort: T): KBitVecValue = mkBv(value as Number, sort) /** @@ -1914,9 +2031,15 @@ open class KContext( private fun Number.toBv(sizeBits: UInt) = mkBv(this, sizeBits) + /** + * Create a BitVec value with [sizeBits] bit length from the given binary stirng [value]. + * */ fun mkBv(value: String, sizeBits: UInt): KBitVecValue = mkBv(value.toBigInteger(radix = 2), sizeBits) + /** + * Create a BitVec value with [sizeBits] bit length from the given hex stirng [value]. + * */ fun mkBvHex(value: String, sizeBits: UInt): KBitVecValue = mkBv(value.toBigInteger(radix = 16), sizeBits) @@ -1941,9 +2064,15 @@ open class KContext( private val bvNotExprCache = mkAstInterner>() + /** + * Create bitwise NOT (`bvnot`) expression. + * */ open fun mkBvNotExpr(value: KExpr): KExpr = mkSimplified(value, KContext::simplifyBvNotExpr, ::mkBvNotExprNoSimplify) + /** + * Create bitwise NOT (`bvnot`) expression. + * */ open fun mkBvNotExprNoSimplify(value: KExpr): KBvNotExpr = bvNotExprCache.createIfContextActive { ensureContextMatch(value) @@ -1952,9 +2081,17 @@ open class KContext( private val bvRedAndExprCache = mkAstInterner>() + /** + * Create bitwise AND reduction (`bvredand`) expression. + * Reduce all bits to a single bit with AND operation. + * */ open fun mkBvReductionAndExpr(value: KExpr): KExpr = mkSimplified(value, KContext::simplifyBvReductionAndExpr, ::mkBvReductionAndExprNoSimplify) + /** + * Create bitwise AND reduction (`bvredand`) expression. + * Reduce all bits to a single bit with AND operation. + * */ open fun mkBvReductionAndExprNoSimplify(value: KExpr): KBvReductionAndExpr = bvRedAndExprCache.createIfContextActive { ensureContextMatch(value) @@ -1965,9 +2102,17 @@ open class KContext( private val bvRedOrExprCache = mkAstInterner>() + /** + * Create bitwise OR reduction (`bvredor`) expression. + * Reduce all bits to a single bit with OR operation. + * */ open fun mkBvReductionOrExpr(value: KExpr): KExpr = mkSimplified(value, KContext::simplifyBvReductionOrExpr, ::mkBvReductionOrExprNoSimplify) + /** + * Create bitwise OR reduction (`bvredor`) expression. + * Reduce all bits to a single bit with OR operation. + * */ open fun mkBvReductionOrExprNoSimplify(value: KExpr): KBvReductionOrExpr = bvRedOrExprCache.createIfContextActive { ensureContextMatch(value) @@ -1978,9 +2123,15 @@ open class KContext( private val bvAndExprCache = mkAstInterner>() + /** + * Create bitwise AND (`bvand`) expression. + * */ open fun mkBvAndExpr(arg0: KExpr, arg1: KExpr): KExpr = mkSimplified(arg0, arg1, KContext::simplifyBvAndExpr, ::mkBvAndExprNoSimplify) + /** + * Create bitwise AND (`bvand`) expression. + * */ open fun mkBvAndExprNoSimplify(arg0: KExpr, arg1: KExpr): KBvAndExpr = bvAndExprCache.createIfContextActive { ensureContextMatch(arg0, arg1) @@ -1989,9 +2140,16 @@ open class KContext( private val bvOrExprCache = mkAstInterner>() + + /** + * Create bitwise OR (`bvor`) expression. + * */ open fun mkBvOrExpr(arg0: KExpr, arg1: KExpr): KExpr = mkSimplified(arg0, arg1, KContext::simplifyBvOrExpr, ::mkBvOrExprNoSimplify) + /** + * Create bitwise OR (`bvor`) expression. + * */ open fun mkBvOrExprNoSimplify(arg0: KExpr, arg1: KExpr): KBvOrExpr = bvOrExprCache.createIfContextActive { ensureContextMatch(arg0, arg1) @@ -2000,9 +2158,15 @@ open class KContext( private val bvXorExprCache = mkAstInterner>() + /** + * Create bitwise XOR (`bvxor`) expression. + * */ open fun mkBvXorExpr(arg0: KExpr, arg1: KExpr): KExpr = mkSimplified(arg0, arg1, KContext::simplifyBvXorExpr, ::mkBvXorExprNoSimplify) + /** + * Create bitwise XOR (`bvxor`) expression. + * */ open fun mkBvXorExprNoSimplify(arg0: KExpr, arg1: KExpr): KBvXorExpr = bvXorExprCache.createIfContextActive { ensureContextMatch(arg0, arg1) @@ -2011,9 +2175,15 @@ open class KContext( private val bvNAndExprCache = mkAstInterner>() + /** + * Create bitwise NAND (`bvnand`) expression. + * */ open fun mkBvNAndExpr(arg0: KExpr, arg1: KExpr): KExpr = mkSimplified(arg0, arg1, KContext::simplifyBvNAndExpr, ::mkBvNAndExprNoSimplify) + /** + * Create bitwise NAND (`bvnand`) expression. + * */ open fun mkBvNAndExprNoSimplify(arg0: KExpr, arg1: KExpr): KBvNAndExpr = bvNAndExprCache.createIfContextActive { ensureContextMatch(arg0, arg1) @@ -2022,9 +2192,15 @@ open class KContext( private val bvNorExprCache = mkAstInterner>() + /** + * Create bitwise NOR (`bvnor`) expression. + * */ open fun mkBvNorExpr(arg0: KExpr, arg1: KExpr): KExpr = mkSimplified(arg0, arg1, KContext::simplifyBvNorExpr, ::mkBvNorExprNoSimplify) + /** + * Create bitwise NOR (`bvnor`) expression. + * */ open fun mkBvNorExprNoSimplify(arg0: KExpr, arg1: KExpr): KBvNorExpr = bvNorExprCache.createIfContextActive { ensureContextMatch(arg0, arg1) @@ -2033,9 +2209,15 @@ open class KContext( private val bvXNorExprCache = mkAstInterner>() + /** + * Create bitwise XNOR (`bvxnor`) expression. + * */ open fun mkBvXNorExpr(arg0: KExpr, arg1: KExpr): KExpr = mkSimplified(arg0, arg1, KContext::simplifyBvXNorExpr, ::mkBvXNorExprNoSimplify) + /** + * Create bitwise XNOR (`bvxnor`) expression. + * */ open fun mkBvXNorExprNoSimplify(arg0: KExpr, arg1: KExpr): KBvXNorExpr = bvXNorExprCache.createIfContextActive { ensureContextMatch(arg0, arg1) @@ -2044,9 +2226,19 @@ open class KContext( private val bvNegationExprCache = mkAstInterner>() + /** + * Create BitVec arithmetic negation (`bvneg`) expression. + * + * @see mkBvNotExpr for bitwise not. + * */ open fun mkBvNegationExpr(value: KExpr): KExpr = mkSimplified(value, KContext::simplifyBvNegationExpr, ::mkBvNegationExprNoSimplify) + /** + * Create BitVec arithmetic negation (`bvneg`) expression. + * + * @see mkBvNotExpr for bitwise not. + * */ open fun mkBvNegationExprNoSimplify(value: KExpr): KBvNegationExpr = bvNegationExprCache.createIfContextActive { ensureContextMatch(value) @@ -2055,9 +2247,15 @@ open class KContext( private val bvAddExprCache = mkAstInterner>() + /** + * Create BitVec arithmetic addition (`bvadd`) expression. + * */ open fun mkBvAddExpr(arg0: KExpr, arg1: KExpr): KExpr = mkSimplified(arg0, arg1, KContext::simplifyBvAddExpr, ::mkBvAddExprNoSimplify) + /** + * Create BitVec arithmetic addition (`bvadd`) expression. + * */ open fun mkBvAddExprNoSimplify(arg0: KExpr, arg1: KExpr): KBvAddExpr = bvAddExprCache.createIfContextActive { ensureContextMatch(arg0, arg1) @@ -2066,9 +2264,15 @@ open class KContext( private val bvSubExprCache = mkAstInterner>() + /** + * Create BitVec arithmetic subtraction (`bvsub`) expression. + * */ open fun mkBvSubExpr(arg0: KExpr, arg1: KExpr): KExpr = mkSimplified(arg0, arg1, KContext::simplifyBvSubExpr, ::mkBvSubExprNoSimplify) + /** + * Create BitVec arithmetic subtraction (`bvsub`) expression. + * */ open fun mkBvSubExprNoSimplify(arg0: KExpr, arg1: KExpr): KBvSubExpr = bvSubExprCache.createIfContextActive { ensureContextMatch(arg0, arg1) @@ -2077,9 +2281,15 @@ open class KContext( private val bvMulExprCache = mkAstInterner>() + /** + * Create BitVec arithmetic multiplication (`bvmul`) expression. + * */ open fun mkBvMulExpr(arg0: KExpr, arg1: KExpr): KExpr = mkSimplified(arg0, arg1, KContext::simplifyBvMulExpr, ::mkBvMulExprNoSimplify) + /** + * Create BitVec arithmetic multiplication (`bvmul`) expression. + * */ open fun mkBvMulExprNoSimplify(arg0: KExpr, arg1: KExpr): KBvMulExpr = bvMulExprCache.createIfContextActive { ensureContextMatch(arg0, arg1) @@ -2088,9 +2298,19 @@ open class KContext( private val bvUnsignedDivExprCache = mkAstInterner>() + /** + * Create BitVec arithmetic unsigned division (`bvudiv`) expression. + * + * @see mkBvSignedDivExpr for the signed division. + * */ open fun mkBvUnsignedDivExpr(arg0: KExpr, arg1: KExpr): KExpr = mkSimplified(arg0, arg1, KContext::simplifyBvUnsignedDivExpr, ::mkBvUnsignedDivExprNoSimplify) + /** + * Create BitVec arithmetic unsigned division (`bvudiv`) expression. + * + * @see mkBvSignedDivExpr for the signed division. + * */ open fun mkBvUnsignedDivExprNoSimplify(arg0: KExpr, arg1: KExpr): KBvUnsignedDivExpr = bvUnsignedDivExprCache.createIfContextActive { ensureContextMatch(arg0, arg1) @@ -2099,9 +2319,21 @@ open class KContext( private val bvSignedDivExprCache = mkAstInterner>() + /** + * Create BitVec arithmetic signed division (`bvsdiv`) expression. + * The division result sign depends on the arguments signs. + * + * @see mkBvUnsignedDivExpr for the unsigned division. + * */ open fun mkBvSignedDivExpr(arg0: KExpr, arg1: KExpr): KExpr = mkSimplified(arg0, arg1, KContext::simplifyBvSignedDivExpr, ::mkBvSignedDivExprNoSimplify) + /** + * Create BitVec arithmetic signed division (`bvsdiv`) expression. + * The division result sign depends on the arguments signs. + * + * @see mkBvUnsignedDivExpr for the unsigned division. + * */ open fun mkBvSignedDivExprNoSimplify(arg0: KExpr, arg1: KExpr): KBvSignedDivExpr = bvSignedDivExprCache.createIfContextActive { ensureContextMatch(arg0, arg1) @@ -2110,9 +2342,19 @@ open class KContext( private val bvUnsignedRemExprCache = mkAstInterner>() + /** + * Create BitVec arithmetic unsigned reminder (`bvurem`) expression. + * + * @see mkBvSignedRemExpr for the signed remainder. + * */ open fun mkBvUnsignedRemExpr(arg0: KExpr, arg1: KExpr): KExpr = mkSimplified(arg0, arg1, KContext::simplifyBvUnsignedRemExpr, ::mkBvUnsignedRemExprNoSimplify) + /** + * Create BitVec arithmetic unsigned reminder (`bvurem`) expression. + * + * @see mkBvSignedRemExpr for the signed remainder. + * */ open fun mkBvUnsignedRemExprNoSimplify(arg0: KExpr, arg1: KExpr): KBvUnsignedRemExpr = bvUnsignedRemExprCache.createIfContextActive { ensureContextMatch(arg0, arg1) @@ -2121,9 +2363,23 @@ open class KContext( private val bvSignedRemExprCache = mkAstInterner>() + /** + * Create BitVec arithmetic signed reminder (`bvsrem`) expression. + * + * todo: clarify + * + * @see mkBvUnsignedRemExpr for the unsigned remainder. + * */ open fun mkBvSignedRemExpr(arg0: KExpr, arg1: KExpr): KExpr = mkSimplified(arg0, arg1, KContext::simplifyBvSignedRemExpr, ::mkBvSignedRemExprNoSimplify) + /** + * Create BitVec arithmetic signed reminder (`bvsrem`) expression. + * + * todo: clarify + * + * @see mkBvUnsignedRemExpr for the unsigned remainder. + * */ open fun mkBvSignedRemExprNoSimplify(arg0: KExpr, arg1: KExpr): KBvSignedRemExpr = bvSignedRemExprCache.createIfContextActive { ensureContextMatch(arg0, arg1) @@ -2132,9 +2388,19 @@ open class KContext( private val bvSignedModExprCache = mkAstInterner>() + /** + * Create BitVec arithmetic signed mod (`bvsmod`) expression. + * + * todo: clarify + * */ open fun mkBvSignedModExpr(arg0: KExpr, arg1: KExpr): KExpr = mkSimplified(arg0, arg1, KContext::simplifyBvSignedModExpr, ::mkBvSignedModExprNoSimplify) + /** + * Create BitVec arithmetic signed mod (`bvsmod`) expression. + * + * todo: clarify + * */ open fun mkBvSignedModExprNoSimplify(arg0: KExpr, arg1: KExpr): KBvSignedModExpr = bvSignedModExprCache.createIfContextActive { ensureContextMatch(arg0, arg1) @@ -2143,9 +2409,15 @@ open class KContext( private val bvUnsignedLessExprCache = mkAstInterner>() + /** + * Create BitVec unsigned less (`bvult`) expression. + * */ open fun mkBvUnsignedLessExpr(arg0: KExpr, arg1: KExpr): KExpr = mkSimplified(arg0, arg1, KContext::simplifyBvUnsignedLessExpr, ::mkBvUnsignedLessExprNoSimplify) + /** + * Create BitVec unsigned less (`bvult`) expression. + * */ open fun mkBvUnsignedLessExprNoSimplify(arg0: KExpr, arg1: KExpr): KBvUnsignedLessExpr = bvUnsignedLessExprCache.createIfContextActive { ensureContextMatch(arg0, arg1) @@ -2154,9 +2426,15 @@ open class KContext( private val bvSignedLessExprCache = mkAstInterner>() + /** + * Create BitVec signed less (`bvslt`) expression. + * */ open fun mkBvSignedLessExpr(arg0: KExpr, arg1: KExpr): KExpr = mkSimplified(arg0, arg1, KContext::simplifyBvSignedLessExpr, ::mkBvSignedLessExprNoSimplify) + /** + * Create BitVec signed less (`bvslt`) expression. + * */ open fun mkBvSignedLessExprNoSimplify(arg0: KExpr, arg1: KExpr): KBvSignedLessExpr = bvSignedLessExprCache.createIfContextActive { ensureContextMatch(arg0, arg1) @@ -2165,9 +2443,15 @@ open class KContext( private val bvSignedLessOrEqualExprCache = mkAstInterner>() + /** + * Create BitVec signed less-or-equal (`bvsle`) expression. + * */ open fun mkBvSignedLessOrEqualExpr(arg0: KExpr, arg1: KExpr): KExpr = mkSimplified(arg0, arg1, KContext::simplifyBvSignedLessOrEqualExpr, ::mkBvSignedLessOrEqualExprNoSimplify) + /** + * Create BitVec signed less-or-equal (`bvsle`) expression. + * */ open fun mkBvSignedLessOrEqualExprNoSimplify( arg0: KExpr, arg1: KExpr ): KBvSignedLessOrEqualExpr = @@ -2178,9 +2462,15 @@ open class KContext( private val bvUnsignedLessOrEqualExprCache = mkAstInterner>() + /** + * Create BitVec unsigned less-or-equal (`bvule`) expression. + * */ open fun mkBvUnsignedLessOrEqualExpr(arg0: KExpr, arg1: KExpr): KExpr = mkSimplified(arg0, arg1, KContext::simplifyBvUnsignedLessOrEqualExpr, ::mkBvUnsignedLessOrEqualExprNoSimplify) + /** + * Create BitVec unsigned less-or-equal (`bvule`) expression. + * */ open fun mkBvUnsignedLessOrEqualExprNoSimplify( arg0: KExpr, arg1: KExpr @@ -2191,6 +2481,9 @@ open class KContext( private val bvUnsignedGreaterOrEqualExprCache = mkAstInterner>() + /** + * Create BitVec unsigned greater-or-equal (`bvuge`) expression. + * */ open fun mkBvUnsignedGreaterOrEqualExpr(arg0: KExpr, arg1: KExpr): KExpr = mkSimplified( arg0, @@ -2199,6 +2492,9 @@ open class KContext( ::mkBvUnsignedGreaterOrEqualExprNoSimplify ) + /** + * Create BitVec unsigned greater-or-equal (`bvuge`) expression. + * */ open fun mkBvUnsignedGreaterOrEqualExprNoSimplify( arg0: KExpr, arg1: KExpr @@ -2209,9 +2505,15 @@ open class KContext( private val bvSignedGreaterOrEqualExprCache = mkAstInterner>() + /** + * Create BitVec signed greater-or-equal (`bvsge`) expression. + * */ open fun mkBvSignedGreaterOrEqualExpr(arg0: KExpr, arg1: KExpr): KExpr = mkSimplified(arg0, arg1, KContext::simplifyBvSignedGreaterOrEqualExpr, ::mkBvSignedGreaterOrEqualExprNoSimplify) + /** + * Create BitVec signed greater-or-equal (`bvsge`) expression. + * */ open fun mkBvSignedGreaterOrEqualExprNoSimplify( arg0: KExpr, arg1: KExpr @@ -2222,9 +2524,15 @@ open class KContext( private val bvUnsignedGreaterExprCache = mkAstInterner>() + /** + * Create BitVec unsigned greater (`bvugt`) expression. + * */ open fun mkBvUnsignedGreaterExpr(arg0: KExpr, arg1: KExpr): KExpr = mkSimplified(arg0, arg1, KContext::simplifyBvUnsignedGreaterExpr, ::mkBvUnsignedGreaterExprNoSimplify) + /** + * Create BitVec unsigned greater (`bvugt`) expression. + * */ open fun mkBvUnsignedGreaterExprNoSimplify( arg0: KExpr, arg1: KExpr ): KBvUnsignedGreaterExpr = @@ -2235,9 +2543,15 @@ open class KContext( private val bvSignedGreaterExprCache = mkAstInterner>() + /** + * Create BitVec signed greater (`bvsgt`) expression. + * */ open fun mkBvSignedGreaterExpr(arg0: KExpr, arg1: KExpr): KExpr = mkSimplified(arg0, arg1, KContext::simplifyBvSignedGreaterExpr, ::mkBvSignedGreaterExprNoSimplify) + /** + * Create BitVec signed greater (`bvsgt`) expression. + * */ open fun mkBvSignedGreaterExprNoSimplify(arg0: KExpr, arg1: KExpr): KBvSignedGreaterExpr = bvSignedGreaterExprCache.createIfContextActive { ensureContextMatch(arg0, arg1) @@ -2246,9 +2560,15 @@ open class KContext( private val concatExprCache = mkAstInterner() + /** + * Create BitVec concatenation (`concat`) expression. + * */ open fun mkBvConcatExpr(arg0: KExpr, arg1: KExpr): KExpr = mkSimplified(arg0, arg1, KContext::simplifyBvConcatExpr, ::mkBvConcatExprNoSimplify) + /** + * Create BitVec concatenation (`concat`) expression. + * */ open fun mkBvConcatExprNoSimplify(arg0: KExpr, arg1: KExpr): KBvConcatExpr = concatExprCache.createIfContextActive { ensureContextMatch(arg0, arg1) @@ -2257,9 +2577,17 @@ open class KContext( private val extractExprCache = mkAstInterner() + /** + * Create BitVec extract (`extract`) expression. + * Extract bits from [low] (including) to [high] (including) as a new BitVec. + * */ open fun mkBvExtractExpr(high: Int, low: Int, value: KExpr): KExpr = mkSimplified(high, low, value, KContext::simplifyBvExtractExpr, ::mkBvExtractExprNoSimplify) + /** + * Create BitVec extract (`extract`) expression. + * Extract bits from [low] (including) to [high] (including) as a new BitVec. + * */ open fun mkBvExtractExprNoSimplify(high: Int, low: Int, value: KExpr): KBvExtractExpr = extractExprCache.createIfContextActive { ensureContextMatch(value) @@ -2268,9 +2596,19 @@ open class KContext( private val signExtensionExprCache = mkAstInterner() + /** + * 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]. + * */ open fun mkBvSignExtensionExpr(extensionSize: Int, value: KExpr): KExpr = mkSimplified(extensionSize, value, KContext::simplifyBvSignExtensionExpr, ::mkBvSignExtensionExprNoSimplify) + /** + * 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]. + * */ open fun mkBvSignExtensionExprNoSimplify( extensionSize: Int, value: KExpr @@ -2281,9 +2619,19 @@ open class KContext( private val zeroExtensionExprCache = mkAstInterner() + /** + * 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]. + * */ open fun mkBvZeroExtensionExpr(extensionSize: Int, value: KExpr): KExpr = mkSimplified(extensionSize, value, KContext::simplifyBvZeroExtensionExpr, ::mkBvZeroExtensionExprNoSimplify) + /** + * 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]. + * */ open fun mkBvZeroExtensionExprNoSimplify( extensionSize: Int, value: KExpr @@ -2294,9 +2642,17 @@ open class KContext( private val repeatExprCache = mkAstInterner() + /* + * Create BitVec repeat (`repeat`) expression. + * Returns a BitVec expression with [repeatNumber] concatenated copies of [value]. + * */ open fun mkBvRepeatExpr(repeatNumber: Int, value: KExpr): KExpr = mkSimplified(repeatNumber, value, KContext::simplifyBvRepeatExpr, ::mkBvRepeatExprNoSimplify) + /** + * Create BitVec repeat (`repeat`) expression. + * Returns a BitVec expression with [repeatNumber] concatenated copies of [value]. + * */ open fun mkBvRepeatExprNoSimplify( repeatNumber: Int, value: KExpr @@ -2307,9 +2663,15 @@ open class KContext( private val bvShiftLeftExprCache = mkAstInterner>() + /** + * Create BitVec shift left (`bvshl`) expression. + * */ open fun mkBvShiftLeftExpr(arg: KExpr, shift: KExpr): KExpr = mkSimplified(arg, shift, KContext::simplifyBvShiftLeftExpr, ::mkBvShiftLeftExprNoSimplify) + /** + * Create BitVec shift left (`bvshl`) expression. + * */ open fun mkBvShiftLeftExprNoSimplify(arg: KExpr, shift: KExpr): KBvShiftLeftExpr = bvShiftLeftExprCache.createIfContextActive { ensureContextMatch(arg, shift) @@ -2318,9 +2680,17 @@ open class KContext( private val bvLogicalShiftRightExprCache = mkAstInterner>() + /** + * Create BitVec logical shift right (`bvlshr`) expression. + * The shifted expressions is padded with zero bits. + * */ open fun mkBvLogicalShiftRightExpr(arg: KExpr, shift: KExpr): KExpr = mkSimplified(arg, shift, KContext::simplifyBvLogicalShiftRightExpr, ::mkBvLogicalShiftRightExprNoSimplify) + /** + * Create BitVec logical shift right (`bvlshr`) expression. + * The shifted expressions is padded with zero bits. + * */ open fun mkBvLogicalShiftRightExprNoSimplify( arg: KExpr, shift: KExpr ): KBvLogicalShiftRightExpr = @@ -2331,9 +2701,17 @@ open class KContext( private val bvArithShiftRightExprCache = mkAstInterner>() + /** + * Create BitVec arithmetic shift right (`bvashr`) expression. + * The shifted expressions is padded with sign (leftmost, highest) bits. + * */ open fun mkBvArithShiftRightExpr(arg: KExpr, shift: KExpr): KExpr = mkSimplified(arg, shift, KContext::simplifyBvArithShiftRightExpr, ::mkBvArithShiftRightExprNoSimplify) + /** + * Create BitVec arithmetic shift right (`bvashr`) expression. + * The shifted expressions is padded with sign (leftmost, highest) bits. + * */ open fun mkBvArithShiftRightExprNoSimplify( arg: KExpr, shift: KExpr ): KBvArithShiftRightExpr = @@ -2344,9 +2722,17 @@ open class KContext( private val bvRotateLeftExprCache = mkAstInterner>() + /** + * Create BitVec rotate left (`rotateleft`) expression. + * The result expression is rotated left [rotation] times. + * */ open fun mkBvRotateLeftExpr(arg: KExpr, rotation: KExpr): KExpr = mkSimplified(arg, rotation, KContext::simplifyBvRotateLeftExpr, ::mkBvRotateLeftExprNoSimplify) + /** + * Create BitVec rotate left (`rotateleft`) expression. + * The result expression is rotated left [rotation] times. + * */ open fun mkBvRotateLeftExprNoSimplify(arg: KExpr, rotation: KExpr): KBvRotateLeftExpr = bvRotateLeftExprCache.createIfContextActive { ensureContextMatch(arg, rotation) @@ -2355,9 +2741,17 @@ open class KContext( private val bvRotateLeftIndexedExprCache = mkAstInterner>() + /** + * Create BitVec rotate left (`rotateleft`) expression. + * The result expression is rotated left [rotation] times. + * */ open fun mkBvRotateLeftIndexedExpr(rotation: Int, value: KExpr): KExpr = mkSimplified(rotation, value, KContext::simplifyBvRotateLeftIndexedExpr, ::mkBvRotateLeftIndexedExprNoSimplify) + /** + * Create BitVec rotate left (`rotateleft`) expression. + * The result expression is rotated left [rotation] times. + * */ open fun mkBvRotateLeftIndexedExprNoSimplify( rotation: Int, value: KExpr ): KBvRotateLeftIndexedExpr = @@ -2368,6 +2762,10 @@ open class KContext( private val bvRotateRightIndexedExprCache = mkAstInterner>() + /** + * Create BitVec rotate right (`rotateright`) expression. + * The result expression is rotated right [rotation] times. + * */ open fun mkBvRotateRightIndexedExpr(rotation: Int, value: KExpr): KExpr = mkSimplified( rotation, @@ -2376,6 +2774,10 @@ open class KContext( ::mkBvRotateRightIndexedExprNoSimplify ) + /** + * Create BitVec rotate right (`rotateright`) expression. + * The result expression is rotated right [rotation] times. + * */ open fun mkBvRotateRightIndexedExprNoSimplify( rotation: Int, value: KExpr @@ -2387,9 +2789,17 @@ open class KContext( private val bvRotateRightExprCache = mkAstInterner>() + /** + * Create BitVec rotate right (`rotateright`) expression. + * The result expression is rotated right [rotation] times. + * */ open fun mkBvRotateRightExpr(arg: KExpr, rotation: KExpr): KExpr = mkSimplified(arg, rotation, KContext::simplifyBvRotateRightExpr, ::mkBvRotateRightExprNoSimplify) + /** + * Create BitVec rotate right (`rotateright`) expression. + * The result expression is rotated right [rotation] times. + * */ open fun mkBvRotateRightExprNoSimplify(arg: KExpr, rotation: KExpr): KBvRotateRightExpr = bvRotateRightExprCache.createIfContextActive { ensureContextMatch(arg, rotation) @@ -2398,9 +2808,17 @@ open class KContext( private val bv2IntExprCache = mkAstInterner() + /** + * Convert BitVec expressions [value] to the arithmetic Int expressions. + * When [isSigned] is set, the sign (highest, leftmost) bit is treated as the [value] sign. + * */ open fun mkBv2IntExpr(value: KExpr, isSigned: Boolean): KExpr = mkSimplified(value, isSigned, KContext::simplifyBv2IntExpr, ::mkBv2IntExprNoSimplify) + /** + * Convert BitVec expressions [value] to the arithmetic Int expressions. + * When [isSigned] is set, the sign (highest, leftmost) bit is treated as the [value] sign. + * */ open fun mkBv2IntExprNoSimplify(value: KExpr, isSigned: Boolean): KBv2IntExpr = bv2IntExprCache.createIfContextActive { ensureContextMatch(value) @@ -2409,9 +2827,23 @@ open class KContext( private val bvAddNoOverflowExprCache = mkAstInterner>() + /** + * 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. + * + * @see mkBvAddNoUnderflowExpr for the underflow check. + * */ open fun mkBvAddNoOverflowExpr(arg0: KExpr, arg1: KExpr, isSigned: Boolean): KExpr = mkSimplified(arg0, arg1, isSigned, KContext::simplifyBvAddNoOverflowExpr, ::mkBvAddNoOverflowExprNoSimplify) + /** + * 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. + * + * @see mkBvAddNoUnderflowExpr for the underflow check. + * */ open fun mkBvAddNoOverflowExprNoSimplify( arg0: KExpr, arg1: KExpr, @@ -2423,9 +2855,23 @@ open class KContext( private val bvAddNoUnderflowExprCache = mkAstInterner>() + /** + * 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. + * + * @see mkBvAddNoOverflowExpr for the overflow check. + * */ open fun mkBvAddNoUnderflowExpr(arg0: KExpr, arg1: KExpr): KExpr = mkSimplified(arg0, arg1, KContext::simplifyBvAddNoUnderflowExpr, ::mkBvAddNoUnderflowExprNoSimplify) + /** + * 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. + * + * @see mkBvAddNoOverflowExpr for the overflow check. + * */ open fun mkBvAddNoUnderflowExprNoSimplify(arg0: KExpr, arg1: KExpr): KBvAddNoUnderflowExpr = bvAddNoUnderflowExprCache.createIfContextActive { ensureContextMatch(arg0, arg1) @@ -2434,9 +2880,23 @@ open class KContext( private val bvSubNoOverflowExprCache = mkAstInterner>() + /** + * 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. + * + * @see mkBvSubNoUnderflowExpr for the underflow check. + * */ open fun mkBvSubNoOverflowExpr(arg0: KExpr, arg1: KExpr): KExpr = mkSimplified(arg0, arg1, KContext::simplifyBvSubNoOverflowExpr, ::mkBvSubNoOverflowExprNoSimplify) + /** + * 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. + * + * @see mkBvSubNoUnderflowExpr for the underflow check. + * */ open fun mkBvSubNoOverflowExprNoSimplify(arg0: KExpr, arg1: KExpr): KBvSubNoOverflowExpr = bvSubNoOverflowExprCache.createIfContextActive { ensureContextMatch(arg0, arg1) @@ -2445,9 +2905,23 @@ open class KContext( private val bvSubNoUnderflowExprCache = mkAstInterner>() + /** + * 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. + * + * @see mkBvSubNoOverflowExpr for the overflow check. + * */ open fun mkBvSubNoUnderflowExpr(arg0: KExpr, arg1: KExpr, isSigned: Boolean): KExpr = mkSimplified(arg0, arg1, isSigned, KContext::simplifyBvSubNoUnderflowExpr, ::mkBvSubNoUnderflowExprNoSimplify) + /** + * 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. + * + * @see mkBvSubNoOverflowExpr for the overflow check. + * */ open fun mkBvSubNoUnderflowExprNoSimplify( arg0: KExpr, arg1: KExpr, @@ -2459,9 +2933,17 @@ open class KContext( private val bvDivNoOverflowExprCache = mkAstInterner>() + /** + * Create BitVec div-no-overflow check expression. + * Determines that BitVec arithmetic signed division does not overflow. + * */ open fun mkBvDivNoOverflowExpr(arg0: KExpr, arg1: KExpr): KExpr = mkSimplified(arg0, arg1, KContext::simplifyBvDivNoOverflowExpr, ::mkBvDivNoOverflowExprNoSimplify) + /** + * Create BitVec div-no-overflow check expression. + * Determines that BitVec arithmetic signed division does not overflow. + * */ open fun mkBvDivNoOverflowExprNoSimplify(arg0: KExpr, arg1: KExpr): KBvDivNoOverflowExpr = bvDivNoOverflowExprCache.createIfContextActive { ensureContextMatch(arg0, arg1) @@ -2470,9 +2952,17 @@ open class KContext( private val bvNegNoOverflowExprCache = mkAstInterner>() + /** + * Create BitVec neg-no-overflow check expression. + * Determines that BitVec arithmetic negation does not overflow. + * */ open fun mkBvNegationNoOverflowExpr(value: KExpr): KExpr = mkSimplified(value, KContext::simplifyBvNegationNoOverflowExpr, ::mkBvNegationNoOverflowExprNoSimplify) + /** + * Create BitVec neg-no-overflow check expression. + * Determines that BitVec arithmetic negation does not overflow. + * */ open fun mkBvNegationNoOverflowExprNoSimplify(value: KExpr): KBvNegNoOverflowExpr = bvNegNoOverflowExprCache.createIfContextActive { ensureContextMatch(value) @@ -2481,9 +2971,23 @@ open class KContext( private val bvMulNoOverflowExprCache = mkAstInterner>() + /** + * 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. + * + * @see mkBvMulNoUnderflowExpr for the underflow check. + * */ open fun mkBvMulNoOverflowExpr(arg0: KExpr, arg1: KExpr, isSigned: Boolean): KExpr = mkSimplified(arg0, arg1, isSigned, KContext::simplifyBvMulNoOverflowExpr, ::mkBvMulNoOverflowExprNoSimplify) + /** + * 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. + * + * @see mkBvMulNoUnderflowExpr for the underflow check. + * */ open fun mkBvMulNoOverflowExprNoSimplify( arg0: KExpr, arg1: KExpr, @@ -2495,9 +2999,23 @@ open class KContext( private val bvMulNoUnderflowExprCache = mkAstInterner>() + /** + * 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. + * + * @see mkBvMulNoOverflowExpr for the overflow check. + * */ open fun mkBvMulNoUnderflowExpr(arg0: KExpr, arg1: KExpr): KExpr = mkSimplified(arg0, arg1, KContext::simplifyBvMulNoUnderflowExpr, ::mkBvMulNoUnderflowExprNoSimplify) + /** + * 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. + * + * @see mkBvMulNoOverflowExpr for the overflow check. + * */ open fun mkBvMulNoUnderflowExprNoSimplify(arg0: KExpr, arg1: KExpr): KBvMulNoUnderflowExpr = bvMulNoUnderflowExprCache.createIfContextActive { ensureContextMatch(arg0, arg1) From 98f3925b33c51a0055543370f1a82118365e62ce Mon Sep 17 00:00:00 2001 From: Saloed Date: Tue, 6 Jun 2023 14:26:38 +0300 Subject: [PATCH 3/6] Fp docs --- ksmt-core/src/main/kotlin/io/ksmt/KContext.kt | 297 +++++++++++++++++- 1 file changed, 293 insertions(+), 4 deletions(-) diff --git a/ksmt-core/src/main/kotlin/io/ksmt/KContext.kt b/ksmt-core/src/main/kotlin/io/ksmt/KContext.kt index 0111ac106..bade8be36 100644 --- a/ksmt-core/src/main/kotlin/io/ksmt/KContext.kt +++ b/ksmt-core/src/main/kotlin/io/ksmt/KContext.kt @@ -3030,7 +3030,7 @@ open class KContext( private val fpCustomSizeCache = mkAstInterner() /** - * Creates FP16 from the [value]. + * Create FP16 from the [value]. * * Important: we suppose that [value] has biased exponent, but FP16 will be created from the unbiased one. * So, at first, we'll subtract [KFp16Sort.exponentShiftSize] from the [value]'s exponent, @@ -3048,20 +3048,41 @@ open class KContext( } } + /** + * Create FP16 NaN value. + * */ fun mkFp16NaN(): KFp16Value = mkFp16WithoutNaNCheck(Float.NaN) private fun mkFp16WithoutNaNCheck(value: Float): KFp16Value = fp16Cache.createIfContextActive { KFp16Value(this, value) } + /** + * Create FP32 from the [value]. + * */ fun mkFp32(value: Float): KFp32Value = if (value.isNaN()) mkFp32NaN() else mkFp32WithoutNaNCheck(value) + + /** + * Create FP32 NaN value. + * */ fun mkFp32NaN(): KFp32Value = mkFp32WithoutNaNCheck(Float.NaN) private fun mkFp32WithoutNaNCheck(value: Float): KFp32Value = fp32Cache.createIfContextActive { KFp32Value(this, value) } + /** + * Create FP64 from the [value]. + * */ fun mkFp64(value: Double): KFp64Value = if (value.isNaN()) mkFp64NaN() else mkFp64WithoutNaNCheck(value) + + /** + * Create FP64 NaN value. + * */ fun mkFp64NaN(): KFp64Value = mkFp64WithoutNaNCheck(Double.NaN) private fun mkFp64WithoutNaNCheck(value: Double): KFp64Value = fp64Cache.createIfContextActive { KFp64Value(this, value) } + /** + * Create FP128 from the IEEE binary representation. + * Note: [biasedExponent] here is biased, i.e. unsigned. + * */ fun mkFp128Biased(significand: KBitVecValue<*>, biasedExponent: KBitVecValue<*>, signBit: Boolean): KFp128Value = if (KFp128Value(this, significand, biasedExponent, signBit).isNaN()) { mkFp128NaN() @@ -3069,6 +3090,9 @@ open class KContext( mkFp128BiasedWithoutNaNCheck(significand, biasedExponent, signBit) } + /** + * Create FP128 NaN value. + * */ fun mkFp128NaN(): KFp128Value = mkFpNaN(mkFp128Sort()).cast() private fun mkFp128BiasedWithoutNaNCheck( significand: KBitVecValue<*>, @@ -3079,6 +3103,10 @@ open class KContext( KFp128Value(this, significand, biasedExponent, signBit) } + /** + * Create FP128 from the IEEE binary representation. + * Note: [unbiasedExponent] here is unbiased, i.e. signed. + * */ fun mkFp128(significand: KBitVecValue<*>, unbiasedExponent: KBitVecValue<*>, signBit: Boolean): KFp128Value = mkFp128Biased( significand = significand, @@ -3086,6 +3114,10 @@ open class KContext( signBit = signBit ) + /** + * Create FP128 from the IEEE binary representation. + * Note: [unbiasedExponent] here is unbiased, i.e. signed. + * */ fun mkFp128(significand: Long, unbiasedExponent: Long, signBit: Boolean): KFp128Value = mkFp128( significand = mkBvUnsigned(significand, KFp128Sort.significandBits - 1u), @@ -3100,7 +3132,7 @@ open class KContext( get() = mkFp64(this) /** - * Creates FP with a custom size. + * Create FP with a custom size from the IEEE binary representation. * Important: [unbiasedExponent] here is an **unbiased** value. */ fun mkFpCustomSize( @@ -3140,7 +3172,7 @@ open class KContext( } /** - * Creates FP with a custom size. + * Create FP with a custom size from the IEEE binary representation. * Important: [biasedExponent] here is an **biased** value. */ fun mkFpCustomSizeBiased( @@ -3224,6 +3256,10 @@ open class KContext( } } + /** + * Create FP with a custom size from the IEEE binary representation. + * Important: [unbiasedExponent] here is an **unbiased** value. + */ fun mkFpCustomSize( unbiasedExponent: KBitVecValue, significand: KBitVecValue, @@ -3421,7 +3457,7 @@ open class KContext( ) /** - * Special Fp values + * Create Fp zero value with [signBit] sign. * */ @Suppress("MagicNumber") fun mkFpZero(signBit: Boolean, sort: T): KFpValue = when (sort) { @@ -3437,6 +3473,9 @@ open class KContext( ) } + /** + * Create Fp Inf value with [signBit] sign. + * */ fun mkFpInf(signBit: Boolean, sort: T): KFpValue = when (sort) { is KFp16Sort -> mkFp16(if (signBit) Float.NEGATIVE_INFINITY else Float.POSITIVE_INFINITY).cast() is KFp32Sort -> mkFp32(if (signBit) Float.NEGATIVE_INFINITY else Float.POSITIVE_INFINITY).cast() @@ -3450,6 +3489,9 @@ open class KContext( ) } + /** + * Create Fp NaN value. + * */ fun mkFpNaN(sort: T): KFpValue = when (sort) { is KFp16Sort -> mkFp16NaN().cast() is KFp32Sort -> mkFp32NaN().cast() @@ -3464,6 +3506,11 @@ open class KContext( private val roundingModeCache = mkAstInterner() + /** + * Create Fp rounding mode. + * + * @see [KFpRoundingMode] + * */ fun mkFpRoundingModeExpr( value: KFpRoundingMode ): KFpRoundingModeExpr = roundingModeCache.createIfContextActive { @@ -3472,9 +3519,15 @@ open class KContext( private val fpAbsExprCache = mkAstInterner>() + /** + * Create Fp absolute value (`fp.abs`) expression. + * */ open fun mkFpAbsExpr(value: KExpr): KExpr = mkSimplified(value, KContext::simplifyFpAbsExpr, ::mkFpAbsExprNoSimplify) + /** + * Create Fp absolute value (`fp.abs`) expression. + * */ open fun mkFpAbsExprNoSimplify( value: KExpr ): KFpAbsExpr = fpAbsExprCache.createIfContextActive { @@ -3484,9 +3537,15 @@ open class KContext( private val fpNegationExprCache = mkAstInterner>() + /** + * Create Fp negation (`fp.neg`) expression. + * */ open fun mkFpNegationExpr(value: KExpr): KExpr = mkSimplified(value, KContext::simplifyFpNegationExpr, ::mkFpNegationExprNoSimplify) + /** + * Create Fp negation (`fp.neg`) expression. + * */ open fun mkFpNegationExprNoSimplify( value: KExpr ): KFpNegationExpr = fpNegationExprCache.createIfContextActive { @@ -3496,11 +3555,19 @@ open class KContext( private val fpAddExprCache = mkAstInterner>() + /** + * Create Fp addition (`fp.add`) expression. + * The result is rounded according to the provided [roundingMode]. + * */ open fun mkFpAddExpr( roundingMode: KExpr, arg0: KExpr, arg1: KExpr ): KExpr = mkSimplified(roundingMode, arg0, arg1, KContext::simplifyFpAddExpr, ::mkFpAddExprNoSimplify) + /** + * Create Fp addition (`fp.add`) expression. + * The result is rounded according to the provided [roundingMode]. + * */ open fun mkFpAddExprNoSimplify( roundingMode: KExpr, arg0: KExpr, @@ -3512,11 +3579,19 @@ open class KContext( private val fpSubExprCache = mkAstInterner>() + /** + * Create Fp subtraction (`fp.sub`) expression. + * The result is rounded according to the provided [roundingMode]. + * */ open fun mkFpSubExpr( roundingMode: KExpr, arg0: KExpr, arg1: KExpr ): KExpr = mkSimplified(roundingMode, arg0, arg1, KContext::simplifyFpSubExpr, ::mkFpSubExprNoSimplify) + /** + * Create Fp subtraction (`fp.sub`) expression. + * The result is rounded according to the provided [roundingMode]. + * */ open fun mkFpSubExprNoSimplify( roundingMode: KExpr, arg0: KExpr, @@ -3528,11 +3603,19 @@ open class KContext( private val fpMulExprCache = mkAstInterner>() + /** + * Create Fp multiplication (`fp.mul`) expression. + * The result is rounded according to the provided [roundingMode]. + * */ open fun mkFpMulExpr( roundingMode: KExpr, arg0: KExpr, arg1: KExpr ): KExpr = mkSimplified(roundingMode, arg0, arg1, KContext::simplifyFpMulExpr, ::mkFpMulExprNoSimplify) + /** + * Create Fp multiplication (`fp.mul`) expression. + * The result is rounded according to the provided [roundingMode]. + * */ open fun mkFpMulExprNoSimplify( roundingMode: KExpr, arg0: KExpr, @@ -3544,11 +3627,19 @@ open class KContext( private val fpDivExprCache = mkAstInterner>() + /** + * Create Fp division (`fp.div`) expression. + * The result is rounded according to the provided [roundingMode]. + * */ open fun mkFpDivExpr( roundingMode: KExpr, arg0: KExpr, arg1: KExpr ): KExpr = mkSimplified(roundingMode, arg0, arg1, KContext::simplifyFpDivExpr, ::mkFpDivExprNoSimplify) + /** + * Create Fp division (`fp.div`) expression. + * The result is rounded according to the provided [roundingMode]. + * */ open fun mkFpDivExprNoSimplify( roundingMode: KExpr, arg0: KExpr, @@ -3560,6 +3651,11 @@ open class KContext( private val fpFusedMulAddExprCache = mkAstInterner>() + /** + * Create Fp fused multiplication and addition (`fp.fma`) expression. + * Computes ([arg0] * [arg1]) + [arg2]. + * The result is rounded according to the provided [roundingMode]. + * */ open fun mkFpFusedMulAddExpr( roundingMode: KExpr, arg0: KExpr, @@ -3574,6 +3670,12 @@ open class KContext( ::mkFpFusedMulAddExprNoSimplify ) + + /** + * Create Fp fused multiplication and addition (`fp.fma`) expression. + * Computes ([arg0] * [arg1]) + [arg2]. + * The result is rounded according to the provided [roundingMode]. + * */ open fun mkFpFusedMulAddExprNoSimplify( roundingMode: KExpr, arg0: KExpr, @@ -3586,9 +3688,17 @@ open class KContext( private val fpSqrtExprCache = mkAstInterner>() + /** + * Create Fp square root (`fp.sqrt`) expression. + * The result is rounded according to the provided [roundingMode]. + * */ open fun mkFpSqrtExpr(roundingMode: KExpr, value: KExpr): KExpr = mkSimplified(roundingMode, value, KContext::simplifyFpSqrtExpr, ::mkFpSqrtExprNoSimplify) + /** + * Create Fp square root (`fp.sqrt`) expression. + * The result is rounded according to the provided [roundingMode]. + * */ open fun mkFpSqrtExprNoSimplify( roundingMode: KExpr, value: KExpr @@ -3599,9 +3709,15 @@ open class KContext( private val fpRemExprCache = mkAstInterner>() + /** + * Create Fp IEEE remainder (`fp.IEEERem`) expression. + * */ open fun mkFpRemExpr(arg0: KExpr, arg1: KExpr): KExpr = mkSimplified(arg0, arg1, KContext::simplifyFpRemExpr, ::mkFpRemExprNoSimplify) + /** + * Create Fp IEEE remainder (`fp.IEEERem`) expression. + * */ open fun mkFpRemExprNoSimplify(arg0: KExpr, arg1: KExpr): KFpRemExpr = fpRemExprCache.createIfContextActive { ensureContextMatch(arg0, arg1) @@ -3610,11 +3726,19 @@ open class KContext( private val fpRoundToIntegralExprCache = mkAstInterner>() + /** + * Create Fp round to integral (`fp.roundToIntegral`) expression. + * The rounding is performed according to the provided [roundingMode]. + * */ open fun mkFpRoundToIntegralExpr( roundingMode: KExpr, value: KExpr ): KExpr = mkSimplified(roundingMode, value, KContext::simplifyFpRoundToIntegralExpr, ::mkFpRoundToIntegralExprNoSimplify) + /** + * Create Fp round to integral (`fp.roundToIntegral`) expression. + * The rounding is performed according to the provided [roundingMode]. + * */ open fun mkFpRoundToIntegralExprNoSimplify( roundingMode: KExpr, value: KExpr @@ -3625,9 +3749,15 @@ open class KContext( private val fpMinExprCache = mkAstInterner>() + /** + * Create Fp minimum (`fp.min`) expression. + * */ open fun mkFpMinExpr(arg0: KExpr, arg1: KExpr): KExpr = mkSimplified(arg0, arg1, KContext::simplifyFpMinExpr, ::mkFpMinExprNoSimplify) + /** + * Create Fp minimum (`fp.min`) expression. + * */ open fun mkFpMinExprNoSimplify(arg0: KExpr, arg1: KExpr): KFpMinExpr = fpMinExprCache.createIfContextActive { ensureContextMatch(arg0, arg1) @@ -3636,9 +3766,15 @@ open class KContext( private val fpMaxExprCache = mkAstInterner>() + /** + * Create Fp maximum (`fp.max`) expression. + * */ open fun mkFpMaxExpr(arg0: KExpr, arg1: KExpr): KExpr = mkSimplified(arg0, arg1, KContext::simplifyFpMaxExpr, ::mkFpMaxExprNoSimplify) + /** + * Create Fp maximum (`fp.max`) expression. + * */ open fun mkFpMaxExprNoSimplify(arg0: KExpr, arg1: KExpr): KFpMaxExpr = fpMaxExprCache.createIfContextActive { ensureContextMatch(arg0, arg1) @@ -3647,9 +3783,15 @@ open class KContext( private val fpLessOrEqualExprCache = mkAstInterner>() + /** + * Create Fp less-or-equal comparison (`fp.leq`) expression. + * */ open fun mkFpLessOrEqualExpr(arg0: KExpr, arg1: KExpr): KExpr = mkSimplified(arg0, arg1, KContext::simplifyFpLessOrEqualExpr, ::mkFpLessOrEqualExprNoSimplify) + /** + * Create Fp less-or-equal comparison (`fp.leq`) expression. + * */ open fun mkFpLessOrEqualExprNoSimplify(arg0: KExpr, arg1: KExpr): KFpLessOrEqualExpr = fpLessOrEqualExprCache.createIfContextActive { ensureContextMatch(arg0, arg1) @@ -3658,9 +3800,15 @@ open class KContext( private val fpLessExprCache = mkAstInterner>() + /** + * Create Fp less comparison (`fp.lt`) expression. + * */ open fun mkFpLessExpr(arg0: KExpr, arg1: KExpr): KExpr = mkSimplified(arg0, arg1, KContext::simplifyFpLessExpr, ::mkFpLessExprNoSimplify) + /** + * Create Fp less comparison (`fp.lt`) expression. + * */ open fun mkFpLessExprNoSimplify(arg0: KExpr, arg1: KExpr): KFpLessExpr = fpLessExprCache.createIfContextActive { ensureContextMatch(arg0, arg1) @@ -3669,9 +3817,15 @@ open class KContext( private val fpGreaterOrEqualExprCache = mkAstInterner>() + /** + * Create Fp greater-or-equal comparison (`fp.geq`) expression. + * */ open fun mkFpGreaterOrEqualExpr(arg0: KExpr, arg1: KExpr): KExpr = mkSimplified(arg0, arg1, KContext::simplifyFpGreaterOrEqualExpr, ::mkFpGreaterOrEqualExprNoSimplify) + /** + * Create Fp greater-or-equal comparison (`fp.geq`) expression. + * */ open fun mkFpGreaterOrEqualExprNoSimplify(arg0: KExpr, arg1: KExpr): KFpGreaterOrEqualExpr = fpGreaterOrEqualExprCache.createIfContextActive { ensureContextMatch(arg0, arg1) @@ -3680,9 +3834,15 @@ open class KContext( private val fpGreaterExprCache = mkAstInterner>() + /** + * Create Fp greater comparison (`fp.gt`) expression. + * */ open fun mkFpGreaterExpr(arg0: KExpr, arg1: KExpr): KExpr = mkSimplified(arg0, arg1, KContext::simplifyFpGreaterExpr, ::mkFpGreaterExprNoSimplify) + /** + * Create Fp greater comparison (`fp.gt`) expression. + * */ open fun mkFpGreaterExprNoSimplify(arg0: KExpr, arg1: KExpr): KFpGreaterExpr = fpGreaterExprCache.createIfContextActive { ensureContextMatch(arg0, arg1) @@ -3691,9 +3851,21 @@ open class KContext( private val fpEqualExprCache = mkAstInterner>() + /** + * Create Fp equality comparison (`fp.eq`) expression. + * Checks arguments equality using IEEE 754-2008 rules. + * + * @see [mkEq] for smt equality. + * */ open fun mkFpEqualExpr(arg0: KExpr, arg1: KExpr): KExpr = mkSimplified(arg0, arg1, KContext::simplifyFpEqualExpr, ::mkFpEqualExprNoSimplify) + /** + * Create Fp equality comparison (`fp.eq`) expression. + * Checks arguments equality using IEEE 754-2008 rules. + * + * @see [mkEq] for smt equality. + * */ open fun mkFpEqualExprNoSimplify(arg0: KExpr, arg1: KExpr): KFpEqualExpr = fpEqualExprCache.createIfContextActive { ensureContextMatch(arg0, arg1) @@ -3702,9 +3874,15 @@ open class KContext( private val fpIsNormalExprCache = mkAstInterner>() + /** + * Create Fp is-normal check (`fp.isNormal`) expression. + * */ open fun mkFpIsNormalExpr(value: KExpr): KExpr = mkSimplified(value, KContext::simplifyFpIsNormalExpr, ::mkFpIsNormalExprNoSimplify) + /** + * Create Fp is-normal check (`fp.isNormal`) expression. + * */ open fun mkFpIsNormalExprNoSimplify(value: KExpr): KFpIsNormalExpr = fpIsNormalExprCache.createIfContextActive { ensureContextMatch(value) @@ -3713,9 +3891,15 @@ open class KContext( private val fpIsSubnormalExprCache = mkAstInterner>() + /** + * Create Fp is-subnormal check (`fp.isSubnormal`) expression. + * */ open fun mkFpIsSubnormalExpr(value: KExpr): KExpr = mkSimplified(value, KContext::simplifyFpIsSubnormalExpr, ::mkFpIsSubnormalExprNoSimplify) + /** + * Create Fp is-subnormal check (`fp.isSubnormal`) expression. + * */ open fun mkFpIsSubnormalExprNoSimplify(value: KExpr): KFpIsSubnormalExpr = fpIsSubnormalExprCache.createIfContextActive { ensureContextMatch(value) @@ -3724,9 +3908,15 @@ open class KContext( private val fpIsZeroExprCache = mkAstInterner>() + /** + * Create Fp is-zero check (`fp.isZero`) expression. + * */ open fun mkFpIsZeroExpr(value: KExpr): KExpr = mkSimplified(value, KContext::simplifyFpIsZeroExpr, ::mkFpIsZeroExprNoSimplify) + /** + * Create Fp is-zero check (`fp.isZero`) expression. + * */ open fun mkFpIsZeroExprNoSimplify(value: KExpr): KFpIsZeroExpr = fpIsZeroExprCache.createIfContextActive { ensureContextMatch(value) @@ -3735,9 +3925,15 @@ open class KContext( private val fpIsInfiniteExprCache = mkAstInterner>() + /** + * Create Fp is-inf check (`fp.isInfinite`) expression. + * */ open fun mkFpIsInfiniteExpr(value: KExpr): KExpr = mkSimplified(value, KContext::simplifyFpIsInfiniteExpr, ::mkFpIsInfiniteExprNoSimplify) + /** + * Create Fp is-inf check (`fp.isInfinite`) expression. + * */ open fun mkFpIsInfiniteExprNoSimplify(value: KExpr): KFpIsInfiniteExpr = fpIsInfiniteExprCache.createIfContextActive { ensureContextMatch(value) @@ -3746,9 +3942,15 @@ open class KContext( private val fpIsNaNExprCache = mkAstInterner>() + /** + * Create Fp is-nan check (`fp.isNaN`) expression. + * */ open fun mkFpIsNaNExpr(value: KExpr): KExpr = mkSimplified(value, KContext::simplifyFpIsNaNExpr, ::mkFpIsNaNExprNoSimplify) + /** + * Create Fp is-nan check (`fp.isNaN`) expression. + * */ open fun mkFpIsNaNExprNoSimplify(value: KExpr): KFpIsNaNExpr = fpIsNaNExprCache.createIfContextActive { ensureContextMatch(value) @@ -3757,9 +3959,15 @@ open class KContext( private val fpIsNegativeExprCache = mkAstInterner>() + /** + * Create Fp is-negative check (`fp.isNegative`) expression. + * */ open fun mkFpIsNegativeExpr(value: KExpr): KExpr = mkSimplified(value, KContext::simplifyFpIsNegativeExpr, ::mkFpIsNegativeExprNoSimplify) + /** + * Create Fp is-negative check (`fp.isNegative`) expression. + * */ open fun mkFpIsNegativeExprNoSimplify(value: KExpr): KFpIsNegativeExpr = fpIsNegativeExprCache.createIfContextActive { ensureContextMatch(value) @@ -3768,9 +3976,15 @@ open class KContext( private val fpIsPositiveExprCache = mkAstInterner>() + /** + * Create Fp is-positive check (`fp.isPositive`) expression. + * */ open fun mkFpIsPositiveExpr(value: KExpr): KExpr = mkSimplified(value, KContext::simplifyFpIsPositiveExpr, ::mkFpIsPositiveExprNoSimplify) + /** + * Create Fp is-positive check (`fp.isPositive`) expression. + * */ open fun mkFpIsPositiveExprNoSimplify(value: KExpr): KFpIsPositiveExpr = fpIsPositiveExprCache.createIfContextActive { ensureContextMatch(value) @@ -3779,6 +3993,12 @@ open class KContext( private val fpToBvExprCache = mkAstInterner>() + /** + * 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]. + * + * @see [mkFpToIEEEBvExpr] for binary conversion. + * */ open fun mkFpToBvExpr( roundingMode: KExpr, value: KExpr, @@ -3787,6 +4007,12 @@ open class KContext( ): KExpr = mkSimplified(roundingMode, value, bvSize, isSigned, KContext::simplifyFpToBvExpr, ::mkFpToBvExprNoSimplify) + /** + * 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]. + * + * @see [mkFpToIEEEBvExpr] for binary conversion. + * */ open fun mkFpToBvExprNoSimplify( roundingMode: KExpr, value: KExpr, @@ -3799,9 +4025,15 @@ open class KContext( private val fpToRealExprCache = mkAstInterner>() + /** + * Create Fp to Real conversion (`fp.to_real`) expression. + * */ open fun mkFpToRealExpr(value: KExpr): KExpr = mkSimplified(value, KContext::simplifyFpToRealExpr, ::mkFpToRealExprNoSimplify) + /** + * Create Fp to Real conversion (`fp.to_real`) expression. + * */ open fun mkFpToRealExprNoSimplify(value: KExpr): KFpToRealExpr = fpToRealExprCache.createIfContextActive { ensureContextMatch(value) @@ -3810,9 +4042,21 @@ open class KContext( private val fpToIEEEBvExprCache = mkAstInterner>() + /** + * Create Fp to IEEE BitVec conversion expression. + * Converts Fp value to the corresponding IEEE 754-2008 binary format. + * + * Note: conversion is unspecified for NaN values. + * */ open fun mkFpToIEEEBvExpr(value: KExpr): KExpr = mkSimplified(value, KContext::simplifyFpToIEEEBvExpr, ::mkFpToIEEEBvExprNoSimplify) + /** + * Create Fp to IEEE BitVec conversion expression. + * Converts Fp value to the corresponding IEEE 754-2008 binary format. + * + * Note: conversion is unspecified for NaN values. + * */ open fun mkFpToIEEEBvExprNoSimplify(value: KExpr): KFpToIEEEBvExpr = fpToIEEEBvExprCache.createIfContextActive { ensureContextMatch(value) @@ -3821,6 +4065,9 @@ open class KContext( private val fpFromBvExprCache = mkAstInterner>() + /** + * Create Fp from IEEE BitVec expressions. + * */ open fun mkFpFromBvExpr( sign: KExpr, biasedExponent: KExpr, @@ -3833,6 +4080,9 @@ open class KContext( ::mkFpFromBvExprNoSimplify ) + /** + * Create Fp from IEEE BitVec expressions. + * */ open fun mkFpFromBvExprNoSimplify( sign: KExpr, biasedExponent: KExpr, @@ -3852,12 +4102,20 @@ open class KContext( private val realToFpExprCache = mkAstInterner>() private val bvToFpExprCache = mkAstInterner>() + /** + * Create Fp to another Fp. + * Rounding is performed according to the [roundingMode]. + * */ open fun mkFpToFpExpr( sort: T, roundingMode: KExpr, value: KExpr ): KExpr = mkSimplified(sort, roundingMode, value, KContext::simplifyFpToFpExpr, ::mkFpToFpExprNoSimplify) + /** + * Create Fp to another Fp. + * Rounding is performed according to the [roundingMode]. + * */ open fun mkFpToFpExprNoSimplify( sort: T, roundingMode: KExpr, @@ -3867,12 +4125,20 @@ open class KContext( KFpToFpExpr(this, sort, roundingMode, value) }.cast() + /** + * Create Fp from Real expression. + * Rounding is performed according to the [roundingMode]. + * */ open fun mkRealToFpExpr( sort: T, roundingMode: KExpr, value: KExpr ): KExpr = mkSimplified(sort, roundingMode, value, KContext::simplifyRealToFpExpr, ::mkRealToFpExprNoSimplify) + /** + * Create Fp from Real expression. + * Rounding is performed according to the [roundingMode]. + * */ open fun mkRealToFpExprNoSimplify( sort: T, roundingMode: KExpr, @@ -3882,6 +4148,12 @@ open class KContext( KRealToFpExpr(this, sort, roundingMode, value) }.cast() + /** + * Create Fp from BitVec value. + * Rounding is performed according to the [roundingMode]. + * + * @see [mkFpFromBvExpr] for IEEE binary conversion. + * */ open fun mkBvToFpExpr( sort: T, roundingMode: KExpr, @@ -3890,6 +4162,12 @@ open class KContext( ): KExpr = mkSimplified(sort, roundingMode, value, signed, KContext::simplifyBvToFpExpr, ::mkBvToFpExprNoSimplify) + /** + * Create Fp from BitVec value. + * Rounding is performed according to the [roundingMode]. + * + * @see [mkFpFromBvExpr] for IEEE binary conversion. + * */ open fun mkBvToFpExprNoSimplify( sort: T, roundingMode: KExpr, @@ -3903,6 +4181,9 @@ open class KContext( // quantifiers private val existentialQuantifierCache = mkAstInterner() + /** + * Create existential quantifier (`exists`). + * */ open fun mkExistentialQuantifier(body: KExpr, bounds: List>) = existentialQuantifierCache.createIfContextActive { ensureContextMatch(body) @@ -3912,6 +4193,9 @@ open class KContext( private val universalQuantifierCache = mkAstInterner() + /** + * Create universal quantifier (`forall`). + * */ open fun mkUniversalQuantifier(body: KExpr, bounds: List>) = universalQuantifierCache.createIfContextActive { ensureContextMatch(body) @@ -3921,6 +4205,11 @@ open class KContext( private val uninterpretedSortValueCache = mkAstInterner() + /** + * Create uninterpreted sort value. + * + * Note: uninterpreted sort values with different [valueIdx] are distinct. + * */ open fun mkUninterpretedSortValue(sort: KUninterpretedSort, valueIdx: Int): KUninterpretedSortValue = uninterpretedSortValueCache.createIfContextActive { ensureContextMatch(sort) From 44c9bbb037e085d46712943b58f0eef535e74f38 Mon Sep 17 00:00:00 2001 From: Saloed Date: Tue, 6 Jun 2023 16:55:53 +0300 Subject: [PATCH 4/6] Docs for mod/rem operations --- ksmt-core/src/main/kotlin/io/ksmt/KContext.kt | 60 +++++++++++++++---- 1 file changed, 49 insertions(+), 11 deletions(-) diff --git a/ksmt-core/src/main/kotlin/io/ksmt/KContext.kt b/ksmt-core/src/main/kotlin/io/ksmt/KContext.kt index bade8be36..a73f9dfc2 100644 --- a/ksmt-core/src/main/kotlin/io/ksmt/KContext.kt +++ b/ksmt-core/src/main/kotlin/io/ksmt/KContext.kt @@ -1521,12 +1521,28 @@ open class KContext( /** * Create an Int/Real arithmetic division expression. + * + * Note for Int division: + * + * when [rhs] is positive, (div [lhs] [rhs]) is the floor (round toward zero) + * of the rational number [lhs]/[rhs] + * + * when [rhs] is negative, (div [lhs] [rhs]) is the ceiling (round toward positive infinity) + * of the rational number [lhs]/[rhs] + * + * For example: + * `47 div 13 = 3` + * `47 div -13 = -3` + * `-47 div 13 = -4` + * `-47 div -13 = 4` * */ open fun mkArithDiv(lhs: KExpr, rhs: KExpr): KExpr = mkSimplified(lhs, rhs, KContext::simplifyArithDiv, ::mkArithDivNoSimplify) /** * Create an Int/Real arithmetic division expression. + * + * @see mkArithDiv for the operation details. * */ open fun mkArithDivNoSimplify(lhs: KExpr, rhs: KExpr): KDivArithExpr = arithDivCache.createIfContextActive { @@ -1637,7 +1653,16 @@ open class KContext( /** * Create an Int mod expression. * - * todo: clarify + * The result value is a number `r` such that + * [lhs] = `r` + ([rhs] * (div [lhs] [rhs])) + * where `div` is an Int division that works according to the [mkArithDiv] rules. + * The result value is always positive or zero. + * + * For example: + * `47 mod 13 = 8` + * `47 mod -13 = 8` + * `-47 mod 13 = 5` + * `-47 mod -13 = 5` * */ open fun mkIntMod(lhs: KExpr, rhs: KExpr): KExpr = mkSimplified(lhs, rhs, KContext::simplifyIntMod, ::mkIntModNoSimplify) @@ -1645,7 +1670,7 @@ open class KContext( /** * Create an Int mod expression. * - * @see mkIntMod + * @see mkIntMod for the operation details. * */ open fun mkIntModNoSimplify( lhs: KExpr, @@ -1659,8 +1684,10 @@ open class KContext( /** * 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. * - * todo: clarify + * @see mkIntMod * */ open fun mkIntRem(lhs: KExpr, rhs: KExpr): KExpr = mkSimplified(lhs, rhs, KContext::simplifyIntRem, ::mkIntRemNoSimplify) @@ -1668,7 +1695,7 @@ open class KContext( /** * Create an Int rem expression. * - * @see mkIntRem + * @see mkIntRem for the operation details. * */ open fun mkIntRemNoSimplify( lhs: KExpr, @@ -2366,7 +2393,14 @@ open class KContext( /** * Create BitVec arithmetic signed reminder (`bvsrem`) expression. * - * todo: clarify + * Computes remainder of a `truncate` (round toward zero) division. + * The result sign matches the [arg0] sign. + * + * For example: + * `47 bvsrem 13 = 8` + * `47 bvsrem -13 = 8` + * `-47 bvsrem 13 = -8` + * `-47 bvsrem -13 = -8` * * @see mkBvUnsignedRemExpr for the unsigned remainder. * */ @@ -2375,9 +2409,7 @@ open class KContext( /** * Create BitVec arithmetic signed reminder (`bvsrem`) expression. - * - * todo: clarify - * + * @see [mkBvSignedRemExpr] for the operation details. * @see mkBvUnsignedRemExpr for the unsigned remainder. * */ open fun mkBvSignedRemExprNoSimplify(arg0: KExpr, arg1: KExpr): KBvSignedRemExpr = @@ -2391,15 +2423,21 @@ open class KContext( /** * Create BitVec arithmetic signed mod (`bvsmod`) expression. * - * todo: clarify + * Computes remainder of a `floor` (round toward negative infinity) division. + * The result sign matches the [arg1] sign. + * + * For example: + * `47 bvsmod 13 = 8` + * `47 bvsmod -13 = -5` + * `-47 bvsmod 13 = 5` + * `-47 bvsmod -13 = -8` * */ open fun mkBvSignedModExpr(arg0: KExpr, arg1: KExpr): KExpr = mkSimplified(arg0, arg1, KContext::simplifyBvSignedModExpr, ::mkBvSignedModExprNoSimplify) /** * Create BitVec arithmetic signed mod (`bvsmod`) expression. - * - * todo: clarify + * @see [mkBvSignedModExpr] for the operation details. * */ open fun mkBvSignedModExprNoSimplify(arg0: KExpr, arg1: KExpr): KBvSignedModExpr = bvSignedModExprCache.createIfContextActive { From 35eb72e554a2aed056cee5bec3d2c07212f8ff31 Mon Sep 17 00:00:00 2001 From: Saloed Date: Fri, 9 Jun 2023 11:38:04 +0300 Subject: [PATCH 5/6] Fix documentation text issues --- ksmt-core/src/main/kotlin/io/ksmt/KContext.kt | 44 ++++++++++++++----- 1 file changed, 34 insertions(+), 10 deletions(-) diff --git a/ksmt-core/src/main/kotlin/io/ksmt/KContext.kt b/ksmt-core/src/main/kotlin/io/ksmt/KContext.kt index a73f9dfc2..c62a352ff 100644 --- a/ksmt-core/src/main/kotlin/io/ksmt/KContext.kt +++ b/ksmt-core/src/main/kotlin/io/ksmt/KContext.kt @@ -1161,8 +1161,10 @@ open class KContext( /** * Create an array store expression (store [array] [index] [value]) without cache. + * Cache is used to speed up [mkArraySelect] operation simplification + * but can result in a huge memory consumption. * - * @see [KArrayStoreBase] + * @see [KArrayStoreBase] for the cache details. * */ open fun mkArrayStoreNoSimplifyNoAnalyze( array: KExpr>, @@ -1174,9 +1176,11 @@ open class KContext( }.cast() /** - * Create an array store expression (store [array] [index0] [index1] [value]). + * Create an array store expression (store [array] [index0] [index1] [value]) without cache. + * Cache is used to speed up [mkArraySelect] operation simplification + * but can result in a huge memory consumption. * - * @see [KArrayStoreBase] + * @see [KArrayStoreBase] for the cache details. * */ open fun mkArrayStoreNoSimplifyNoAnalyze( array: KExpr>, @@ -1189,9 +1193,11 @@ open class KContext( }.cast() /** - * Create an array store expression (store [array] [index0] [index1] [index2] [value]). + * Create an array store expression (store [array] [index0] [index1] [index2] [value]) without cache. + * Cache is used to speed up [mkArraySelect] operation simplification + * but can result in a huge memory consumption. * - * @see [KArrayStoreBase] + * @see [KArrayStoreBase] for the cache details. * */ open fun mkArrayStoreNoSimplifyNoAnalyze( array: KExpr>, @@ -1206,8 +1212,10 @@ open class KContext( /** * Create n-ary array store expression (store [array] [indices]_0 ... [indices]_n [value]) without cache. + * Cache is used to speed up [mkArrayNSelect] operation simplification + * but can result in a huge memory consumption. * - * @see [KArrayStoreBase] + * @see [KArrayStoreBase] for the cache details. * */ open fun mkArrayNStoreNoSimplifyNoAnalyze( array: KExpr>, @@ -1996,10 +2004,10 @@ open class KContext( /** * Create a BitVec value with [sizeBits] bit length. * - * Note: if [sizeBits] is less than 32, + * Note: if [sizeBits] is less than 64, * the last [sizeBits] bits of the [value] will be taken. * - * At the same time, if [sizeBits] is greater than 32, + * At the same time, if [sizeBits] is greater than 64, * binary representation of the [value] will be padded from the start with its sign bit. * */ fun mkBv(value: Long, sizeBits: UInt): KBitVecValue = mkBv(value as Number, sizeBits) @@ -2059,13 +2067,13 @@ open class KContext( private fun Number.toBv(sizeBits: UInt) = mkBv(this, sizeBits) /** - * Create a BitVec value with [sizeBits] bit length from the given binary stirng [value]. + * Create a BitVec value with [sizeBits] bit length from the given binary string [value]. * */ fun mkBv(value: String, sizeBits: UInt): KBitVecValue = mkBv(value.toBigInteger(radix = 2), sizeBits) /** - * Create a BitVec value with [sizeBits] bit length from the given hex stirng [value]. + * Create a BitVec value with [sizeBits] bit length from the given hex string [value]. * */ fun mkBvHex(value: String, sizeBits: UInt): KBitVecValue = mkBv(value.toBigInteger(radix = 16), sizeBits) @@ -2763,6 +2771,8 @@ open class KContext( /** * Create BitVec rotate left (`rotateleft`) expression. * The result expression is rotated left [rotation] times. + * + * @see [mkBvRotateLeftIndexedExpr] for the rotation by a known number of bits. * */ open fun mkBvRotateLeftExpr(arg: KExpr, rotation: KExpr): KExpr = mkSimplified(arg, rotation, KContext::simplifyBvRotateLeftExpr, ::mkBvRotateLeftExprNoSimplify) @@ -2770,6 +2780,8 @@ open class KContext( /** * Create BitVec rotate left (`rotateleft`) expression. * The result expression is rotated left [rotation] times. + * + * @see [mkBvRotateLeftIndexedExpr] for the rotation by a known number of bits. * */ open fun mkBvRotateLeftExprNoSimplify(arg: KExpr, rotation: KExpr): KBvRotateLeftExpr = bvRotateLeftExprCache.createIfContextActive { @@ -2782,6 +2794,8 @@ open class KContext( /** * Create BitVec rotate left (`rotateleft`) expression. * The result expression is rotated left [rotation] times. + * + * @see [mkBvRotateLeftExpr] for the rotation by a symbolic (any BitVec expression) number of bits. * */ open fun mkBvRotateLeftIndexedExpr(rotation: Int, value: KExpr): KExpr = mkSimplified(rotation, value, KContext::simplifyBvRotateLeftIndexedExpr, ::mkBvRotateLeftIndexedExprNoSimplify) @@ -2789,6 +2803,8 @@ open class KContext( /** * Create BitVec rotate left (`rotateleft`) expression. * The result expression is rotated left [rotation] times. + * + * @see [mkBvRotateLeftExpr] for the rotation by a symbolic (any BitVec expression) number of bits. * */ open fun mkBvRotateLeftIndexedExprNoSimplify( rotation: Int, value: KExpr @@ -2803,6 +2819,8 @@ open class KContext( /** * Create BitVec rotate right (`rotateright`) expression. * The result expression is rotated right [rotation] times. + * + * @see [mkBvRotateRightExpr] for the rotation by a symbolic (any BitVec expression) number of bits. * */ open fun mkBvRotateRightIndexedExpr(rotation: Int, value: KExpr): KExpr = mkSimplified( @@ -2815,6 +2833,8 @@ open class KContext( /** * Create BitVec rotate right (`rotateright`) expression. * The result expression is rotated right [rotation] times. + * + * @see [mkBvRotateRightExpr] for the rotation by a symbolic (any BitVec expression) number of bits. * */ open fun mkBvRotateRightIndexedExprNoSimplify( rotation: Int, @@ -2830,6 +2850,8 @@ open class KContext( /** * Create BitVec rotate right (`rotateright`) expression. * The result expression is rotated right [rotation] times. + * + * @see [mkBvRotateRightIndexedExpr] for the rotation by a known number of bits. * */ open fun mkBvRotateRightExpr(arg: KExpr, rotation: KExpr): KExpr = mkSimplified(arg, rotation, KContext::simplifyBvRotateRightExpr, ::mkBvRotateRightExprNoSimplify) @@ -2837,6 +2859,8 @@ open class KContext( /** * Create BitVec rotate right (`rotateright`) expression. * The result expression is rotated right [rotation] times. + * + * @see [mkBvRotateRightIndexedExpr] for the rotation by a known number of bits. * */ open fun mkBvRotateRightExprNoSimplify(arg: KExpr, rotation: KExpr): KBvRotateRightExpr = bvRotateRightExprCache.createIfContextActive { From a4edeef2a4b94d175595e4ced0bb1753b904ed14 Mon Sep 17 00:00:00 2001 From: Saloed Date: Fri, 9 Jun 2023 15:04:53 +0300 Subject: [PATCH 6/6] Upgrade version to 0.5.4 --- README.md | 6 +++--- buildSrc/src/main/kotlin/io.ksmt.ksmt-base.gradle.kts | 2 +- docs/getting-started.md | 6 +++--- examples/build.gradle.kts | 6 +++--- 4 files changed, 10 insertions(+), 10 deletions(-) diff --git a/README.md b/README.md index b5a33c9dd..765b480ff 100644 --- a/README.md +++ b/README.md @@ -11,7 +11,7 @@ Get the most out of SMT solving with KSMT features: * Streamlined [solver delivery](#ksmt-distribution) with no need for building a solver or implementing JVM bindings [![KSMT: build](https://github.com/UnitTestBot/ksmt/actions/workflows/build-and-run-tests.yml/badge.svg)](https://github.com/UnitTestBot/ksmt/actions/workflows/build-and-run-tests.yml) -[![Maven Central](https://img.shields.io/maven-central/v/io.ksmt/ksmt-core)](https://central.sonatype.com/artifact/io.ksmt/ksmt-core/0.5.3) +[![Maven Central](https://img.shields.io/maven-central/v/io.ksmt/ksmt-core)](https://central.sonatype.com/artifact/io.ksmt/ksmt-core/0.5.4) [![javadoc](https://javadoc.io/badge2/io.ksmt/ksmt-core/javadoc.svg)](https://javadoc.io/doc/io.ksmt/ksmt-core) ## Get started @@ -20,9 +20,9 @@ To start using KSMT, install it via [Gradle](https://gradle.org/): ```kotlin // core -implementation("io.ksmt:ksmt-core:0.5.3") +implementation("io.ksmt:ksmt-core:0.5.4") // z3 solver -implementation("io.ksmt:ksmt-z3:0.5.3") +implementation("io.ksmt:ksmt-z3:0.5.4") ``` Find basic instructions in the [Getting started](docs/getting-started.md) guide and try it out with the diff --git a/buildSrc/src/main/kotlin/io.ksmt.ksmt-base.gradle.kts b/buildSrc/src/main/kotlin/io.ksmt.ksmt-base.gradle.kts index a18a25763..2d8323a84 100644 --- a/buildSrc/src/main/kotlin/io.ksmt.ksmt-base.gradle.kts +++ b/buildSrc/src/main/kotlin/io.ksmt.ksmt-base.gradle.kts @@ -11,7 +11,7 @@ plugins { } group = "io.ksmt" -version = "0.5.3" +version = "0.5.4" repositories { mavenCentral() diff --git a/docs/getting-started.md b/docs/getting-started.md index 9b5e990f3..cc67839d7 100644 --- a/docs/getting-started.md +++ b/docs/getting-started.md @@ -34,7 +34,7 @@ repositories { ```kotlin dependencies { // core - implementation("io.ksmt:ksmt-core:0.5.3") + implementation("io.ksmt:ksmt-core:0.5.4") } ``` @@ -43,9 +43,9 @@ dependencies { ```kotlin dependencies { // z3 - implementation("io.ksmt:ksmt-z3:0.5.3") + implementation("io.ksmt:ksmt-z3:0.5.4") // bitwuzla - implementation("io.ksmt:ksmt-bitwuzla:0.5.3") + implementation("io.ksmt:ksmt-bitwuzla:0.5.4") } ``` diff --git a/examples/build.gradle.kts b/examples/build.gradle.kts index af06a95c4..b61c0a6dc 100644 --- a/examples/build.gradle.kts +++ b/examples/build.gradle.kts @@ -9,11 +9,11 @@ repositories { dependencies { // core - implementation("io.ksmt:ksmt-core:0.5.3") + implementation("io.ksmt:ksmt-core:0.5.4") // z3 solver - implementation("io.ksmt:ksmt-z3:0.5.3") + implementation("io.ksmt:ksmt-z3:0.5.4") // Runner and portfolio solver - implementation("io.ksmt:ksmt-runner:0.5.3") + implementation("io.ksmt:ksmt-runner:0.5.4") } java {