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.