From ea5ae604abae77fa8db057303506356c060cc0db Mon Sep 17 00:00:00 2001 From: Agustina Aldasoro Date: Thu, 19 Mar 2026 17:43:47 -0300 Subject: [PATCH 1/5] Add support for special characters --- .../core/solver/SMTConditionVisitor.kt | 2 +- .../core/solver/SMTLibZ3DbConstraintSolver.kt | 28 +++++---- .../evomaster/core/solver/SmtLibGenerator.kt | 61 +++++++++++++------ 3 files changed, 61 insertions(+), 30 deletions(-) diff --git a/core/src/main/kotlin/org/evomaster/core/solver/SMTConditionVisitor.kt b/core/src/main/kotlin/org/evomaster/core/solver/SMTConditionVisitor.kt index eb12789a79..65b83bead8 100644 --- a/core/src/main/kotlin/org/evomaster/core/solver/SMTConditionVisitor.kt +++ b/core/src/main/kotlin/org/evomaster/core/solver/SMTConditionVisitor.kt @@ -31,7 +31,7 @@ class SMTConditionVisitor( * @return The SMT-LIB column reference string. */ private fun getColumnReference(tableName: String, columnName: String): String { - return "(${columnName.uppercase()} ${tableName.lowercase()}$rowIndex)" + return "(${SmtLibGenerator.sanitizeSmtIdentifier(columnName).uppercase()} ${SmtLibGenerator.sanitizeSmtIdentifier(tableName).lowercase()}$rowIndex)" } /** diff --git a/core/src/main/kotlin/org/evomaster/core/solver/SMTLibZ3DbConstraintSolver.kt b/core/src/main/kotlin/org/evomaster/core/solver/SMTLibZ3DbConstraintSolver.kt index f2cbbc287e..860f0b2159 100644 --- a/core/src/main/kotlin/org/evomaster/core/solver/SMTLibZ3DbConstraintSolver.kt +++ b/core/src/main/kotlin/org/evomaster/core/solver/SMTLibZ3DbConstraintSolver.kt @@ -94,6 +94,7 @@ class SMTLibZ3DbConstraintSolver() : DbConstraintSolver { val queryStatement = parseStatement(sqlQuery) val smtLib = generator.generateSMT(queryStatement) val fileName = storeToTmpFile(smtLib) + println(smtLib) val z3Response = executor.solveFromFile(fileName) return toSqlActionList(schemaDto, z3Response) @@ -153,17 +154,23 @@ class SMTLibZ3DbConstraintSolver() : DbConstraintSolver { // Create the list of genes with the values val genes = mutableListOf() 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 + val originalColumn = table.columns.firstOrNull { + SmtLibGenerator.sanitizeSmtIdentifier(it.name).equals(columnName, ignoreCase = true) + } + val actualColumnName = originalColumn?.name ?: columnName + + var gene: Gene = IntegerGene(actualColumnName, 0) when (val columnValue = columns.getField(columnName)) { is StringValue -> { - gene = if (hasColumnType(schemaDto, table, columnName, "BOOLEAN")) { - BooleanGene(columnName, toBoolean(columnValue.value)) + gene = if (hasColumnType(schemaDto, table, actualColumnName, "BOOLEAN")) { + BooleanGene(actualColumnName, toBoolean(columnValue.value)) } else { - StringGene(columnName, columnValue.value) + StringGene(actualColumnName, columnValue.value) } } is LongValue -> { - gene = if (hasColumnType(schemaDto, table, columnName, "TIMESTAMP")) { + gene = if (hasColumnType(schemaDto, table, actualColumnName, "TIMESTAMP")) { val epochSeconds = columnValue.value.toLong() val localDateTime = LocalDateTime.ofInstant( Instant.ofEpochSecond(epochSeconds), ZoneOffset.UTC @@ -171,18 +178,17 @@ class SMTLibZ3DbConstraintSolver() : DbConstraintSolver { val formatted = localDateTime.format( DateTimeFormatter.ofPattern("yyyy-MM-dd HH:mm:ss") ) - ImmutableDataHolderGene(columnName, formatted, inQuotes = true) + ImmutableDataHolderGene(actualColumnName, formatted, inQuotes = true) } else { - IntegerGene(columnName, columnValue.value.toInt()) + IntegerGene(actualColumnName, columnValue.value.toInt()) } } is RealValue -> { - gene = DoubleGene(columnName, columnValue.value) + gene = DoubleGene(actualColumnName, columnValue.value) } } - val currentColumn = table.columns.firstOrNull(){ it.name.equals(columnName, ignoreCase = true) } - if (currentColumn != null && currentColumn.primaryKey) { - gene = SqlPrimaryKeyGene(columnName, table.id, gene, actionId) + if (originalColumn != null && originalColumn.primaryKey) { + gene = SqlPrimaryKeyGene(actualColumnName, table.id, gene, actionId) } gene.markAllAsInitialized() genes.add(gene) diff --git a/core/src/main/kotlin/org/evomaster/core/solver/SmtLibGenerator.kt b/core/src/main/kotlin/org/evomaster/core/solver/SmtLibGenerator.kt index a963e53dec..ba25d2ea5c 100644 --- a/core/src/main/kotlin/org/evomaster/core/solver/SmtLibGenerator.kt +++ b/core/src/main/kotlin/org/evomaster/core/solver/SmtLibGenerator.kt @@ -58,7 +58,8 @@ class SmtLibGenerator(private val schema: DbInfoDto, private val numberOfRows: I */ private fun appendTableDefinitions(smt: SMTLib) { for (table in schema.tables) { - val dataTypeName = "${StringUtils.capitalization(table.id.name)}Row" + val sanitizedTableName = sanitizeSmtIdentifier(table.id.name) + val dataTypeName = "${StringUtils.capitalization(sanitizedTableName)}Row" // Declare datatype for the table smt.addNode( @@ -67,7 +68,7 @@ class SmtLibGenerator(private val schema: DbInfoDto, private val numberOfRows: I // Declare constants for each row for (i in 1..numberOfRows) { - smt.addNode(DeclareConstSMTNode("${table.id.name.lowercase()}$i", dataTypeName)) + smt.addNode(DeclareConstSMTNode("${sanitizedTableName.lowercase()}$i", dataTypeName)) } } } @@ -91,10 +92,10 @@ class SmtLibGenerator(private val schema: DbInfoDto, private val numberOfRows: I * @param table The table for which unique constraints are added. */ private fun appendUniqueConstraints(smt: SMTLib, table: TableDto) { - val tableName = table.id.name.lowercase() + val tableName = sanitizeSmtIdentifier(table.id.name).lowercase() for (column in table.columns) { if (column.unique) { - val nodes = assertForDistinctField(column.name, tableName) + val nodes = assertForDistinctField(sanitizeSmtIdentifier(column.name), tableName) smt.addNodes(nodes) } } @@ -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 { - val visitor = SMTConditionVisitor(table.id.name.lowercase(), emptyMap(), schema.tables, index) + val visitor = SMTConditionVisitor(sanitizeSmtIdentifier(table.id.name).lowercase(), emptyMap(), schema.tables, index) return condition.accept(visitor, null) as SMTNode } @@ -167,10 +168,10 @@ class SmtLibGenerator(private val schema: DbInfoDto, private val numberOfRows: I private fun appendBooleanConstraints(smt: SMTLib) { for (table in schema.tables) { - val tableName = table.id.name.lowercase() + val tableName = sanitizeSmtIdentifier(table.id.name).lowercase() for (column in table.columns) { if (column.type.equals("BOOLEAN", ignoreCase = true)) { - val columnName = column.name.uppercase() + val columnName = sanitizeSmtIdentifier(column.name).uppercase() for (i in 1..numberOfRows) { smt.addNode( AssertSMTNode( @@ -194,10 +195,10 @@ class SmtLibGenerator(private val schema: DbInfoDto, private val numberOfRows: I private fun appendTimestampConstraints(smt: SMTLib) { for (table in schema.tables) { - val tableName = table.id.name.lowercase() + val tableName = sanitizeSmtIdentifier(table.id.name).lowercase() for (column in table.columns) { if (column.type.equals("TIMESTAMP", ignoreCase = true)) { - val columnName = column.name.uppercase() + val columnName = sanitizeSmtIdentifier(column.name).uppercase() val lowerBound = 0 // Example for Unix epoch start val upperBound = 32503680000 // Example for year 3000 in seconds @@ -232,11 +233,11 @@ class SmtLibGenerator(private val schema: DbInfoDto, private val numberOfRows: I * @param table The table for which primary key constraints are added. */ private fun appendPrimaryKeyConstraints(smt: SMTLib, table: TableDto) { - val tableName = table.id.name.lowercase() + val tableName = sanitizeSmtIdentifier(table.id.name).lowercase() val primaryKeys = table.columns.filter { it.primaryKey } for (primaryKey in primaryKeys) { - val nodes = assertForDistinctField(primaryKey.name, tableName) + val nodes = assertForDistinctField(sanitizeSmtIdentifier(primaryKey.name), tableName) smt.addNodes(nodes) } } @@ -274,16 +275,16 @@ class SmtLibGenerator(private val schema: DbInfoDto, private val numberOfRows: I * @param table The table for which foreign key constraints are added. */ private fun appendForeignKeyConstraints(smt: SMTLib, table: TableDto) { - val sourceTableName = table.id.name.lowercase() + val sourceTableName = sanitizeSmtIdentifier(table.id.name).lowercase() for (foreignKey in table.foreignKeys) { val referencedTable = findReferencedTable(foreignKey) - val referencedTableName = referencedTable.id.name.lowercase() - val referencedColumnSelector = findReferencedPKSelector(table, referencedTable, foreignKey) + val referencedTableName = sanitizeSmtIdentifier(referencedTable.id.name).lowercase() + val referencedColumnSelector = sanitizeSmtIdentifier(findReferencedPKSelector(table, referencedTable, foreignKey)) for (sourceColumn in foreignKey.sourceColumns) { val nodes = assertForEqualsAny( - sourceColumn, sourceTableName, + sanitizeSmtIdentifier(sourceColumn), sourceTableName, referencedColumnSelector, referencedTableName ) smt.addNodes(nodes) @@ -434,7 +435,7 @@ class SmtLibGenerator(private val schema: DbInfoDto, private val numberOfRows: I * @return The corresponding SMT node. */ private fun parseQueryCondition(tableAliases: Map, defaultTableName: String, condition: SqlCondition, index: Int): SMTNode { - val visitor = SMTConditionVisitor(defaultTableName, tableAliases, schema.tables, index) + val visitor = SMTConditionVisitor(sanitizeSmtIdentifier(defaultTableName), tableAliases, schema.tables, index) return condition.accept(visitor, null) as SMTNode } @@ -519,9 +520,10 @@ class SmtLibGenerator(private val schema: DbInfoDto, private val numberOfRows: I // Only add GetValueSMTNode for the mentioned tables for (table in schema.tables) { val tableNameLower = table.id.name.lowercase() + val sanitizedTableNameLower = sanitizeSmtIdentifier(tableNameLower) if (tablesMentioned.contains(tableNameLower)) { for (i in 1..numberOfRows) { - smt.addNode(GetValueSMTNode("$tableNameLower$i")) + smt.addNode(GetValueSMTNode("$sanitizedTableNameLower$i")) } } } @@ -537,22 +539,45 @@ class SmtLibGenerator(private val schema: DbInfoDto, private val numberOfRows: I return table.columns.map { c -> val smtType = TYPE_MAP[c.type.uppercase()] ?: throw RuntimeException("Unsupported column type: ${c.type}") - DeclareConstSMTNode(c.name, smtType) + DeclareConstSMTNode(sanitizeSmtIdentifier(c.name), smtType) } } companion object { + /** + * Replaces non-ASCII characters in a name to make it a valid SMT-LIB identifier. + * SMT-LIB unquoted symbols are restricted to ASCII, so characters like Æ, Ø, Å must be transliterated. + * + * This is needed because our test suite includes Norwegian APIs whose database schemas + * contain column and table names with Norwegian characters (Æ, Ø, Å). + * + * Characters that do not decompose under NFD (Ø, Æ) are replaced explicitly. + * 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 { + val replaced = name + .replace('Ø', 'O').replace('ø', 'o') + .replace("Æ", "AE").replace("æ", "ae") + return java.text.Normalizer.normalize(replaced, java.text.Normalizer.Form.NFD) + .replace(Regex("[^\\x00-\\x7F]"), "") + } + // Maps database column types to SMT-LIB types private val TYPE_MAP = mapOf( "BIGINT" to "Int", "BIT" to "Int", "INTEGER" to "Int", + "INT" to "Int", "INT2" to "Int", "INT4" to "Int", "INT8" to "Int", "TINYINT" to "Int", "SMALLINT" to "Int", "NUMERIC" to "Int", + "SERIAL" to "Int", + "SMALLSERIAL" to "Int", + "BIGSERIAL" to "Int", "TIMESTAMP" to "Int", "DATE" to "Int", "FLOAT" to "Real", From 0f06153b3b34c83691a313a025f426498b889674 Mon Sep 17 00:00:00 2001 From: Agustina Aldasoro Date: Thu, 19 Mar 2026 17:45:53 -0300 Subject: [PATCH 2/5] Apply suggestion from @agusaldasoro --- .../org/evomaster/core/solver/SMTLibZ3DbConstraintSolver.kt | 1 - 1 file changed, 1 deletion(-) diff --git a/core/src/main/kotlin/org/evomaster/core/solver/SMTLibZ3DbConstraintSolver.kt b/core/src/main/kotlin/org/evomaster/core/solver/SMTLibZ3DbConstraintSolver.kt index 860f0b2159..61b00fa5d1 100644 --- a/core/src/main/kotlin/org/evomaster/core/solver/SMTLibZ3DbConstraintSolver.kt +++ b/core/src/main/kotlin/org/evomaster/core/solver/SMTLibZ3DbConstraintSolver.kt @@ -94,7 +94,6 @@ class SMTLibZ3DbConstraintSolver() : DbConstraintSolver { val queryStatement = parseStatement(sqlQuery) val smtLib = generator.generateSMT(queryStatement) val fileName = storeToTmpFile(smtLib) - println(smtLib) val z3Response = executor.solveFromFile(fileName) return toSqlActionList(schemaDto, z3Response) From 7e5a0e1bad17a0d012e83902facc5dac44f0d62c Mon Sep 17 00:00:00 2001 From: Agustina Aldasoro Date: Thu, 19 Mar 2026 19:15:37 -0300 Subject: [PATCH 3/5] Refactor naming --- .../core/solver/SMTConditionVisitor.kt | 3 +- .../core/solver/SMTLibZ3DbConstraintSolver.kt | 33 +++++------ .../evomaster/core/solver/SmtLibGenerator.kt | 56 +++++++------------ .../org/evomaster/core/utils/StringUtils.kt | 21 ++++++- 4 files changed, 57 insertions(+), 56 deletions(-) diff --git a/core/src/main/kotlin/org/evomaster/core/solver/SMTConditionVisitor.kt b/core/src/main/kotlin/org/evomaster/core/solver/SMTConditionVisitor.kt index 65b83bead8..b92704e159 100644 --- a/core/src/main/kotlin/org/evomaster/core/solver/SMTConditionVisitor.kt +++ b/core/src/main/kotlin/org/evomaster/core/solver/SMTConditionVisitor.kt @@ -1,6 +1,7 @@ package org.evomaster.core.solver import org.evomaster.client.java.controller.api.dto.database.schema.TableDto +import org.evomaster.core.utils.StringUtils.convertToAscii import org.evomaster.dbconstraint.ast.* import org.evomaster.solver.smtlib.AssertSMTNode import org.evomaster.solver.smtlib.EmptySMTNode @@ -31,7 +32,7 @@ class SMTConditionVisitor( * @return The SMT-LIB column reference string. */ private fun getColumnReference(tableName: String, columnName: String): String { - return "(${SmtLibGenerator.sanitizeSmtIdentifier(columnName).uppercase()} ${SmtLibGenerator.sanitizeSmtIdentifier(tableName).lowercase()}$rowIndex)" + return "(${convertToAscii(columnName).uppercase()} ${convertToAscii(tableName).lowercase()}$rowIndex)" } /** diff --git a/core/src/main/kotlin/org/evomaster/core/solver/SMTLibZ3DbConstraintSolver.kt b/core/src/main/kotlin/org/evomaster/core/solver/SMTLibZ3DbConstraintSolver.kt index 61b00fa5d1..13fdb06665 100644 --- a/core/src/main/kotlin/org/evomaster/core/solver/SMTLibZ3DbConstraintSolver.kt +++ b/core/src/main/kotlin/org/evomaster/core/solver/SMTLibZ3DbConstraintSolver.kt @@ -20,6 +20,7 @@ import org.evomaster.core.search.gene.sql.SqlPrimaryKeyGene import org.evomaster.core.search.gene.string.StringGene import org.evomaster.core.sql.SqlAction import org.evomaster.core.sql.schema.* +import org.evomaster.core.utils.StringUtils.convertToAscii import org.evomaster.solver.Z3DockerExecutor import org.evomaster.solver.smtlib.SMTLib import org.evomaster.solver.smtlib.value.* @@ -152,24 +153,24 @@ class SMTLibZ3DbConstraintSolver() : DbConstraintSolver { // Create the list of genes with the values val genes = mutableListOf() - for (columnName in columns.fields) { - // columnName is the sanitized (ASCII) version from Z3; resolve back to original DB column name - val originalColumn = table.columns.firstOrNull { - SmtLibGenerator.sanitizeSmtIdentifier(it.name).equals(columnName, ignoreCase = true) + // smtColumn is the Ascii version from SmtLib; resolve back to original DB column name + for (smtColumn in columns.fields) { + val dbColumn = table.columns.firstOrNull { + convertToAscii(it.name).equals(smtColumn, ignoreCase = true) } - val actualColumnName = originalColumn?.name ?: columnName + val dbColumnName = dbColumn?.name ?: smtColumn - var gene: Gene = IntegerGene(actualColumnName, 0) - when (val columnValue = columns.getField(columnName)) { + var gene: Gene = IntegerGene(dbColumnName, 0) + when (val columnValue = columns.getField(smtColumn)) { is StringValue -> { - gene = if (hasColumnType(schemaDto, table, actualColumnName, "BOOLEAN")) { - BooleanGene(actualColumnName, toBoolean(columnValue.value)) + gene = if (hasColumnType(schemaDto, table, dbColumnName, "BOOLEAN")) { + BooleanGene(dbColumnName, toBoolean(columnValue.value)) } else { - StringGene(actualColumnName, columnValue.value) + StringGene(dbColumnName, columnValue.value) } } is LongValue -> { - gene = if (hasColumnType(schemaDto, table, actualColumnName, "TIMESTAMP")) { + gene = if (hasColumnType(schemaDto, table, dbColumnName, "TIMESTAMP")) { val epochSeconds = columnValue.value.toLong() val localDateTime = LocalDateTime.ofInstant( Instant.ofEpochSecond(epochSeconds), ZoneOffset.UTC @@ -177,17 +178,17 @@ class SMTLibZ3DbConstraintSolver() : DbConstraintSolver { val formatted = localDateTime.format( DateTimeFormatter.ofPattern("yyyy-MM-dd HH:mm:ss") ) - ImmutableDataHolderGene(actualColumnName, formatted, inQuotes = true) + ImmutableDataHolderGene(dbColumnName, formatted, inQuotes = true) } else { - IntegerGene(actualColumnName, columnValue.value.toInt()) + IntegerGene(dbColumnName, columnValue.value.toInt()) } } is RealValue -> { - gene = DoubleGene(actualColumnName, columnValue.value) + gene = DoubleGene(dbColumnName, columnValue.value) } } - if (originalColumn != null && originalColumn.primaryKey) { - gene = SqlPrimaryKeyGene(actualColumnName, table.id, gene, actionId) + if (dbColumn != null && dbColumn.primaryKey) { + gene = SqlPrimaryKeyGene(dbColumnName, table.id, gene, actionId) } gene.markAllAsInitialized() genes.add(gene) diff --git a/core/src/main/kotlin/org/evomaster/core/solver/SmtLibGenerator.kt b/core/src/main/kotlin/org/evomaster/core/solver/SmtLibGenerator.kt index ba25d2ea5c..7396aae19a 100644 --- a/core/src/main/kotlin/org/evomaster/core/solver/SmtLibGenerator.kt +++ b/core/src/main/kotlin/org/evomaster/core/solver/SmtLibGenerator.kt @@ -15,11 +15,11 @@ import org.evomaster.core.utils.StringUtils import org.evomaster.dbconstraint.ConstraintDatabaseType import org.evomaster.dbconstraint.ast.SqlCondition import net.sf.jsqlparser.JSQLParserException +import org.evomaster.core.utils.StringUtils.convertToAscii import org.evomaster.dbconstraint.parser.SqlConditionParserException import org.evomaster.dbconstraint.parser.jsql.JSqlConditionParser import org.evomaster.solver.smtlib.* import org.evomaster.solver.smtlib.assertion.* -import java.util.* /** * Generates SMT-LIB constraints from SQL queries and schema definitions. @@ -58,7 +58,7 @@ class SmtLibGenerator(private val schema: DbInfoDto, private val numberOfRows: I */ private fun appendTableDefinitions(smt: SMTLib) { for (table in schema.tables) { - val sanitizedTableName = sanitizeSmtIdentifier(table.id.name) + val sanitizedTableName = convertToAscii(table.id.name) val dataTypeName = "${StringUtils.capitalization(sanitizedTableName)}Row" // Declare datatype for the table @@ -92,10 +92,10 @@ class SmtLibGenerator(private val schema: DbInfoDto, private val numberOfRows: I * @param table The table for which unique constraints are added. */ private fun appendUniqueConstraints(smt: SMTLib, table: TableDto) { - val tableName = sanitizeSmtIdentifier(table.id.name).lowercase() + val tableName = convertToAscii(table.id.name).lowercase() for (column in table.columns) { if (column.unique) { - val nodes = assertForDistinctField(sanitizeSmtIdentifier(column.name), tableName) + val nodes = assertForDistinctField(convertToAscii(column.name), tableName) smt.addNodes(nodes) } } @@ -132,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 { - val visitor = SMTConditionVisitor(sanitizeSmtIdentifier(table.id.name).lowercase(), emptyMap(), schema.tables, index) + val visitor = SMTConditionVisitor(convertToAscii(table.id.name).lowercase(), emptyMap(), schema.tables, index) return condition.accept(visitor, null) as SMTNode } @@ -168,10 +168,10 @@ class SmtLibGenerator(private val schema: DbInfoDto, private val numberOfRows: I private fun appendBooleanConstraints(smt: SMTLib) { for (table in schema.tables) { - val tableName = sanitizeSmtIdentifier(table.id.name).lowercase() + val tableName = convertToAscii(table.id.name).lowercase() for (column in table.columns) { if (column.type.equals("BOOLEAN", ignoreCase = true)) { - val columnName = sanitizeSmtIdentifier(column.name).uppercase() + val columnName = convertToAscii(column.name).uppercase() for (i in 1..numberOfRows) { smt.addNode( AssertSMTNode( @@ -195,10 +195,10 @@ class SmtLibGenerator(private val schema: DbInfoDto, private val numberOfRows: I private fun appendTimestampConstraints(smt: SMTLib) { for (table in schema.tables) { - val tableName = sanitizeSmtIdentifier(table.id.name).lowercase() + val tableName = convertToAscii(table.id.name).lowercase() for (column in table.columns) { if (column.type.equals("TIMESTAMP", ignoreCase = true)) { - val columnName = sanitizeSmtIdentifier(column.name).uppercase() + val columnName = convertToAscii(column.name).uppercase() val lowerBound = 0 // Example for Unix epoch start val upperBound = 32503680000 // Example for year 3000 in seconds @@ -233,11 +233,11 @@ class SmtLibGenerator(private val schema: DbInfoDto, private val numberOfRows: I * @param table The table for which primary key constraints are added. */ private fun appendPrimaryKeyConstraints(smt: SMTLib, table: TableDto) { - val tableName = sanitizeSmtIdentifier(table.id.name).lowercase() + val tableName = convertToAscii(table.id.name).lowercase() val primaryKeys = table.columns.filter { it.primaryKey } for (primaryKey in primaryKeys) { - val nodes = assertForDistinctField(sanitizeSmtIdentifier(primaryKey.name), tableName) + val nodes = assertForDistinctField(convertToAscii(primaryKey.name), tableName) smt.addNodes(nodes) } } @@ -275,16 +275,16 @@ class SmtLibGenerator(private val schema: DbInfoDto, private val numberOfRows: I * @param table The table for which foreign key constraints are added. */ private fun appendForeignKeyConstraints(smt: SMTLib, table: TableDto) { - val sourceTableName = sanitizeSmtIdentifier(table.id.name).lowercase() + val sourceTableName = convertToAscii(table.id.name).lowercase() for (foreignKey in table.foreignKeys) { val referencedTable = findReferencedTable(foreignKey) - val referencedTableName = sanitizeSmtIdentifier(referencedTable.id.name).lowercase() - val referencedColumnSelector = sanitizeSmtIdentifier(findReferencedPKSelector(table, referencedTable, foreignKey)) + val referencedTableName = convertToAscii(referencedTable.id.name).lowercase() + val referencedColumnSelector = convertToAscii(findReferencedPKSelector(table, referencedTable, foreignKey)) for (sourceColumn in foreignKey.sourceColumns) { val nodes = assertForEqualsAny( - sanitizeSmtIdentifier(sourceColumn), sourceTableName, + convertToAscii(sourceColumn), sourceTableName, referencedColumnSelector, referencedTableName ) smt.addNodes(nodes) @@ -435,7 +435,7 @@ class SmtLibGenerator(private val schema: DbInfoDto, private val numberOfRows: I * @return The corresponding SMT node. */ private fun parseQueryCondition(tableAliases: Map, defaultTableName: String, condition: SqlCondition, index: Int): SMTNode { - val visitor = SMTConditionVisitor(sanitizeSmtIdentifier(defaultTableName), tableAliases, schema.tables, index) + val visitor = SMTConditionVisitor(convertToAscii(defaultTableName), tableAliases, schema.tables, index) return condition.accept(visitor, null) as SMTNode } @@ -520,10 +520,10 @@ class SmtLibGenerator(private val schema: DbInfoDto, private val numberOfRows: I // Only add GetValueSMTNode for the mentioned tables for (table in schema.tables) { val tableNameLower = table.id.name.lowercase() - val sanitizedTableNameLower = sanitizeSmtIdentifier(tableNameLower) + val smtColumnName = convertToAscii(tableNameLower) if (tablesMentioned.contains(tableNameLower)) { for (i in 1..numberOfRows) { - smt.addNode(GetValueSMTNode("$sanitizedTableNameLower$i")) + smt.addNode(GetValueSMTNode("$smtColumnName$i")) } } } @@ -539,29 +539,11 @@ class SmtLibGenerator(private val schema: DbInfoDto, private val numberOfRows: I return table.columns.map { c -> val smtType = TYPE_MAP[c.type.uppercase()] ?: throw RuntimeException("Unsupported column type: ${c.type}") - DeclareConstSMTNode(sanitizeSmtIdentifier(c.name), smtType) + DeclareConstSMTNode(convertToAscii(c.name), smtType) } } companion object { - /** - * Replaces non-ASCII characters in a name to make it a valid SMT-LIB identifier. - * SMT-LIB unquoted symbols are restricted to ASCII, so characters like Æ, Ø, Å must be transliterated. - * - * This is needed because our test suite includes Norwegian APIs whose database schemas - * contain column and table names with Norwegian characters (Æ, Ø, Å). - * - * Characters that do not decompose under NFD (Ø, Æ) are replaced explicitly. - * 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 { - val replaced = name - .replace('Ø', 'O').replace('ø', 'o') - .replace("Æ", "AE").replace("æ", "ae") - return java.text.Normalizer.normalize(replaced, java.text.Normalizer.Form.NFD) - .replace(Regex("[^\\x00-\\x7F]"), "") - } // Maps database column types to SMT-LIB types private val TYPE_MAP = mapOf( diff --git a/core/src/main/kotlin/org/evomaster/core/utils/StringUtils.kt b/core/src/main/kotlin/org/evomaster/core/utils/StringUtils.kt index 426d1a8737..7cccbac206 100644 --- a/core/src/main/kotlin/org/evomaster/core/utils/StringUtils.kt +++ b/core/src/main/kotlin/org/evomaster/core/utils/StringUtils.kt @@ -1,7 +1,5 @@ package org.evomaster.core.utils -import java.util.* - object StringUtils { /** @@ -82,4 +80,23 @@ object StringUtils { } return lines } + + /** + * Replaces non-ASCII characters in a name to make it a valid SMT-LIB identifier. + * SMT-LIB unquoted symbols are restricted to ASCII, so characters like Æ, Ø, Å must be transliterated. + * + * This is needed because our test suite includes Norwegian APIs whose database schemas + * contain column and table names with Norwegian characters (Æ, Ø, Å). + * + * Characters that do not decompose under NFD (Ø, Æ) are replaced explicitly. + * 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 convertToAscii(name: String): String { + val replaced = name + .replace('Ø', 'O').replace('ø', 'o') + .replace("Æ", "AE").replace("æ", "ae") + return java.text.Normalizer.normalize(replaced, java.text.Normalizer.Form.NFD) + .replace(Regex("[^\\x00-\\x7F]"), "") + } } From c003c56de64d6af4c16802b0ef754a21404502dc Mon Sep 17 00:00:00 2001 From: Agustina Aldasoro Date: Thu, 19 Mar 2026 19:20:42 -0300 Subject: [PATCH 4/5] rename vars --- .../evomaster/core/solver/SmtLibGenerator.kt | 36 +++++++++---------- 1 file changed, 18 insertions(+), 18 deletions(-) diff --git a/core/src/main/kotlin/org/evomaster/core/solver/SmtLibGenerator.kt b/core/src/main/kotlin/org/evomaster/core/solver/SmtLibGenerator.kt index 7396aae19a..9b4dab9499 100644 --- a/core/src/main/kotlin/org/evomaster/core/solver/SmtLibGenerator.kt +++ b/core/src/main/kotlin/org/evomaster/core/solver/SmtLibGenerator.kt @@ -58,8 +58,8 @@ class SmtLibGenerator(private val schema: DbInfoDto, private val numberOfRows: I */ private fun appendTableDefinitions(smt: SMTLib) { for (table in schema.tables) { - val sanitizedTableName = convertToAscii(table.id.name) - val dataTypeName = "${StringUtils.capitalization(sanitizedTableName)}Row" + val smtTableName = convertToAscii(table.id.name) + val dataTypeName = "${StringUtils.capitalization(smtTableName)}Row" // Declare datatype for the table smt.addNode( @@ -68,7 +68,7 @@ class SmtLibGenerator(private val schema: DbInfoDto, private val numberOfRows: I // Declare constants for each row for (i in 1..numberOfRows) { - smt.addNode(DeclareConstSMTNode("${sanitizedTableName.lowercase()}$i", dataTypeName)) + smt.addNode(DeclareConstSMTNode("${smtTableName.lowercase()}$i", dataTypeName)) } } } @@ -92,10 +92,10 @@ class SmtLibGenerator(private val schema: DbInfoDto, private val numberOfRows: I * @param table The table for which unique constraints are added. */ private fun appendUniqueConstraints(smt: SMTLib, table: TableDto) { - val tableName = convertToAscii(table.id.name).lowercase() + val smtTableName = convertToAscii(table.id.name).lowercase() for (column in table.columns) { if (column.unique) { - val nodes = assertForDistinctField(convertToAscii(column.name), tableName) + val nodes = assertForDistinctField(convertToAscii(column.name), smtTableName) smt.addNodes(nodes) } } @@ -168,7 +168,7 @@ class SmtLibGenerator(private val schema: DbInfoDto, private val numberOfRows: I private fun appendBooleanConstraints(smt: SMTLib) { for (table in schema.tables) { - val tableName = convertToAscii(table.id.name).lowercase() + val smtTableName = convertToAscii(table.id.name).lowercase() for (column in table.columns) { if (column.type.equals("BOOLEAN", ignoreCase = true)) { val columnName = convertToAscii(column.name).uppercase() @@ -177,12 +177,12 @@ class SmtLibGenerator(private val schema: DbInfoDto, private val numberOfRows: I AssertSMTNode( OrAssertion( listOf( - EqualsAssertion(listOf("($columnName $tableName$i)", "\"true\"")), - EqualsAssertion(listOf("($columnName $tableName$i)", "\"True\"")), - EqualsAssertion(listOf("($columnName $tableName$i)", "\"TRUE\"")), - EqualsAssertion(listOf("($columnName $tableName$i)", "\"false\"")), - EqualsAssertion(listOf("($columnName $tableName$i)", "\"False\"")), - EqualsAssertion(listOf("($columnName $tableName$i)", "\"FALSE\"")) + EqualsAssertion(listOf("($columnName $smtTableName$i)", "\"true\"")), + EqualsAssertion(listOf("($columnName $smtTableName$i)", "\"True\"")), + EqualsAssertion(listOf("($columnName $smtTableName$i)", "\"TRUE\"")), + EqualsAssertion(listOf("($columnName $smtTableName$i)", "\"false\"")), + EqualsAssertion(listOf("($columnName $smtTableName$i)", "\"False\"")), + EqualsAssertion(listOf("($columnName $smtTableName$i)", "\"FALSE\"")) ) ) ) @@ -195,7 +195,7 @@ class SmtLibGenerator(private val schema: DbInfoDto, private val numberOfRows: I private fun appendTimestampConstraints(smt: SMTLib) { for (table in schema.tables) { - val tableName = convertToAscii(table.id.name).lowercase() + val smtTableName = convertToAscii(table.id.name).lowercase() for (column in table.columns) { if (column.type.equals("TIMESTAMP", ignoreCase = true)) { val columnName = convertToAscii(column.name).uppercase() @@ -206,7 +206,7 @@ class SmtLibGenerator(private val schema: DbInfoDto, private val numberOfRows: I smt.addNode( AssertSMTNode( GreaterThanOrEqualsAssertion( - "($columnName $tableName$i)", + "($columnName $smtTableName$i)", lowerBound.toString() ) ) @@ -214,7 +214,7 @@ class SmtLibGenerator(private val schema: DbInfoDto, private val numberOfRows: I smt.addNode( AssertSMTNode( LessThanOrEqualsAssertion( - "($columnName $tableName$i)", + "($columnName $smtTableName$i)", upperBound.toString() ) ) @@ -233,11 +233,11 @@ class SmtLibGenerator(private val schema: DbInfoDto, private val numberOfRows: I * @param table The table for which primary key constraints are added. */ private fun appendPrimaryKeyConstraints(smt: SMTLib, table: TableDto) { - val tableName = convertToAscii(table.id.name).lowercase() + val smtTableName = convertToAscii(table.id.name).lowercase() val primaryKeys = table.columns.filter { it.primaryKey } for (primaryKey in primaryKeys) { - val nodes = assertForDistinctField(convertToAscii(primaryKey.name), tableName) + val nodes = assertForDistinctField(convertToAscii(primaryKey.name), smtTableName) smt.addNodes(nodes) } } @@ -249,7 +249,7 @@ class SmtLibGenerator(private val schema: DbInfoDto, private val numberOfRows: I * @param tableName The name of the table. * @return A list of SMT nodes representing distinct assertions. */ - private fun assertForDistinctField(pkSelector: String, tableName: String): List { + private fun assertForDistinctField(pkSelector: String, t st: String): List { val nodes = mutableListOf() for (i in 1..numberOfRows) { for (j in i + 1..numberOfRows) { From 03099b497d7bafb223de464a60cf849073882481 Mon Sep 17 00:00:00 2001 From: Agustina Aldasoro Date: Thu, 19 Mar 2026 19:26:24 -0300 Subject: [PATCH 5/5] Fix type --- .../main/kotlin/org/evomaster/core/solver/SmtLibGenerator.kt | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/core/src/main/kotlin/org/evomaster/core/solver/SmtLibGenerator.kt b/core/src/main/kotlin/org/evomaster/core/solver/SmtLibGenerator.kt index 9b4dab9499..7795220e0b 100644 --- a/core/src/main/kotlin/org/evomaster/core/solver/SmtLibGenerator.kt +++ b/core/src/main/kotlin/org/evomaster/core/solver/SmtLibGenerator.kt @@ -249,7 +249,7 @@ class SmtLibGenerator(private val schema: DbInfoDto, private val numberOfRows: I * @param tableName The name of the table. * @return A list of SMT nodes representing distinct assertions. */ - private fun assertForDistinctField(pkSelector: String, t st: String): List { + private fun assertForDistinctField(pkSelector: String, tableName: String): List { val nodes = mutableListOf() for (i in 1..numberOfRows) { for (j in i + 1..numberOfRows) {