Add comments

Author: agusaldasoro

core-extra/solver/src/main/java/org/evomaster/solver/smtlib/SMTResultParser.java

@@ -18,6 +18,11 @@ public class SMTResultParser {
     /**
      * Parses the Z3 solver response and extracts variable values.
      *
+     * FRAGILITY: parsing is regex- and position-based and assumes Z3's textual get-value layout
+     * (one struct per line, constructor name split on '-', values split on whitespace). It therefore
+     * assumes string values contain no spaces, hyphens, quotes or parentheses; such values would be
+     * mis-split. Hardening the parser (or requesting values in a more robust format) is future work.
+     *
      * @param z3Response the raw response from Z3 solver
      * @return a {@link Z3Solution} mapping variable names to the {@link SMTLibValue} objects Z3 assigned to them
      */

core-extra/solver/src/test/java/org/evomaster/solver/Z3DockerExecutorTest.java

@@ -13,8 +13,6 @@
 import java.nio.file.Path;
 import java.nio.file.Paths;
 import java.nio.file.StandardCopyOption;
-import java.util.HashMap;
-import java.util.Map;
 
 import static org.junit.jupiter.api.Assertions.*;
 
@@ -95,21 +93,31 @@ public void composedTypes() {
         assertEquals(Z3Result.Status.SAT, result.getStatus(), "Response should be SAT for composed_types.smt");
 
         assertTrue(result.getSolution().containsKey("users1"), "Response should contain users1");
-        Map<String, SMTLibValue> users1Expected = new HashMap<>();
-        users1Expected.put("ID", new LongValue(3L));
-        users1Expected.put("NAME", new StringValue("Alice"));
-        users1Expected.put("AGE", new LongValue(31L));
-        users1Expected.put("POINTS", new LongValue(7L));
-
-        assertEquals(new StructValue(users1Expected), result.getSolution().get("users1"), "The value for users1 is incorrect");
-
         assertTrue(result.getSolution().containsKey("users2"), "Response should contain users2");
-        Map<String, SMTLibValue> users2Expected = new HashMap<>();
-        users2Expected.put("ID", new LongValue(3L));
-        users2Expected.put("NAME", new StringValue("Bob"));
-        users2Expected.put("AGE", new LongValue(31L));
-        users2Expected.put("POINTS", new LongValue(7L));
-        assertEquals(new StructValue(users2Expected), result.getSolution().get("users2"), "The value for users2 is incorrect");
+
+        // NOTE: assert the individual field VALUES, not StructValue equality: StructValue.equals only
+        // compares the set of field names, so a whole-struct assertEquals would pass regardless of the
+        // actual values Z3 returned. We assert the fully-constrained fields exactly (NAME, POINTS) and
+        // the underconstrained fields against their SMT-LIB constraints (AGE range, distinct IDs).
+        StructValue users1 = (StructValue) result.getSolution().get("users1");
+        StructValue users2 = (StructValue) result.getSolution().get("users2");
+
+        // NAME and POINTS are pinned by the SMT-LIB (NAME = "Alice"/"Bob", POINTS = 7), so deterministic.
+        assertEquals(new StringValue("Alice"), users1.getField("NAME"), "NAME users1");
+        assertEquals(new StringValue("Bob"), users2.getField("NAME"), "NAME users2");
+        assertEquals(new LongValue(7L), users1.getField("POINTS"), "POINTS users1");
+        assertEquals(new LongValue(7L), users2.getField("POINTS"), "POINTS users2");
+
+        // AGE is constrained to (30, 100): assert the constraint holds rather than a specific value.
+        long age1 = ((LongValue) users1.getField("AGE")).getValue();
+        long age2 = ((LongValue) users2.getField("AGE")).getValue();
+        assertTrue(age1 > 30 && age1 < 100, "AGE users1 out of range: " + age1);
+        assertTrue(age2 > 30 && age2 < 100, "AGE users2 out of range: " + age2);
+
+        // IDs must be distinct (the 'distinct' assertion over the PK).
+        long id1 = ((LongValue) users1.getField("ID")).getValue();
+        long id2 = ((LongValue) users2.getField("ID")).getValue();
+        assertNotEquals(id1, id2, "user IDs must be distinct");
     }
 
     /**

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

@@ -70,6 +70,12 @@ class SMTLibZ3DbConstraintSolver() : DbConstraintSolver {
     // Memoization cache: (sqlQuery, numberOfRows) -> Z3Result (SAT or UNSAT only; errors are not cached)
     // Schema is assumed stable within a single run, so only query + row count form the key.
     // Null until Z3 SQL generation is enabled in postConstruct — avoids allocating the map in runs where Z3 SQL generation is off.
+    //
+    // THREAD-SAFETY: this is an access-ordered LinkedHashMap (LRU), whose get() mutates internal order,
+    // so it is NOT thread-safe. It relies on solve() being called from a single thread, which holds today
+    // because the MIO search loop (and thus fitness evaluation / structure mutation) is single-threaded.
+    // If fitness evaluation is ever parallelized, this cache must be synchronized or replaced with a
+    // concurrent LRU, otherwise concurrent access would corrupt it (lost entries / ConcurrentModificationException).
     private var z3ResultCache: MutableMap<Pair<String, Int>, Z3Result>? = null
 
     companion object {
@@ -206,6 +212,11 @@ class SMTLibZ3DbConstraintSolver() : DbConstraintSolver {
                      * (SELECT, DELETE, UPDATE). In the future this could be extended to verify
                      * that the generated rows satisfy insertion preconditions such as FK constraints
                      * or NOT NULL columns that Z3 SQL generation currently leaves unconstrained.
+                     *
+                     * Note: SqlHeuristicsCalculator is SELECT-oriented. For DELETE/UPDATE the distance
+                     * computation may fail and be reported as an evaluation failure (sqlDistanceEvaluationFailure)
+                     * rather than a real distance; such failures are counted separately and are excluded
+                     * from the average, so they do not distort the correctness metric.
                      */
                     val distResult = computeCorrectnessDistance(sqlQuery, schemaDto, sqlActions)
                     if (distResult.sqlDistanceEvaluationFailure) {