Upgrade solvers

.github/workflows/run-long-tests.yml

@@ -100,8 +100,18 @@ jobs:
             --no-daemon
             '-PtestDataRevision=${{ env.TEST_DATA_REVISION }}'
 
+  show_info:
+    needs: [setup]
+    runs-on: ubuntu-latest
+    steps:
+      - name: Show test info
+        run: echo "${{ fromJSON(needs.setup.outputs.matrix-tests) }}"
+
+      - name: Show chunk info
+        run: echo "${{ fromJSON(needs.setup.outputs.matrix-chunks) }}"
+
   run_tests:
-    needs: [setup, prepare_test_data]
+    needs: [setup, show_info, prepare_test_data]
     continue-on-error: true
     strategy:
       matrix:

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.30)
+[![Maven Central](https://img.shields.io/maven-central/v/io.ksmt/ksmt-core)](https://central.sonatype.com/artifact/io.ksmt/ksmt-core/0.6.1)
 [![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.30")
+implementation("io.ksmt:ksmt-core:0.6.1")
 // z3 solver
-implementation("io.ksmt:ksmt-z3:0.5.30")
+implementation("io.ksmt:ksmt-z3:0.6.1")
 ```
 
 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

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

docs/getting-started.md

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

examples/build.gradle.kts

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

ksmt-cvc5/ksmt-cvc5-core/build.gradle.kts

@@ -11,7 +11,7 @@ repositories {
     mavenCentral()
 }
 
-val cvc5Version = "1.2.0"
+val cvc5Version = "1.3.0"
 val cvc5Jar = distDir.resolve("cvc5-$cvc5Version.jar")
 
 dependencies {

ksmt-cvc5/ksmt-cvc5-core/src/main/kotlin/io/ksmt/solver/cvc5/KCvc5ExprConverter.kt

@@ -255,6 +255,15 @@ open class KCvc5ExprConverter(
             Kind.BITVECTOR_TO_NAT -> expr.convert { bvExpr: KExpr<KBvSort> ->
                 mkBv2IntExpr(bvExpr, false)
             }
+
+            Kind.BITVECTOR_SBV_TO_INT -> expr.convert { bvExpr: KExpr<KBvSort> ->
+                mkBv2IntExpr(bvExpr, isSigned = true)
+            }
+
+            Kind.BITVECTOR_UBV_TO_INT -> expr.convert { bvExpr: KExpr<KBvSort> ->
+                mkBv2IntExpr(bvExpr, isSigned = false)
+            }
+
             Kind.BITVECTOR_COMP -> throw KSolverUnsupportedFeatureException(
                 "No direct mapping of ${Kind.BITVECTOR_COMP} in ksmt"
             )
@@ -430,6 +439,8 @@ open class KCvc5ExprConverter(
             Kind.SET_MAP,
             Kind.SET_FILTER,
             Kind.SET_IS_EMPTY,
+            Kind.SET_ALL,
+            Kind.SET_SOME,
             Kind.SET_FOLD -> throw KSolverUnsupportedFeatureException("currently ksmt does not support sets")
 
             Kind.RELATION_JOIN,
@@ -460,6 +471,8 @@ open class KCvc5ExprConverter(
             Kind.BAG_FILTER,
             Kind.BAG_FOLD,
             Kind.BAG_SETOF,
+            Kind.BAG_ALL,
+            Kind.BAG_SOME,
             Kind.BAG_PARTITION -> throw KSolverUnsupportedFeatureException("currently ksmt does not support bags")
 
             Kind.TABLE_PRODUCT,

ksmt-cvc5/ksmt-cvc5-core/src/main/kotlin/io/ksmt/solver/cvc5/KCvc5ExprInternalizer.kt

@@ -158,11 +158,11 @@ import io.ksmt.expr.KXorExpr
 import io.ksmt.expr.rewrite.simplify.rewriteBvAddNoOverflowExpr
 import io.ksmt.expr.rewrite.simplify.rewriteBvAddNoUnderflowExpr
 import io.ksmt.expr.rewrite.simplify.rewriteBvDivNoOverflowExpr
+import io.ksmt.expr.rewrite.simplify.rewriteBvMulNoOverflowExpr
+import io.ksmt.expr.rewrite.simplify.rewriteBvMulNoUnderflowExpr
 import io.ksmt.expr.rewrite.simplify.rewriteBvNegNoOverflowExpr
 import io.ksmt.expr.rewrite.simplify.rewriteBvSubNoOverflowExpr
 import io.ksmt.expr.rewrite.simplify.rewriteBvSubNoUnderflowExpr
-import io.ksmt.expr.rewrite.simplify.rewriteBvMulNoOverflowExpr
-import io.ksmt.expr.rewrite.simplify.rewriteBvMulNoUnderflowExpr
 import io.ksmt.expr.rewrite.simplify.simplifyBvRotateLeftExpr
 import io.ksmt.expr.rewrite.simplify.simplifyBvRotateRightExpr
 import io.ksmt.solver.KSolverUnsupportedFeatureException
@@ -183,8 +183,6 @@ import io.ksmt.sort.KFpSort
 import io.ksmt.sort.KRealSort
 import io.ksmt.sort.KSort
 import io.ksmt.sort.KUninterpretedSort
-import io.ksmt.utils.powerOfTwo
-import java.math.BigInteger
 
 @Suppress("LargeClass")
 class KCvc5ExprInternalizer(
@@ -580,26 +578,13 @@ class KCvc5ExprInternalizer(
         }
     }
 
-    // custom implementation
-    @Suppress("MagicNumber")
     override fun transform(expr: KBv2IntExpr) = with(expr) {
         transform(value) { value: Term ->
-            // by default, it is unsigned in cvc5
-            val intTerm = tm.mkTerm(Kind.BITVECTOR_TO_NAT, value)
-
-            if (isSigned) {
-                val size = this.value.sort.sizeBits.toInt()
-                val modulo = powerOfTwo(size.toUInt())
-                val maxInt = (powerOfTwo((size - 1).toUInt())) - BigInteger.ONE
-
-                val moduloTerm = tm.builder { mkInteger(modulo.toString(10)) }
-                val maxIntTerm = tm.builder { mkInteger(maxInt.toString(10)) }
-
-                val gtTerm = tm.mkTerm(Kind.GT, intTerm, maxIntTerm)
-                val subTerm = tm.mkTerm(Kind.SUB, intTerm, moduloTerm)
-
-                tm.mkTerm(Kind.ITE, gtTerm, subTerm, intTerm)
-            } else intTerm
+            if (expr.isSigned) {
+                tm.mkTerm(Kind.BITVECTOR_SBV_TO_INT, value)
+            } else {
+                tm.mkTerm(Kind.BITVECTOR_UBV_TO_INT, value)
+            }
         }
     }
 

ksmt-cvc5/ksmt-cvc5-native/build.gradle.kts

@@ -29,7 +29,7 @@ val cvc5Binaries = mapOf(
 
 cvc5Binaries.keys.forEach { it.compileClasspath = compileConfig }
 
-val cvc5Version = "1.2.0"
+val cvc5Version = "1.3.0"
 
 dependencies {
     compileConfig(project(":ksmt-cvc5:ksmt-cvc5-core"))

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

@@ -9,25 +9,18 @@ import io.ksmt.decl.KDecl
 import io.ksmt.decl.KFuncDecl
 import io.ksmt.expr.KExpr
 import io.ksmt.expr.KUninterpretedSortValue
+import io.ksmt.solver.KModel
 import io.ksmt.solver.model.KFuncInterp
 import io.ksmt.solver.model.KFuncInterpEntryVarsFree
 import io.ksmt.solver.model.KFuncInterpVarsFree
-import io.ksmt.solver.KModel
 import io.ksmt.solver.model.KModelEvaluator
 import io.ksmt.solver.model.KModelImpl
-import io.ksmt.sort.KArray2Sort
-import io.ksmt.sort.KArray3Sort
-import io.ksmt.sort.KArrayNSort
-import io.ksmt.sort.KArraySort
 import io.ksmt.sort.KArraySortBase
 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
 import io.ksmt.utils.uncheckedCast
 
@@ -46,35 +39,44 @@ class KYicesModel(
         model.collectDefinedTerms().mapTo(hashSetOf()) { converter.convertDecl(it) }
     }
 
-    override val uninterpretedSorts: Set<KUninterpretedSort> by lazy {
-        uninterpretedSortDependencies.keys
-    }
+    private val uninterpretedSortValueIndex by lazy { hashMapOf<Pair<Int, Int>, Int>() }
 
-    private val uninterpretedSortDependencies: Map<KUninterpretedSort, Set<KDecl<*>>> by lazy {
-        val sortsWithDependencies = hashMapOf<KUninterpretedSort, MutableSet<KDecl<*>>>()
-        val sortCollector = UninterpretedSortCollector(sortsWithDependencies)
-        declarations.forEach { sortCollector.collect(it) }
-        sortsWithDependencies
-    }
+    private fun uninterpretedSortValueIdx(valueId: Int, sortId: Int): Int =
+        uninterpretedSortValueIndex.getOrPut(valueId to sortId) {
+            yicesCtx.convertUninterpretedSortValueIndex(valueId)
+        }
 
-    private val uninterpretedSortUniverse =
-        hashMapOf<KUninterpretedSort, Set<KUninterpretedSortValue>>()
+    private val uninterpretedSortUniverse: Map<KUninterpretedSort, Set<KUninterpretedSortValue>> by lazy {
+        val values = model.uninterpretedSortValues()
 
-    private val knownUninterpretedSortValues =
-        hashMapOf<KUninterpretedSort, MutableMap<Int, KUninterpretedSortValue>>()
+        val sortValues = hashMapOf<YicesSort, MutableSet<Int>>()
+        for (value in values) {
+            val (valueId, internalizedSort) = model.scalarValue(value)
+            val valueIdx = uninterpretedSortValueIdx(valueId, internalizedSort)
+            sortValues.getOrPut(internalizedSort, ::hashSetOf).add(valueIdx)
+        }
 
-    private val interpretations = hashMapOf<KDecl<*>, KFuncInterp<*>>()
-    private val funcInterpretationsToDo = arrayListOf<Pair<YVal, KFuncDecl<*>>>()
+        val result = hashMapOf<KUninterpretedSort, Set<KUninterpretedSortValue>>()
+        for ((internalizedSort, valueIndices) in sortValues) {
+            val sort = converter.convertSort(internalizedSort)
+            check(sort is KUninterpretedSort) { "Unexpected sort with uninterpreted value: $sort" }
+            val sortUniverse = valueIndices.mapTo(hashSetOf()) {
+                ctx.mkUninterpretedSortValue(sort, it)
+            }
+            result[sort] = sortUniverse
+        }
 
-    override fun uninterpretedSortUniverse(
-        sort: KUninterpretedSort
-    ): Set<KUninterpretedSortValue>? = uninterpretedSortUniverse.getOrPut(sort) {
-        val sortDependencies = uninterpretedSortDependencies[sort] ?: return null
+        result
+    }
 
-        sortDependencies.forEach { interpretation(it) }
+    override val uninterpretedSorts: Set<KUninterpretedSort>
+        get() = uninterpretedSortUniverse.keys
 
-        knownUninterpretedSortValues[sort]?.values?.toHashSet() ?: hashSetOf()
-    }
+    private val interpretations = hashMapOf<KDecl<*>, KFuncInterp<*>>()
+    private val funcInterpretationsToDo = arrayListOf<Pair<YVal, KFuncDecl<*>>>()
+
+    override fun uninterpretedSortUniverse(sort: KUninterpretedSort): Set<KUninterpretedSortValue>? =
+        uninterpretedSortUniverse[sort]
 
     private val evaluatorWithModelCompletion by lazy { KModelEvaluator(ctx, this, isComplete = true) }
     private val evaluatorWithoutModelCompletion by lazy { KModelEvaluator(ctx, this, isComplete = false) }
@@ -93,12 +95,9 @@ class KYicesModel(
             is KRealSort -> mkRealNum(model.bigRationalValue(yval))
             is KIntSort -> mkIntNum(model.bigRationalValue(yval))
             is KUninterpretedSort -> {
-                val uninterpretedSortValueId = model.scalarValue(yval)[0]
-                val sortValues = knownUninterpretedSortValues.getOrPut(sort) { hashMapOf() }
-                sortValues.getOrPut(uninterpretedSortValueId) {
-                    val valueIndex = yicesCtx.convertUninterpretedSortValueIndex(uninterpretedSortValueId)
-                    mkUninterpretedSortValue(sort, valueIndex)
-                }
+                val (uninterpretedSortValueId, sortTypeId) = model.scalarValue(yval)
+                val valueIndex = uninterpretedSortValueIdx(uninterpretedSortValueId, sortTypeId)
+                mkUninterpretedSortValue(sort, valueIndex)
             }
             is KArraySortBase<*> -> {
                 val funcDecl = ctx.mkFreshFuncDecl("array", sort.range, sort.domainSorts)
@@ -184,52 +183,4 @@ class KYicesModel(
         nativeModel?.close()
         nativeModel = null
     }
-
-    private class UninterpretedSortCollector(
-        private val sorts: MutableMap<KUninterpretedSort, MutableSet<KDecl<*>>>
-    ) : KSortVisitor<Unit> {
-        private lateinit var currentDecl: KDecl<*>
-
-        fun collect(decl: KDecl<*>) {
-            currentDecl = decl
-
-            decl.sort.accept(this)
-            decl.argSorts.forEach { it.accept(this) }
-        }
-
-        override fun <D : KSort, R : KSort> visit(sort: KArraySort<D, R>) {
-            sort.range.accept(this)
-            sort.domain.accept(this)
-        }
-
-        override fun <D0 : KSort, D1 : KSort, R : KSort> visit(sort: KArray2Sort<D0, D1, R>) {
-            sort.range.accept(this)
-            sort.domain0.accept(this)
-            sort.domain1.accept(this)
-        }
-
-        override fun <D0 : KSort, D1 : KSort, D2 : KSort, R : KSort> visit(sort: KArray3Sort<D0, D1, D2, R>) {
-            sort.range.accept(this)
-            sort.domain0.accept(this)
-            sort.domain1.accept(this)
-            sort.domain2.accept(this)
-        }
-
-        override fun <R : KSort> visit(sort: KArrayNSort<R>) {
-            sort.range.accept(this)
-            sort.domainSorts.forEach { it.accept(this) }
-        }
-
-        override fun visit(sort: KUninterpretedSort) {
-            val sortDependencies = sorts.getOrPut(sort) { hashSetOf() }
-            sortDependencies.add(currentDecl)
-        }
-
-        override fun visit(sort: KBoolSort) = Unit
-        override fun visit(sort: KIntSort) = Unit
-        override fun visit(sort: KRealSort) = Unit
-        override fun <S : KBvSort> visit(sort: S) = Unit
-        override fun <S : KFpSort> visit(sort: S) = Unit
-        override fun visit(sort: KFpRoundingModeSort) = Unit
-    }
 }