Bring z3 back

build.gradle.kts

@@ -134,7 +134,6 @@ 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

@@ -40,7 +40,8 @@ junit4PlatformVersion=1.9.0
 # NOTE: Mockito versions 5+ are not compatible with Java 8: https://www.davidvlijmincx.com/posts/upgrade-to-mockito-5
 mockitoVersion=4.11.0
 mockitoInlineVersion=4.11.0
-ksmtVersion=0.4.3
+z3Version=4.8.9.1
+z3JavaApiVersion=4.8.9
 sootVersion=4.2.1
 kotlinVersion=1.8.0
 log4j2Version=2.13.3
@@ -75,6 +76,7 @@ asmVersion=9.2
 testNgVersion=7.6.0
 kamlVersion=0.51.0
 jacksonVersion=2.12.3
+javasmtSolverZ3Version=4.8.9-sosy1
 kotlinxSerializationVersion=1.5.0
 slf4jVersion=1.7.36
 eclipseAetherVersion=1.1.0

utbot-framework/build.gradle

@@ -7,11 +7,17 @@ configurations {
     fetchInstrumentationJar
 }
 
-dependencies {
+repositories {
+    flatDir {
+        dirs 'dist'
+    }
+}
+
+configurations {
+    z3native
+}
 
-//    api project(':utbot-java-fuzzing')
-//    api project(':utbot-instrumentation')
-//    api project(':utbot-summary')
+dependencies {
     api project(':utbot-framework-api')
     api project(':utbot-rd')
 
@@ -26,6 +32,7 @@ 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: 'org.jetbrains.kotlinx', name: 'kotlinx-serialization-cbor', version: kotlinxSerializationVersion
     implementation group: 'com.github.curious-odd-man', name: 'rgxgen', version: rgxgenVersion
     implementation group: 'org.apache.logging.log4j', name: 'log4j-slf4j-impl', version: log4j2Version
@@ -40,25 +47,15 @@ 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'
 
-    implementation group: 'com.github.UnitTestBot.ksmt', name: 'ksmt-core', version: ksmtVersion
-    implementation group: 'com.github.UnitTestBot.ksmt', name: 'ksmt-z3', version: ksmtVersion
-
-//    fetchInstrumentationJar project(path: ':utbot-instrumentation', configuration: 'instrumentationArchive')
-
-//    implementation project(':utbot-spring-commons-api')
-//    implementation project(':utbot-spring-analyzer')
+    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'
 
-//    if (projectType == springEdition || projectType==ultimateEdition) {
-//        fetchSpringAnalyzerJar project(path: ':utbot-spring-analyzer', configuration: 'springAnalyzerJar')
-//    }
 }
 
 processResources {
-    from(configurations.fetchInstrumentationJar) {
-        into "lib"
-    }
-
-    from(configurations.fetchSpringAnalyzerJar) {
-        into "lib"
+    configurations.z3native.resolvedConfiguration.resolvedArtifacts.each { artifact ->
+        from(zipTree(artifact.getFile())) {
+            into "lib/x64"
+        }
     }
 }

utbot-framework/src/main/kotlin/org/utbot/engine/pc/UtExpression.kt

@@ -978,7 +978,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 {
@@ -996,6 +996,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

utbot-framework/src/main/kotlin/org/utbot/engine/pc/UtSolverStatus.kt

@@ -47,7 +47,7 @@ class UtSolverStatusSAT(
 
     private val evaluator: Z3EvaluatorVisitor = translator.evaluator(model)
 
-    fun eval(expression: UtExpression): Expr<*> = evaluator.eval(expression)
+    fun eval(expression: UtExpression): Expr = evaluator.eval(expression)
 
     fun concreteAddr(expression: UtAddrExpression): Address = eval(expression).intValue()
 
@@ -65,7 +65,7 @@ class UtSolverStatusSAT(
      * - val arrayInterpretationFuncDecl: FuncDecl = mfd.parameters[[0]].funcDecl
      * - val interpretation: FuncInterp = z3Solver.model.getFuncInterp(arrayInterpretationFuncDecl)
      */
-    internal fun evalArrayDescriptor(mval: Expr<*>, unsigned: Boolean, filter: (Int) -> Boolean): ArrayDescriptor {
+    internal fun evalArrayDescriptor(mval: Expr, unsigned: Boolean, filter: (Int) -> Boolean): ArrayDescriptor {
         var next = mval
         val stores = mutableMapOf<Int, Any>()
         var const: Any? = null
@@ -79,7 +79,7 @@ class UtSolverStatusSAT(
                     next = next.args[0]
                 }
                 Z3_OP_UNINTERPRETED -> next = model.eval(next)
-                Z3_OP_CONST_ARRAY -> const = if (next.args[0] is ArrayExpr<*, *>) {
+                Z3_OP_CONST_ARRAY -> const = if (next.args[0] is ArrayExpr) {
                     // if we have an array as const value, create a corresponding descriptor for it
                     evalArrayDescriptor(next.args[0], unsigned, filter)
                 } else {

utbot-framework/src/main/kotlin/org/utbot/engine/pc/Z3EvaluatorVisitor.kt

@@ -20,38 +20,38 @@ import soot.ByteType
 import soot.CharType
 
 class Z3EvaluatorVisitor(private val model: Model, private val translator: Z3TranslatorVisitor) :
-    UtExpressionVisitor<Expr<*>> by translator {
+    UtExpressionVisitor<Expr> by translator {
 
     // stack of indexes that are visited in expression in derivation tree.
     // For example, we call eval(select(select(a, i), j)
     // On visiting term a, the stack will be equals to [i, j]
-    private val selectIndexStack = mutableListOf<Expr<*>>()
+    private val selectIndexStack = mutableListOf<Expr>()
 
-    private inline fun withPushedSelectIndex(index: UtExpression, block: () -> Expr<*>): Expr<*> {
+    private inline fun withPushedSelectIndex(index: UtExpression, block: () -> Expr): Expr {
         selectIndexStack += eval(index)
         return block().also {
             selectIndexStack.removeLast()
         }
     }
 
-    private inline fun withPoppedSelectIndex(block: () -> Expr<*>): Expr<*> {
+    private inline fun withPoppedSelectIndex(block: () -> Expr): Expr {
         val lastIndex = selectIndexStack.removeLast()
         return block().also {
             selectIndexStack += lastIndex
         }
     }
 
-    private fun foldSelectsFromStack(expr: Expr<*>): Expr<*> {
+    private fun foldSelectsFromStack(expr: Expr): Expr {
         var result = expr
         var i = selectIndexStack.size
-        while (i > 0 && result.sort is ArraySort<*, *>) {
-            result = translator.withContext { mkSelect(result as ArrayExpr<*, *>, selectIndexStack[--i].cast()) }
+        while (i > 0 && result.sort is ArraySort) {
+            result = translator.withContext { mkSelect(result as ArrayExpr, selectIndexStack[--i]) }
         }
         return result
     }
 
 
-    fun eval(expr: UtExpression): Expr<*> {
+    fun eval(expr: UtExpression): Expr {
         val translated = if (expr.sort is UtArraySort) {
             translator.lookUpCache(expr)?.let { foldSelectsFromStack(it) } ?: expr.accept(this)
         } else {
@@ -60,14 +60,14 @@ class Z3EvaluatorVisitor(private val model: Model, private val translator: Z3Tra
         return model.eval(translated)
     }
 
-    override fun visit(expr: UtArraySelectExpression): Expr<*> = expr.run {
+    override fun visit(expr: UtArraySelectExpression): Expr = expr.run {
         // translate arrayExpression here will return evaluation of arrayExpression.select(index)
         withPushedSelectIndex(index) {
             eval(arrayExpression)
         }
     }
 
-    override fun visit(expr: UtConstArrayExpression): Expr<*> = expr.run {
+    override fun visit(expr: UtConstArrayExpression): Expr = expr.run {
         // expr.select(index) = constValue for any index
         if (selectIndexStack.size == 0) {
             translator.withContext { mkConstArray(sort.indexSort.toZ3Sort(this), eval(constValue)) }
@@ -78,17 +78,17 @@ class Z3EvaluatorVisitor(private val model: Model, private val translator: Z3Tra
         }
     }
 
-    override fun visit(expr: UtMkArrayExpression): Expr<*> =
+    override fun visit(expr: UtMkArrayExpression): Expr =
     // mkArray expression can have more than one dimension
     // so for such case select(select(mkArray(...), i), j))
         // indices i and j are currently in the stack and we need to fold them.
         foldSelectsFromStack(translator.translate(expr))
 
-    override fun visit(expr: UtArrayMultiStoreExpression): Expr<*> = expr.run {
+    override fun visit(expr: UtArrayMultiStoreExpression): Expr = expr.run {
         val lastIndex = selectIndexStack.lastOrNull()
             ?: return translator.withContext {
-                stores.fold(translator.translate(initial) as ArrayExpr<*, *>) { acc, (index, item) ->
-                    mkStore(acc, eval(index).cast(), eval(item).cast())
+                stores.fold(translator.translate(initial) as ArrayExpr) { acc, (index, item) ->
+                    mkStore(acc, eval(index), eval(item))
                 }
             }
         for (store in stores.asReversed()) {
@@ -99,12 +99,12 @@ class Z3EvaluatorVisitor(private val model: Model, private val translator: Z3Tra
         eval(initial)
     }
 
-    override fun visit(expr: UtMkTermArrayExpression): Expr<*> = expr.run {
+    override fun visit(expr: UtMkTermArrayExpression): Expr = expr.run {
         // should we make eval(mkTerm) always true??
         translator.translate(UtTrue)
     }
 
-    override fun visit(expr: UtArrayInsert): Expr<*> = expr.run {
+    override fun visit(expr: UtArrayInsert): Expr = expr.run {
         val lastIndex = selectIndexStack.last().intValue()
         val index = eval(index.expr).intValue()
         when {
@@ -114,7 +114,7 @@ class Z3EvaluatorVisitor(private val model: Model, private val translator: Z3Tra
         }
     }
 
-    override fun visit(expr: UtArrayInsertRange): Expr<*> = expr.run {
+    override fun visit(expr: UtArrayInsertRange): Expr = expr.run {
         val lastIndex = selectIndexStack.last().intValue()
         val index = eval(index.expr).intValue()
         val length = eval(length.expr).intValue()
@@ -128,7 +128,7 @@ class Z3EvaluatorVisitor(private val model: Model, private val translator: Z3Tra
         }
     }
 
-    override fun visit(expr: UtArrayRemove): Expr<*> = expr.run {
+    override fun visit(expr: UtArrayRemove): Expr = expr.run {
         val lastIndex = selectIndexStack.last().intValue()
         val index = eval(index.expr).intValue()
         if (lastIndex < index) {
@@ -138,7 +138,7 @@ class Z3EvaluatorVisitor(private val model: Model, private val translator: Z3Tra
         }
     }
 
-    override fun visit(expr: UtArrayRemoveRange): Expr<*> = expr.run {
+    override fun visit(expr: UtArrayRemoveRange): Expr = expr.run {
         val lastIndex = selectIndexStack.last().intValue()
         val index = eval(index.expr).intValue()
         if (lastIndex < index) {
@@ -149,7 +149,7 @@ class Z3EvaluatorVisitor(private val model: Model, private val translator: Z3Tra
         }
     }
 
-    override fun visit(expr: UtArraySetRange): Expr<*> = expr.run {
+    override fun visit(expr: UtArraySetRange): Expr = expr.run {
         val lastIndex = selectIndexStack.last().intValue()
         val index = eval(index.expr).intValue()
         val length = eval(length.expr).intValue()
@@ -162,95 +162,95 @@ class Z3EvaluatorVisitor(private val model: Model, private val translator: Z3Tra
         }
     }
 
-    override fun visit(expr: UtArrayShiftIndexes): Expr<*> = expr.run {
+    override fun visit(expr: UtArrayShiftIndexes): Expr = expr.run {
         val lastIndex = selectIndexStack.last().intValue()
         val offset = eval(offset.expr).intValue()
         eval(arrayExpression.select(mkInt(lastIndex - offset)))
     }
 
-    override fun visit(expr: UtAddrExpression): Expr<*> = eval(expr.internal)
+    override fun visit(expr: UtAddrExpression): Expr = eval(expr.internal)
 
-    override fun visit(expr: UtOpExpression): Expr<*> = expr.run {
+    override fun visit(expr: UtOpExpression): Expr = expr.run {
         val leftResolve = eval(left.expr).z3Variable(left.type)
         val rightResolve = eval(right.expr).z3Variable(right.type)
         translator.withContext {
             operator.delegate(this, leftResolve, rightResolve)
         }
     }
 
-    override fun visit(expr: UtEqExpression): Expr<*> = expr.run {
+    override fun visit(expr: UtEqExpression): Expr = expr.run {
         translator.withContext { mkEq(eval(left), eval(right)) }
     }
 
-    override fun visit(expr: NotBoolExpression): Expr<*> =
+    override fun visit(expr: NotBoolExpression): Expr =
         translator.withContext { mkNot(eval(expr.expr) as BoolExpr) }
 
-    override fun visit(expr: UtOrBoolExpression): Expr<*> = expr.run {
+    override fun visit(expr: UtOrBoolExpression): Expr = expr.run {
         translator.withContext {
             mkOr(*expr.exprs.map { eval(it) as BoolExpr }.toTypedArray())
         }
     }
 
-    override fun visit(expr: UtAndBoolExpression): Expr<*> = expr.run {
+    override fun visit(expr: UtAndBoolExpression): Expr = expr.run {
         translator.withContext {
             mkAnd(*expr.exprs.map { eval(it) as BoolExpr }.toTypedArray())
         }
     }
 
-    override fun visit(expr: UtAddNoOverflowExpression): Expr<*> = expr.run {
+    override fun visit(expr: UtAddNoOverflowExpression): Expr = expr.run {
         translator.withContext {
             mkBVAddNoOverflow(eval(expr.left) as BitVecExpr, eval(expr.right) as BitVecExpr, true)
         }
     }
 
-    override fun visit(expr: UtSubNoOverflowExpression): Expr<*> = expr.run {
+    override fun visit(expr: UtSubNoOverflowExpression): Expr = expr.run {
         translator.withContext {
             // For some reason mkBVSubNoOverflow does not take "signed" as an argument, yet still works for signed integers
             mkBVSubNoOverflow(eval(expr.left) as BitVecExpr, eval(expr.right) as BitVecExpr) //, true)
         }
     }
 
-    override fun visit(expr: UtMulNoOverflowExpression): Expr<*> = expr.run {
+    override fun visit(expr: UtMulNoOverflowExpression): Expr = expr.run {
         translator.withContext {
             mkBVMulNoOverflow(eval(expr.left) as BitVecExpr, eval(expr.right) as BitVecExpr , true)
         }
     }
 
-    override fun visit(expr: UtNegExpression): Expr<*> = expr.run {
+    override fun visit(expr: UtNegExpression): Expr = expr.run {
         translator.withContext {
             negate(this, eval(variable.expr).z3Variable(variable.type))
         }
     }
 
-    override fun visit(expr: UtBvNotExpression): Expr<*> = expr.run {
+    override fun visit(expr: UtBvNotExpression): Expr = expr.run {
         translator.withContext {
             mkBVNot(eval(variable.expr) as BitVecExpr)
         }
     }
 
-    override fun visit(expr: UtCastExpression): Expr<*> = expr.run {
+    override fun visit(expr: UtCastExpression): Expr = expr.run {
         val z3var = eval(variable.expr).z3Variable(variable.type)
         translator.withContext { convertVar(z3var, type).expr }
     }
 
-    override fun visit(expr: UtBoolOpExpression): Expr<*> = expr.run {
+    override fun visit(expr: UtBoolOpExpression): Expr = expr.run {
         val leftResolve = eval(left.expr).z3Variable(left.type)
         val rightResolve = eval(right.expr).z3Variable(right.type)
         translator.withContext {
             operator.delegate(this, leftResolve, rightResolve)
         }
     }
 
-    override fun visit(expr: UtIsExpression): Expr<*> = translator.translate(expr)
+    override fun visit(expr: UtIsExpression): Expr = translator.translate(expr)
 
-    override fun visit(expr: UtInstanceOfExpression): Expr<*> =
+    override fun visit(expr: UtInstanceOfExpression): Expr =
         expr.run { eval(expr.constraint) }
 
-    override fun visit(expr: UtIteExpression): Expr<*> = expr.run {
+    override fun visit(expr: UtIteExpression): Expr = expr.run {
         if (eval(condition).value() as Boolean) eval(thenExpr) else eval(elseExpr)
     }
 
-    override fun visit(expr: UtArrayApplyForAll): Expr<*> = expr.run {
+    override fun visit(expr: UtArrayApplyForAll): Expr = expr.run {
         eval(expr.arrayExpression.select(mkInt(selectIndexStack.last().intValue())))
     }
 }