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

Author: Saloed

Diff for: README.md

@@ -11,7 +11,7 @@ Get the most out of SMT solving with KSMT features:
 * Streamlined [solver delivery](#ksmt-distribution) with no need for building a solver or implementing JVM bindings
 
 [![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)
-[![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)
+[![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)
 [![javadoc](https://javadoc.io/badge2/io.ksmt/ksmt-core/javadoc.svg)](https://javadoc.io/doc/io.ksmt/ksmt-core)
 
 ## Get started
@@ -20,9 +20,9 @@ To start using KSMT, install it via [Gradle](https://gradle.org/):
 
 ```kotlin
 // core 
-implementation("io.ksmt:ksmt-core:0.5.25")
+implementation("io.ksmt:ksmt-core:0.5.26")
 // z3 solver
-implementation("io.ksmt:ksmt-z3:0.5.25")
+implementation("io.ksmt:ksmt-z3:0.5.26")
 ```
 
 Find basic instructions in the [Getting started](docs/getting-started.md) guide and try it out with the 

Diff for: buildSrc/src/main/kotlin/io.ksmt.ksmt-base.gradle.kts

@@ -11,7 +11,7 @@ plugins {
 }
 
 group = "io.ksmt"
-version = "0.5.25"
+version = "0.5.26"
 
 repositories {
     mavenCentral()

Diff for: docs/getting-started.md

@@ -34,7 +34,7 @@ repositories {
 ```kotlin
 dependencies {
     // core 
-    implementation("io.ksmt:ksmt-core:0.5.25")    
+    implementation("io.ksmt:ksmt-core:0.5.26")    
 }
 ```
 
@@ -43,9 +43,9 @@ dependencies {
 ```kotlin
 dependencies {
     // z3 
-    implementation("io.ksmt:ksmt-z3:0.5.25")
+    implementation("io.ksmt:ksmt-z3:0.5.26")
     // bitwuzla
-    implementation("io.ksmt:ksmt-bitwuzla:0.5.25")
+    implementation("io.ksmt:ksmt-bitwuzla:0.5.26")
 }
 ```
 

Diff for: examples/build.gradle.kts

@@ -9,11 +9,11 @@ repositories {
 
 dependencies {
     // core
-    implementation("io.ksmt:ksmt-core:0.5.25")
+    implementation("io.ksmt:ksmt-core:0.5.26")
     // z3 solver
-    implementation("io.ksmt:ksmt-z3:0.5.25")
+    implementation("io.ksmt:ksmt-z3:0.5.26")
     // Runner and portfolio solver
-    implementation("io.ksmt:ksmt-runner:0.5.25")
+    implementation("io.ksmt:ksmt-runner:0.5.26")
 }
 
 java {

Diff for: ksmt-bitwuzla/ksmt-bitwuzla-core/src/main/kotlin/io/ksmt/solver/bitwuzla/KBitwuzlaSolverConfiguration.kt

@@ -2,7 +2,13 @@ package io.ksmt.solver.bitwuzla
 
 import io.ksmt.solver.KSolverConfiguration
 import io.ksmt.solver.KSolverUniversalConfigurationBuilder
+import io.ksmt.solver.KSolverUnsupportedFeatureException
 import io.ksmt.solver.KSolverUnsupportedParameterException
+import io.ksmt.solver.KTheory
+import io.ksmt.solver.KTheory.LIA
+import io.ksmt.solver.KTheory.LRA
+import io.ksmt.solver.KTheory.NIA
+import io.ksmt.solver.KTheory.NRA
 import org.ksmt.solver.bitwuzla.bindings.Bitwuzla
 import org.ksmt.solver.bitwuzla.bindings.BitwuzlaOption
 import org.ksmt.solver.bitwuzla.bindings.Native
@@ -42,11 +48,23 @@ class KBitwuzlaSolverConfigurationImpl(private val bitwuzla: Bitwuzla) : KBitwuz
     override fun setBitwuzlaOption(option: BitwuzlaOption, value: String) {
         Native.bitwuzlaSetOptionStr(bitwuzla, option, value)
     }
+
+    override fun optimizeForTheories(theories: Set<KTheory>?, quantifiersAllowed: Boolean) {
+        if (theories.isNullOrEmpty()) return
+
+        if (setOf(LIA, LRA, NIA, NRA).intersect(theories).isNotEmpty()) {
+            throw KSolverUnsupportedFeatureException("Unsupported theories $theories")
+        }
+    }
 }
 
 class KBitwuzlaSolverUniversalConfiguration(
     private val builder: KSolverUniversalConfigurationBuilder
 ) : KBitwuzlaSolverConfiguration {
+    override fun optimizeForTheories(theories: Set<KTheory>?, quantifiersAllowed: Boolean) {
+        builder.buildOptimizeForTheories(theories, quantifiersAllowed)
+    }
+
     override fun setBitwuzlaOption(option: BitwuzlaOption, value: Int) {
         builder.buildIntParameter(option.name, value)
     }

Diff for: ksmt-core/src/main/kotlin/io/ksmt/solver/KSolverConfiguration.kt

@@ -1,8 +1,23 @@
 package io.ksmt.solver
 
+@Suppress("OVERLOADS_INTERFACE", "INAPPLICABLE_JVM_NAME")
 interface KSolverConfiguration {
     fun setBoolParameter(param: String, value: Boolean)
     fun setIntParameter(param: String, value: Int)
     fun setStringParameter(param: String, value: String)
     fun setDoubleParameter(param: String, value: Double)
+
+    /**
+     * Specialize the solver to work with the provided theories.
+     *
+     * [theories] a set of theories.
+     * If the provided theories are null, the solver is specialized to work with all supported theories.
+     * If the provided theory set is empty, the solver is configured to work only with propositional formulas.
+     *
+     * [quantifiersAllowed] allows or disallows formulas with quantifiers.
+     * If quantifiers are not allowed, the solver is specialized to work with Quantifier Free formulas.
+     * * */
+    @JvmOverloads
+    @JvmName("optimizeForTheories")
+    fun optimizeForTheories(theories: Set<KTheory>? = null, quantifiersAllowed: Boolean = false)
 }

Diff for: ksmt-core/src/main/kotlin/io/ksmt/solver/KSolverUniversalConfigurationBuilder.kt

@@ -5,4 +5,5 @@ interface KSolverUniversalConfigurationBuilder {
     fun buildIntParameter(param: String, value: Int)
     fun buildStringParameter(param: String, value: String)
     fun buildDoubleParameter(param: String, value: Double)
+    fun buildOptimizeForTheories(theories: Set<KTheory>?, quantifiersAllowed: Boolean)
 }

Diff for: ksmt-core/src/main/kotlin/io/ksmt/solver/KTheory.kt

@@ -0,0 +1,79 @@
+package io.ksmt.solver
+
+import io.ksmt.solver.KTheory.Array
+import io.ksmt.solver.KTheory.BV
+import io.ksmt.solver.KTheory.FP
+import io.ksmt.solver.KTheory.LIA
+import io.ksmt.solver.KTheory.LRA
+import io.ksmt.solver.KTheory.NIA
+import io.ksmt.solver.KTheory.NRA
+import io.ksmt.solver.KTheory.UF
+
+/**
+ * SMT theory
+ * */
+enum class KTheory {
+    UF, BV, FP, Array,
+    LIA, NIA, LRA, NRA
+}
+
+@Suppress("ComplexMethod", "ComplexCondition")
+fun Set<KTheory>?.smtLib2String(quantifiersAllowed: Boolean = false): String = buildString {
+    val theories = this@smtLib2String
+
+    if (!quantifiersAllowed) {
+        append("QF_")
+    }
+
+    if (theories == null) {
+        append("ALL")
+        return@buildString
+    }
+
+    if (theories.isEmpty()) {
+        append("SAT")
+        return@buildString
+    }
+
+    if (Array in theories) {
+        if (theories.size == 1) {
+            append("AX")
+            return@buildString
+        }
+        append("A")
+    }
+
+    if (UF in theories) {
+        append("UF")
+    }
+
+    if (BV in theories) {
+        append("BV")
+    }
+
+    if (FP in theories) {
+        append("FP")
+    }
+
+    if (LIA in theories || NIA in theories || LRA in theories || NRA in theories) {
+        val hasNonLinear = NIA in theories || NRA in theories
+        val hasReal = LRA in theories || NRA in theories
+        val hasInt = LIA in theories || NIA in theories
+
+        if (hasNonLinear) {
+            append("N")
+        } else {
+            append("L")
+        }
+
+        if (hasInt) {
+            append("I")
+        }
+
+        if (hasReal) {
+            append("R")
+        }
+
+        append("A")
+    }
+}

Diff for: ksmt-core/src/main/kotlin/io/ksmt/utils/KExprTheoryRequirement.kt

@@ -0,0 +1,133 @@
+package io.ksmt.utils
+
+import io.ksmt.KContext
+import io.ksmt.expr.KDivArithExpr
+import io.ksmt.expr.KExistentialQuantifier
+import io.ksmt.expr.KExpr
+import io.ksmt.expr.KFunctionApp
+import io.ksmt.expr.KMulArithExpr
+import io.ksmt.expr.KPowerArithExpr
+import io.ksmt.expr.KUniversalQuantifier
+import io.ksmt.expr.transformer.KNonRecursiveTransformer
+import io.ksmt.solver.KTheory
+import io.ksmt.solver.KTheory.Array
+import io.ksmt.solver.KTheory.BV
+import io.ksmt.solver.KTheory.FP
+import io.ksmt.solver.KTheory.LIA
+import io.ksmt.solver.KTheory.LRA
+import io.ksmt.solver.KTheory.NIA
+import io.ksmt.solver.KTheory.NRA
+import io.ksmt.solver.KTheory.UF
+import io.ksmt.sort.KArithSort
+import io.ksmt.sort.KArray2Sort
+import io.ksmt.sort.KArray3Sort
+import io.ksmt.sort.KArrayNSort
+import io.ksmt.sort.KArraySort
+import io.ksmt.sort.KBoolSort
+import io.ksmt.sort.KBvSort
+import io.ksmt.sort.KFpRoundingModeSort
+import io.ksmt.sort.KFpSort
+import io.ksmt.sort.KIntSort
+import io.ksmt.sort.KRealSort
+import io.ksmt.sort.KSort
+import io.ksmt.sort.KSortVisitor
+import io.ksmt.sort.KUninterpretedSort
+
+class KExprTheoryRequirement(ctx: KContext) : KNonRecursiveTransformer(ctx) {
+    val usedTheories = hashSetOf<KTheory>()
+
+    var hasQuantifiers: Boolean = false
+        private set
+
+    private val sortRequirementCollector = Sort2TheoryRequirement()
+
+    override fun <T : KSort> transformExpr(expr: KExpr<T>): KExpr<T> {
+        expr.sort.accept(sortRequirementCollector)
+        return super.transformExpr(expr)
+    }
+
+    override fun <T : KSort> transform(expr: KFunctionApp<T>): KExpr<T> {
+        if (expr.args.isNotEmpty()) {
+            usedTheories += UF
+        }
+        return super.transform(expr)
+    }
+
+    override fun transform(expr: KExistentialQuantifier): KExpr<KBoolSort> {
+        hasQuantifiers = true
+        return super.transform(expr)
+    }
+
+    override fun transform(expr: KUniversalQuantifier): KExpr<KBoolSort> {
+        hasQuantifiers = true
+        return super.transform(expr)
+    }
+
+    override fun <T : KArithSort> transform(expr: KMulArithExpr<T>): KExpr<T> {
+        usedTheories += if (expr.sort is KIntSort) NIA else NRA
+        return super.transform(expr)
+    }
+
+    override fun <T : KArithSort> transform(expr: KDivArithExpr<T>): KExpr<T> {
+        usedTheories += if (expr.sort is KIntSort) NIA else NRA
+        return super.transform(expr)
+    }
+
+    override fun <T : KArithSort> transform(expr: KPowerArithExpr<T>): KExpr<T> {
+        usedTheories += if (expr.sort is KIntSort) NIA else NRA
+        return super.transform(expr)
+    }
+
+    private inner class Sort2TheoryRequirement : KSortVisitor<Unit> {
+        override fun visit(sort: KBoolSort) {
+        }
+
+        override fun visit(sort: KIntSort) {
+            usedTheories += LIA
+        }
+
+        override fun visit(sort: KRealSort) {
+            usedTheories += LRA
+        }
+
+        override fun <S : KBvSort> visit(sort: S) {
+            usedTheories += BV
+        }
+
+        override fun <S : KFpSort> visit(sort: S) {
+            usedTheories += FP
+        }
+
+        override fun <D : KSort, R : KSort> visit(sort: KArraySort<D, R>) {
+            usedTheories += Array
+            sort.range.accept(this)
+            sort.domainSorts.forEach { it.accept(this) }
+        }
+
+        override fun <D0 : KSort, D1 : KSort, R : KSort> visit(sort: KArray2Sort<D0, D1, R>) {
+            usedTheories += Array
+            sort.range.accept(this)
+            sort.domainSorts.forEach { it.accept(this) }
+        }
+
+        override fun <D0 : KSort, D1 : KSort, D2 : KSort, R : KSort> visit(sort: KArray3Sort<D0, D1, D2, R>) {
+            usedTheories += Array
+            sort.range.accept(this)
+            sort.domainSorts.forEach { it.accept(this) }
+        }
+
+        override fun <R : KSort> visit(sort: KArrayNSort<R>) {
+            usedTheories += Array
+            sort.range.accept(this)
+            sort.domainSorts.forEach { it.accept(this) }
+        }
+
+        override fun visit(sort: KFpRoundingModeSort) {
+            usedTheories += FP
+        }
+
+        override fun visit(sort: KUninterpretedSort) {
+            usedTheories += UF
+        }
+    }
+}