Skip to content

Commit 957ead4

Browse files
SaloedSaloed
authored
Theories specialization (#163)
* Theories * Fix theory requirements collector * Fix theory requirements collector * List all supported Z3 theory combinations * Try remove cvc5 limits * Upgrade ksmt version
1 parent fdd016d commit 957ead4

28 files changed

Lines changed: 865 additions & 76 deletions

File tree

‎README.md‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -11,7 +11,7 @@ Get the most out of SMT solving with KSMT features:
1111
* Streamlined [solver delivery](#ksmt-distribution) with no need for building a solver or implementing JVM bindings
1212

1313
[![KSMT: build](https://github.com/UnitTestBot/ksmt/actions/workflows/build-and-run-tests.yml/badge.svg)](https://github.com/UnitTestBot/ksmt/actions/workflows/build-and-run-tests.yml)
14-
[![Maven Central](https://img.shields.io/maven-central/v/io.ksmt/ksmt-core)](https://central.sonatype.com/artifact/io.ksmt/ksmt-core/0.5.25)
14+
[![Maven Central](https://img.shields.io/maven-central/v/io.ksmt/ksmt-core)](https://central.sonatype.com/artifact/io.ksmt/ksmt-core/0.5.26)
1515
[![javadoc](https://javadoc.io/badge2/io.ksmt/ksmt-core/javadoc.svg)](https://javadoc.io/doc/io.ksmt/ksmt-core)
1616

1717
## Get started
@@ -20,9 +20,9 @@ To start using KSMT, install it via [Gradle](https://gradle.org/):
2020

2121
```kotlin
2222
// core
23-
implementation("io.ksmt:ksmt-core:0.5.25")
23+
implementation("io.ksmt:ksmt-core:0.5.26")
2424
// z3 solver
25-
implementation("io.ksmt:ksmt-z3:0.5.25")
25+
implementation("io.ksmt:ksmt-z3:0.5.26")
2626
```
2727

2828
Find basic instructions in the [Getting started](docs/getting-started.md) guide and try it out with the

‎buildSrc/src/main/kotlin/io.ksmt.ksmt-base.gradle.kts‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -11,7 +11,7 @@ plugins {
1111
}
1212

1313
group = "io.ksmt"
14-
version = "0.5.25"
14+
version = "0.5.26"
1515

1616
repositories {
1717
mavenCentral()

‎docs/getting-started.md‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -34,7 +34,7 @@ repositories {
3434
```kotlin
3535
dependencies {
3636
// core
37-
implementation("io.ksmt:ksmt-core:0.5.25")
37+
implementation("io.ksmt:ksmt-core:0.5.26")
3838
}
3939
```
4040

@@ -43,9 +43,9 @@ dependencies {
4343
```kotlin
4444
dependencies {
4545
// z3
46-
implementation("io.ksmt:ksmt-z3:0.5.25")
46+
implementation("io.ksmt:ksmt-z3:0.5.26")
4747
// bitwuzla
48-
implementation("io.ksmt:ksmt-bitwuzla:0.5.25")
48+
implementation("io.ksmt:ksmt-bitwuzla:0.5.26")
4949
}
5050
```
5151

‎examples/build.gradle.kts‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -9,11 +9,11 @@ repositories {
99

1010
dependencies {
1111
// core
12-
implementation("io.ksmt:ksmt-core:0.5.25")
12+
implementation("io.ksmt:ksmt-core:0.5.26")
1313
// z3 solver
14-
implementation("io.ksmt:ksmt-z3:0.5.25")
14+
implementation("io.ksmt:ksmt-z3:0.5.26")
1515
// Runner and portfolio solver
16-
implementation("io.ksmt:ksmt-runner:0.5.25")
16+
implementation("io.ksmt:ksmt-runner:0.5.26")
1717
}
1818

1919
java {

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

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

33
import io.ksmt.solver.KSolverConfiguration
44
import io.ksmt.solver.KSolverUniversalConfigurationBuilder
5+
import io.ksmt.solver.KSolverUnsupportedFeatureException
56
import io.ksmt.solver.KSolverUnsupportedParameterException
7+
import io.ksmt.solver.KTheory
8+
import io.ksmt.solver.KTheory.LIA
9+
import io.ksmt.solver.KTheory.LRA
10+
import io.ksmt.solver.KTheory.NIA
11+
import io.ksmt.solver.KTheory.NRA
612
import org.ksmt.solver.bitwuzla.bindings.Bitwuzla
713
import org.ksmt.solver.bitwuzla.bindings.BitwuzlaOption
814
import org.ksmt.solver.bitwuzla.bindings.Native
@@ -42,11 +48,23 @@ class KBitwuzlaSolverConfigurationImpl(private val bitwuzla: Bitwuzla) : KBitwuz
4248
override fun setBitwuzlaOption(option: BitwuzlaOption, value: String) {
4349
Native.bitwuzlaSetOptionStr(bitwuzla, option, value)
4450
}
51+
52+
override fun optimizeForTheories(theories: Set<KTheory>?, quantifiersAllowed: Boolean) {
53+
if (theories.isNullOrEmpty()) return
54+
55+
if (setOf(LIA, LRA, NIA, NRA).intersect(theories).isNotEmpty()) {
56+
throw KSolverUnsupportedFeatureException("Unsupported theories $theories")
57+
}
58+
}
4559
}
4660

4761
class KBitwuzlaSolverUniversalConfiguration(
4862
private val builder: KSolverUniversalConfigurationBuilder
4963
) : KBitwuzlaSolverConfiguration {
64+
override fun optimizeForTheories(theories: Set<KTheory>?, quantifiersAllowed: Boolean) {
65+
builder.buildOptimizeForTheories(theories, quantifiersAllowed)
66+
}
67+
5068
override fun setBitwuzlaOption(option: BitwuzlaOption, value: Int) {
5169
builder.buildIntParameter(option.name, value)
5270
}

‎ksmt-core/src/main/kotlin/io/ksmt/solver/KSolverConfiguration.kt‎

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,23 @@
11
package io.ksmt.solver
22

3+
@Suppress("OVERLOADS_INTERFACE", "INAPPLICABLE_JVM_NAME")
34
interface KSolverConfiguration {
45
fun setBoolParameter(param: String, value: Boolean)
56
fun setIntParameter(param: String, value: Int)
67
fun setStringParameter(param: String, value: String)
78
fun setDoubleParameter(param: String, value: Double)
9+
10+
/**
11+
* Specialize the solver to work with the provided theories.
12+
*
13+
* [theories] a set of theories.
14+
* If the provided theories are null, the solver is specialized to work with all supported theories.
15+
* If the provided theory set is empty, the solver is configured to work only with propositional formulas.
16+
*
17+
* [quantifiersAllowed] allows or disallows formulas with quantifiers.
18+
* If quantifiers are not allowed, the solver is specialized to work with Quantifier Free formulas.
19+
* * */
20+
@JvmOverloads
21+
@JvmName("optimizeForTheories")
22+
fun optimizeForTheories(theories: Set<KTheory>? = null, quantifiersAllowed: Boolean = false)
823
}

‎ksmt-core/src/main/kotlin/io/ksmt/solver/KSolverUniversalConfigurationBuilder.kt‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -5,4 +5,5 @@ interface KSolverUniversalConfigurationBuilder {
55
fun buildIntParameter(param: String, value: Int)
66
fun buildStringParameter(param: String, value: String)
77
fun buildDoubleParameter(param: String, value: Double)
8+
fun buildOptimizeForTheories(theories: Set<KTheory>?, quantifiersAllowed: Boolean)
89
}

‎ksmt-core/src/main/kotlin/io/ksmt/solver/KTheory.kt‎

Lines changed: 79 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,79 @@
1+
package io.ksmt.solver
2+
3+
import io.ksmt.solver.KTheory.Array
4+
import io.ksmt.solver.KTheory.BV
5+
import io.ksmt.solver.KTheory.FP
6+
import io.ksmt.solver.KTheory.LIA
7+
import io.ksmt.solver.KTheory.LRA
8+
import io.ksmt.solver.KTheory.NIA
9+
import io.ksmt.solver.KTheory.NRA
10+
import io.ksmt.solver.KTheory.UF
11+
12+
/**
13+
* SMT theory
14+
* */
15+
enum class KTheory {
16+
UF, BV, FP, Array,
17+
LIA, NIA, LRA, NRA
18+
}
19+
20+
@Suppress("ComplexMethod", "ComplexCondition")
21+
fun Set<KTheory>?.smtLib2String(quantifiersAllowed: Boolean = false): String = buildString {
22+
val theories = this@smtLib2String
23+
24+
if (!quantifiersAllowed) {
25+
append("QF_")
26+
}
27+
28+
if (theories == null) {
29+
append("ALL")
30+
return@buildString
31+
}
32+
33+
if (theories.isEmpty()) {
34+
append("SAT")
35+
return@buildString
36+
}
37+
38+
if (Array in theories) {
39+
if (theories.size == 1) {
40+
append("AX")
41+
return@buildString
42+
}
43+
append("A")
44+
}
45+
46+
if (UF in theories) {
47+
append("UF")
48+
}
49+
50+
if (BV in theories) {
51+
append("BV")
52+
}
53+
54+
if (FP in theories) {
55+
append("FP")
56+
}
57+
58+
if (LIA in theories || NIA in theories || LRA in theories || NRA in theories) {
59+
val hasNonLinear = NIA in theories || NRA in theories
60+
val hasReal = LRA in theories || NRA in theories
61+
val hasInt = LIA in theories || NIA in theories
62+
63+
if (hasNonLinear) {
64+
append("N")
65+
} else {
66+
append("L")
67+
}
68+
69+
if (hasInt) {
70+
append("I")
71+
}
72+
73+
if (hasReal) {
74+
append("R")
75+
}
76+
77+
append("A")
78+
}
79+
}

‎ksmt-core/src/main/kotlin/io/ksmt/utils/KExprTheoryRequirement.kt‎

Lines changed: 133 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,133 @@
1+
package io.ksmt.utils
2+
3+
import io.ksmt.KContext
4+
import io.ksmt.expr.KDivArithExpr
5+
import io.ksmt.expr.KExistentialQuantifier
6+
import io.ksmt.expr.KExpr
7+
import io.ksmt.expr.KFunctionApp
8+
import io.ksmt.expr.KMulArithExpr
9+
import io.ksmt.expr.KPowerArithExpr
10+
import io.ksmt.expr.KUniversalQuantifier
11+
import io.ksmt.expr.transformer.KNonRecursiveTransformer
12+
import io.ksmt.solver.KTheory
13+
import io.ksmt.solver.KTheory.Array
14+
import io.ksmt.solver.KTheory.BV
15+
import io.ksmt.solver.KTheory.FP
16+
import io.ksmt.solver.KTheory.LIA
17+
import io.ksmt.solver.KTheory.LRA
18+
import io.ksmt.solver.KTheory.NIA
19+
import io.ksmt.solver.KTheory.NRA
20+
import io.ksmt.solver.KTheory.UF
21+
import io.ksmt.sort.KArithSort
22+
import io.ksmt.sort.KArray2Sort
23+
import io.ksmt.sort.KArray3Sort
24+
import io.ksmt.sort.KArrayNSort
25+
import io.ksmt.sort.KArraySort
26+
import io.ksmt.sort.KBoolSort
27+
import io.ksmt.sort.KBvSort
28+
import io.ksmt.sort.KFpRoundingModeSort
29+
import io.ksmt.sort.KFpSort
30+
import io.ksmt.sort.KIntSort
31+
import io.ksmt.sort.KRealSort
32+
import io.ksmt.sort.KSort
33+
import io.ksmt.sort.KSortVisitor
34+
import io.ksmt.sort.KUninterpretedSort
35+
36+
class KExprTheoryRequirement(ctx: KContext) : KNonRecursiveTransformer(ctx) {
37+
val usedTheories = hashSetOf<KTheory>()
38+
39+
var hasQuantifiers: Boolean = false
40+
private set
41+
42+
private val sortRequirementCollector = Sort2TheoryRequirement()
43+
44+
override fun <T : KSort> transformExpr(expr: KExpr<T>): KExpr<T> {
45+
expr.sort.accept(sortRequirementCollector)
46+
return super.transformExpr(expr)
47+
}
48+
49+
override fun <T : KSort> transform(expr: KFunctionApp<T>): KExpr<T> {
50+
if (expr.args.isNotEmpty()) {
51+
usedTheories += UF
52+
}
53+
return super.transform(expr)
54+
}
55+
56+
override fun transform(expr: KExistentialQuantifier): KExpr<KBoolSort> {
57+
hasQuantifiers = true
58+
return super.transform(expr)
59+
}
60+
61+
override fun transform(expr: KUniversalQuantifier): KExpr<KBoolSort> {
62+
hasQuantifiers = true
63+
return super.transform(expr)
64+
}
65+
66+
override fun <T : KArithSort> transform(expr: KMulArithExpr<T>): KExpr<T> {
67+
usedTheories += if (expr.sort is KIntSort) NIA else NRA
68+
return super.transform(expr)
69+
}
70+
71+
override fun <T : KArithSort> transform(expr: KDivArithExpr<T>): KExpr<T> {
72+
usedTheories += if (expr.sort is KIntSort) NIA else NRA
73+
return super.transform(expr)
74+
}
75+
76+
override fun <T : KArithSort> transform(expr: KPowerArithExpr<T>): KExpr<T> {
77+
usedTheories += if (expr.sort is KIntSort) NIA else NRA
78+
return super.transform(expr)
79+
}
80+
81+
private inner class Sort2TheoryRequirement : KSortVisitor<Unit> {
82+
override fun visit(sort: KBoolSort) {
83+
}
84+
85+
override fun visit(sort: KIntSort) {
86+
usedTheories += LIA
87+
}
88+
89+
override fun visit(sort: KRealSort) {
90+
usedTheories += LRA
91+
}
92+
93+
override fun <S : KBvSort> visit(sort: S) {
94+
usedTheories += BV
95+
}
96+
97+
override fun <S : KFpSort> visit(sort: S) {
98+
usedTheories += FP
99+
}
100+
101+
override fun <D : KSort, R : KSort> visit(sort: KArraySort<D, R>) {
102+
usedTheories += Array
103+
sort.range.accept(this)
104+
sort.domainSorts.forEach { it.accept(this) }
105+
}
106+
107+
override fun <D0 : KSort, D1 : KSort, R : KSort> visit(sort: KArray2Sort<D0, D1, R>) {
108+
usedTheories += Array
109+
sort.range.accept(this)
110+
sort.domainSorts.forEach { it.accept(this) }
111+
}
112+
113+
override fun <D0 : KSort, D1 : KSort, D2 : KSort, R : KSort> visit(sort: KArray3Sort<D0, D1, D2, R>) {
114+
usedTheories += Array
115+
sort.range.accept(this)
116+
sort.domainSorts.forEach { it.accept(this) }
117+
}
118+
119+
override fun <R : KSort> visit(sort: KArrayNSort<R>) {
120+
usedTheories += Array
121+
sort.range.accept(this)
122+
sort.domainSorts.forEach { it.accept(this) }
123+
}
124+
125+
override fun visit(sort: KFpRoundingModeSort) {
126+
usedTheories += FP
127+
}
128+
129+
override fun visit(sort: KUninterpretedSort) {
130+
usedTheories += UF
131+
}
132+
}
133+
}

0 commit comments

Comments
 (0)