DSE Memoization + Statistics

[agusaldasoro]

Summary

• Adds memoization to the Z3 SMT solver to skip redundant Docker executions for identical SQL queries
• Introduces Z3Result (SAT/UNSAT/ERROR) to replace Optional<Map<String, SMTLibValue>>, making error handling explicit and enabling cache-safe distinction between UNSAT and transient errors
• Adds optional DSE statistics (collectDseStats flag) tracking SAT/UNSAT/error counts, timing, SMT-LIB size, and query uniqueness — written to CSV only when enabled
• Fixes AI classifier stable feature-space keying via modelKeys (parameter path strings), so each parameter always maps to the same input dimension across calls
• Fixes NN400EndpointModel.initializeIfNeeded to guard against re-initialization — without this, weight matrices were re-allocated and trained weights discarded on every
  classify()/updateModel() call

Motivation

The solver was re-running expensive Docker Z3 executions for the same SQL constraint on repeated calls. Memoizing SAT/UNSAT results avoids this. Errors are not cached to tolerate transient Docker
failures. The collectDseStats flag gives observability into DSE efficiency with zero overhead when disabled. The modelKeys fix ensures classifiers train on a consistent feature space rather
than one that shifts as new parameters are observed.

New Stats

CSV column	Description
dseTotalQueries	Total solver invocations (SAT + UNSAT + errors + parse failures)
dseUniqueQueries	Distinct queries seen (by hash)
dseDuplicateQueries	Invocations that hit the memoization cache
dseSat	Queries Z3 solved as SAT
dseUnsat	Queries Z3 solved as UNSAT
dseErrors	Queries that returned a Z3/Docker error
dseParseFailures	Queries that failed SQL→SMT-LIB parsing
dseZ3TotalMs	Total wall time spent in Z3 (ms)
dseSmtlibGenTotalMs	Total wall time generating SMT-LIB (ms)
dseAvgSmtlibSizeBytes	Average SMT-LIB file size (bytes)