Restore experimental Z3 SQL correctness-measurement feature

[agusaldasoro]

Overview

Restores the experimental Z3 SQL correctness-measurement feature that was removed in commit c8712da5, and reinstates the core → evomaster-client-java-sql dependency it relies on. This is a revert of that removal, merged on top of dse/memoization.

Motivation

When Z3 generates SQL INSERT data to satisfy a failing WHERE clause, there was no way to verify that the generated rows actually satisfy the original predicate. This feature adds an optional, self-checking correctness metric so we can measure — during experiments — how often Z3-generated data is truly correct.

What it does

Behind a new experimental flag measureSqlZ3Correctness (default false, depends on generateSqlDataWithZ3=true), after Z3 returns a SAT model the solver:

1. Reconstructs a QueryResultSet from the generated SqlActions (toQueryResultSet / extractGeneValue).
2. Runs SqlHeuristicsCalculator to compute the heuristic distance between the original WHERE query and the generated data.
   • distance == 0 → the generated insert satisfies the query.
   • distance > 0 → it does not.
3. Reports the results into Statistics (reportSqlZ3CorrectnessDistance), which emits five new stats when the flag is on: sqlZ3CorrectnessChecks, sqlZ3CorrectnessZeroDistance, sqlZ3CorrectnessNonZero, sqlZ3CorrectnessAvgDist, sqlZ3CorrectnessEvalFailures.

INSERT statements are skipped (no WHERE to evaluate against); DELETE/UPDATE evaluation failures are counted separately and excluded from the average so they don't distort the metric.

Changes

• core/pom.xml — re-add evomaster-client-java-sql dependency.
• EMConfig.kt — re-add measureSqlZ3Correctness experimental option.
• Statistics.kt — re-add correctness-distance counters and reportSqlZ3CorrectnessDistance.
• SMTLibZ3DbConstraintSolver.kt — re-add computeCorrectnessDistance, toQueryResultSet, extractGeneValue, and the post-SAT measurement hook.

Notes

The flag is off by default, so there is no behavioral impact on normal runs; the measurement path is exercised only during correctness experiments.

[arcuri82]

adding a dependency from core to a module inside driver is a MAJOR architectural change. we are in the process of reducing dependencies between the 2, not adding. adding this dependency does add all of the other dependencies it relies on, and so recursively. this is major issue that has prevented so far the upgrade of some libraries. unfortunately, we cannot have this, unless we do a major refactoring of that module