Remove z3 string theory from String wrapper (#1050)

* Remove Z3 string theory support

* Removed `UtNativeString`, `NativeStringWrapper`, string-related `UtExpression` subclasses

* Implemented `toString` methods for numeric wrappers in Java

* Restored temporarily disabled `testByteToString` test

* Complex `GenericExamples` string tests are disabled until symbolic part of the wrapper is enabled.

* Additional logging for `checkAllCombinations`

* Fixed array offset in UtString.concat()

* Updated compilation stage in (disabled) strings/GenericExamplesTest
  + updated string tests w.r.t. running without concrete execution

Author: dtim

utbot-analytics/src/main/kotlin/org/utbot/features/UtExpressionStructureCounter.kt

@@ -34,21 +34,6 @@ val featureIndex = listOf(
         UtBoolOpExpression::class.simpleName,
         UtIsExpression::class.simpleName,
         UtIteExpression::class.simpleName,
-        UtStringConst::class.simpleName,
-        UtConcatExpression::class.simpleName,
-        UtConvertToString::class.simpleName,
-        UtStringLength::class.simpleName,
-        UtStringPositiveLength::class.simpleName,
-        UtStringCharAt::class.simpleName,
-        UtStringEq::class.simpleName,
-        UtSubstringExpression::class.simpleName,
-        UtReplaceExpression::class.simpleName,
-        UtStartsWithExpression::class.simpleName,
-        UtEndsWithExpression::class.simpleName,
-        UtIndexOfExpression::class.simpleName,
-        UtContainsExpression::class.simpleName,
-        UtToStringExpression::class.simpleName,
-        UtSeqLiteral::class.simpleName,
         TREES,
         MAX_NODES,
         MIN_NODES,
@@ -216,59 +201,6 @@ class UtExpressionStructureCounter(private val input: Iterable<UtExpression>) :
         )
     }
 
-    //const string value
-    override fun visit(expr: UtStringConst) = NestStat()
-
-    override fun visit(expr: UtConcatExpression) = multipleExpression(expr.parts)
-
-    override fun visit(expr: UtConvertToString): NestStat {
-        val stat = buildState(expr.expression)
-        stat.level++
-        stat.nodes++
-        return stat
-    }
-
-    override fun visit(expr: UtStringToInt): NestStat {
-        val stat = buildState(expr.expression)
-        stat.level++
-        stat.nodes++
-        return stat
-    }
-
-    override fun visit(expr: UtStringLength): NestStat {
-        val stat = buildState(expr.string)
-        stat.level++
-        stat.nodes++
-        return stat
-    }
-
-    override fun visit(expr: UtStringPositiveLength): NestStat {
-        val stat = buildState(expr.string)
-        stat.level++
-        stat.nodes++
-        return stat
-    }
-
-    override fun visit(expr: UtStringCharAt) = multipleExpressions(expr.string, expr.index)
-
-    override fun visit(expr: UtStringEq) = multipleExpressions(expr.left, expr.right)
-
-    override fun visit(expr: UtSubstringExpression) = multipleExpressions(expr.string, expr.beginIndex, expr.length)
-
-    override fun visit(expr: UtReplaceExpression) = multipleExpressions(expr.string, expr.regex, expr.replacement)
-
-    override fun visit(expr: UtStartsWithExpression) = multipleExpressions(expr.string, expr.prefix)
-
-    override fun visit(expr: UtEndsWithExpression) = multipleExpressions(expr.string, expr.suffix)
-
-    override fun visit(expr: UtIndexOfExpression) = multipleExpressions(expr.string, expr.substring)
-
-    override fun visit(expr: UtContainsExpression) = multipleExpressions(expr.string, expr.substring)
-
-    override fun visit(expr: UtToStringExpression) = multipleExpressions(expr.notNullExpr, expr.isNull)
-
-    override fun visit(expr: UtSeqLiteral) = NestStat()
-
     private fun multipleExpressions(vararg expressions: UtExpression) = multipleExpression(expressions.toList())
 
     private fun multipleExpression(expressions: List<UtExpression>): NestStat {
@@ -311,14 +243,6 @@ class UtExpressionStructureCounter(private val input: Iterable<UtExpression>) :
     override fun visit(expr: UtArrayApplyForAll): NestStat {
         return NestStat()
     }
-
-    override fun visit(expr: UtStringToArray): NestStat {
-        return NestStat()
-    }
-
-    override fun visit(expr: UtArrayToString): NestStat {
-        return NestStat()
-    }
 }
 
 data class NestStat(var nodes: Int = 1, var level: Int = 1)

utbot-framework-test/src/test/kotlin/org/utbot/examples/strings/GenericExamplesTest.kt

@@ -0,0 +1,38 @@
+package org.utbot.examples.strings
+
+import org.utbot.tests.infrastructure.UtValueTestCaseChecker
+import org.utbot.tests.infrastructure.isException
+import org.utbot.tests.infrastructure.CodeGeneration
+import org.utbot.framework.plugin.api.CodegenLanguage
+import org.junit.jupiter.api.Disabled
+import org.junit.jupiter.api.Test
+import org.utbot.testcheckers.eq
+
+@Disabled("TODO: Fails and takes too long")
+internal class GenericExamplesTest : UtValueTestCaseChecker(
+    testClass = GenericExamples::class,
+    testCodeGeneration = true,
+    pipelines = listOf(
+        TestLastStage(CodegenLanguage.JAVA),
+        TestLastStage(CodegenLanguage.KOTLIN, CodeGeneration)
+    )
+) {
+    @Test
+    fun testContainsOkWithIntegerType() {
+        checkWithException(
+            GenericExamples<Int>::containsOk,
+            eq(2),
+            { obj, result -> obj == null && result.isException<NullPointerException>() },
+            { obj, result -> obj != null && result.isSuccess && result.getOrNull() == false }
+        )
+    }
+
+    @Test
+    fun testContainsOkExampleTest() {
+        check(
+            GenericExamples<String>::containsOkExample,
+            eq(1),
+            { result -> result == true }
+        )
+    }
+}

utbot-framework-test/src/test/kotlin/org/utbot/examples/strings/StringExamplesTest.kt

@@ -26,17 +26,32 @@ internal class StringExamplesTest : UtValueTestCaseChecker(
     )
 ) {
     @Test
-    @Disabled("Flaky test: https://github.com/UnitTestBot/UTBotJava/issues/131 (will be enabled in new strings PR)")
     fun testByteToString() {
-        // TODO related to the https://github.com/UnitTestBot/UTBotJava/issues/131
-        withSolverTimeoutInMillis(5000) {
-            check(
-                StringExamples::byteToString,
-                eq(2),
-                { a, b, r -> a > b && r == a.toString() },
-                { a, b, r -> a <= b && r == b.toString() },
-            )
-        }
+        check(
+            StringExamples::byteToString,
+            eq(2),
+            { a, b, r -> a > b && r == a.toString() },
+            { a, b, r -> a <= b && r == b.toString() },
+        )
+    }
+
+    @Test
+    fun testByteToStringWithConstants() {
+        val values: Array<Byte> = arrayOf(
+            Byte.MIN_VALUE,
+            (Byte.MIN_VALUE + 100).toByte(),
+            0.toByte(),
+            (Byte.MAX_VALUE - 100).toByte(),
+            Byte.MAX_VALUE
+        )
+
+        val expected = values.map { it.toString() }
+
+        check(
+            StringExamples::byteToStringWithConstants,
+            eq(1),
+            { r -> r != null && r.indices.all { r[it] == expected[it] } }
+        )
     }
 
     @Test
@@ -53,45 +68,91 @@ internal class StringExamplesTest : UtValueTestCaseChecker(
 
     @Test
     fun testShortToString() {
-        // TODO related to the https://github.com/UnitTestBot/UTBotJava/issues/131
-        withSolverTimeoutInMillis(5000) {
-            check(
-                StringExamples::shortToString,
-                eq(2),
-                { a, b, r -> a > b && r == a.toString() },
-                { a, b, r -> a <= b && r == b.toString() },
-            )
-        }
+        check(
+            StringExamples::shortToString,
+            ignoreExecutionsNumber,
+            { a, b, r -> a > b && r == a.toString() },
+            { a, b, r -> a <= b && r == b.toString() },
+        )
     }
 
+    @Test
+    fun testShortToStringWithConstants() {
+        val values: Array<Short> = arrayOf(
+            Short.MIN_VALUE,
+            (Short.MIN_VALUE + 100).toShort(),
+            0.toShort(),
+            (Short.MAX_VALUE - 100).toShort(),
+            Short.MAX_VALUE
+        )
+
+        val expected = values.map { it.toString() }
+
+        check(
+            StringExamples::shortToStringWithConstants,
+            eq(1),
+            { r -> r != null && r.indices.all { r[it] == expected[it] } }
+        )
+    }
 
     @Test
     fun testIntToString() {
-        // TODO related to the https://github.com/UnitTestBot/UTBotJava/issues/131
-        withSolverTimeoutInMillis(5000) {
-            check(
-                StringExamples::intToString,
-                ignoreExecutionsNumber,
-                { a, b, r -> a > b && r == a.toString() },
-                { a, b, r -> a <= b && r == b.toString() },
-            )
-        }
+        check(
+            StringExamples::intToString,
+            ignoreExecutionsNumber,
+            { a, b, r -> a > b && r == a.toString() },
+            { a, b, r -> a <= b && r == b.toString() },
+        )
     }
 
+    @Test
+    fun testIntToStringWithConstants() {
+        val values: Array<Int> = arrayOf(
+            Integer.MIN_VALUE,
+            Integer.MIN_VALUE + 100,
+            0,
+            Integer.MAX_VALUE - 100,
+            Integer.MAX_VALUE
+        )
+
+        val expected = values.map { it.toString() }
+
+        check(
+            StringExamples::intToStringWithConstants,
+            eq(1),
+            { r -> r != null && r.indices.all { r[it] == expected[it] } }
+        )
+    }
 
     @Test
     fun testLongToString() {
-        // TODO related to the https://github.com/UnitTestBot/UTBotJava/issues/131
-        withSolverTimeoutInMillis(5000) {
-            check(
-                StringExamples::longToString,
-                ignoreExecutionsNumber,
-                { a, b, r -> a > b && r == a.toString() },
-                { a, b, r -> a <= b && r == b.toString() },
-            )
-        }
+        check(
+            StringExamples::longToString,
+            ignoreExecutionsNumber,
+            { a, b, r -> a > b && r == a.toString() },
+            { a, b, r -> a <= b && r == b.toString() },
+        )
     }
 
+    @Test
+    fun testLongToStringWithConstants() {
+        val values: Array<Long> = arrayOf(
+            Long.MIN_VALUE,
+            Long.MIN_VALUE + 100L,
+            0L,
+            Long.MAX_VALUE - 100L,
+            Long.MAX_VALUE
+        )
+
+        val expected = values.map { it.toString() }
+
+        check(
+            StringExamples::longToStringWithConstants,
+            eq(1),
+            { r -> r != null && r.indices.all { r[it] == expected[it] } }
+        )
+    }
+    
     @Test
     fun testStartsWithLiteral() {
         check(
@@ -250,6 +311,15 @@ internal class StringExamplesTest : UtValueTestCaseChecker(
         )
     }
 
+    @Test
+    fun testIsStringBuilderEmpty() {
+        check(
+            StringExamples::isStringBuilderEmpty,
+            eq(2),
+            { stringBuilder, result -> result == stringBuilder.isEmpty() }
+        )
+    }
+
     @Test
     @Disabled("Flaky on GitHub: https://github.com/UnitTestBot/UTBotJava/issues/1004")
     fun testIsValidUuid() {
@@ -332,7 +402,7 @@ internal class StringExamplesTest : UtValueTestCaseChecker(
     fun testSubstring() {
         checkWithException(
             StringExamples::substring,
-            between(5..7),
+            between(5..8),
             { s, _, r -> s == null && r.isException<NullPointerException>() },
             { s, i, r -> s != null && i < 0 || i > s.length && r.isException<StringIndexOutOfBoundsException>() },
             { s, i, r -> s != null && i in 0..s.length && r.getOrThrow() == s.substring(i) && s.substring(i) != "password" },
@@ -585,13 +655,14 @@ internal class StringExamplesTest : UtValueTestCaseChecker(
         withPushingStateFromPathSelectorForConcrete {
             check(
                 StringExamples::equalsIgnoreCase,
-                eq(2),
+                ignoreExecutionsNumber,
                 { s, r -> "SUCCESS".equals(s, ignoreCase = true) && r == "success" },
                 { s, r -> !"SUCCESS".equals(s, ignoreCase = true) && r == "failure" },
             )
         }
     }
 
+    // TODO: This test fails without concrete execution as it uses a symbolic variable
     @Test
     fun testListToString() {
         check(