Upgrade cvc to 1.2.0 (#168)

* Upgrade cvc to 1.2.0

* Rebuild cvc

* Treat internal expressions as unsupported

* Upgrade ksmt version to 0.5.28

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.27)
+[![Maven Central](https://img.shields.io/maven-central/v/io.ksmt/ksmt-core)](https://central.sonatype.com/artifact/io.ksmt/ksmt-core/0.5.28)
 [![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.27")
+implementation("io.ksmt:ksmt-core:0.5.28")
 // z3 solver
-implementation("io.ksmt:ksmt-z3:0.5.27")
+implementation("io.ksmt:ksmt-z3:0.5.28")
 ```
 
 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.27"
+version = "0.5.28"
 
 repositories {
     mavenCentral()

docs/getting-started.md

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

examples/build.gradle.kts

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

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

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

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

@@ -300,6 +300,21 @@ open class KCvc5ExprConverter(
                 mkBvDivNoOverflowExpr(arg0, arg1)
             }
 
+            Kind.BITVECTOR_FROM_BOOLS -> expr.convertList { bits: List<KExpr<KBoolSort>> ->
+                val oneBit = mkBv(true)
+                val zeroBit = mkBv(false)
+
+                bits
+                    .map<_, KExpr<out KBvSort>> { mkIte(it, oneBit, zeroBit) }
+                    .reduce { acc, bit -> mkBvConcatExpr(acc, bit) }
+            }
+
+            Kind.BITVECTOR_BIT -> expr.convert { arg: KExpr<KBvSort> ->
+                val bitIndex = expr.bvBitIndex
+                val bitValue: KExpr<KBv1Sort> = mkBvExtractExpr(bitIndex, bitIndex, arg).uncheckedCast()
+                mkEq(bitValue, mkBv(true))
+            }
+
             // fp
             Kind.FLOATINGPOINT_FP -> {
                 expr.convert { bvSign: KExpr<KBv1Sort>, bvExponent: KExpr<KBvSort>, bvSignificand: KExpr<KBvSort> ->
@@ -414,6 +429,7 @@ open class KCvc5ExprConverter(
             Kind.SET_IS_SINGLETON,
             Kind.SET_MAP,
             Kind.SET_FILTER,
+            Kind.SET_IS_EMPTY,
             Kind.SET_FOLD -> throw KSolverUnsupportedFeatureException("currently ksmt does not support sets")
 
             Kind.RELATION_JOIN,
@@ -450,6 +466,7 @@ open class KCvc5ExprConverter(
             Kind.TABLE_PROJECT,
             Kind.TABLE_AGGREGATE,
             Kind.TABLE_JOIN,
+            Kind.RELATION_TABLE_JOIN,
             Kind.TABLE_GROUP -> throw KSolverUnsupportedFeatureException("currently ksmt does not support tables")
 
             Kind.STRING_CONCAT,
@@ -522,8 +539,10 @@ open class KCvc5ExprConverter(
 
             Kind.WITNESS -> error("no direct mapping in ksmt")
             Kind.LAST_KIND -> error("should not be here. Marks the upper-bound of this enumeration, not op kind")
-            Kind.INTERNAL_KIND -> error("should not be here. Not exposed via the API")
-            Kind.UNDEFINED_KIND -> error("should not be here. Not exposed via the API")
+
+            Kind.INTERNAL_KIND -> throw KSolverUnsupportedFeatureException("Unsupported internal expr $expr")
+
+            Kind.UNDEFINED_KIND -> error("$expr should not be here. Not exposed via the API")
             Kind.NULL_TERM,
             Kind.NULLABLE_LIFT,
             Kind.SKOLEM -> error("no support in ksmt")
@@ -972,6 +991,12 @@ open class KCvc5ExprConverter(
             return termOpArg(this, 0).integerValue.toInt()
         }
 
+    private val Term.bvBitIndex: Int
+        get() {
+            require(kind == Kind.BITVECTOR_BIT) { "Required op is ${Kind.BITVECTOR_BIT}, but was $kind" }
+            return termOpArg(this, 0).integerValue.toInt()
+        }
+
     private val toBvAllowedOps = listOf(
         Kind.INT_TO_BITVECTOR,
         Kind.FLOATINGPOINT_TO_SBV,

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

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

ksmt-cvc5/ksmt-cvc5-native/src/linux-x64/kotlin/io/ksmt/solver/cvc5/KCvc5NativeLibraryLoaderLinuxX64.kt

@@ -18,8 +18,6 @@ class KCvc5NativeLibraryLoaderLinuxX64 :
 
     companion object {
         private val libraries = listOf(
-            "libpoly.so.0.1.13",
-            "libpolyxx.so.0.1.13",
             "libcvc5.so.1",
             "libcvc5parser.so.1",
             "libcvc5jni.so",

ksmt-cvc5/ksmt-cvc5-native/src/mac-arm/kotlin/io/ksmt/solver/cvc5/KCvc5NativeLibraryLoaderMacArm.kt

@@ -15,8 +15,6 @@ class KCvc5NativeLibraryLoaderMacArm :
 
     companion object {
         private val libraries = listOf(
-            "libpoly.0.1.13",
-            "libpolyxx.0.1.13",
             "libcvc5.1",
             "libcvc5parser.1",
             "libcvc5jni",

ksmt-cvc5/ksmt-cvc5-native/src/windows-x64/kotlin/io/ksmt/solver/cvc5/KCvc5NativeLibraryLoaderWindowsX64.kt

@@ -15,8 +15,6 @@ class KCvc5NativeLibraryLoaderWindowsX64 :
 
     companion object {
         private val libraries = listOf(
-            "libpoly",
-            "libpolyxx",
             "libcvc5",
             "libcvc5parser",
             "libcvc5jni"