Add support for special characters by agusaldasoro · Pull Request #1479 · WebFuzzing/EvoMaster

agusaldasoro · 2026-03-19T20:44:09Z

This pull request refactors and improves the handling of table and column names in the SMT-LIB generation logic, ensuring consistent ASCII conversion and proper mapping between original database schema names and their SMT-LIB representations. The changes introduce a new SmtTable abstraction to encapsulate SMT-specific naming, update all relevant logic to use this abstraction, and fix issues related to non-ASCII schema names. The most important changes are as follows:

SMT-LIB Name Handling and Abstraction:

Introduced the SmtTable abstraction in SmtLibGenerator to encapsulate SMT-LIB-specific names and maintain a mapping between original schema names and their ASCII-converted SMT-LIB counterparts, ensuring consistent handling of table and column names throughout the SMT generation process. [1] [2]

Consistent ASCII Conversion:

Updated all relevant code paths to consistently use ASCII-converted names for SMT-LIB symbols, including in table/column references, constraints, and value retrieval, to avoid issues with non-ASCII schema names. [1] [2] [3]

Constraint Generation Refactor:

Refactored the logic for generating table, key, and column constraints (unique, check, primary key, foreign key, boolean, and timestamp) to use the new SmtTable abstraction and ASCII-converted names, replacing direct access to the original schema DTOs. [1] [2] [3] [4] [5] [6] [7] [8]

Query Condition Parsing:

Modified the logic for parsing query conditions to use the correct SMT-LIB table name, falling back to ASCII conversion if the table is not found in the mapping.

Gene Mapping Fixes:

Fixed gene mapping in SMTLibZ3DbConstraintSolver to resolve SMT-LIB column names back to their original database column names, ensuring correct gene creation and type handling for database operations.

These changes collectively improve the robustness and correctness of SMT-LIB constraint generation, especially for schemas with non-ASCII identifiers.

core/src/main/kotlin/org/evomaster/core/solver/SMTLibZ3DbConstraintSolver.kt

arcuri82 · 2026-03-19T21:08:50Z

hi @agusaldasoro ,

thx. first ask @jgaleotti for a review. once he has given it, and you address it, then I can be asked for my review :)

jgaleotti · 2026-03-19T21:36:23Z

core/src/main/kotlin/org/evomaster/core/solver/SmtLibGenerator.kt

+         * Characters that decompose under NFD (Å→A, and other accented letters like é, ü, ñ)
+         * are handled by normalizing to NFD form and stripping the remaining non-ASCII combining marks.
+         */
+        fun sanitizeSmtIdentifier(name: String): String {


I think this belongs to org.evomaster.core.utils.StringUtils, perhapss a more suitable method name could be transliterateIdentifier()

jgaleotti · 2026-03-19T21:36:51Z

core/src/main/kotlin/org/evomaster/core/solver/SMTLibZ3DbConstraintSolver.kt

            val genes = mutableListOf<Gene>()
            for (columnName in columns.fields) {
-                var gene: Gene = IntegerGene(columnName, 0)
+                // columnName is the sanitized (ASCII) version from Z3; resolve back to original DB column name


I am not sure the right term for this should be sanitized

jgaleotti · 2026-03-19T21:37:28Z

core/src/main/kotlin/org/evomaster/core/solver/SmtLibGenerator.kt

        // Only add GetValueSMTNode for the mentioned tables
        for (table in schema.tables) {
            val tableNameLower = table.id.name.lowercase()
+            val sanitizedTableNameLower = sanitizeSmtIdentifier(tableNameLower)


I am not sure the right term should be "sanitized"

jgaleotti · 2026-03-19T21:46:33Z

core/src/main/kotlin/org/evomaster/core/solver/SMTLibZ3DbConstraintSolver.kt

+                val originalColumn = table.columns.firstOrNull {
+                    SmtLibGenerator.sanitizeSmtIdentifier(it.name).equals(columnName, ignoreCase = true)
+                }
+                val actualColumnName = originalColumn?.name ?: columnName


actualColumnName -> columnName?

jgaleotti · 2026-03-19T21:47:25Z

core/src/main/kotlin/org/evomaster/core/solver/SMTLibZ3DbConstraintSolver.kt

@@ -153,36 +153,41 @@ class SMTLibZ3DbConstraintSolver() : DbConstraintSolver {
            // Create the list of genes with the values
            val genes = mutableListOf<Gene>()
            for (columnName in columns.fields) {


columnName -> smtColumnName?

jgaleotti · 2026-03-19T22:17:05Z

core/src/main/kotlin/org/evomaster/core/solver/SmtLibGenerator.kt

    private fun appendTableDefinitions(smt: SMTLib) {
        for (table in schema.tables) {
-            val dataTypeName = "${StringUtils.capitalization(table.id.name)}Row"
+            val sanitizedTableName = convertToAscii(table.id.name)


sanitizedTableName -> smtTableName?

jgaleotti · 2026-03-19T22:17:29Z

core/src/main/kotlin/org/evomaster/core/solver/SmtLibGenerator.kt

     */
    private fun appendUniqueConstraints(smt: SMTLib, table: TableDto) {
-        val tableName = table.id.name.lowercase()
+        val tableName = convertToAscii(table.id.name).lowercase()


tableName -> smtTableName?

jgaleotti · 2026-03-19T22:17:50Z

core/src/main/kotlin/org/evomaster/core/solver/SmtLibGenerator.kt

     */
    private fun appendPrimaryKeyConstraints(smt: SMTLib, table: TableDto) {
-        val tableName = table.id.name.lowercase()
+        val tableName = convertToAscii(table.id.name).lowercase()


tableName -> smtTableName ?

arcuri82 · 2026-03-24T08:22:23Z

core/src/main/kotlin/org/evomaster/core/solver/SMTConditionVisitor.kt

     */
    private fun getColumnReference(tableName: String, columnName: String): String {
-        return "(${columnName.uppercase()} ${tableName.lowercase()}$rowIndex)"
+        return "(${convertToAscii(columnName).uppercase()} ${convertToAscii(tableName).lowercase()}$rowIndex)"


add a comment to explain why this needs to be converted to ASCII

arcuri82 · 2026-03-24T08:26:25Z

core/src/main/kotlin/org/evomaster/core/solver/SmtLibGenerator.kt

@@ -131,7 +132,7 @@ class SmtLibGenerator(private val schema: DbInfoDto, private val numberOfRows: I
     * @return The corresponding SMT node.
     */
    private fun parseCheckExpression(table: TableDto, condition: SqlCondition, index: Int): SMTNode {


maybe not for this PR, but something to discuss as well with @jgaleotti , why is most of the code here relaying on TableDto and not org.evomaster.core.sql.schema.Table. DTOs are only meant as simple POJOs for transfer of data between processes, and not for business logic computation

I did a draft PR with that change, I'm not sure if the interface for fun solve(schemaDto: DbInfoDto, sqlQuery: String, numberOfRows: Int): List<SqlAction> should remain the same or we should change it too.

arcuri82 · 2026-03-24T08:36:24Z

core/src/main/kotlin/org/evomaster/core/solver/SmtLibGenerator.kt

    private fun appendTimestampConstraints(smt: SMTLib) {
        for (table in schema.tables) {
-            val tableName = table.id.name.lowercase()
+            val smtTableName = convertToAscii(table.id.name).lowercase()


there are so many calls to this convertToAscii, which makes it more difficult to read, and possibly easy to make mistake in future if code needs changing and missing a needed call. maybe create a new SmtTable class with that that you need, and pass that around the code instead of doing the conversions each time?

arcuri82 · 2026-03-24T08:41:08Z

core/src/main/kotlin/org/evomaster/core/utils/StringUtils.kt

+    fun convertToAscii(name: String): String {
+        val replaced = name
+            .replace('Ø', 'O').replace('ø', 'o')
+            .replace("Æ", "AE").replace("æ", "ae")


what about Norwegian å and Å? or Swedish characters like Ä, ä, Ö and ö ? or other special characters in all other languages?
we cannot have ad-hoc solutions like this, only specific to our test data. Need a general solution.

Add support for special characters

ea5ae60

agusaldasoro commented Mar 19, 2026

View reviewed changes

core/src/main/kotlin/org/evomaster/core/solver/SMTLibZ3DbConstraintSolver.kt Outdated Show resolved Hide resolved

Apply suggestion from @agusaldasoro

0f06153

agusaldasoro marked this pull request as ready for review March 19, 2026 21:04

agusaldasoro requested review from arcuri82 and jgaleotti March 19, 2026 21:05

arcuri82 removed their request for review March 19, 2026 21:08

jgaleotti requested changes Mar 19, 2026

View reviewed changes

Refactor naming

7e5a0e1

jgaleotti requested changes Mar 19, 2026

View reviewed changes

rename vars

c003c56

jgaleotti approved these changes Mar 19, 2026

View reviewed changes

jgaleotti requested a review from arcuri82 March 19, 2026 22:22

Fix type

03099b4

arcuri82 requested changes Mar 24, 2026

View reviewed changes

agusaldasoro and others added 4 commits April 6, 2026 19:00

Support for any language special characters

47e2f90

Create SmtTable class to handle name conversion

3caf6fd

add comment

3f39f8b

Merge branch 'master' into fix/more-types

b10bbe3

agusaldasoro requested a review from arcuri82 April 7, 2026 04:15

Conversation

agusaldasoro commented Mar 19, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Uh oh!

arcuri82 commented Mar 19, 2026

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

agusaldasoro commented Mar 19, 2026 •

edited

Loading