Skip to content

Commit 39046b5

Browse files
SaloedSaloed
authored
Fix array model conversion (#102)
* Fix array model conversion * Better conversion for model lambda expressions
1 parent 6532b35 commit 39046b5

3 files changed

Lines changed: 194 additions & 23 deletions

File tree

‎ksmt-bitwuzla/src/main/kotlin/org/ksmt/solver/bitwuzla/KBitwuzlaExprConverter.kt‎

Lines changed: 64 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -6,12 +6,17 @@ import org.ksmt.cache.structurallyEqual
66
import org.ksmt.decl.KConstDecl
77
import org.ksmt.decl.KDecl
88
import org.ksmt.decl.KFuncDecl
9+
import org.ksmt.expr.KAndExpr
910
import org.ksmt.expr.KArrayConst
11+
import org.ksmt.expr.KArraySelectBase
1012
import org.ksmt.expr.KBitVec32Value
1113
import org.ksmt.expr.KBitVecValue
14+
import org.ksmt.expr.KConst
15+
import org.ksmt.expr.KEqExpr
1216
import org.ksmt.expr.KExpr
1317
import org.ksmt.expr.KFpRoundingMode
1418
import org.ksmt.expr.KInterpretedValue
19+
import org.ksmt.expr.KIteExpr
1520
import org.ksmt.expr.printer.ExpressionPrinter
1621
import org.ksmt.expr.transformer.KNonRecursiveTransformer
1722
import org.ksmt.expr.transformer.KTransformerBase
@@ -671,13 +676,69 @@ open class KBitwuzlaExprConverter(
671676

672677
BitwuzlaKind.BITWUZLA_KIND_LAMBDA -> {
673678
val convertedBody = bodyConverter.convertFromNative<KSort>(body)
674-
ctx.mkAnyArrayLambda(convertedBounds, convertedBody)
679+
ctx.convertArrayLambdaSimplified(convertedBounds, convertedBody)
675680
}
676681

677682
else -> error("Unexpected quantifier: $kind")
678683
}
679684
}
680685

686+
private fun KContext.convertArrayLambdaSimplified(
687+
bounds: List<KDecl<*>>,
688+
body: KExpr<*>
689+
): KExpr<*> {
690+
if (body is KInterpretedValue<*>) {
691+
val sort = mkAnyArraySort(bounds.map { it.sort }, body.sort)
692+
return mkArrayConst(sort, body.uncheckedCast())
693+
}
694+
695+
if (body is KIteExpr<*>) {
696+
tryRecognizeArrayStore(body, bounds)?.let { return it }
697+
}
698+
699+
return mkAnyArrayLambda(bounds, body)
700+
}
701+
702+
/**
703+
* In a case of multidimensional array store expressions in model are represented as:
704+
* (lambda (i0 ... in) (ite (and (= i0 c0) .. (= in cn)) value (select array i0...in)))
705+
* We try to recognize this pattern and rewrite such lambda expressions as normal
706+
* array stores.
707+
* */
708+
private fun KContext.tryRecognizeArrayStore(
709+
body: KIteExpr<*>,
710+
bounds: List<KDecl<*>>
711+
): KExpr<*>? {
712+
val storedValue = body.trueBranch as? KInterpretedValue<*> ?: return null
713+
val conditionArgs = (body.condition as? KAndExpr)?.args ?: return null
714+
715+
val boundConsts = bounds.map { it.apply(emptyList()) }
716+
717+
val indexBindings = conditionArgs.associate {
718+
val binding = it as? KEqExpr<*> ?: return null
719+
val lhs = binding.lhs
720+
val rhs = binding.rhs
721+
722+
when {
723+
lhs is KInterpretedValue<*> && rhs is KConst<*> -> rhs to lhs
724+
lhs is KConst<*> && rhs is KInterpretedValue<*> -> lhs to rhs
725+
else -> return null
726+
}
727+
}
728+
729+
val indices = boundConsts.map { indexBindings[it] ?: return null }
730+
731+
val nestedValue = body.falseBranch
732+
if (nestedValue is KArraySelectBase<*, *>) {
733+
if (boundConsts != nestedValue.indices) return null
734+
735+
val nestedArray = nestedValue.array
736+
return mkAnyArrayStore(nestedArray, indices.uncheckedCast(), storedValue.uncheckedCast())
737+
}
738+
739+
return null
740+
}
741+
681742
fun convertEqExpr(lhs: KExpr<KSort>, rhs: KExpr<KSort>): KExpr<KBoolSort> = with(ctx) {
682743
val expectedSort = selectExpectedSort(lhs.sort, rhs.sort)
683744
return mkEq(
@@ -741,7 +802,7 @@ open class KBitwuzlaExprConverter(
741802
).uncheckedCast()
742803
}
743804

744-
private fun <A : KArraySortBase<*>> KContext.mkAnyArraySelect(
805+
fun <A : KArraySortBase<*>> KContext.mkAnyArraySelect(
745806
array: KExpr<A>,
746807
indices: List<KExpr<KSort>>
747808
): KExpr<KSort> = mkAnyArrayOperation(
@@ -790,7 +851,7 @@ open class KBitwuzlaExprConverter(
790851
{ mkArrayNLambda(it, body) }
791852
)
792853

793-
private fun KContext.mkAnyArraySort(domain: List<KSort>, range: KSort): KArraySortBase<KSort> =
854+
fun KContext.mkAnyArraySort(domain: List<KSort>, range: KSort): KArraySortBase<KSort> =
794855
mkAnyArrayOperation(
795856
domain,
796857
{ d0 -> mkArraySort(d0, range) },

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

Lines changed: 93 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -1,18 +1,20 @@
11
package org.ksmt.solver.bitwuzla
22

33
import org.ksmt.KContext
4+
import org.ksmt.decl.KConstDecl
45
import org.ksmt.decl.KDecl
5-
import org.ksmt.decl.KFuncDecl
66
import org.ksmt.expr.KExpr
77
import org.ksmt.expr.KUninterpretedSortValue
88
import org.ksmt.solver.KModel
99
import org.ksmt.solver.KSolverUnsupportedFeatureException
1010
import org.ksmt.solver.bitwuzla.bindings.BitwuzlaNativeException
1111
import org.ksmt.solver.bitwuzla.bindings.BitwuzlaTerm
12+
import org.ksmt.solver.bitwuzla.bindings.FunValue
1213
import org.ksmt.solver.bitwuzla.bindings.Native
1314
import org.ksmt.solver.model.KModelEvaluator
1415
import org.ksmt.solver.model.KModelImpl
1516
import org.ksmt.sort.KArraySort
17+
import org.ksmt.sort.KArraySortBase
1618
import org.ksmt.sort.KSort
1719
import org.ksmt.sort.KUninterpretedSort
1820
import org.ksmt.utils.mkFreshConstDecl
@@ -99,7 +101,7 @@ open class KBitwuzlaModel(
99101
term: BitwuzlaTerm
100102
): KModel.KFuncInterp<T> = converter.withUninterpretedSortValueContext(uninterpretedSortValueContext) {
101103
when {
102-
Native.bitwuzlaTermIsArray(term) -> ctx.arrayInterpretation(decl, term)
104+
Native.bitwuzlaTermIsArray(term) -> arrayInterpretation(decl, term)
103105
Native.bitwuzlaTermIsFun(term) -> functionInterpretation(decl, term)
104106
else -> {
105107
val value = Native.bitwuzlaGetValue(bitwuzlaCtx.bitwuzla, term)
@@ -117,36 +119,56 @@ open class KBitwuzlaModel(
117119
private fun <T : KSort> functionInterpretation(
118120
decl: KDecl<T>,
119121
term: BitwuzlaTerm
120-
): KModel.KFuncInterp<T> = with(converter) {
121-
check(decl is KFuncDecl<T>) { "function expected but actual is $decl" }
122-
123-
val entries = mutableListOf<KModel.KFuncInterpEntry<T>>()
122+
): KModel.KFuncInterp<T> {
124123
val interp = Native.bitwuzlaGetFunValue(bitwuzlaCtx.bitwuzla, term)
125-
126-
check(interp.arity == decl.argSorts.size) {
127-
"function arity mismatch: ${interp.arity} and ${decl.argSorts.size}"
124+
return if (interp.size != 0) {
125+
handleArrayFunctionDecl(decl) { functionDecl, vars ->
126+
functionValueInterpretation(functionDecl, vars, interp)
127+
}
128+
} else {
129+
/**
130+
* Function has default value or bitwuzla can't retrieve its entries.
131+
* Try parse function interpretation from value term.
132+
* */
133+
converter.retrieveFunctionValue(decl, term)
128134
}
135+
}
136+
137+
private fun <T : KSort> KBitwuzlaExprConverter.functionValueInterpretation(
138+
decl: KDecl<T>,
139+
vars: List<KConstDecl<*>>,
140+
interp: FunValue
141+
): KModel.KFuncInterp<T> {
142+
val entries = mutableListOf<KModel.KFuncInterpEntry<T>>()
129143

130-
val vars = decl.argSorts.map { it.mkFreshConstDecl("x") }
131144
for (i in 0 until interp.size) {
132145
// Don't substitute vars since arguments in Bitwuzla model are always constants
133146
val args = interp.args!![i].zip(decl.argSorts) { arg, sort -> arg.convertExpr(sort) }
134147
val value = interp.values!![i].convertExpr(decl.sort)
135148
entries += KModel.KFuncInterpEntry(args, value)
136149
}
137150

138-
KModel.KFuncInterp(
151+
return KModel.KFuncInterp(
139152
decl = decl,
140153
vars = vars,
141154
entries = entries,
142155
default = null
143156
)
144157
}
145158

146-
private fun <T : KSort> KContext.arrayInterpretation(
159+
private fun <T : KSort> KBitwuzlaExprConverter.retrieveFunctionValue(
160+
decl: KDecl<T>,
161+
functionTerm: BitwuzlaTerm
162+
): KModel.KFuncInterp<T> = handleArrayFunctionInterpretation(decl) { arraySort ->
163+
// We expect lambda expression here. Therefore, we convert function interpretation as array.
164+
val functionValue = Native.bitwuzlaGetValue(bitwuzlaCtx.bitwuzla, functionTerm)
165+
functionValue.convertExpr(arraySort)
166+
}
167+
168+
private fun <T : KSort> arrayInterpretation(
147169
decl: KDecl<T>,
148170
term: BitwuzlaTerm
149-
): KModel.KFuncInterp<T> = with(converter) {
171+
): KModel.KFuncInterp<T> = handleArrayFunctionDecl(decl) { arrayFunctionDecl, vars ->
150172
val sort: KArraySort<KSort, KSort> = decl.sort.uncheckedCast()
151173
val entries = mutableListOf<KModel.KFuncInterpEntry<KSort>>()
152174
val interp = Native.bitwuzlaGetArrayValue(bitwuzlaCtx.bitwuzla, term)
@@ -158,22 +180,73 @@ open class KBitwuzlaModel(
158180
}
159181

160182
val default = interp.defaultValue.takeIf { it != 0L }?.convertExpr(sort.range)
161-
val arrayInterpDecl = mkFreshFuncDecl("array", sort.range, listOf(sort.domain))
162-
val arrayInterpIndexDecl = mkFreshConstDecl("idx", sort.domain)
163183

164-
modelDeclarations += arrayInterpDecl
165-
interpretations[arrayInterpDecl] = KModel.KFuncInterp(
166-
decl = arrayInterpDecl,
167-
vars = listOf(arrayInterpIndexDecl),
184+
KModel.KFuncInterp(
185+
decl = arrayFunctionDecl,
186+
vars = vars,
168187
entries = entries,
169188
default = default
170189
)
190+
}
191+
192+
private inline fun <T : KSort> handleArrayFunctionDecl(
193+
decl: KDecl<T>,
194+
body: KBitwuzlaExprConverter.(KDecl<KSort>, List<KConstDecl<*>>) -> KModel.KFuncInterp<*>
195+
): KModel.KFuncInterp<T> = with(ctx) {
196+
val sort = decl.sort
197+
198+
if (sort !is KArraySortBase<*>) {
199+
val vars = decl.argSorts.mapIndexed { i, s -> s.mkFreshConstDecl("x!$i") }
200+
return converter.body(decl.uncheckedCast(), vars).uncheckedCast()
201+
}
202+
203+
check(decl.argSorts.isEmpty()) { "Unexpected function with array range" }
204+
205+
val arrayInterpDecl = mkFreshFuncDecl("array", sort.range, sort.domainSorts)
206+
val arrayInterpIndicesDecls = sort.domainSorts.mapIndexed { i, s ->
207+
s.mkFreshConstDecl("idx!$i")
208+
}
209+
210+
modelDeclarations += arrayInterpDecl
211+
interpretations[arrayInterpDecl] = converter.body(arrayInterpDecl, arrayInterpIndicesDecls)
171212

172213
KModel.KFuncInterp(
173214
decl = decl,
174215
vars = emptyList(),
175216
entries = emptyList(),
176-
default = mkFunctionAsArray(sort, arrayInterpDecl).uncheckedCast()
217+
default = mkFunctionAsArray(sort.uncheckedCast(), arrayInterpDecl).uncheckedCast()
218+
)
219+
}
220+
221+
private inline fun <T : KSort> KBitwuzlaExprConverter.handleArrayFunctionInterpretation(
222+
decl: KDecl<T>,
223+
convertInterpretation: (KArraySortBase<*>) -> KExpr<KArraySortBase<*>>
224+
): KModel.KFuncInterp<T> {
225+
val sort = decl.sort
226+
227+
if (sort is KArraySortBase<*> && decl.argSorts.isEmpty()) {
228+
val arrayInterpretation = convertInterpretation(sort)
229+
return KModel.KFuncInterp(
230+
decl = decl,
231+
vars = emptyList(),
232+
entries = emptyList(),
233+
default = arrayInterpretation.uncheckedCast()
234+
)
235+
}
236+
237+
check(decl.argSorts.isEmpty()) { "Unexpected function with array range" }
238+
239+
val interpretationSort = ctx.mkAnyArraySort(decl.argSorts, decl.sort)
240+
val arrayInterpretation = convertInterpretation(interpretationSort)
241+
242+
val functionVars = decl.argSorts.mapIndexed { i, s -> s.mkFreshConstDecl("x!$i") }
243+
val functionValue = ctx.mkAnyArraySelect(arrayInterpretation, functionVars.map { it.apply() })
244+
245+
return KModel.KFuncInterp(
246+
decl = decl,
247+
vars = functionVars,
248+
entries = emptyList(),
249+
default = functionValue.uncheckedCast()
177250
)
178251
}
179252

‎ksmt-bitwuzla/src/test/kotlin/org/ksmt/solver/bitwuzla/SolverTest.kt‎

Lines changed: 37 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -6,6 +6,7 @@ import org.ksmt.solver.KSolverStatus
66
import org.ksmt.solver.bitwuzla.bindings.BitwuzlaKind
77
import org.ksmt.solver.bitwuzla.bindings.BitwuzlaNativeException
88
import org.ksmt.solver.bitwuzla.bindings.Native
9+
import org.ksmt.sort.KArray2Sort
910
import org.ksmt.sort.KArraySort
1011
import org.ksmt.sort.KBv32Sort
1112
import org.ksmt.utils.getValue
@@ -222,4 +223,40 @@ class SolverTest {
222223

223224
assertEquals(KSolverStatus.UNSAT, solver.check())
224225
}
226+
227+
@Test
228+
fun testArray2Model(): Unit = with(ctx) {
229+
val sort = mkArraySort(bv32Sort, bv32Sort, bv32Sort)
230+
val a by sort
231+
val b by sort
232+
233+
var expr: KExpr<KArray2Sort<KBv32Sort, KBv32Sort, KBv32Sort>> = a
234+
for (i in 0 until 10) {
235+
expr = expr.store(mkBv(i), mkBv(i), mkBv(i))
236+
}
237+
238+
solver.assert(b eq expr)
239+
assertEquals(KSolverStatus.SAT, solver.check())
240+
241+
val model = solver.model()
242+
243+
val modelValue = model.eval(b eq expr)
244+
assertEquals(trueExpr, modelValue)
245+
}
246+
247+
@Test
248+
fun testFunModel(): Unit = with(ctx) {
249+
val f = mkFuncDecl("f", bv32Sort, listOf(bv32Sort, bv32Sort))
250+
251+
for (i in 0 until 10) {
252+
solver.assert(f.apply(listOf(mkBv(i), mkBv(i))) eq mkBv(i))
253+
}
254+
255+
assertEquals(KSolverStatus.SAT, solver.check())
256+
257+
val model = solver.model()
258+
259+
assertEquals(10, model.interpretation(f)?.entries?.size)
260+
}
261+
225262
}

0 commit comments

Comments
 (0)