Fix stats

Author: agusaldasoro

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

@@ -87,7 +87,11 @@ class Statistics : SearchListener {
     private val sqlRowsAverageCalculator = IncrementalAverage()
 
     // Z3-based SQL data generation statistics
-    private var sqlZ3TotalQueriesProcessed = 0
+    // Invariant: sqlZ3QueriesSeenCount == sqlZ3CacheHitCount + sqlZ3CacheMissCount
+    // (every solve() call is either served from the memoization cache or handled as a miss).
+    private var sqlZ3QueriesSeenCount = 0
+    private var sqlZ3CacheHitCount = 0
+    private var sqlZ3CacheMissCount = 0
     private var sqlZ3SatCount = 0
     private var sqlZ3UnsatCount = 0
     private var sqlZ3UnknownCount = 0
@@ -244,31 +248,31 @@ class Statistics : SearchListener {
     }
 
     fun reportSqlZ3Sat(z3TimeMs: Long) {
-        sqlZ3TotalQueriesProcessed++
+        sqlZ3CacheMissCount++
         sqlZ3SatCount++
         sqlZ3TimeMs += z3TimeMs
     }
 
     fun reportSqlZ3Unsat(z3TimeMs: Long) {
-        sqlZ3TotalQueriesProcessed++
+        sqlZ3CacheMissCount++
         sqlZ3UnsatCount++
         sqlZ3TimeMs += z3TimeMs
     }
 
     fun reportSqlZ3Unknown(z3TimeMs: Long) {
-        sqlZ3TotalQueriesProcessed++
+        sqlZ3CacheMissCount++
         sqlZ3UnknownCount++
         sqlZ3TimeMs += z3TimeMs
     }
 
     fun reportSqlZ3Error(z3TimeMs: Long) {
-        sqlZ3TotalQueriesProcessed++
+        sqlZ3CacheMissCount++
         sqlZ3ErrorCount++
         sqlZ3TimeMs += z3TimeMs
     }
 
     fun reportSqlZ3ParseFailure() {
-        sqlZ3TotalQueriesProcessed++
+        sqlZ3CacheMissCount++
         sqlZ3ParseFailureCount++
     }
 
@@ -278,11 +282,22 @@ class Statistics : SearchListener {
     }
 
     fun reportSqlZ3QuerySeen(queryHash: Int) {
+        sqlZ3QueriesSeenCount++
         if (sqlZ3SeenQueryHashes.add(queryHash)) {
             sqlZ3UniqueQueriesCount++
         }
     }
 
+    fun reportSqlZ3CacheHit() {
+        sqlZ3CacheHitCount++
+    }
+
+    // Exposed for tests: verify the memoization accounting invariant
+    // (seen == cacheHits + cacheMisses).
+    internal fun getSqlZ3QueriesSeenCount() = sqlZ3QueriesSeenCount
+    internal fun getSqlZ3CacheHitCount() = sqlZ3CacheHitCount
+    internal fun getSqlZ3CacheMissCount() = sqlZ3CacheMissCount
+
     fun reportSqlZ3CorrectnessDistance(sqlDistance: Double, evaluationFailure: Boolean) {
         sqlZ3CorrectnessCheckCount++
         if (evaluationFailure) {
@@ -459,9 +474,11 @@ class Statistics : SearchListener {
 
             // statistics info for Z3-based SQL data generation (only emitted when collectSqlZ3Stats=true)
             if (config.collectSqlZ3Stats) {
-                add(Pair("sqlZ3TotalQueries", "$sqlZ3TotalQueriesProcessed"))
+                add(Pair("sqlZ3QueriesSeen", "$sqlZ3QueriesSeenCount"))
                 add(Pair("sqlZ3UniqueQueries", "$sqlZ3UniqueQueriesCount"))
-                add(Pair("sqlZ3DuplicateQueries", "${sqlZ3TotalQueriesProcessed - sqlZ3ParseFailureCount - sqlZ3UniqueQueriesCount}"))
+                add(Pair("sqlZ3DuplicateQueries", "${sqlZ3QueriesSeenCount - sqlZ3UniqueQueriesCount}"))
+                add(Pair("sqlZ3CacheHits", "$sqlZ3CacheHitCount"))
+                add(Pair("sqlZ3CacheMisses", "$sqlZ3CacheMissCount"))
                 add(Pair("sqlZ3Sat", "$sqlZ3SatCount"))
                 add(Pair("sqlZ3Unsat", "$sqlZ3UnsatCount"))
                 add(Pair("sqlZ3Unknown", "$sqlZ3UnknownCount"))

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

@@ -139,11 +139,14 @@ class SMTLibZ3DbConstraintSolver() : DbConstraintSolver {
         val collectStats = ::config.isInitialized && config.collectSqlZ3Stats
         val stats: Statistics? = if (collectStats) statisticsRef?.get() else null
 
-        stats?.reportSqlZ3QuerySeen(sqlQuery.hashCode())
-
         val cacheKey = Pair(sqlQuery, numberOfRows)
+        // Track "seen" against the same key the cache uses, so unique/duplicate counts
+        // line up with actual cache granularity.
+        stats?.reportSqlZ3QuerySeen(cacheKey.hashCode())
+
         val cached = z3ResultCache?.get(cacheKey)
         if (cached != null) {
+            stats?.reportSqlZ3CacheHit()
             return when (cached.status) {
                 Z3Result.Status.SAT -> toSqlActionList(schemaDto, cached.solution)
                 else -> emptyList()

core/src/test/kotlin/org/evomaster/core/search/service/StatisticsTest.kt

@@ -1,6 +1,6 @@
 package org.evomaster.core.search.service
 
-import org.junit.Test
+import org.junit.jupiter.api.Test
 import org.junit.jupiter.api.Assertions.assertEquals
 
 class StatisticsTest {
@@ -36,4 +36,31 @@ class StatisticsTest {
         assertEquals((5 + 7 + 11 + 13).toDouble() / 4, statistics.averageNumberOfEvaluatedRowsForSqlHeuristics())
     }
 
+    @Test
+    fun testSqlZ3CacheAccountingInvariant() {
+        val statistics = Statistics()
+
+        // Query #1: first sighting -> cache miss, solved as SAT
+        statistics.reportSqlZ3QuerySeen(1)
+        statistics.reportSqlZ3Sat(10)
+
+        // Query #2: first sighting -> cache miss, solved as UNSAT
+        statistics.reportSqlZ3QuerySeen(2)
+        statistics.reportSqlZ3Unsat(5)
+
+        // Query #1 seen again -> served from the memoization cache (a hit, not a miss)
+        statistics.reportSqlZ3QuerySeen(1)
+        statistics.reportSqlZ3CacheHit()
+
+        assertEquals(3, statistics.getSqlZ3QueriesSeenCount())
+        assertEquals(1, statistics.getSqlZ3CacheHitCount())
+        assertEquals(2, statistics.getSqlZ3CacheMissCount())
+
+        // Every solve() is either a cache hit or a miss.
+        assertEquals(
+            statistics.getSqlZ3QueriesSeenCount(),
+            statistics.getSqlZ3CacheHitCount() + statistics.getSqlZ3CacheMissCount()
+        )
+    }
+
 }