Add stats

Author: agusaldasoro

core/src/main/kotlin/org/evomaster/core/search/service/Statistics.kt

@@ -97,6 +97,7 @@ class Statistics : SearchListener {
     private var sqlZ3UnknownCount = 0
     private var sqlZ3ErrorCount = 0
     private var sqlZ3ParseFailureCount = 0
+    private var sqlZ3PartialTranslationCount = 0
     private var sqlZ3TimeMs = 0L
     private var sqlZ3SmtlibGenTimeMs = 0L
     private val sqlZ3SmtlibSizeBytes = IncrementalAverage()
@@ -276,6 +277,15 @@ class Statistics : SearchListener {
         sqlZ3ParseFailureCount++
     }
 
+    /**
+     * A query whose WHERE/JOIN condition could not be fully translated to SMT-LIB (the untranslatable
+     * part was dropped). Counted independently of the SAT/UNSAT outcome, since the weakened formula is
+     * usually still SAT: the generated data may not satisfy the original query.
+     */
+    fun reportSqlZ3PartialTranslation() {
+        sqlZ3PartialTranslationCount++
+    }
+
     fun reportSqlZ3SmtlibGenTime(ms: Long, sizeBytes: Int) {
         sqlZ3SmtlibGenTimeMs += ms
         sqlZ3SmtlibSizeBytes.addValue(sizeBytes)
@@ -484,6 +494,7 @@ class Statistics : SearchListener {
                 add(Pair("sqlZ3Unknown", "$sqlZ3UnknownCount"))
                 add(Pair("sqlZ3Errors", "$sqlZ3ErrorCount"))
                 add(Pair("sqlZ3ParseFailures", "$sqlZ3ParseFailureCount"))
+                add(Pair("sqlZ3PartialTranslations", "$sqlZ3PartialTranslationCount"))
                 add(Pair("sqlZ3TotalMs", "$sqlZ3TimeMs"))
                 add(Pair("sqlZ3SmtlibGenTotalMs", "$sqlZ3SmtlibGenTimeMs"))
                 add(Pair("sqlZ3AvgSmtlibSizeBytes", "%.1f".format(sqlZ3SmtlibSizeBytes.mean)))

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

@@ -187,6 +187,13 @@ class SMTLibZ3DbConstraintSolver() : DbConstraintSolver {
         val smtlibGenMs = System.currentTimeMillis() - smtlibGenStart
         stats?.reportSqlZ3SmtlibGenTime(smtlibGenMs, smtlibBytes)
 
+        // If a WHERE/JOIN condition could not be translated, it was dropped from the SMT problem, so the
+        // generated data may not satisfy the original query. Record it: this failure mode is otherwise
+        // invisible in the stats (Z3 typically still returns SAT on the weakened formula).
+        if (generator.skippedQueryConstraints > 0) {
+            stats?.reportSqlZ3PartialTranslation()
+        }
+
         val fileName = storeToTmpFile(smtLib)
 
         val z3Start = System.currentTimeMillis()

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

@@ -32,6 +32,15 @@ class SmtLibGenerator(private val schema: DbInfoDto, private val numberOfRows: I
 
     private var parser = JSqlConditionParser()
 
+    /**
+     * Number of query constraints (WHERE conditions, JOIN ON conditions) that could not be translated
+     * to SMT-LIB and were skipped during [generateSMT]. When greater than 0, the generated formula is
+     * weaker than the original query, so Z3 may return SAT with rows that do not satisfy the dropped
+     * predicate. Exposed so the caller can record it in the solver statistics.
+     */
+    var skippedQueryConstraints = 0
+        private set
+
     private val smtTables: List<SmtTable> = schema.tables.map { SmtTable(it) }
     private val smtTableByOriginalName: Map<String, SmtTable> = smtTables.associateBy { it.originalName }
 
@@ -420,6 +429,7 @@ class SmtLibGenerator(private val schema: DbInfoDto, private val numberOfRows: I
                     smt.addNode(constraint)
                 }
             } catch (e: RuntimeException) {
+                skippedQueryConstraints++
                 LoggingUtil.getInfoLogger().warn("Could not translate WHERE clause to SMT-LIB, skipping: ${where}. Reason: ${e.message}")
             }
         }
@@ -457,6 +467,7 @@ class SmtLibGenerator(private val schema: DbInfoDto, private val numberOfRows: I
                                 smt.addNode(constraint)
                             }
                         } catch (e: RuntimeException) {
+                            skippedQueryConstraints++
                             LoggingUtil.getInfoLogger().warn("Could not translate JOIN ON clause to SMT-LIB, skipping: ${onExpression}. Reason: ${e.message}")
                         }
                     }