From ea5ae604abae77fa8db057303506356c060cc0db Mon Sep 17 00:00:00 2001 From: Agustina Aldasoro Date: Thu, 19 Mar 2026 17:43:47 -0300 Subject: [PATCH 1/8] 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/8] 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/8] 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/8] 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/8] 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) { From 47e2f90df345ca00f7551ff9e2febdaa546c0dd9 Mon Sep 17 00:00:00 2001 From: Agustina Aldasoro Date: Mon, 6 Apr 2026 19:00:14 -0300 Subject: [PATCH 6/8] Support for any language special characters --- .../org/evomaster/core/utils/StringUtils.kt | 78 ++++++++++++++++--- .../evomaster/core/utils/StringUtilsTest.kt | 62 +++++++++++++++ 2 files changed, 129 insertions(+), 11 deletions(-) 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 7cccbac206..7557b4ccfa 100644 --- a/core/src/main/kotlin/org/evomaster/core/utils/StringUtils.kt +++ b/core/src/main/kotlin/org/evomaster/core/utils/StringUtils.kt @@ -82,21 +82,77 @@ object StringUtils { } /** - * 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. + * Converts a string to a valid ASCII identifier for use in SMT-LIB. + * SMT-LIB unquoted symbols are restricted to ASCII. * - * This is needed because our test suite includes Norwegian APIs whose database schemas - * contain column and table names with Norwegian characters (Æ, Ø, Å). + * The conversion uses two complementary steps: + * 1. An explicit folding map for characters that have no canonical decomposition under NFD + * (e.g., Ø→O, Æ→AE, ß→ss, ð→d, þ→th, Ł→L, Œ→OE, ŋ→n, ħ→h, ı→i, …), + * covering non-decomposable characters from the Unicode Latin Extended blocks. + * 2. NFD normalization followed by stripping of non-ASCII combining marks, which handles + * all accented characters that do decompose (e.g., é→e, ü→u, ñ→n, Ä→A, ö→o, å→a). * - * 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. + * Any remaining non-ASCII characters (e.g., from non-Latin scripts) are dropped. */ 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) + val sb = StringBuilder(name.length * 2) + for (ch in name) { + sb.append(ASCII_FOLD_MAP[ch] ?: ch.toString()) + } + return java.text.Normalizer.normalize(sb.toString(), java.text.Normalizer.Form.NFD) .replace(Regex("[^\\x00-\\x7F]"), "") } + + /** + * Explicit ASCII replacements for Unicode characters that do not decompose under NFD normalization. + * Covers non-decomposable characters from the Unicode Latin-1 Supplement and Latin Extended-A/B blocks. + * Characters that DO decompose under NFD (e.g., Ä, ö, å, é, ü, ñ) are handled by the NFD step in + * [convertToAscii] and need no entry here. + */ + private val ASCII_FOLD_MAP: Map = mapOf( + // Latin-1 Supplement + 'Æ' to "AE", 'æ' to "ae", // AE ligature (Danish, Norwegian, Old English) + 'Ð' to "D", 'ð' to "d", // Eth (Icelandic, Old English) + 'Ø' to "O", 'ø' to "o", // O with stroke (Danish, Norwegian) + 'Þ' to "TH", 'þ' to "th", // Thorn (Icelandic, Old English) + 'ß' to "ss", // Sharp S (German) + // Latin Extended-A + 'Ħ' to "H", 'ħ' to "h", // H with stroke (Maltese) + 'ı' to "i", // Dotless i (Turkish, Azerbaijani) + 'IJ' to "IJ", 'ij' to "ij", // IJ digraph (Dutch) + 'ĸ' to "k", // Kra (Greenlandic) + 'Ł' to "L", 'ł' to "l", // L with stroke (Polish, Croatian, Sorbian) + 'Ŋ' to "N", 'ŋ' to "n", // Eng (Sami, African languages) + 'Œ' to "OE", 'œ' to "oe", // OE ligature (French) + 'Ŧ' to "T", 'ŧ' to "t", // T with stroke (Sami) + // Latin Extended-B + 'ƀ' to "b", 'Ƀ' to "B", // B with stroke + 'Ɓ' to "B", // B with hook + 'Ƈ' to "C", 'ƈ' to "c", // C with hook + 'Ɗ' to "D", // D with hook + 'ƌ' to "d", // D with topbar + 'Ƒ' to "F", 'ƒ' to "f", // F with hook + 'Ɠ' to "G", // G with hook + 'Ɨ' to "I", // I with stroke + 'Ƙ' to "K", 'ƙ' to "k", // K with hook + 'ƚ' to "l", // L with bar + 'Ɲ' to "N", 'ƞ' to "n", // N with hook / N with long right leg + 'Œ' to "OE", 'œ' to "oe", + 'Ƥ' to "P", 'ƥ' to "p", // P with hook + 'ƫ' to "t", // T with palatal hook + 'Ƭ' to "T", 'ƭ' to "t", // T with hook + 'Ʈ' to "T", // T with retroflex hook + 'Ư' to "U", 'ư' to "u", // U with horn (Vietnamese) + 'Ʋ' to "V", // V with hook + 'Ƴ' to "Y", 'ƴ' to "y", // Y with hook + 'Ƶ' to "Z", 'ƶ' to "z", // Z with stroke + 'Ǝ' to "E", 'ǝ' to "e", // Reversed E / Schwa + 'Ɵ' to "O", // O with middle tilde + 'Ȼ' to "C", 'ȼ' to "c", // C with stroke + 'Ɇ' to "E", 'ɇ' to "e", // E with stroke + 'Ɉ' to "J", 'ɉ' to "j", // J with stroke + 'Ɋ' to "Q", 'ɋ' to "q", // Q with hook tail + 'Ɍ' to "R", 'ɍ' to "r", // R with stroke + 'Ɏ' to "Y", 'ɏ' to "y", // Y with stroke + ) } diff --git a/core/src/test/kotlin/org/evomaster/core/utils/StringUtilsTest.kt b/core/src/test/kotlin/org/evomaster/core/utils/StringUtilsTest.kt index 6575a6f981..ebe7bbb7d5 100644 --- a/core/src/test/kotlin/org/evomaster/core/utils/StringUtilsTest.kt +++ b/core/src/test/kotlin/org/evomaster/core/utils/StringUtilsTest.kt @@ -19,4 +19,66 @@ class StringUtilsTest{ assertEquals(", Hello",lines[2]) assertEquals(", C, D",lines[3]) } + + @Test + fun testConvertToAsciiPlainAsciiUnchanged() { + assertEquals("hello_world", StringUtils.convertToAscii("hello_world")) + assertEquals("FooBar123", StringUtils.convertToAscii("FooBar123")) + } + + @Test + fun testConvertToAsciiNorwegianDanish() { + // Ø/ø and Æ/æ do not decompose under NFD — handled by explicit map + assertEquals("O", StringUtils.convertToAscii("Ø")) + assertEquals("o", StringUtils.convertToAscii("ø")) + assertEquals("AE", StringUtils.convertToAscii("Æ")) + assertEquals("ae", StringUtils.convertToAscii("æ")) + // Å/å decomposes under NFD + assertEquals("A", StringUtils.convertToAscii("Å")) + assertEquals("a", StringUtils.convertToAscii("å")) + } + + @Test + fun testConvertToAsciiSwedishGerman() { + // These all decompose under NFD (base letter + combining diacritic) + assertEquals("A", StringUtils.convertToAscii("Ä")) + assertEquals("a", StringUtils.convertToAscii("ä")) + assertEquals("O", StringUtils.convertToAscii("Ö")) + assertEquals("o", StringUtils.convertToAscii("ö")) + assertEquals("U", StringUtils.convertToAscii("Ü")) + assertEquals("u", StringUtils.convertToAscii("ü")) + // ß does not decompose under NFD — handled by explicit map + assertEquals("ss", StringUtils.convertToAscii("ß")) + } + + @Test + fun testConvertToAsciiIcelandic() { + assertEquals("D", StringUtils.convertToAscii("Ð")) + assertEquals("d", StringUtils.convertToAscii("ð")) + assertEquals("TH", StringUtils.convertToAscii("Þ")) + assertEquals("th", StringUtils.convertToAscii("þ")) + } + + @Test + fun testConvertToAsciiPolishFrench() { + assertEquals("L", StringUtils.convertToAscii("Ł")) + assertEquals("l", StringUtils.convertToAscii("ł")) + assertEquals("OE", StringUtils.convertToAscii("Œ")) + assertEquals("oe", StringUtils.convertToAscii("œ")) + } + + @Test + fun testConvertToAsciiOtherAccented() { + // Common accented characters that decompose under NFD + assertEquals("e", StringUtils.convertToAscii("é")) + assertEquals("e", StringUtils.convertToAscii("è")) + assertEquals("n", StringUtils.convertToAscii("ñ")) + assertEquals("c", StringUtils.convertToAscii("ç")) + } + + @Test + fun testConvertToAsciiMixedString() { + assertEquals("StromsAElv", StringUtils.convertToAscii("StrømsÆlv")) + assertEquals("Malostranke_namesti", StringUtils.convertToAscii("Malostranké_náměstí")) + } } \ No newline at end of file From 3caf6fdbe6a07e3e84353e394b63e762aaa82cb2 Mon Sep 17 00:00:00 2001 From: Agustina Aldasoro Date: Mon, 6 Apr 2026 19:24:40 -0300 Subject: [PATCH 7/8] Create SmtTable class to handle name conversion --- .../evomaster/core/solver/SmtLibGenerator.kt | 134 +++++++++--------- .../org/evomaster/core/solver/SmtTable.kt | 30 ++++ 2 files changed, 94 insertions(+), 70 deletions(-) create mode 100644 core/src/main/kotlin/org/evomaster/core/solver/SmtTable.kt 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 7795220e0b..26c76bb849 100644 --- a/core/src/main/kotlin/org/evomaster/core/solver/SmtLibGenerator.kt +++ b/core/src/main/kotlin/org/evomaster/core/solver/SmtLibGenerator.kt @@ -11,7 +11,6 @@ import org.evomaster.client.java.controller.api.dto.database.schema.DbInfoDto import org.evomaster.client.java.controller.api.dto.database.schema.ForeignKeyDto import org.evomaster.client.java.controller.api.dto.database.schema.TableDto import org.evomaster.core.logging.LoggingUtil -import org.evomaster.core.utils.StringUtils import org.evomaster.dbconstraint.ConstraintDatabaseType import org.evomaster.dbconstraint.ast.SqlCondition import net.sf.jsqlparser.JSQLParserException @@ -31,6 +30,9 @@ class SmtLibGenerator(private val schema: DbInfoDto, private val numberOfRows: I private var parser = JSqlConditionParser() + private val smtTables: List = schema.tables.map { SmtTable(it) } + private val smtTableByOriginalName: Map = smtTables.associateBy { it.originalName } + /** * Main method to generate SMT-LIB representation from SQL query. * @@ -57,18 +59,15 @@ class SmtLibGenerator(private val schema: DbInfoDto, private val numberOfRows: I * @param smt The SMT-LIB object to which table definitions are added. */ private fun appendTableDefinitions(smt: SMTLib) { - for (table in schema.tables) { - val smtTableName = convertToAscii(table.id.name) - val dataTypeName = "${StringUtils.capitalization(smtTableName)}Row" - + for (smtTable in smtTables) { // Declare datatype for the table smt.addNode( - DeclareDatatypeSMTNode(dataTypeName, getConstructors(table)) + DeclareDatatypeSMTNode(smtTable.dataTypeName, getConstructors(smtTable)) ) // Declare constants for each row for (i in 1..numberOfRows) { - smt.addNode(DeclareConstSMTNode("${smtTableName.lowercase()}$i", dataTypeName)) + smt.addNode(DeclareConstSMTNode("${smtTable.smtName}$i", smtTable.dataTypeName)) } } } @@ -79,9 +78,9 @@ class SmtLibGenerator(private val schema: DbInfoDto, private val numberOfRows: I * @param smt The SMT-LIB object to which table constraints are added. */ private fun appendTableConstraints(smt: SMTLib) { - for (table in schema.tables) { - appendUniqueConstraints(smt, table) - appendCheckConstraints(smt, table) + for (smtTable in smtTables) { + appendUniqueConstraints(smt, smtTable) + appendCheckConstraints(smt, smtTable) } } @@ -89,13 +88,12 @@ class SmtLibGenerator(private val schema: DbInfoDto, private val numberOfRows: I * Appends unique constraints for each table to the SMT-LIB. * * @param smt The SMT-LIB object to which unique constraints are added. - * @param table The table for which unique constraints are added. + * @param smtTable The table for which unique constraints are added. */ - private fun appendUniqueConstraints(smt: SMTLib, table: TableDto) { - val smtTableName = convertToAscii(table.id.name).lowercase() - for (column in table.columns) { + private fun appendUniqueConstraints(smt: SMTLib, smtTable: SmtTable) { + for (column in smtTable.dto.columns) { if (column.unique) { - val nodes = assertForDistinctField(convertToAscii(column.name), smtTableName) + val nodes = assertForDistinctField(smtTable.smtColumnName(column.name), smtTable.smtName) smt.addNodes(nodes) } } @@ -105,14 +103,14 @@ class SmtLibGenerator(private val schema: DbInfoDto, private val numberOfRows: I * Appends check constraints for each table to the SMT-LIB. * * @param smt The SMT-LIB object to which check constraints are added. - * @param table The table for which check constraints are added. + * @param smtTable The table for which check constraints are added. */ - private fun appendCheckConstraints(smt: SMTLib, table: TableDto) { - for (check in table.tableCheckExpressions) { + private fun appendCheckConstraints(smt: SMTLib, smtTable: SmtTable) { + for (check in smtTable.dto.tableCheckExpressions) { try { val condition: SqlCondition = parser.parse(check.sqlCheckExpression, toDBType(schema.databaseType)) for (i in 1..numberOfRows) { - val constraint: SMTNode = parseCheckExpression(table, condition, i) + val constraint: SMTNode = parseCheckExpression(smtTable, condition, i) smt.addNode(constraint) } } catch (e: SqlConditionParserException) { @@ -126,13 +124,13 @@ class SmtLibGenerator(private val schema: DbInfoDto, private val numberOfRows: I /** * Parses a check expression and returns the corresponding SMT node. * - * @param table The table containing the check expression. + * @param smtTable The table containing the check expression. * @param condition The SQL condition to be parsed. * @param index The index of the row. * @return The corresponding SMT node. */ - private fun parseCheckExpression(table: TableDto, condition: SqlCondition, index: Int): SMTNode { - val visitor = SMTConditionVisitor(convertToAscii(table.id.name).lowercase(), emptyMap(), schema.tables, index) + private fun parseCheckExpression(smtTable: SmtTable, condition: SqlCondition, index: Int): SMTNode { + val visitor = SMTConditionVisitor(smtTable.smtName, emptyMap(), schema.tables, index) return condition.accept(visitor, null) as SMTNode } @@ -160,29 +158,28 @@ class SmtLibGenerator(private val schema: DbInfoDto, private val numberOfRows: I * @param smt The SMT-LIB object to which key constraints are added. */ private fun appendKeyConstraints(smt: SMTLib) { - for (table in schema.tables) { - appendPrimaryKeyConstraints(smt, table) - appendForeignKeyConstraints(smt, table) + for (smtTable in smtTables) { + appendPrimaryKeyConstraints(smt, smtTable) + appendForeignKeyConstraints(smt, smtTable) } } private fun appendBooleanConstraints(smt: SMTLib) { - for (table in schema.tables) { - val smtTableName = convertToAscii(table.id.name).lowercase() - for (column in table.columns) { + for (smtTable in smtTables) { + for (column in smtTable.dto.columns) { if (column.type.equals("BOOLEAN", ignoreCase = true)) { - val columnName = convertToAscii(column.name).uppercase() + val columnName = smtTable.smtColumnName(column.name).uppercase() for (i in 1..numberOfRows) { smt.addNode( AssertSMTNode( OrAssertion( listOf( - 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\"")) + EqualsAssertion(listOf("($columnName ${smtTable.smtName}$i)", "\"true\"")), + EqualsAssertion(listOf("($columnName ${smtTable.smtName}$i)", "\"True\"")), + EqualsAssertion(listOf("($columnName ${smtTable.smtName}$i)", "\"TRUE\"")), + EqualsAssertion(listOf("($columnName ${smtTable.smtName}$i)", "\"false\"")), + EqualsAssertion(listOf("($columnName ${smtTable.smtName}$i)", "\"False\"")), + EqualsAssertion(listOf("($columnName ${smtTable.smtName}$i)", "\"FALSE\"")) ) ) ) @@ -194,11 +191,10 @@ class SmtLibGenerator(private val schema: DbInfoDto, private val numberOfRows: I } private fun appendTimestampConstraints(smt: SMTLib) { - for (table in schema.tables) { - val smtTableName = convertToAscii(table.id.name).lowercase() - for (column in table.columns) { + for (smtTable in smtTables) { + for (column in smtTable.dto.columns) { if (column.type.equals("TIMESTAMP", ignoreCase = true)) { - val columnName = convertToAscii(column.name).uppercase() + val columnName = smtTable.smtColumnName(column.name).uppercase() val lowerBound = 0 // Example for Unix epoch start val upperBound = 32503680000 // Example for year 3000 in seconds @@ -206,7 +202,7 @@ class SmtLibGenerator(private val schema: DbInfoDto, private val numberOfRows: I smt.addNode( AssertSMTNode( GreaterThanOrEqualsAssertion( - "($columnName $smtTableName$i)", + "($columnName ${smtTable.smtName}$i)", lowerBound.toString() ) ) @@ -214,7 +210,7 @@ class SmtLibGenerator(private val schema: DbInfoDto, private val numberOfRows: I smt.addNode( AssertSMTNode( LessThanOrEqualsAssertion( - "($columnName $smtTableName$i)", + "($columnName ${smtTable.smtName}$i)", upperBound.toString() ) ) @@ -230,14 +226,13 @@ class SmtLibGenerator(private val schema: DbInfoDto, private val numberOfRows: I * Appends primary key constraints for each table to the SMT-LIB. * * @param smt The SMT-LIB object to which primary key constraints are added. - * @param table The table for which primary key constraints are added. + * @param smtTable The table for which primary key constraints are added. */ - private fun appendPrimaryKeyConstraints(smt: SMTLib, table: TableDto) { - val smtTableName = convertToAscii(table.id.name).lowercase() - val primaryKeys = table.columns.filter { it.primaryKey } + private fun appendPrimaryKeyConstraints(smt: SMTLib, smtTable: SmtTable) { + val primaryKeys = smtTable.dto.columns.filter { it.primaryKey } for (primaryKey in primaryKeys) { - val nodes = assertForDistinctField(convertToAscii(primaryKey.name), smtTableName) + val nodes = assertForDistinctField(smtTable.smtColumnName(primaryKey.name), smtTable.smtName) smt.addNodes(nodes) } } @@ -272,20 +267,19 @@ class SmtLibGenerator(private val schema: DbInfoDto, private val numberOfRows: I * Appends foreign key constraints for each table to the SMT-LIB. * * @param smt The SMT-LIB object to which foreign key constraints are added. - * @param table The table for which foreign key constraints are added. + * @param smtTable The table for which foreign key constraints are added. */ - private fun appendForeignKeyConstraints(smt: SMTLib, table: TableDto) { - val sourceTableName = convertToAscii(table.id.name).lowercase() - - for (foreignKey in table.foreignKeys) { - val referencedTable = findReferencedTable(foreignKey) - val referencedTableName = convertToAscii(referencedTable.id.name).lowercase() - val referencedColumnSelector = convertToAscii(findReferencedPKSelector(table, referencedTable, foreignKey)) + private fun appendForeignKeyConstraints(smt: SMTLib, smtTable: SmtTable) { + for (foreignKey in smtTable.dto.foreignKeys) { + val referencedSmtTable = findReferencedSmtTable(foreignKey) + val referencedColumnSelector = referencedSmtTable.smtColumnName( + findReferencedPKSelector(smtTable.dto, referencedSmtTable.dto, foreignKey) + ) for (sourceColumn in foreignKey.sourceColumns) { val nodes = assertForEqualsAny( - convertToAscii(sourceColumn), sourceTableName, - referencedColumnSelector, referencedTableName + smtTable.smtColumnName(sourceColumn), smtTable.smtName, + referencedColumnSelector, referencedSmtTable.smtName ) smt.addNodes(nodes) } @@ -353,13 +347,13 @@ class SmtLibGenerator(private val schema: DbInfoDto, private val numberOfRows: I } /** - * Finds the referenced table based on the foreign key. + * Finds the [SmtTable] for the table referenced by the given foreign key. * * @param foreignKey The foreign key constraint. - * @return The referenced table. + * @return The referenced [SmtTable]. */ - private fun findReferencedTable(foreignKey: ForeignKeyDto): TableDto { - return schema.tables.firstOrNull { it.id.name.equals(foreignKey.targetTable, ignoreCase = true) } + private fun findReferencedSmtTable(foreignKey: ForeignKeyDto): SmtTable { + return smtTableByOriginalName[foreignKey.targetTable.lowercase()] ?: throw RuntimeException("Referenced table not found: ${foreignKey.targetTable}") } @@ -435,7 +429,9 @@ 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(convertToAscii(defaultTableName), tableAliases, schema.tables, index) + val smtDefaultTableName = smtTableByOriginalName[defaultTableName.lowercase()]?.smtName + ?: convertToAscii(defaultTableName) + val visitor = SMTConditionVisitor(smtDefaultTableName, tableAliases, schema.tables, index) return condition.accept(visitor, null) as SMTNode } @@ -518,12 +514,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 smtColumnName = convertToAscii(tableNameLower) - if (tablesMentioned.contains(tableNameLower)) { + for (smtTable in smtTables) { + if (tablesMentioned.contains(smtTable.originalName)) { for (i in 1..numberOfRows) { - smt.addNode(GetValueSMTNode("$smtColumnName$i")) + smt.addNode(GetValueSMTNode("${smtTable.smtName}$i")) } } } @@ -532,14 +526,14 @@ class SmtLibGenerator(private val schema: DbInfoDto, private val numberOfRows: I /** * Gets the constructors for a table's columns to be used in SMT-LIB. * - * @param table The table for which constructors are generated. + * @param smtTable The table for which constructors are generated. * @return A list of SMT nodes for column constructors. */ - private fun getConstructors(table: TableDto): List { - return table.columns.map { c -> + private fun getConstructors(smtTable: SmtTable): List { + return smtTable.dto.columns.map { c -> val smtType = TYPE_MAP[c.type.uppercase()] ?: throw RuntimeException("Unsupported column type: ${c.type}") - DeclareConstSMTNode(convertToAscii(c.name), smtType) + DeclareConstSMTNode(smtTable.smtColumnName(c.name), smtType) } } diff --git a/core/src/main/kotlin/org/evomaster/core/solver/SmtTable.kt b/core/src/main/kotlin/org/evomaster/core/solver/SmtTable.kt new file mode 100644 index 0000000000..06b5e5bdc8 --- /dev/null +++ b/core/src/main/kotlin/org/evomaster/core/solver/SmtTable.kt @@ -0,0 +1,30 @@ +package org.evomaster.core.solver + +import org.evomaster.client.java.controller.api.dto.database.schema.TableDto +import org.evomaster.core.utils.StringUtils +import org.evomaster.core.utils.StringUtils.convertToAscii + +/** + * A view of a [TableDto] with pre-computed SMT-safe identifiers. + * + * All table and column names are converted to ASCII once at construction time, + * avoiding repeated [convertToAscii] calls throughout [SmtLibGenerator]. + */ +class SmtTable(val dto: TableDto) { + + /** Original lowercase table name, used to match against SQL query table references. */ + val originalName: String = dto.id.name.lowercase() + + /** SMT-safe lowercase identifier used in row constant declarations (e.g., "person1", "person2"). */ + val smtName: String = convertToAscii(dto.id.name).lowercase() + + /** SMT-LIB datatype name for this table's rows (e.g., "PersonRow"). */ + val dataTypeName: String = "${StringUtils.capitalization(smtName)}Row" + + private val columnSmtNames: Map = + dto.columns.associate { col -> col.name to convertToAscii(col.name) } + + /** Returns the SMT-safe identifier for the given column name. */ + fun smtColumnName(columnName: String): String = + columnSmtNames[columnName] ?: convertToAscii(columnName) +} From 3f39f8bc5d70e78eab4f5807aefc60a741a1e606 Mon Sep 17 00:00:00 2001 From: Agustina Aldasoro Date: Mon, 6 Apr 2026 19:25:44 -0300 Subject: [PATCH 8/8] add comment --- .../kotlin/org/evomaster/core/solver/SMTConditionVisitor.kt | 6 ++++++ 1 file changed, 6 insertions(+) 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 b92704e159..91364728db 100644 --- a/core/src/main/kotlin/org/evomaster/core/solver/SMTConditionVisitor.kt +++ b/core/src/main/kotlin/org/evomaster/core/solver/SMTConditionVisitor.kt @@ -27,6 +27,12 @@ class SMTConditionVisitor( /** * Constructs a column reference string for SMT-LIB from a table name and column name. * + * Both names are converted to ASCII because SMT-LIB unquoted symbols only allow ASCII characters. + * Table and column names may come directly from SQL query text (e.g., a WHERE clause), which can + * contain non-ASCII characters if the schema uses them. The conversion must happen here because, + * unlike schema-derived names that are pre-converted via [SmtTable], query-derived names are + * parsed at runtime from raw SQL strings. + * * @param tableName The name of the table. * @param columnName The name of the column. * @return The SMT-LIB column reference string.