Add comments

Author: agusaldasoro

core-extra/solver/src/main/java/org/evomaster/solver/smtlib/SMTResultParser.java

@@ -45,6 +45,9 @@ public static Z3Solution parseZ3Response(String z3Response) {
         String[] lines = z3Response.split("\n");
 
         for (String line : lines) {
+            // Defensive: Z3DockerExecutor already classifies 'unsat'/'unknown' before invoking this
+            // parser, so in practice only 'sat' models reach here. This guard is kept as a safety net
+            // in case the parser is ever called directly with an unsat response.
             if (line.startsWith("unsat")) {
                 throw new RuntimeException("Unsatisfiable problem");
             }

core/src/main/kotlin/org/evomaster/core/EMConfig.kt

@@ -1988,6 +1988,16 @@ class EMConfig {
     @Min(0.0)
     var sqlZ3TimeoutMs = DEFAULT_SQL_Z3_TIMEOUT_MS
 
+    @Experimental
+    @Cfg("Number of rows the Z3 solver generates per table when solving a failed SQL query. " +
+            "The default of 1 is sufficient for the currently supported queries; generating a single " +
+            "row per table already forces the query to return a non-empty result. This will need to be " +
+            "increased once support for more complex JOINs (matching arbitrary row combinations, not just " +
+            "the diagonal pairing of row i with row i) is added. Only meaningful when generateSqlDataWithZ3=true.")
+    @DependsOnTrueFor("generateSqlDataWithZ3")
+    @Min(1.0)
+    var sqlZ3NumberOfRows = 1
+
     @Cfg("Enable EvoMaster to generate SQL data with direct accesses to the database. Use a search algorithm")
     @DependsOnFalseFor("blackBox")
     var generateSqlDataWithSearch = true

core/src/main/kotlin/org/evomaster/core/problem/api/service/ApiWsStructureMutator.kt

@@ -442,7 +442,10 @@ abstract class ApiWsStructureMutator : StructureMutator() {
 
         val newActions = mutableListOf<List<SqlAction>>()
         for (query in failedWhereQueries) {
-            val newActionsForQuery = z3Solver.solve(schemaDto, query)
+            // numberOfRows is kept at 1 by default, which is enough to force a non-empty result for the
+            // currently supported queries. It is configurable to allow experimenting with more rows once
+            // support for complex JOINs (arbitrary row combinations) is added.
+            val newActionsForQuery = z3Solver.solve(schemaDto, query, config.sqlZ3NumberOfRows)
             newActions.addAll(mutableListOf(newActionsForQuery))
             ind.addInitializingDbActions(actions = newActionsForQuery)
         }

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

@@ -167,7 +167,16 @@ class SMTLibZ3DbConstraintSolver() : DbConstraintSolver {
 
         val smtlibGenStart = System.currentTimeMillis()
         val generator = SmtLibGenerator(schemaDto, numberOfRows)
-        val smtLib = generator.generateSMT(queryStatement)
+        // SMT-LIB generation can throw for unsupported column types or query shapes it cannot handle
+        // (e.g. a cast failure on an unexpected statement structure). Degrade gracefully to an empty
+        // result instead of letting the exception propagate into the structure mutator.
+        val smtLib = try {
+            generator.generateSMT(queryStatement)
+        } catch (e: RuntimeException) {
+            LoggingUtil.getInfoLogger().warn("SQL-Z3: failed to generate SMT-LIB for query '$sqlQuery': ${e.message}")
+            stats?.reportSqlZ3ParseFailure()
+            return emptyList()
+        }
         val smtlibBytes = smtLib.toString().toByteArray(StandardCharsets.UTF_8).size
         val smtlibGenMs = System.currentTimeMillis() - smtlibGenStart
         stats?.reportSqlZ3SmtlibGenTime(smtlibGenMs, smtlibBytes)
@@ -325,6 +334,18 @@ class SMTLibZ3DbConstraintSolver() : DbConstraintSolver {
         return value.equals("True", ignoreCase = true)
     }
 
+    /**
+     * Whether the given column's SQL type (as reported in [ColumnDto.type]) equals [expectedType],
+     * compared case-insensitively as a raw string.
+     *
+     * CAVEAT: this relies on [ColumnDto.type] containing the exact spelling passed in (currently
+     * "BOOLEAN" and "TIMESTAMP"). It is needed because the SMT sort alone cannot recover these types
+     * (BOOLEAN is encoded as an SMT String, TIMESTAMP as an SMT Int), so gene reconstruction must
+     * consult the original SQL type. The set of type spellings recognized here must stay consistent
+     * with [SmtLibGenerator.TYPE_MAP]; if a backend reports a variant spelling (e.g. "BOOL" or
+     * "TIMESTAMP WITHOUT TIME ZONE"), the special handling is silently skipped. Consolidating these
+     * type vocabularies into a single source of truth is future work.
+     */
     private fun hasColumnType(
         schemaDto: DbInfoDto,
         table: Table,
@@ -346,13 +367,17 @@ class SMTLibZ3DbConstraintSolver() : DbConstraintSolver {
     }
 
     /**
-     * Extracts the table name from the key by removing the last character (index).
+     * Extracts the table name from a row-constant key by removing the trailing row index.
+     *
+     * Row constants are named "${smtName}${i}" (e.g. "users1", "users2"). The trailing digits are
+     * stripped so this works for any number of rows (e.g. "users10" -> "users"), not just single-digit
+     * indices. Note: this still assumes table names themselves do not end in a digit.
      *
      * @param key The key containing the table name and index.
      * @return The extracted table name.
      */
     private fun getTableName(key: String): String {
-        return key.substring(0, key.length - 1)
+        return key.replace(Regex("\\d+$"), "")
     }
 
     /**
@@ -445,6 +470,13 @@ class SMTLibZ3DbConstraintSolver() : DbConstraintSolver {
     /**
      * Maps column types to ColumnDataType.
      *
+     * FUTURE WORK: this recognizes only a small subset of SQL type spellings and falls back to
+     * CHARACTER_VARYING for everything else. It is one of three independent type vocabularies that
+     * interpret [ColumnDto.type] — the others being [SmtLibGenerator.TYPE_MAP] (SQL type -> SMT sort)
+     * and [hasColumnType] (BOOLEAN/TIMESTAMP special-casing). These can silently disagree when a
+     * backend reports a variant spelling. They should be consolidated into a single source of truth
+     * so that generation and interpretation cannot drift; see the note on [hasColumnType].
+     *
      * @param type The column type as a string.
      * @return The corresponding ColumnDataType.
      */

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

@@ -312,6 +312,11 @@ class SmtLibGenerator(private val schema: DbInfoDto, private val numberOfRows: I
                 findReferencedPKSelector(smtTable.dto, referencedSmtTable.dto, foreignKey)
             )
 
+            // KNOWN LIMITATION: composite foreign keys are not fully supported. Each source column is
+            // matched independently against a single referenced column, rather than constraining the
+            // whole tuple of source columns to match a referenced tuple. This is correct for
+            // single-column FKs (the common case) but under-models multi-column FKs. Fully supporting
+            // composite FKs (as a tuple-level OR over referenced rows) is future work.
             for (sourceColumn in foreignKey.sourceColumns) {
                 val nodes = assertForEqualsAny(
                     smtTable.smtColumnName(sourceColumn), smtTable.smtName,
@@ -442,10 +447,18 @@ class SmtLibGenerator(private val schema: DbInfoDto, private val numberOfRows: I
                 for (join in joins) {
                     val onExpressions = join.onExpressions
                     if (onExpressions.isNotEmpty()) {
+                        // KNOWN LIMITATION: only the first ON expression is used; a composite ON
+                        // (e.g. "a = b AND c = d") drops all but the first conjunct.
                         val onExpression = onExpressions.elementAt(0)
                         try {
                             val condition = parser.parse(onExpression.toString(), toDBType(schema.databaseType))
                             val tableFromQuery = TablesNamesFinder().getTables(sqlQuery as Statement).first()
+                            // KNOWN LIMITATION: the ON condition is translated with the SAME row index on
+                            // both sides ("diagonal pairing"): row i of one table is matched only with row i
+                            // of the other. This is sufficient at the default numberOfRows=1 to force a
+                            // non-empty JOIN, but it does not model full INNER JOIN semantics: for
+                            // numberOfRows>=2 it never explores mismatched-index pairs (e.g. users2 with
+                            // products1). Matching arbitrary row combinations is future work.
                             for (i in 1..numberOfRows) {
                                 val constraint = parseQueryCondition(tableAliases, tableFromQuery, condition, i)
                                 smt.addNode(constraint)
@@ -591,7 +604,11 @@ class SmtLibGenerator(private val schema: DbInfoDto, private val numberOfRows: I
 
     companion object {
 
-        // Maps database column types to SMT-LIB types
+        // Maps database column types to SMT-LIB types.
+        // FUTURE WORK: this is one of three independent type vocabularies interpreting ColumnDto.type
+        // (the others are SMTLibZ3DbConstraintSolver.getColumnDataType and .hasColumnType). They can
+        // silently disagree when a backend reports a variant spelling; consolidating them into a single
+        // source of truth is future work (see the note on SMTLibZ3DbConstraintSolver.hasColumnType).
         private val TYPE_MAP = mapOf(
             "BIGINT" to "Int",
             "BIT" to "Int",
@@ -602,6 +619,9 @@ class SmtLibGenerator(private val schema: DbInfoDto, private val numberOfRows: I
             "INT8" to "Int",
             "TINYINT" to "Int",
             "SMALLINT" to "Int",
+            // KNOWN LIMITATION: NUMERIC is mapped to Int, so any fractional part is truncated. This is
+            // inconsistent with DECIMAL (mapped to Real). Mapping NUMERIC to Real (to preserve decimals)
+            // is future work.
             "NUMERIC" to "Int",
             "SERIAL" to "Int",
             "SMALLSERIAL" to "Int",

docs/options.md

@@ -347,6 +347,7 @@ There are 3 types of options:
 |`seedTestCasesPath`| __String__. File path where the seeded test cases are located. *Default value*: `postman.postman_collection.json`.|
 |`skipAIModelUpdateWhenResponseIs5xx`| __Boolean__. Determines whether the AI response classifier skips model updates when the response indicates a server-side error with status code 5xx. *Default value*: `false`.|
 |`skipAIModelUpdateWhenResponseIsNot2xxOr400`| __Boolean__. Determines whether the AI response classifier skips model updates when the response is not 2xx or 400. *Default value*: `false`.|
+|`sqlZ3NumberOfRows`| __Int__. Number of rows the Z3 solver generates per table when solving a failed SQL query. The default of 1 is sufficient for the currently supported queries; generating a single row per table already forces the query to return a non-empty result. This will need to be increased once support for more complex JOINs (matching arbitrary row combinations, not just the diagonal pairing of row i with row i) is added. Only meaningful when generateSqlDataWithZ3=true. *Constraints*: `min=1.0`. *Depends on*: `generateSqlDataWithZ3=true`. *Default value*: `1`.|
 |`sqlZ3TimeoutMs`| __Int__. Soft timeout, in milliseconds, for each Z3 solver invocation when generating SQL data. If a query exceeds it, Z3 returns 'unknown' for that query instead of running unbounded. A value of 0 disables the timeout. Only meaningful when generateSqlDataWithZ3=true. *Constraints*: `min=0.0`. *Depends on*: `generateSqlDataWithZ3=true`. *Default value*: `5000`.|
 |`statusOracles`| __Boolean__. Lightweight checks on HTTP status codes, e.g., a GET should not return a 201 Created. *Default value*: `false`.|
 |`structureMutationProFS`| __Double__. Specify a probability of applying structure mutator during the focused search. *Constraints*: `probability 0.0-1.0`. *Default value*: `0.0`.|