Add support for special characters #1479
+74
−43
There are no files selected for viewing
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
|
|
@@ -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.* | ||
|
|
||
| /** | ||
| * Generates SMT-LIB constraints from SQL queries and schema definitions. | ||
|
|
@@ -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 smtTableName = convertToAscii(table.id.name) | ||
| val dataTypeName = "${StringUtils.capitalization(smtTableName)}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("${smtTableName.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 smtTableName = convertToAscii(table.id.name).lowercase() | ||
| for (column in table.columns) { | ||
| if (column.unique) { | ||
| val nodes = assertForDistinctField(convertToAscii(column.name), smtTableName) | ||
| 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 { | ||
|
Collaborator
There was a problem hiding this comment. maybe not for this PR, but something to discuss as well with @jgaleotti , why is most of the code here relaying on |
||
| val visitor = SMTConditionVisitor(convertToAscii(table.id.name).lowercase(), emptyMap(), schema.tables, index) | ||
| return condition.accept(visitor, null) as SMTNode | ||
| } | ||
|
|
||
|
|
@@ -167,21 +168,21 @@ class SmtLibGenerator(private val schema: DbInfoDto, private val numberOfRows: I | |
|
|
||
| private fun appendBooleanConstraints(smt: SMTLib) { | ||
| for (table in schema.tables) { | ||
| 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() | ||
| 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\"")) | ||
| ) | ||
| ) | ||
| ) | ||
|
|
@@ -194,26 +195,26 @@ 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() | ||
|
Collaborator
There was a problem hiding this comment. there are so many calls to this |
||
| for (column in table.columns) { | ||
| if (column.type.equals("TIMESTAMP", ignoreCase = true)) { | ||
| val columnName = convertToAscii(column.name).uppercase() | ||
| val lowerBound = 0 // Example for Unix epoch start | ||
| val upperBound = 32503680000 // Example for year 3000 in seconds | ||
|
|
||
| for (i in 1..numberOfRows) { | ||
| smt.addNode( | ||
| AssertSMTNode( | ||
| GreaterThanOrEqualsAssertion( | ||
| "($columnName $smtTableName$i)", | ||
| lowerBound.toString() | ||
| ) | ||
| ) | ||
| ) | ||
| smt.addNode( | ||
| AssertSMTNode( | ||
| LessThanOrEqualsAssertion( | ||
| "($columnName $smtTableName$i)", | ||
| upperBound.toString() | ||
| ) | ||
| ) | ||
|
|
@@ -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 smtTableName = convertToAscii(table.id.name).lowercase() | ||
| val primaryKeys = table.columns.filter { it.primaryKey } | ||
|
|
||
| for (primaryKey in primaryKeys) { | ||
| val nodes = assertForDistinctField(convertToAscii(primaryKey.name), smtTableName) | ||
| 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 = 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)) | ||
|
|
||
| for (sourceColumn in foreignKey.sourceColumns) { | ||
| val nodes = assertForEqualsAny( | ||
| convertToAscii(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<String, String>, defaultTableName: String, condition: SqlCondition, index: Int): SMTNode { | ||
| val visitor = SMTConditionVisitor(convertToAscii(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 smtColumnName = convertToAscii(tableNameLower) | ||
| if (tablesMentioned.contains(tableNameLower)) { | ||
| for (i in 1..numberOfRows) { | ||
| smt.addNode(GetValueSMTNode("$smtColumnName$i")) | ||
| } | ||
| } | ||
| } | ||
|
|
@@ -537,22 +539,27 @@ 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(convertToAscii(c.name), smtType) | ||
| } | ||
| } | ||
|
|
||
| companion object { | ||
|
|
||
| // 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", | ||
|
|
||
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Oops, something went wrong.
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
add a comment to explain why this needs to be converted to ASCII