Skip to content

Commit

Permalink
Multi indexed arrays (#77)
Browse files Browse the repository at this point in the history 
* Multi indexed array sorts

* Array expressions cls

* transformer

* Sort builders

* Array declarations

* Array lightweight rules

* Transformers

* Fix model evaluator

* Fix model evaluator

* more aux array expressions

* array store

* array select simplification

* Simplifier

* Z3 internalizer

* z3 converter

* Specify types to avoid kotlin compiler issues

* Fix array sort conversion

* Array tests

* Fixes and refactoring

* Bitwuzla stubs

* Yices stubs

* Serializer

* Fix tests

* Rename with N

* N-Array guards

* Minor fixes

* Array-N decls

* Remove domain field from ArrayNSort

* Use list builder to avoid auxiliary lists

* Consistent name for flatStore

* Upgrade version
  • Loading branch information
@Saloed
Saloed authored Feb 28, 2023
1 parent 5c4a30d commit 98c560b
Show file tree
Hide file tree
Showing 43 changed files with 3,458 additions and 528 deletions.
4 changes: 2 additions & 2 deletions README.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -14,9 +14,9 @@ repositories {
}

// core
implementation("com.github.UnitTestBot.ksmt:ksmt-core:0.4.0")
implementation("com.github.UnitTestBot.ksmt:ksmt-core:0.4.1")
// z3 solver
implementation("com.github.UnitTestBot.ksmt:ksmt-z3:0.4.0")
implementation("com.github.UnitTestBot.ksmt:ksmt-z3:0.4.1")
```

## Usage
Expand Down
2 changes: 1 addition & 1 deletion Requirements.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -12,7 +12,7 @@
| [Yices2 solver support](#yices2-solver-support) | Done |
| [CVC5 solver support](#cvc5-solver-support) | In progress |
| [External process runner](#external-process-runner) | Done |
| [Portfolio solver](#portfolio-solver) | In progress |
| [Portfolio solver](#portfolio-solver) | Done |
| [Solver configuration API](#solver-configuration-api) | Done |
| [Deployment](#deployment) | Done partially |
| [Expression simplification / evaluation](#expression-simplification--evaluation) | Done |
Expand Down
2 changes: 1 addition & 1 deletion buildSrc/src/main/kotlin/org.ksmt.ksmt-base.gradle.kts
View file
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,7 @@ plugins {
}

group = "org.ksmt"
version = "0.4.0"
version = "0.4.1"

repositories {
mavenCentral()
Expand Down
6 changes: 3 additions & 3 deletions docs/getting-started.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -18,17 +18,17 @@ repositories {
```kotlin
dependencies {
// core
implementation("com.github.UnitTestBot.ksmt:ksmt-core:0.4.0")
implementation("com.github.UnitTestBot.ksmt:ksmt-core:0.4.1")
}
```

#### 3. Add one or more SMT solver dependencies:
```kotlin
dependencies {
// z3
implementation("com.github.UnitTestBot.ksmt:ksmt-z3:0.4.0")
implementation("com.github.UnitTestBot.ksmt:ksmt-z3:0.4.1")
// bitwuzla
implementation("com.github.UnitTestBot.ksmt:ksmt-bitwuzla:0.4.0")
implementation("com.github.UnitTestBot.ksmt:ksmt-bitwuzla:0.4.1")
}
```
SMT solver specific packages are provided with solver native binaries.
Expand Down
4 changes: 2 additions & 2 deletions examples/build.gradle.kts
View file
Original file line number Diff line number Diff line change
Expand Up @@ -10,9 +10,9 @@ repositories {

dependencies {
// core
implementation("com.github.UnitTestBot.ksmt:ksmt-core:0.4.0")
implementation("com.github.UnitTestBot.ksmt:ksmt-core:0.4.1")
// z3 solver
implementation("com.github.UnitTestBot.ksmt:ksmt-z3:0.4.0")
implementation("com.github.UnitTestBot.ksmt:ksmt-z3:0.4.1")
}

java {
Expand Down
42 changes: 40 additions & 2 deletions ksmt-bitwuzla/src/main/kotlin/org/ksmt/solver/bitwuzla/KBitwuzlaContext.kt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,10 @@ package org.ksmt.solver.bitwuzla
import org.ksmt.KContext
import org.ksmt.decl.KDecl
import org.ksmt.decl.KFuncDecl
import org.ksmt.expr.KArray2Lambda
import org.ksmt.expr.KArray3Lambda
import org.ksmt.expr.KArrayLambda
import org.ksmt.expr.KArrayNLambda
import org.ksmt.expr.KConst
import org.ksmt.expr.KExistentialQuantifier
import org.ksmt.expr.KExpr
Expand All @@ -16,7 +19,11 @@ import org.ksmt.solver.bitwuzla.bindings.BitwuzlaNativeException
import org.ksmt.solver.bitwuzla.bindings.BitwuzlaSort
import org.ksmt.solver.bitwuzla.bindings.BitwuzlaTerm
import org.ksmt.solver.bitwuzla.bindings.Native
import org.ksmt.sort.KArray2Sort
import org.ksmt.sort.KArray3Sort
import org.ksmt.sort.KArrayNSort
import org.ksmt.sort.KArraySort
import org.ksmt.sort.KArraySortBase
import org.ksmt.sort.KBoolSort
import org.ksmt.sort.KBvSort
import org.ksmt.sort.KFpRoundingModeSort
Expand Down Expand Up @@ -277,6 +284,24 @@ open class KBitwuzlaContext(val ctx: KContext) : AutoCloseable {
sort.range.accept(this)
}

override fun <D0 : KSort, D1 : KSort, R : KSort> visit(sort: KArray2Sort<D0, D1, R>) {
sort.domain0.accept(this)
sort.domain1.accept(this)
sort.range.accept(this)
}

override fun <D0 : KSort, D1 : KSort, D2 : KSort, R : KSort> visit(sort: KArray3Sort<D0, D1, D2, R>) {
sort.domain0.accept(this)
sort.domain1.accept(this)
sort.domain2.accept(this)
sort.range.accept(this)
}

override fun <R : KSort> visit(sort: KArrayNSort<R>) {
sort.domainSorts.forEach { it.accept(this) }
sort.range.accept(this)
}

override fun visit(sort: KBoolSort) {
}

Expand Down Expand Up @@ -344,7 +369,7 @@ open class KBitwuzlaContext(val ctx: KContext) : AutoCloseable {
return super.transform(expr)
}

override fun <D : KSort, R : KSort> transform(expr: KFunctionAsArray<D, R>): KExpr<KArraySort<D, R>> {
override fun <A : KArraySortBase<R>, R : KSort> transform(expr: KFunctionAsArray<A, R>): KExpr<A> {
registerDeclIfNotIgnored(expr.function)
return super.transform(expr)
}
Expand All @@ -365,7 +390,20 @@ open class KBitwuzlaContext(val ctx: KContext) : AutoCloseable {
}

override fun <D : KSort, R : KSort> transform(expr: KArrayLambda<D, R>): KExpr<KArraySort<D, R>> =
expr.transformQuantifier(listOf(expr.indexVarDecl), expr.body)
expr.transformQuantifier(expr.indexVarDeclarations, expr.body)

override fun <D0 : KSort, D1 : KSort, R : KSort> transform(
expr: KArray2Lambda<D0, D1, R>
): KExpr<KArray2Sort<D0, D1, R>> =
expr.transformQuantifier(expr.indexVarDeclarations, expr.body)

override fun <D0 : KSort, D1 : KSort, D2 : KSort, R : KSort> transform(
expr: KArray3Lambda<D0, D1, D2, R>
): KExpr<KArray3Sort<D0, D1, D2, R>> =
expr.transformQuantifier(expr.indexVarDeclarations, expr.body)

override fun <R : KSort> transform(expr: KArrayNLambda<R>): KExpr<KArrayNSort<R>> =
expr.transformQuantifier(expr.indexVarDeclarations, expr.body)

override fun transform(expr: KExistentialQuantifier): KExpr<KBoolSort> =
expr.transformQuantifier(expr.bounds, expr.body)
Expand Down
7 changes: 4 additions & 3 deletions ksmt-bitwuzla/src/main/kotlin/org/ksmt/solver/bitwuzla/KBitwuzlaExprConverter.kt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -136,7 +136,7 @@ open class KBitwuzlaExprConverter(

// array
BitwuzlaKind.BITWUZLA_KIND_CONST_ARRAY -> expr.convert { value: KExpr<KSort> ->
val sort = Native.bitwuzlaTermGetSort(expr).convertSort() as KArraySort<*, *>
val sort: KArraySort<KSort, KSort> = Native.bitwuzlaTermGetSort(expr).convertSort().uncheckedCast()
convertConstArrayExpr(sort, value)
}

Expand Down Expand Up @@ -652,7 +652,7 @@ open class KBitwuzlaExprConverter(
fun convertConstArrayExpr(
currentSort: KArraySort<KSort, KSort>,
value: KExpr<KSort>
): KArrayConst<KSort, KSort> = with(ctx) {
): KArrayConst<KArraySort<KSort, KSort>, KSort> = with(ctx) {
val expectedValueSort = selectExpectedSort(currentSort.range, value.sort)
val expectedArraySort = mkArraySort(currentSort.domain, expectedValueSort)
return mkArrayConst(expectedArraySort, value.convertToExpectedIfNeeded(expectedValueSort))
Expand Down Expand Up @@ -796,7 +796,8 @@ open class KBitwuzlaExprConverter(
check(expectedDomain !is KArraySort<*, *> && expectedRange !is KArraySort<*, *>) {
"Bitwuzla doesn't support nested arrays"
}
ArrayAdapterExpr(this@ensureArrayExprSortMatch, expectedDomain, expectedRange)
val array: KExpr<KArraySort<KSort, KSort>> = this@ensureArrayExprSortMatch.uncheckedCast()
ArrayAdapterExpr(array, expectedDomain, expectedRange)
}
}
}
Expand Down
89 changes: 87 additions & 2 deletions ksmt-bitwuzla/src/main/kotlin/org/ksmt/solver/bitwuzla/KBitwuzlaExprInternalizer.kt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -7,8 +7,17 @@ import org.ksmt.decl.KDeclVisitor
import org.ksmt.decl.KFuncDecl
import org.ksmt.expr.KAddArithExpr
import org.ksmt.expr.KAndExpr
import org.ksmt.expr.KArray2Lambda
import org.ksmt.expr.KArray2Select
import org.ksmt.expr.KArray2Store
import org.ksmt.expr.KArray3Lambda
import org.ksmt.expr.KArray3Select
import org.ksmt.expr.KArray3Store
import org.ksmt.expr.KArrayConst
import org.ksmt.expr.KArrayLambda
import org.ksmt.expr.KArrayNLambda
import org.ksmt.expr.KArrayNSelect
import org.ksmt.expr.KArrayNStore
import org.ksmt.expr.KArraySelect
import org.ksmt.expr.KArrayStore
import org.ksmt.expr.KBitVec16Value
Expand Down Expand Up @@ -148,7 +157,11 @@ import org.ksmt.solver.bitwuzla.bindings.BitwuzlaTerm
import org.ksmt.solver.bitwuzla.bindings.Native
import org.ksmt.solver.util.KExprInternalizerBase
import org.ksmt.sort.KArithSort
import org.ksmt.sort.KArray2Sort
import org.ksmt.sort.KArray3Sort
import org.ksmt.sort.KArrayNSort
import org.ksmt.sort.KArraySort
import org.ksmt.sort.KArraySortBase
import org.ksmt.sort.KBoolSort
import org.ksmt.sort.KBv16Sort
import org.ksmt.sort.KBv32Sort
Expand Down Expand Up @@ -696,6 +709,22 @@ open class KBitwuzlaExprInternalizer(
}
}

override fun <D0 : KSort, D1 : KSort, R : KSort> transform(
expr: KArray2Store<D0, D1, R>
): KExpr<KArray2Sort<D0, D1, R>> {
TODO("Multi-indexed arrays are not supported")
}

override fun <D0 : KSort, D1 : KSort, D2 : KSort, R : KSort> transform(
expr: KArray3Store<D0, D1, D2, R>
): KExpr<KArray3Sort<D0, D1, D2, R>> {
TODO("Multi-indexed arrays are not supported")
}

override fun <R : KSort> transform(expr: KArrayNStore<R>): KExpr<KArrayNSort<R>> {
TODO("Multi-indexed arrays are not supported")
}

override fun <D : KSort, R : KSort> transform(expr: KArraySelect<D, R>) = with(expr) {
transform(array, index) { a: BitwuzlaTerm, i: BitwuzlaTerm ->
mkArraySelectTerm(Native.bitwuzlaTermGetBitwuzlaKind(a), a, i)
Expand All @@ -709,7 +738,21 @@ open class KBitwuzlaExprInternalizer(
Native.bitwuzlaMkTerm2(bitwuzlaCtx.bitwuzla, BitwuzlaKind.BITWUZLA_KIND_ARRAY_SELECT, array, idx)
}

override fun <D : KSort, R : KSort> transform(expr: KArrayConst<D, R>) = with(expr) {
override fun <D0 : KSort, D1 : KSort, R : KSort> transform(expr: KArray2Select<D0, D1, R>): KExpr<R> {
TODO("Multi-indexed arrays are not supported")
}

override fun <D0 : KSort, D1 : KSort, D2 : KSort, R : KSort> transform(
expr: KArray3Select<D0, D1, D2, R>
): KExpr<R> {
TODO("Multi-indexed arrays are not supported")
}

override fun <R : KSort> transform(expr: KArrayNSelect<R>): KExpr<R> {
TODO("Multi-indexed arrays are not supported")
}

override fun <A : KArraySortBase<R>, R : KSort> transform(expr: KArrayConst<A, R>) = with(expr) {
transform(value) { value: BitwuzlaTerm ->
Native.bitwuzlaMkConstArray(bitwuzlaCtx.bitwuzla, sort.internalizeSort(), value)
}
Expand All @@ -732,6 +775,24 @@ open class KBitwuzlaExprInternalizer(
private fun mkLambdaTerm(boundVar: BitwuzlaTerm, body: BitwuzlaTerm): BitwuzlaTerm =
Native.bitwuzlaMkTerm2(bitwuzlaCtx.bitwuzla, BitwuzlaKind.BITWUZLA_KIND_LAMBDA, boundVar, body)

override fun <D0 : KSort, D1 : KSort, R : KSort> transform(
expr: KArray2Lambda<D0, D1, R>
): KExpr<KArray2Sort<D0, D1, R>> {
TODO("Multi-indexed arrays are not supported")
}

override fun <D0 : KSort, D1 : KSort, D2 : KSort, R : KSort> transform(
expr: KArray3Lambda<D0, D1, D2, R>
): KExpr<KArray3Sort<D0, D1, D2, R>> {
TODO("Multi-indexed arrays are not supported")
}

override fun <R : KSort> transform(
expr: KArrayNLambda<R>
): KExpr<KArrayNSort<R>> {
TODO("Multi-indexed arrays are not supported")
}

override fun transform(
expr: KExistentialQuantifier
): KExpr<KBoolSort> = expr.internalizeQuantifier { args ->
Expand Down Expand Up @@ -1007,7 +1068,7 @@ open class KBitwuzlaExprInternalizer(
}
}

override fun <D : KSort, R : KSort> transform(expr: KFunctionAsArray<D, R>): KExpr<KArraySort<D, R>> {
override fun <A : KArraySortBase<R>, R : KSort> transform(expr: KFunctionAsArray<A, R>): KExpr<A> {
TODO("KFunctionAsArray internalization is not implemented in bitwuzla")
}

Expand Down Expand Up @@ -1079,6 +1140,20 @@ open class KBitwuzlaExprInternalizer(
Native.bitwuzlaMkArraySort(bitwuzlaCtx.bitwuzla, domain, range)
}

override fun <D0 : KSort, D1 : KSort, R : KSort> visit(sort: KArray2Sort<D0, D1, R>): BitwuzlaSort {
TODO("Multi-indexed arrays are not supported")
}

override fun <D0 : KSort, D1 : KSort, D2 : KSort, R : KSort> visit(
sort: KArray3Sort<D0, D1, D2, R>
): BitwuzlaSort {
TODO("Multi-indexed arrays are not supported")
}

override fun <R : KSort> visit(sort: KArrayNSort<R>): BitwuzlaSort {
TODO("Multi-indexed arrays are not supported")
}

override fun <S : KBvSort> visit(sort: S): BitwuzlaSort =
bitwuzlaCtx.internalizeSort(sort) {
val size = sort.sizeBits.toInt()
Expand Down Expand Up @@ -1208,6 +1283,16 @@ open class KBitwuzlaExprInternalizer(
override fun <D : KSort, R : KSort> visit(sort: KArraySort<D, R>): Boolean =
sort.domain.accept(this) || sort.range.accept(this)

override fun <D0 : KSort, D1 : KSort, R : KSort> visit(sort: KArray2Sort<D0, D1, R>): Boolean =
sort.domain0.accept(this) || sort.domain1.accept(this) || sort.range.accept(this)

override fun <D0 : KSort, D1 : KSort, D2 : KSort, R : KSort> visit(sort: KArray3Sort<D0, D1, D2, R>): Boolean =
sort.domain0.accept(this) || sort.domain1.accept(this)
|| sort.domain2.accept(this) || sort.range.accept(this)

override fun <R : KSort> visit(sort: KArrayNSort<R>): Boolean =
sort.domainSorts.any { it.accept(this) } || sort.range.accept(this)

override fun visit(sort: KBoolSort): Boolean = false
override fun visit(sort: KIntSort): Boolean = false
override fun visit(sort: KRealSort): Boolean = false
Expand Down
4 changes: 2 additions & 2 deletions ksmt-bitwuzla/src/main/kotlin/org/ksmt/solver/bitwuzla/KBitwuzlaModel.kt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -142,7 +142,7 @@ open class KBitwuzlaModel(
decl: KDecl<T>,
term: BitwuzlaTerm
): KModel.KFuncInterp<T> = with(converter) {
val sort = decl.sort as KArraySort<*, *>
val sort: KArraySort<KSort, KSort> = decl.sort.uncheckedCast()
val entries = mutableListOf<KModel.KFuncInterpEntry<KSort>>()
val interp = Native.bitwuzlaGetArrayValue(bitwuzlaCtx.bitwuzla, term)

Expand All @@ -168,7 +168,7 @@ open class KBitwuzlaModel(
decl = decl,
vars = emptyList(),
entries = emptyList(),
default = mkFunctionAsArray<KSort, KSort>(arrayInterpDecl).uncheckedCast()
default = mkFunctionAsArray(sort, arrayInterpDecl).uncheckedCast()
)
}

Expand Down
Loading

0 comments on commit 98c560b

Please sign in to comment.