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.

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,
+    languagePipelines = listOf(
+        CodeGenerationLanguageLastStage(CodegenLanguage.JAVA),
+        CodeGenerationLanguageLastStage(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,13 @@ 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
@@ -53,43 +49,34 @@ 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 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 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
@@ -250,6 +237,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() {
@@ -585,7 +581,7 @@ 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" },
             )

utbot-framework/src/main/java/org/utbot/engine/overrides/Byte.java

@@ -1,10 +1,10 @@
 package org.utbot.engine.overrides;
 
 import org.utbot.api.annotation.UtClassMock;
-import org.utbot.engine.overrides.strings.UtNativeString;
-import org.utbot.engine.overrides.strings.UtString;
 import org.utbot.engine.overrides.strings.UtStringBuilder;
 
+import java.util.Arrays;
+
 import static org.utbot.api.mock.UtMock.assume;
 import static org.utbot.engine.overrides.UtLogicMock.ite;
 import static org.utbot.api.mock.UtMock.assumeOrExecuteConcretely;
@@ -54,11 +54,31 @@ public static String toString(byte b) {
         // and reduce time of solving queries with bv2int expressions
         assume(b < 128);
         assume(b >= -128);
-        // prefix = condition ? "-" : ""
-        String prefix = ite(condition, "-", "");
-        UtStringBuilder sb = new UtStringBuilder(prefix);
-        // value = condition ? -i : i
-        int value = ite(condition, (byte) -b, b);
-        return sb.append(new UtString(new UtNativeString(value)).toStringImpl()).toString();
+
+        if (b == -128) {
+            return "-128";
+        } else {
+            String prefix = ite(condition, "-", "");
+            int value = ite(condition, (byte) -b, b);
+            char[] reversed = new char[3];
+            int offset = 0;
+            while (value > 0) {
+                reversed[offset] = (char) ('0' + value % 10);
+                value = value / 10;
+                offset++;
+            }
+
+            if (offset > 0) {
+                char[] buffer = new char[offset];
+                int counter = 0;
+                while (offset > 0) {
+                    offset--;
+                    buffer[counter++] = reversed[offset];
+                }
+                return prefix + new String(buffer);
+            } else {
+                return "0";
+            }
+        }
     }
 }

utbot-framework/src/main/java/org/utbot/engine/overrides/Integer.java

@@ -1,8 +1,6 @@
 package org.utbot.engine.overrides;
 
 import org.utbot.api.annotation.UtClassMock;
-import org.utbot.engine.overrides.strings.UtNativeString;
-import org.utbot.engine.overrides.strings.UtString;
 import org.utbot.engine.overrides.strings.UtStringBuilder;
 
 import static org.utbot.api.mock.UtMock.assumeOrExecuteConcretely;
@@ -75,17 +73,30 @@ public static String toString(int i) {
         if (i == 0x80000000) { // java.lang.MIN_VALUE
             return "-2147483648";
         }
-        // assumes are placed here to limit search space of solver
-        // and reduce time of solving queries with bv2int expressions
-        assumeOrExecuteConcretely(i <= 0x8000);
-        assumeOrExecuteConcretely(i >= -0x8000);
+
         // condition = i < 0
         boolean condition = less(i, 0);
         // prefix = condition ? "-" : ""
         String prefix = ite(condition, "-", "");
-        UtStringBuilder sb = new UtStringBuilder(prefix);
-        // value = condition ? -i : i
         int value = ite(condition, -i, i);
-        return sb.append(new UtString(new UtNativeString(value)).toStringImpl()).toString();
+        char[] reversed = new char[10];
+        int offset = 0;
+        while (value > 0) {
+            reversed[offset] = (char) ('0' + value % 10);
+            value = value / 10;
+            offset++;
+        }
+
+        if (offset > 0) {
+            char[] buffer = new char[offset];
+            int counter = 0;
+            while (offset > 0) {
+                offset--;
+                buffer[counter++] = reversed[offset];
+            }
+            return prefix + new String(buffer);
+        } else {
+            return "0";
+        }
     }
 }

utbot-framework/src/main/java/org/utbot/engine/overrides/Long.java

@@ -1,8 +1,6 @@
 package org.utbot.engine.overrides;
 
 import org.utbot.api.annotation.UtClassMock;
-import org.utbot.engine.overrides.strings.UtNativeString;
-import org.utbot.engine.overrides.strings.UtString;
 import org.utbot.engine.overrides.strings.UtStringBuilder;
 
 import static org.utbot.api.mock.UtMock.assumeOrExecuteConcretely;
@@ -75,17 +73,30 @@ public static String toString(long l) {
         if (l == 0x8000000000000000L) { // java.lang.Long.MIN_VALUE
             return "-9223372036854775808";
         }
-        // assumes are placed here to limit search space of solver
-        // and reduce time of solving queries with bv2int expressions
-        assumeOrExecuteConcretely(l <= 10000);
-        assumeOrExecuteConcretely(l >= -10000);
         // condition = l < 0
         boolean condition = less(l, 0);
         // prefix = condition ? "-" : ""
         String prefix = ite(condition, "-", "");
-        UtStringBuilder sb = new UtStringBuilder(prefix);
         // value = condition ? -l : l
         long value = ite(condition, -l, l);
-        return sb.append(new UtString(new UtNativeString(value)).toStringImpl()).toString();
+        char[] reversed = new char[19];
+        int offset = 0;
+        while (value > 0) {
+            reversed[offset] = (char) ('0' + value % 10);
+            value = value / 10;
+            offset++;
+        }
+
+        if (offset > 0) {
+            char[] buffer = new char[offset];
+            int i = 0;
+            while (offset > 0) {
+                offset--;
+                buffer[i++] = reversed[offset];
+            }
+            return prefix + new String(buffer);
+        } else {
+            return "0";
+        }
     }
 }