Skip to content

Commit fd1abcb

Browse files
committed
Fix
1 parent b09cd63 commit fd1abcb

File tree

1 file changed

+7
-2
lines changed
  • ksmt-yices/ksmt-yices-core/src/main/kotlin/io/ksmt/solver/yices

1 file changed

+7
-2
lines changed

ksmt-yices/ksmt-yices-core/src/main/kotlin/io/ksmt/solver/yices/KYicesModel.kt

Lines changed: 7 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -39,13 +39,18 @@ class KYicesModel(
3939
model.collectDefinedTerms().mapTo(hashSetOf()) { converter.convertDecl(it) }
4040
}
4141

42+
private val uninterpretedSortValueIndex by lazy { hashMapOf<Int, Int>() }
43+
private fun uninterpretedSortValueIdx(valueId: Int): Int = uninterpretedSortValueIndex.getOrPut(valueId) {
44+
yicesCtx.convertUninterpretedSortValueIndex(valueId)
45+
}
46+
4247
private val uninterpretedSortUniverse: Map<KUninterpretedSort, Set<KUninterpretedSortValue>> by lazy {
4348
val values = model.uninterpretedSortValues()
4449

4550
val sortValues = hashMapOf<YicesSort, MutableSet<Int>>()
4651
for (value in values) {
4752
val (valueId, internalizedSort) = model.scalarValue(value)
48-
val valueIdx = yicesCtx.convertUninterpretedSortValueIndex(valueId)
53+
val valueIdx = uninterpretedSortValueIdx(valueId)
4954
sortValues.getOrPut(internalizedSort, ::hashSetOf).add(valueIdx)
5055
}
5156

@@ -89,7 +94,7 @@ class KYicesModel(
8994
is KIntSort -> mkIntNum(model.bigRationalValue(yval))
9095
is KUninterpretedSort -> {
9196
val uninterpretedSortValueId = model.scalarValue(yval)[0]
92-
val valueIndex = yicesCtx.convertUninterpretedSortValueIndex(uninterpretedSortValueId)
97+
val valueIndex = uninterpretedSortValueIdx(uninterpretedSortValueId)
9398
mkUninterpretedSortValue(sort, valueIndex)
9499
}
95100
is KArraySortBase<*> -> {

0 commit comments

Comments
 (0)