Replace z3 jar files with KSMT dependency

Author: CaelmBleidd

build.gradle.kts

@@ -89,6 +89,7 @@ allprojects {
 
     repositories {
         mavenCentral()
+        maven("https://jitpack.io")
         maven("https://s01.oss.sonatype.org/content/repositories/orgunittestbotsoot-1004/")
         maven("https://plugins.gradle.org/m2")
         maven("https://www.jetbrains.com/intellij-repository/releases")

gradle.properties

@@ -28,8 +28,7 @@ junit5Version=5.8.0-RC1
 junit4Version=4.13.2
 junit4PlatformVersion=1.9.0
 mockitoVersion=3.5.13
-z3Version=4.8.9.1
-z3JavaApiVersion=4.8.9
+ksmtVersion=0.4.2
 sootVersion=4.4.0-FORK-2
 kotlinVersion=1.7.20
 log4j2Version=2.13.3
@@ -65,7 +64,6 @@ testNgVersion=7.6.0
 mockitoInlineVersion=4.0.0
 kamlVersion = 0.51.0
 jacksonVersion = 2.12.3
-javasmtSolverZ3Version=4.8.9-sosy1
 slf4jVersion=1.7.36
 eclipseAetherVersion=1.1.0
 mavenWagonVersion=3.5.1

utbot-framework-test/build.gradle

@@ -10,16 +10,6 @@ tasks.withType(JavaCompile) {
     targetCompatibility = JavaVersion.VERSION_11
 }
 
-repositories {
-    flatDir {
-        dirs 'dist'
-    }
-}
-
-configurations {
-    z3native
-}
-
 dependencies {
     api project(':utbot-framework-api')
     testImplementation project(':utbot-testing')
@@ -39,7 +29,6 @@ dependencies {
 
     implementation group: 'com.charleskorn.kaml', name: 'kaml', version: kamlVersion
     implementation group: 'com.fasterxml.jackson.module', name: 'jackson-module-kotlin', version: jacksonVersion
-    implementation group: 'org.sosy-lab', name: 'javasmt-solver-z3', version: javasmtSolverZ3Version
     implementation group: 'com.github.curious-odd-man', name: 'rgxgen', version: rgxgenVersion
     implementation group: 'org.apache.logging.log4j', name: 'log4j-slf4j-impl', version: log4j2Version
     implementation group: 'io.github.microutils', name: 'kotlin-logging', version: kotlinLoggingVersion
@@ -66,12 +55,10 @@ dependencies {
     testImplementation group: 'org.mockito', name: 'mockito-inline', version: mockitoInlineVersion
     testImplementation group: 'org.apache.logging.log4j', name: 'log4j-core', version: log4j2Version
 
-    z3native group: 'com.microsoft.z3', name: 'z3-native-win64', version: z3Version, ext: 'zip'
-    z3native group: 'com.microsoft.z3', name: 'z3-native-linux64', version: z3Version, ext: 'zip'
-    z3native group: 'com.microsoft.z3', name: 'z3-native-osx', version: z3Version, ext: 'zip'
+    implementation group: 'com.github.UnitTestBot.ksmt', name: 'ksmt-core', version: ksmtVersion
+    implementation group: 'com.github.UnitTestBot.ksmt', name: 'ksmt-z3', version: ksmtVersion
 }
 
-
 test {
 
     minHeapSize = "128m"

utbot-framework-test/src/test/kotlin/org/utbot/framework/z3/extension/Z3ExtensionForTests.kt

@@ -5,19 +5,19 @@ package com.microsoft.z3
 import kotlin.reflect.KProperty
 
 
-operator fun ArithExpr.plus(other: ArithExpr): ArithExpr = context.mkAdd(this, other)
-operator fun ArithExpr.plus(other: Int): ArithExpr = this + context.mkInt(other)
+operator fun ArithExpr<*>.plus(other: ArithExpr<*>): ArithExpr<*> = context.mkAdd(this, other)
+operator fun ArithExpr<*>.plus(other: Int): ArithExpr<*> = this + context.mkInt(other)
 
-operator fun ArithExpr.minus(other: ArithExpr): ArithExpr = context.mkSub(this, other)
-operator fun ArithExpr.minus(other: Int): ArithExpr = this - context.mkInt(other)
+operator fun ArithExpr<*>.minus(other: ArithExpr<*>): ArithExpr<*> = context.mkSub(this, other)
+operator fun ArithExpr<*>.minus(other: Int): ArithExpr<*> = this - context.mkInt(other)
 
-operator fun ArithExpr.times(other: ArithExpr): ArithExpr = context.mkMul(this, other)
-operator fun ArithExpr.times(other: Int): ArithExpr = this * context.mkInt(other)
+operator fun ArithExpr<*>.times(other: ArithExpr<*>): ArithExpr<*> = context.mkMul(this, other)
+operator fun ArithExpr<*>.times(other: Int): ArithExpr<*> = this * context.mkInt(other)
 
-infix fun Expr.`=`(other: Int): BoolExpr = this eq context.mkInt(other)
-infix fun Expr.`=`(other: Expr): BoolExpr = this eq other
-infix fun Expr.eq(other: Expr): BoolExpr = context.mkEq(this, other)
-infix fun Expr.`!=`(other: Expr): BoolExpr = context.mkNot(this `=` other)
+infix fun Expr<*>.`=`(other: Int): BoolExpr = this eq context.mkInt(other)
+infix fun Expr<*>.`=`(other: Expr<*>): BoolExpr = this eq other
+infix fun Expr<*>.eq(other: Expr<*>): BoolExpr = context.mkEq(this, other)
+infix fun Expr<*>.`!=`(other: Expr<*>): BoolExpr = context.mkNot(this `=` other)
 operator fun BoolExpr.not(): BoolExpr = context.mkNot(this)
 
 infix fun BoolExpr.`⇒`(other: BoolExpr): BoolExpr = this implies other
@@ -27,20 +27,24 @@ infix fun BoolExpr.implies(other: BoolExpr): BoolExpr = context.mkImplies(this,
 infix fun BoolExpr.and(other: BoolExpr): BoolExpr = context.mkAnd(this, other)
 infix fun BoolExpr.or(other: BoolExpr): BoolExpr = context.mkOr(this, other)
 
-infix fun ArithExpr.gt(other: ArithExpr): BoolExpr = context.mkGt(this, other)
-infix fun ArithExpr.gt(other: Int): BoolExpr = context.mkGt(this, context.mkInt(other))
+infix fun ArithExpr<*>.gt(other: ArithExpr<*>): BoolExpr = context.mkGt(this, other)
+infix fun ArithExpr<*>.gt(other: Int): BoolExpr = context.mkGt(this, context.mkInt(other))
 
-infix fun ArithExpr.`=`(other: Int): BoolExpr = context.mkEq(this, context.mkInt(other))
+infix fun ArithExpr<*>.`=`(other: Int): BoolExpr = context.mkEq(this, context.mkInt(other))
 
-operator fun ArrayExpr.get(index: IntExpr): Expr = context.mkSelect(this, index)
-operator fun ArrayExpr.get(index: Int): Expr = this[context.mkInt(index)]
-fun ArrayExpr.set(index: IntExpr, value: Expr): ArrayExpr = context.mkStore(this, index, value)
-fun ArrayExpr.set(index: Int, value: Expr): ArrayExpr = set(context.mkInt(index), value)
+operator fun  ArrayExpr<*, *>.get(index: IntExpr): Expr<*> = context.mkSelect(this, index.cast())
+operator fun  ArrayExpr<*, *>.get(index: Int): Expr<*> = this[context.mkInt(index)]
+fun  ArrayExpr<*, *>.set(index: IntExpr, value: Expr<*>):  ArrayExpr<*, *> = context.mkStore(this, index.cast(), value.cast())
+fun  ArrayExpr<*, *>.set(index: Int, value: Expr<*>):  ArrayExpr<*, *> = set(context.mkInt(index), value)
 
-operator fun SeqExpr.plus(other: SeqExpr): SeqExpr = context.mkConcat(this, other)
-operator fun SeqExpr.plus(other: String): SeqExpr = context.mkConcat(context.mkString(other))
+operator fun SeqExpr<*>.plus(other: SeqExpr<*>): SeqExpr<*> = context.mkConcat(this, other.cast())
+operator fun SeqExpr<*>.plus(other: String): SeqExpr<*> = context.mkConcat(context.mkString(other))
 
-infix fun SeqExpr.`=`(other: String): BoolExpr = context.mkEq(this, context.mkString(other))
+@Suppress("UNCHECKED_CAST")
+fun <T : Sort, R : Sort> Expr<T>.cast(): Expr<R> = this as Expr<R>
+
+
+infix fun SeqExpr<*>.`=`(other: String): BoolExpr = context.mkEq(this, context.mkString(other))
 
 class Const<T>(private val ctx: Context, val produce: (Context, name: String) -> T) {
     operator fun getValue(thisRef: Nothing?, property: KProperty<*>): T = produce(ctx, property.name)
@@ -49,12 +53,12 @@ class Const<T>(private val ctx: Context, val produce: (Context, name: String) ->
 fun Context.declareInt() = Const(this) { ctx, name -> ctx.mkIntConst(name) }
 fun Context.declareBool() = Const(this) { ctx, name -> ctx.mkBoolConst(name) }
 fun Context.declareReal() = Const(this) { ctx, name -> ctx.mkRealConst(name) }
-fun Context.declareString() = Const(this) { ctx, name -> ctx.mkConst(name, stringSort) as SeqExpr }
-fun Context.declareList(sort: ListSort) = Const(this) { ctx, name -> ctx.mkConst(name, sort) }
+fun Context.declareString() = Const(this) { ctx, name -> ctx.mkConst(name, stringSort) as SeqExpr<*> }
+fun Context.declareList(sort: ListSort<*>) = Const(this) { ctx, name -> ctx.mkConst(name, sort) }
 fun Context.declareIntArray() = Const(this) { ctx, name -> ctx.mkArrayConst(name, intSort, intSort) }
 
 
-operator fun FuncDecl.invoke(vararg expr: Expr): Expr = context.mkApp(this, *expr)
+operator fun FuncDecl<*>.invoke(vararg expr: Expr<*>): Expr<*> = context.mkApp(this, *expr)
 
-fun Model.eval(expr: Expr): Expr = this.eval(expr, true)
-fun Model.eval(vararg exprs: Expr): List<Expr> = exprs.map { this.eval(it, true) }
+fun Model.eval(expr: Expr<*>): Expr<*> = this.eval(expr, true)
+fun Model.eval(vararg exprs: Expr<*>): List<Expr<*>> = exprs.map { this.eval(it, true) }

utbot-framework-test/src/test/kotlin/org/utbot/framework/z3/extension/Z3ExtensionTest.kt

@@ -99,8 +99,8 @@ class Z3ExtensionTest : Z3Initializer() {
 
             val (aVal, bVal, cVal) = solver.model
                 .eval(a, b, c)
-                .filterIsInstance<SeqExpr>()
-                .map(SeqExpr::getString)
+                .filterIsInstance<SeqExpr<*>>()
+                .map(SeqExpr<*>::getString)
                 .also { list -> assertEquals(3, list.size) }
 
             assertEquals("abcd", "$aVal$bVal")

utbot-framework/build.gradle

@@ -1,13 +1,3 @@
-repositories {
-    flatDir {
-        dirs 'dist'
-    }
-}
-
-configurations {
-    z3native
-}
-
 dependencies {
 
     api project(':utbot-fuzzers')
@@ -29,7 +19,6 @@ dependencies {
 
     implementation group: 'com.charleskorn.kaml', name: 'kaml', version: kamlVersion
     implementation group: 'com.fasterxml.jackson.module', name: 'jackson-module-kotlin', version: jacksonVersion
-    implementation group: 'org.sosy-lab', name: 'javasmt-solver-z3', version: javasmtSolverZ3Version
     implementation group: 'com.github.curious-odd-man', name: 'rgxgen', version: rgxgenVersion
     implementation group: 'org.apache.logging.log4j', name: 'log4j-slf4j-impl', version: log4j2Version
     implementation group: 'io.github.microutils', name: 'kotlin-logging', version: kotlinLoggingVersion
@@ -43,15 +32,6 @@ dependencies {
     implementation group: 'org.junit.jupiter', name: 'junit-jupiter-params', version: '5.8.1'
     implementation group: 'org.junit.jupiter', name: 'junit-jupiter-engine', version: '5.8.1'
 
-    z3native group: 'com.microsoft.z3', name: 'z3-native-win64', version: z3Version, ext: 'zip'
-    z3native group: 'com.microsoft.z3', name: 'z3-native-linux64', version: z3Version, ext: 'zip'
-    z3native group: 'com.microsoft.z3', name: 'z3-native-osx', version: z3Version, ext: 'zip'
-}
-
-processResources {
-    configurations.z3native.resolvedConfiguration.resolvedArtifacts.each { artifact ->
-        from(zipTree(artifact.getFile())) {
-            into "lib/x64"
-        }
-    }
+    implementation group: 'com.github.UnitTestBot.ksmt', name: 'ksmt-core', version: ksmtVersion
+    implementation group: 'com.github.UnitTestBot.ksmt', name: 'ksmt-z3', version: ksmtVersion
 }

utbot-framework/dist/z3-native-linux64-4.8.9.1.zip

@@ -932,7 +932,7 @@ data class UtMkTermArrayExpression(val array: UtArrayExpressionBase, val default
     override fun hashCode() = hashCode
 }
 
-data class Z3Variable(val type: Type, val expr: Expr) {
+data class Z3Variable(val type: Type, val expr: Expr<*>) {
     private val hashCode = Objects.hash(type, expr)
 
     override fun equals(other: Any?): Boolean {
@@ -950,6 +950,6 @@ data class Z3Variable(val type: Type, val expr: Expr) {
     override fun hashCode() = hashCode
 }
 
-fun Expr.z3Variable(type: Type) = Z3Variable(type, this)
+fun Expr<*>.z3Variable(type: Type) = Z3Variable(type, this)
 
 fun UtExpression.isInteger() = this.sort is UtBvSort