Context bound default values (#99)

* Context bound default values
UnitTestBot · Apr 14, 2023 · fbe2aa1 · fbe2aa1
1 parent 4f1e626
commit fbe2aa1
Show file tree

Hide file tree

Showing 6 changed files with 84 additions and 75 deletions.
diff --git a/ksmt-core/src/main/kotlin/org/ksmt/KContext.kt b/ksmt-core/src/main/kotlin/org/ksmt/KContext.kt
@@ -423,7 +423,9 @@ import org.ksmt.sort.KFpSort
 import org.ksmt.sort.KIntSort
 import org.ksmt.sort.KRealSort
 import org.ksmt.sort.KSort
+import org.ksmt.sort.KSortVisitor
 import org.ksmt.sort.KUninterpretedSort
+import org.ksmt.utils.DefaultValueSampler
 import org.ksmt.utils.FpUtils.biasFpExponent
 import org.ksmt.utils.FpUtils.fpInfExponentBiased
 import org.ksmt.utils.FpUtils.fpInfSignificand
@@ -440,6 +442,7 @@ import org.ksmt.utils.extractSignificand
 import org.ksmt.utils.getHalfPrecisionExponent
 import org.ksmt.utils.halfPrecisionSignificand
 import org.ksmt.utils.normalizeValue
+import org.ksmt.utils.sampleValue
 import org.ksmt.utils.signBit
 import org.ksmt.utils.toBigInteger
 import org.ksmt.utils.toULongValue
@@ -3062,6 +3065,30 @@ open class KContext(
             KUninterpretedSortValue(this, sort, valueIdx)
         }
 
+    // default values
+    val defaultValueSampler: KSortVisitor<KExpr<*>> by lazy {
+        mkDefaultValueSampler()
+    }
+
+    open fun mkDefaultValueSampler(): KSortVisitor<KExpr<*>> =
+        DefaultValueSampler(this)
+
+    open fun boolSortDefaultValue(): KExpr<KBoolSort> = trueExpr
+
+    open fun intSortDefaultValue(): KExpr<KIntSort> = mkIntNum(0)
+
+    open fun realSortDefaultValue(): KExpr<KRealSort> = mkRealNum(0)
+
+    open fun <S : KBvSort> bvSortDefaultValue(sort: S): KExpr<S> = mkBv(0, sort)
+
+    open fun <S : KFpSort> fpSortDefaultValue(sort: S): KExpr<S> = mkFpZero(signBit = false, sort)
+
+    open fun fpRoundingModeSortDefaultValue(): KExpr<KFpRoundingModeSort> =
+        mkFpRoundingModeExpr(KFpRoundingMode.RoundNearestTiesToEven)
+
+    open fun <A : KArraySortBase<R>, R : KSort> arraySortDefaultValue(sort: A): KExpr<A> =
+        mkArrayConst(sort, sort.range.sampleValue())
+
     open fun uninterpretedSortDefaultValue(sort: KUninterpretedSort): KUninterpretedSortValue =
         mkUninterpretedSortValue(sort, valueIdx = 0)
 

diff --git a/ksmt-core/src/main/kotlin/org/ksmt/solver/model/DefaultValueSampler.kt b/ksmt-core/src/main/kotlin/org/ksmt/solver/model/DefaultValueSampler.kt
diff --git a/ksmt-core/src/main/kotlin/org/ksmt/solver/model/KModelEvaluator.kt b/ksmt-core/src/main/kotlin/org/ksmt/solver/model/KModelEvaluator.kt
@@ -19,7 +19,6 @@ import org.ksmt.expr.rewrite.simplify.KExprSimplifier
 import org.ksmt.expr.rewrite.simplify.areDefinitelyDistinct
 import org.ksmt.expr.rewrite.simplify.simplifyExpr
 import org.ksmt.solver.KModel
-import org.ksmt.solver.model.DefaultValueSampler.Companion.sampleValue
 import org.ksmt.sort.KArray2Sort
 import org.ksmt.sort.KArray3Sort
 import org.ksmt.sort.KArrayNSort
@@ -29,6 +28,7 @@ import org.ksmt.sort.KBoolSort
 import org.ksmt.sort.KSort
 import org.ksmt.sort.KUninterpretedSort
 import org.ksmt.utils.asExpr
+import org.ksmt.utils.sampleValue
 import org.ksmt.utils.uncheckedCast
 
 open class KModelEvaluator(

diff --git a/ksmt-core/src/main/kotlin/org/ksmt/utils/ContextUtils.kt b/ksmt-core/src/main/kotlin/org/ksmt/utils/ContextUtils.kt
@@ -24,3 +24,6 @@ fun <T : KSort> KExpr<*>.asExpr(sort: T): KExpr<T> = with(ctx) {
     @Suppress("UNCHECKED_CAST")
     this@asExpr as KExpr<T>
 }
+
+fun <T : KSort> T.sampleValue(): KExpr<T> =
+    accept(ctx.defaultValueSampler).asExpr(this)
diff --git a/ksmt-core/src/main/kotlin/org/ksmt/utils/DefaultValueSampler.kt b/ksmt-core/src/main/kotlin/org/ksmt/utils/DefaultValueSampler.kt
@@ -0,0 +1,52 @@
+package org.ksmt.utils
+
+import org.ksmt.KContext
+import org.ksmt.expr.KExpr
+import org.ksmt.sort.KArray2Sort
+import org.ksmt.sort.KArray3Sort
+import org.ksmt.sort.KArrayNSort
+import org.ksmt.sort.KArraySort
+import org.ksmt.sort.KBoolSort
+import org.ksmt.sort.KBvSort
+import org.ksmt.sort.KFpRoundingModeSort
+import org.ksmt.sort.KFpSort
+import org.ksmt.sort.KIntSort
+import org.ksmt.sort.KRealSort
+import org.ksmt.sort.KSort
+import org.ksmt.sort.KSortVisitor
+import org.ksmt.sort.KUninterpretedSort
+
+open class DefaultValueSampler(val ctx: KContext) : KSortVisitor<KExpr<*>> {
+    override fun visit(sort: KBoolSort): KExpr<*> =
+        ctx.boolSortDefaultValue()
+
+    override fun visit(sort: KIntSort): KExpr<*> =
+        ctx.intSortDefaultValue()
+
+    override fun visit(sort: KRealSort): KExpr<*> =
+        ctx.realSortDefaultValue()
+
+    override fun <S : KBvSort> visit(sort: S): KExpr<*> =
+        ctx.bvSortDefaultValue(sort)
+
+    override fun <S : KFpSort> visit(sort: S): KExpr<*> =
+        ctx.fpSortDefaultValue(sort)
+
+    override fun visit(sort: KFpRoundingModeSort): KExpr<*> =
+        ctx.fpRoundingModeSortDefaultValue()
+
+    override fun <D : KSort, R : KSort> visit(sort: KArraySort<D, R>): KExpr<*> =
+        ctx.arraySortDefaultValue(sort)
+
+    override fun <D0 : KSort, D1 : KSort, R : KSort> visit(sort: KArray2Sort<D0, D1, R>): KExpr<*> =
+        ctx.arraySortDefaultValue(sort)
+
+    override fun <D0 : KSort, D1 : KSort, D2 : KSort, R : KSort> visit(sort: KArray3Sort<D0, D1, D2, R>): KExpr<*> =
+        ctx.arraySortDefaultValue(sort)
+
+    override fun <R : KSort> visit(sort: KArrayNSort<R>): KExpr<*> =
+        ctx.arraySortDefaultValue(sort)
+
+    override fun visit(sort: KUninterpretedSort): KExpr<*> =
+        ctx.uninterpretedSortDefaultValue(sort)
+}
diff --git a/ksmt-core/src/test/kotlin/org/ksmt/ModelEvaluationTest.kt b/ksmt-core/src/test/kotlin/org/ksmt/ModelEvaluationTest.kt
@@ -1,9 +1,9 @@
 package org.ksmt
 
 import org.ksmt.solver.KModel
-import org.ksmt.solver.model.DefaultValueSampler.Companion.sampleValue
 import org.ksmt.solver.model.KModelImpl
 import org.ksmt.utils.getValue
+import org.ksmt.utils.sampleValue
 import kotlin.test.Test
 import kotlin.test.assertEquals