Add DSE Metrics + Memoization

core-extra/solver/src/main/java/org/evomaster/solver/Z3DockerExecutor.java

@@ -54,28 +54,34 @@ public Z3DockerExecutor(String resourcesFolder) {
      * The file must be in the directory specified by containerPath.
      *
      * @param fileName the name of the SMT-LIB file to read and solve
-     * @return the result of the Z3 solver as a map of variable names to their values, if the problem is satisfiable (sat)
-     *         or an empty Optional if the problem is unsatisfiable (unsat)
+     * @return a {@link Z3Result} with status SAT (and the model), UNSAT, or ERROR
      */
-    public Optional<Map<String, SMTLibValue>> solveFromFile(String fileName) {
+    public Z3Result solveFromFile(String fileName) {
         try {
-            // Execute the Z3 solver on the specified file in the container
             Container.ExecResult result = z3Prover.execInContainer("z3", containerPath + fileName);
+
             if (result.getExitCode() != 0) {
-                throw new RuntimeException("Error executing Z3 solver: \n" + result.getStdout() + "\n" + result.getStderr());
+                return Z3Result.error("Z3 exited with code " + result.getExitCode()
+                        + ": " + result.getStdout() + result.getStderr());
             }
+
             String stdout = result.getStdout();
+            if (stdout == null || stdout.trim().isEmpty()) {
+                return Z3Result.error("Z3 produced no output for file: " + fileName
+                        + " stderr: " + result.getStderr());
+            }
 
-            // Check if the solver returned any output
-            if (stdout == null || stdout.isEmpty()) {
-                String stderr = result.getStderr();
-                throw new RuntimeException("No result after solving file " + stderr);
+            if (stdout.trim().startsWith("unsat")) {
+                return Z3Result.unsat();
             }
 
-            // Parse the solver output and return the result
-            return Optional.of(SMTResultParser.parseZ3Response(stdout));
+            Map<String, SMTLibValue> model = SMTResultParser.parseZ3Response(stdout);
+            return Z3Result.sat(model);
+
         } catch (IOException | InterruptedException e) {
-            return Optional.empty();
+            return Z3Result.error("I/O or interruption error running Z3 on " + fileName + ": " + e.getMessage());
+        } catch (RuntimeException e) {
+            return Z3Result.error("Unexpected error parsing Z3 output for " + fileName + ": " + e.getMessage());
         }
     }
 

core-extra/solver/src/main/java/org/evomaster/solver/Z3Result.java

@@ -0,0 +1,46 @@
+package org.evomaster.solver;
+
+import org.evomaster.solver.smtlib.value.SMTLibValue;
+
+import java.util.Map;
+
+/**
+ * Represents the outcome of a Z3 solver invocation.
+ * Distinguishes between three possible states: SAT (satisfiable with a model),
+ * UNSAT (unsatisfiable), and ERROR (solver or parsing failure).
+ */
+public class Z3Result {
+
+    public enum Status {
+        /** Z3 found a satisfying assignment. The model is available. */
+        SAT,
+        /** The problem is unsatisfiable. No model exists. */
+        UNSAT,
+        /** A solver, I/O, or parsing error occurred. */
+        ERROR
+    }
+
+    public final Status status;
+    /** Non-null only when status == SAT. */
+    public final Map<String, SMTLibValue> model;
+    /** Non-null only when status == ERROR. */
+    public final String errorMessage;
+
+    private Z3Result(Status status, Map<String, SMTLibValue> model, String errorMessage) {
+        this.status = status;
+        this.model = model;
+        this.errorMessage = errorMessage;
+    }
+
+    public static Z3Result sat(Map<String, SMTLibValue> model) {
+        return new Z3Result(Status.SAT, model, null);
+    }
+
+    public static Z3Result unsat() {
+        return new Z3Result(Status.UNSAT, null, null);
+    }
+
+    public static Z3Result error(String message) {
+        return new Z3Result(Status.ERROR, null, message);
+    }
+}

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

@@ -15,7 +15,6 @@
 import java.nio.file.StandardCopyOption;
 import java.util.HashMap;
 import java.util.Map;
-import java.util.Optional;
 
 import static org.junit.jupiter.api.Assertions.*;
 
@@ -43,13 +42,13 @@ static void tearDown() {
      */
     @Test
     public void satisfiabilityExample() {
-        Optional<Map<String, SMTLibValue>> response = executor.solveFromFile("example.smt");
+        Z3Result result = executor.solveFromFile("example.smt");
 
-        assertTrue(response.isPresent());
-        assertEquals(2, response.get().size());
+        assertEquals(Z3Result.Status.SAT, result.status);
+        assertEquals(2, result.model.size());
 
-        assertEquals(new LongValue(0L), response.get().get("y"));
-        assertEquals(new LongValue((long) -4), response.get().get("x"));
+        assertEquals(new LongValue(0L), result.model.get("y"));
+        assertEquals(new LongValue((long) -4), result.model.get("x"));
     }
 
     /**
@@ -64,74 +63,72 @@ public void dynamicFile() throws IOException {
 
         Files.copy(originalPath, copied, StandardCopyOption.REPLACE_EXISTING);
 
-        Optional<Map<String, SMTLibValue>> response;
+        Z3Result result;
         try {
-            response = executor.solveFromFile("example2.smt");
+            result = executor.solveFromFile("example2.smt");
         } finally {
-            Files.deleteIfExists(copied); // Ensure the file is deleted
+            Files.deleteIfExists(copied);
         }
 
-        assertTrue(response.isPresent());
+        assertEquals(Z3Result.Status.SAT, result.status);
     }
 
     /**
      * Test solving a model with the example of returning two unique unsigned integers
      */
     @Test
     public void uniqueUInt() {
-        Optional<Map<String, SMTLibValue>> response = executor.solveFromFile("unique_uint.smt");
+        Z3Result result = executor.solveFromFile("unique_uint.smt");
 
-        assertTrue(response.isPresent(), "Response should be present for unique_uint.smt");
-        assertEquals(new LongValue(2L), response.get().get("id_1"), "The value for id_1 should be 2");
-        assertEquals(new LongValue(3L), response.get().get("id_2"), "The value for id_2 should be 3");
+        assertEquals(Z3Result.Status.SAT, result.status, "Response should be SAT for unique_uint.smt");
+        assertEquals(new LongValue(2L), result.model.get("id_1"), "The value for id_1 should be 2");
+        assertEquals(new LongValue(3L), result.model.get("id_2"), "The value for id_2 should be 3");
     }
 
     /**
      * Test solving a model with composed types
      */
     @Test
     public void composedTypes() {
-        Optional<Map<String, SMTLibValue>> response = executor.solveFromFile("composed_types.smt");
+        Z3Result result = executor.solveFromFile("composed_types.smt");
 
-        assertTrue(response.isPresent(), "Response should be present for composed_types.smt");
+        assertEquals(Z3Result.Status.SAT, result.status, "Response should be SAT for composed_types.smt");
 
-        assertTrue(response.get().containsKey("users1"), "Response should contain users1");
+        assertTrue(result.model.containsKey("users1"), "Response should contain users1");
         Map<String, SMTLibValue> users1Expected = new HashMap<>();
         users1Expected.put("ID", new LongValue(3L));
         users1Expected.put("NAME", new StringValue("agus"));
         users1Expected.put("AGE", new LongValue(31L));
         users1Expected.put("POINTS", new LongValue(7L));
 
-        assertEquals(new StructValue(users1Expected), response.get().get("users1"), "The value for users1 is incorrect");
+        assertEquals(new StructValue(users1Expected), result.model.get("users1"), "The value for users1 is incorrect");
 
-        assertTrue(response.get().containsKey("users2"), "Response should contain users2");
+        assertTrue(result.model.containsKey("users2"), "Response should contain users2");
         Map<String, SMTLibValue> users2Expected = new HashMap<>();
         users2Expected.put("ID", new LongValue(3L));
         users2Expected.put("NAME", new StringValue("agus"));
         users2Expected.put("AGE", new LongValue(31L));
         users2Expected.put("POINTS", new LongValue(7L));
-        assertEquals(new StructValue(users2Expected), response.get().get("users2"), "The value for users2 is incorrect");
+        assertEquals(new StructValue(users2Expected), result.model.get("users2"), "The value for users2 is incorrect");
     }
 
     /**
      * Test solving with an invalid file to ensure proper error handling
      */
     @Test
-    public void whenSolvingInvalidFileItFails() {
-        assertThrows(
-                RuntimeException.class,
-                () -> executor.solveFromFile("invalid.smt")
-        );
+    public void whenSolvingInvalidFileItReturnsError() {
+        Z3Result result = executor.solveFromFile("invalid.smt");
+        assertEquals(Z3Result.Status.ERROR, result.status);
+        assertNotNull(result.errorMessage);
     }
 
     /**
      * Test handling an empty file
      */
     @Test
-    public void whenSolvingEmptyFileItFails() {
-        assertThrows(
-                RuntimeException.class,
-                () -> executor.solveFromFile("empty.smt")
-        );
+    public void whenSolvingEmptyFileItReturnsError() {
+        Z3Result result = executor.solveFromFile("empty.smt");
+        assertEquals(Z3Result.Status.ERROR, result.status);
+        assertNotNull(result.errorMessage);
     }
 }

core/src/main/kotlin/org/evomaster/core/EMConfig.kt

@@ -1920,6 +1920,13 @@ class EMConfig {
     @DependsOnFalseFor("blackBox")
     var generateSqlDataWithDSE = false
 
+    @Experimental
+    @Cfg("Collect detailed statistics for DSE SQL generation: SAT/UNSAT/error counts, " +
+            "query uniqueness, Z3 execution time, and SMT-LIB generation time. " +
+            "Only meaningful when generateSqlDataWithDSE=true.")
+    @DependsOnTrueFor("generateSqlDataWithDSE")
+    var collectDseStats = false
+
     @Cfg("Enable EvoMaster to generate SQL data with direct accesses to the database. Use a search algorithm")
     @DependsOnFalseFor("blackBox")
     var generateSqlDataWithSearch = true

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

@@ -86,6 +86,18 @@ class Statistics : SearchListener {
     private var sqlHeuristicEvaluationFailureCount = 0;
     private val sqlRowsAverageCalculator = IncrementalAverage()
 
+    // DSE (Dynamic Symbolic Execution) statistics
+    private var dseTotalQueriesProcessed = 0
+    private var dseSatCount = 0
+    private var dseUnsatCount = 0
+    private var dseErrorCount = 0
+    private var dseParseFailureCount = 0
+    private var dseZ3TimeMs = 0L
+    private var dseSmtlibGenTimeMs = 0L
+    private val dseSmtlibSizeBytes = IncrementalAverage()
+    private val dseSeenQueryHashes = mutableSetOf<Int>()
+    private var dseUniqueQueriesCount = 0
+
     // mongo heuristic evaluation statistic
     private var mongoHeuristicEvaluationSuccessCount = 0
     private var mongoHeuristicEvaluationFailureCount = 0
@@ -223,6 +235,40 @@ class Statistics : SearchListener {
         redisHeuristicEvaluationFailureCount++
     }
 
+    fun reportDseSat(z3TimeMs: Long) {
+        dseTotalQueriesProcessed++
+        dseSatCount++
+        dseZ3TimeMs += z3TimeMs
+    }
+
+    fun reportDseUnsat(z3TimeMs: Long) {
+        dseTotalQueriesProcessed++
+        dseUnsatCount++
+        dseZ3TimeMs += z3TimeMs
+    }
+
+    fun reportDseError(z3TimeMs: Long) {
+        dseTotalQueriesProcessed++
+        dseErrorCount++
+        dseZ3TimeMs += z3TimeMs
+    }
+
+    fun reportDseParseFailure() {
+        dseTotalQueriesProcessed++
+        dseParseFailureCount++
+    }
+
+    fun reportDseSmtlibGenTime(ms: Long, sizeBytes: Int) {
+        dseSmtlibGenTimeMs += ms
+        dseSmtlibSizeBytes.addValue(sizeBytes)
+    }
+
+    fun reportDseQuerySeen(queryHash: Int) {
+        if (dseSeenQueryHashes.add(queryHash)) {
+            dseUniqueQueriesCount++
+        }
+    }
+
     fun getMongoHeuristicsEvaluationCount(): Int = mongoHeuristicEvaluationSuccessCount + mongoHeuristicEvaluationFailureCount
 
     fun getSqlHeuristicsEvaluationCount(): Int = sqlHeuristicEvaluationSuccessCount + sqlHeuristicEvaluationFailureCount
@@ -381,6 +427,20 @@ class Statistics : SearchListener {
             add(Pair("sqlHeuristicsEvaluationFailures","$sqlHeuristicEvaluationFailureCount" ))
             add(Pair("sqlHeuristicsEvaluationCount","${getSqlHeuristicsEvaluationCount()}"))
 
+            // statistics info for DSE (only emitted when collectDseStats=true)
+            if (config.collectDseStats) {
+                add(Pair("dseTotalQueries", "$dseTotalQueriesProcessed"))
+                add(Pair("dseUniqueQueries", "$dseUniqueQueriesCount"))
+                add(Pair("dseDuplicateQueries", "${dseTotalQueriesProcessed - dseParseFailureCount - dseUniqueQueriesCount}"))
+                add(Pair("dseSat", "$dseSatCount"))
+                add(Pair("dseUnsat", "$dseUnsatCount"))
+                add(Pair("dseErrors", "$dseErrorCount"))
+                add(Pair("dseParseFailures", "$dseParseFailureCount"))
+                add(Pair("dseZ3TotalMs", "$dseZ3TimeMs"))
+                add(Pair("dseSmtlibGenTotalMs", "$dseSmtlibGenTimeMs"))
+                add(Pair("dseAvgSmtlibSizeBytes", "%.1f".format(dseSmtlibSizeBytes.mean)))
+            }
+
             for(phase in ExecutionPhaseController.Phase.entries){
                 add(Pair("phase_${phase.name}", "${epc.getPhaseDurationInSeconds(phase)}"))
             }