Skip to content

Commit 92a96da

Browse files
dee-treedee-tree
committed
Bitwuzla uninterpreted sort values universe fix
1 parent ad9ff27 commit 92a96da

File tree

3 files changed

+38
-28
lines changed

3 files changed

+38
-28
lines changed

‎ksmt-bitwuzla/src/main/kotlin/io/ksmt/solver/bitwuzla/KBitwuzlaExprInternalizer.kt‎

Lines changed: 19 additions & 17 deletions
Original file line numberDiff line numberDiff line change
@@ -151,17 +151,11 @@ import io.ksmt.expr.KUnaryMinusArithExpr
151151
import io.ksmt.expr.KUninterpretedSortValue
152152
import io.ksmt.expr.KUniversalQuantifier
153153
import io.ksmt.expr.KXorExpr
154-
import io.ksmt.expr.rewrite.simplify.rewriteBvAddNoUnderflowExpr
155-
import io.ksmt.expr.rewrite.simplify.rewriteBvMulNoUnderflowExpr
156154
import io.ksmt.expr.rewrite.simplify.rewriteBvNegNoOverflowExpr
157155
import io.ksmt.expr.rewrite.simplify.rewriteBvSubNoUnderflowExpr
158156
import io.ksmt.solver.KSolverUnsupportedFeatureException
159-
import org.ksmt.solver.bitwuzla.bindings.Bitwuzla
160-
import org.ksmt.solver.bitwuzla.bindings.BitwuzlaKind
161-
import org.ksmt.solver.bitwuzla.bindings.BitwuzlaRoundingMode
162-
import org.ksmt.solver.bitwuzla.bindings.BitwuzlaSort
163-
import org.ksmt.solver.bitwuzla.bindings.BitwuzlaTerm
164-
import org.ksmt.solver.bitwuzla.bindings.Native
157+
import io.ksmt.solver.bitwuzla.KBitwuzlaExprInternalizer.BvOverflowCheckMode.OVERFLOW
158+
import io.ksmt.solver.bitwuzla.KBitwuzlaExprInternalizer.BvOverflowCheckMode.UNDERFLOW
165159
import io.ksmt.solver.util.KExprLongInternalizerBase
166160
import io.ksmt.sort.KArithSort
167161
import io.ksmt.sort.KArray2Sort
@@ -186,7 +180,13 @@ import io.ksmt.sort.KRealSort
186180
import io.ksmt.sort.KSort
187181
import io.ksmt.sort.KSortVisitor
188182
import io.ksmt.sort.KUninterpretedSort
183+
import org.ksmt.solver.bitwuzla.bindings.Bitwuzla
184+
import org.ksmt.solver.bitwuzla.bindings.BitwuzlaKind
185+
import org.ksmt.solver.bitwuzla.bindings.BitwuzlaRoundingMode
186+
import org.ksmt.solver.bitwuzla.bindings.BitwuzlaSort
187+
import org.ksmt.solver.bitwuzla.bindings.BitwuzlaTerm
189188
import org.ksmt.solver.bitwuzla.bindings.BitwuzlaTermArray
189+
import org.ksmt.solver.bitwuzla.bindings.Native
190190
import java.math.BigInteger
191191

192192
@Suppress("LargeClass")
@@ -726,7 +726,7 @@ open class KBitwuzlaExprInternalizer(val bitwuzlaCtx: KBitwuzlaContext) : KExprL
726726
override fun <T : KBvSort> transform(expr: KBvAddNoOverflowExpr<T>) = with(expr) {
727727
transform(arg0, arg1) { a0: BitwuzlaTerm, a1: BitwuzlaTerm ->
728728
if (isSigned) {
729-
mkBvAddSignedNoOverflowTerm(arg0.sort.sizeBits.toInt(), a0, a1, BvOverflowCheckMode.OVERFLOW)
729+
mkBvAddSignedNoOverflowTerm(arg0.sort.sizeBits.toInt(), a0, a1, OVERFLOW)
730730
} else {
731731
val overflowCheck = Native.bitwuzlaMkTerm2(
732732
bitwuzla, BitwuzlaKind.BITWUZLA_KIND_BV_UADD_OVERFLOW, a0, a1
@@ -738,20 +738,20 @@ open class KBitwuzlaExprInternalizer(val bitwuzlaCtx: KBitwuzlaContext) : KExprL
738738

739739
override fun <T : KBvSort> transform(expr: KBvAddNoUnderflowExpr<T>) = with(expr) {
740740
transform(arg0, arg1) { a0: BitwuzlaTerm, a1: BitwuzlaTerm ->
741-
mkBvAddSignedNoOverflowTerm(arg0.sort.sizeBits.toInt(), a0, a1, BvOverflowCheckMode.UNDERFLOW)
741+
mkBvAddSignedNoOverflowTerm(arg0.sort.sizeBits.toInt(), a0, a1, UNDERFLOW)
742742
}
743743
}
744744

745745
override fun <T : KBvSort> transform(expr: KBvSubNoOverflowExpr<T>) = with(expr) {
746746
transform(arg0, arg1) { a0: BitwuzlaTerm, a1: BitwuzlaTerm ->
747-
mkBvSubSignedNoOverflowTerm(arg0.sort.sizeBits.toInt(), a0, a1, BvOverflowCheckMode.OVERFLOW)
747+
mkBvSubSignedNoOverflowTerm(arg0.sort.sizeBits.toInt(), a0, a1, OVERFLOW)
748748
}
749749
}
750750

751751
override fun <T : KBvSort> transform(expr: KBvSubNoUnderflowExpr<T>) = with(expr) {
752752
if (isSigned) {
753753
transform(arg0, arg1) { a0: BitwuzlaTerm, a1: BitwuzlaTerm ->
754-
mkBvSubSignedNoOverflowTerm(arg0.sort.sizeBits.toInt(), a0, a1, BvOverflowCheckMode.UNDERFLOW)
754+
mkBvSubSignedNoOverflowTerm(arg0.sort.sizeBits.toInt(), a0, a1, UNDERFLOW)
755755
}
756756
} else {
757757
transform {
@@ -776,7 +776,7 @@ open class KBitwuzlaExprInternalizer(val bitwuzlaCtx: KBitwuzlaContext) : KExprL
776776
override fun <T : KBvSort> transform(expr: KBvMulNoOverflowExpr<T>) = with(expr) {
777777
transform(arg0, arg1) { a0: BitwuzlaTerm, a1: BitwuzlaTerm ->
778778
if (isSigned) {
779-
mkBvMulSignedNoOverflowTerm(arg0.sort.sizeBits.toInt(), a0, a1, BvOverflowCheckMode.OVERFLOW)
779+
mkBvMulSignedNoOverflowTerm(arg0.sort.sizeBits.toInt(), a0, a1, OVERFLOW)
780780
} else {
781781
val overflowCheck = Native.bitwuzlaMkTerm2(
782782
bitwuzla, BitwuzlaKind.BITWUZLA_KIND_BV_UMUL_OVERFLOW, a0, a1
@@ -788,7 +788,7 @@ open class KBitwuzlaExprInternalizer(val bitwuzlaCtx: KBitwuzlaContext) : KExprL
788788

789789
override fun <T : KBvSort> transform(expr: KBvMulNoUnderflowExpr<T>) = with(expr) {
790790
transform(arg0, arg1) { a0: BitwuzlaTerm, a1: BitwuzlaTerm ->
791-
mkBvMulSignedNoOverflowTerm(arg0.sort.sizeBits.toInt(), a0, a1, BvOverflowCheckMode.UNDERFLOW)
791+
mkBvMulSignedNoOverflowTerm(arg0.sort.sizeBits.toInt(), a0, a1, UNDERFLOW)
792792
}
793793
}
794794

@@ -813,7 +813,7 @@ open class KBitwuzlaExprInternalizer(val bitwuzlaCtx: KBitwuzlaContext) : KExprL
813813
a1,
814814
BitwuzlaKind.BITWUZLA_KIND_BV_SADD_OVERFLOW
815815
) { a0Sign, a1Sign ->
816-
if (mode == BvOverflowCheckMode.OVERFLOW) {
816+
if (mode == OVERFLOW) {
817817
// Both positive
818818
mkAndTerm(longArrayOf(mkNotTerm(a0Sign), mkNotTerm(a1Sign)))
819819
} else {
@@ -833,7 +833,7 @@ open class KBitwuzlaExprInternalizer(val bitwuzlaCtx: KBitwuzlaContext) : KExprL
833833
a1,
834834
BitwuzlaKind.BITWUZLA_KIND_BV_SSUB_OVERFLOW
835835
) { a0Sign, a1Sign ->
836-
if (mode == BvOverflowCheckMode.OVERFLOW) {
836+
if (mode == OVERFLOW) {
837837
// Positive sub negative
838838
mkAndTerm(longArrayOf(mkNotTerm(a0Sign), a1Sign))
839839
} else {
@@ -853,7 +853,7 @@ open class KBitwuzlaExprInternalizer(val bitwuzlaCtx: KBitwuzlaContext) : KExprL
853853
a1,
854854
BitwuzlaKind.BITWUZLA_KIND_BV_SMUL_OVERFLOW
855855
) { a0Sign, a1Sign ->
856-
if (mode == BvOverflowCheckMode.OVERFLOW) {
856+
if (mode == OVERFLOW) {
857857
// Overflow is possible when sign bits are equal
858858
mkEqTerm(bitwuzlaCtx.ctx.boolSort, a0Sign, a1Sign)
859859
} else {
@@ -1401,6 +1401,8 @@ open class KBitwuzlaExprInternalizer(val bitwuzlaCtx: KBitwuzlaContext) : KExprL
14011401
}
14021402

14031403
override fun transform(expr: KUninterpretedSortValue): KExpr<KUninterpretedSort> = expr.transform {
1404+
// register it for uninterpreted sort universe
1405+
bitwuzlaCtx.registerDeclaration(expr.decl)
14041406
Native.bitwuzlaMkBvValueUint32(
14051407
bitwuzla,
14061408
expr.sort.internalizeSort(),

‎ksmt-bitwuzla/src/main/kotlin/io/ksmt/solver/bitwuzla/KBitwuzlaModel.kt‎

Lines changed: 13 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -2,18 +2,15 @@ package io.ksmt.solver.bitwuzla
22

33
import io.ksmt.KContext
44
import io.ksmt.decl.KDecl
5+
import io.ksmt.decl.KUninterpretedSortValueDecl
56
import io.ksmt.expr.KExpr
67
import io.ksmt.expr.KUninterpretedSortValue
8+
import io.ksmt.solver.KModel
9+
import io.ksmt.solver.KSolverUnsupportedFeatureException
710
import io.ksmt.solver.model.KFuncInterp
811
import io.ksmt.solver.model.KFuncInterpEntryVarsFree
912
import io.ksmt.solver.model.KFuncInterpEntryVarsFreeOneAry
1013
import io.ksmt.solver.model.KFuncInterpVarsFree
11-
import io.ksmt.solver.KModel
12-
import io.ksmt.solver.KSolverUnsupportedFeatureException
13-
import org.ksmt.solver.bitwuzla.bindings.BitwuzlaNativeException
14-
import org.ksmt.solver.bitwuzla.bindings.BitwuzlaTerm
15-
import org.ksmt.solver.bitwuzla.bindings.FunValue
16-
import org.ksmt.solver.bitwuzla.bindings.Native
1714
import io.ksmt.solver.model.KFuncInterpWithVars
1815
import io.ksmt.solver.model.KModelEvaluator
1916
import io.ksmt.solver.model.KModelImpl
@@ -23,6 +20,10 @@ import io.ksmt.sort.KSort
2320
import io.ksmt.sort.KUninterpretedSort
2421
import io.ksmt.utils.mkFreshConstDecl
2522
import io.ksmt.utils.uncheckedCast
23+
import org.ksmt.solver.bitwuzla.bindings.BitwuzlaNativeException
24+
import org.ksmt.solver.bitwuzla.bindings.BitwuzlaTerm
25+
import org.ksmt.solver.bitwuzla.bindings.FunValue
26+
import org.ksmt.solver.bitwuzla.bindings.Native
2627

2728
open class KBitwuzlaModel(
2829
private val ctx: KContext,
@@ -77,7 +78,12 @@ open class KBitwuzlaModel(
7778
* to ensure that [uninterpretedSortValueContext] contains
7879
* all possible values for the given sort.
7980
* */
80-
sortDependency.forEach { interpretation(it) }
81+
sortDependency.forEach {
82+
if (it is KUninterpretedSortValueDecl) {
83+
val value = ctx.mkUninterpretedSortValue(it.sort, it.valueIdx)
84+
uninterpretedSortValueContext.registerValue(value)
85+
} else interpretation(it)
86+
}
8187

8288
uninterpretedSortValueContext.currentSortUniverse(sort)
8389
}

‎ksmt-bitwuzla/src/main/kotlin/io/ksmt/solver/bitwuzla/KBitwuzlaUninterpretedSortValueContext.kt‎

Lines changed: 6 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -10,10 +10,12 @@ class KBitwuzlaUninterpretedSortValueContext(private val ctx: KContext) {
1010
private val sortsUniverses = hashMapOf<KUninterpretedSort, MutableMap<KExpr<*>, KUninterpretedSortValue>>()
1111

1212
fun mkValue(sort: KUninterpretedSort, value: KBitVec32Value): KUninterpretedSortValue {
13-
val sortUniverse = sortsUniverses.getOrPut(sort) { hashMapOf() }
14-
return sortUniverse.getOrPut(value) {
15-
ctx.mkUninterpretedSortValue(sort, value.intValue)
16-
}
13+
return registerValue(ctx.mkUninterpretedSortValue(sort, value.intValue))
14+
}
15+
16+
fun registerValue(value: KUninterpretedSortValue): KUninterpretedSortValue {
17+
val sortsUniverse = sortsUniverses.getOrPut(value.sort) { hashMapOf() }
18+
return sortsUniverse.getOrPut(value) { value }
1719
}
1820

1921
fun currentSortUniverse(sort: KUninterpretedSort): Set<KUninterpretedSortValue> =

0 commit comments

Comments
 (0)