DSE Statistics & Fixes

client-java/sql/src/main/java/org/evomaster/client/java/sql/heuristic/SqlHeuristicsCalculator.java

@@ -124,7 +124,8 @@ public SqlDistanceWithMetrics computeDistance(String sqlCommand) {
             double distanceToTrue = 1.0d - t.getOfTrue();
             return new SqlDistanceWithMetrics(distanceToTrue, 0, false);
         } catch (Exception ex) {
-            SimpleLogger.uniqueWarn("Failed to compute complete SQL heuristics for: " + sqlCommand);
+            SimpleLogger.uniqueWarn("Failed to compute complete SQL heuristics for: " + sqlCommand
+                    + " | cause: " + ex.getClass().getName() + ": " + ex.getMessage());
             return new SqlDistanceWithMetrics(Double.MAX_VALUE, 0, true);
         }
     }

core-extra/dbconstraint/src/main/java/org/evomaster/dbconstraint/parser/jsql/JSqlVisitor.java

@@ -13,6 +13,10 @@
 import net.sf.jsqlparser.statement.select.Select;
 import org.evomaster.dbconstraint.ast.*;
 
+import java.math.BigInteger;
+import java.sql.Timestamp;
+import java.time.ZoneOffset;
+import java.time.format.DateTimeFormatter;
 import java.util.ArrayDeque;
 import java.util.ArrayList;
 import java.util.Deque;
@@ -45,7 +49,14 @@ public void visit(NullValue nullValue) {
 
     @Override
     public void visit(Function function) {
-        // TODO This translation should be implemented
+        String name = function.getName().toUpperCase();
+        if ((name.equals("LOWER") || name.equals("UPPER"))
+                && function.getParameters() != null
+                && function.getParameters().size() == 1) {
+            // Treat LOWER(col)/UPPER(col) as the column itself (case-folding is dropped as an approximation)
+            function.getParameters().get(0).accept(this);
+            return;
+        }
         throw new RuntimeException("Extraction of condition not yet implemented");
     }
 
@@ -113,8 +124,10 @@ public void visit(TimeValue timeValue) {
 
     @Override
     public void visit(TimestampValue timestampValue) {
-        // TODO This translation should be implemented
-        throw new RuntimeException("Extraction of condition not yet implemented");
+        // Treat the timestamp string as UTC so the epoch round-trips consistently with the
+        // UTC-based decoder in SMTLibZ3DbConstraintSolver (LocalDateTime.ofInstant(..., UTC)).
+        long epochSeconds = timestampValue.getValue().toLocalDateTime().toEpochSecond(ZoneOffset.UTC);
+        stack.push(new SqlBigIntegerLiteralValue(BigInteger.valueOf(epochSeconds)));
     }
 
     @Override
@@ -599,7 +612,19 @@ public void visit(TimeKeyExpression timeKeyExpression) {
 
     @Override
     public void visit(DateTimeLiteralExpression dateTimeLiteralExpression) {
-        // TODO This translation should be implemented
+        if (dateTimeLiteralExpression.getType() == DateTimeLiteralExpression.DateTime.TIMESTAMP) {
+            String value = dateTimeLiteralExpression.getValue();
+            if (value.startsWith("'") && value.endsWith("'")) {
+                value = value.substring(1, value.length() - 1);
+            }
+            // Treat the timestamp string as UTC to match the UTC-based decoder in
+            // SMTLibZ3DbConstraintSolver (LocalDateTime.ofInstant(..., UTC)).
+            long epochSeconds = java.time.LocalDateTime.parse(value,
+                    DateTimeFormatter.ofPattern("yyyy-MM-dd HH:mm:ss"))
+                    .toEpochSecond(ZoneOffset.UTC);
+            stack.push(new SqlBigIntegerLiteralValue(BigInteger.valueOf(epochSeconds)));
+            return;
+        }
         throw new RuntimeException("Extraction of condition not yet implemented");
     }
 

core-extra/dbconstraint/src/test/java/org/evomaster/dbconstraint/parser/JSqlConditionParserTest.java

@@ -1,12 +1,12 @@
 package org.evomaster.dbconstraint.parser;
 
 import org.evomaster.dbconstraint.ConstraintDatabaseType;
-import org.evomaster.dbconstraint.ast.SqlCondition;
-import org.evomaster.dbconstraint.ast.SqlInCondition;
+import org.evomaster.dbconstraint.ast.*;
 import org.evomaster.dbconstraint.parser.jsql.JSqlConditionParser;
 import org.junit.jupiter.api.Test;
 
 import static org.junit.jupiter.api.Assertions.assertEquals;
+import static org.junit.jupiter.api.Assertions.assertInstanceOf;
 import static org.junit.jupiter.api.Assertions.assertTrue;
 
 public class JSqlConditionParserTest {
@@ -104,4 +104,51 @@ public void testParseCastAsCharacterLargeObject() throws SqlConditionParserExcep
         assertEquals(expected, actual);
     }
 
+    @Test
+    public void testParseLowerFunction() throws SqlConditionParserException {
+        JSqlConditionParser parser = new JSqlConditionParser();
+        // LOWER(col) should be treated as col (case-folding dropped as approximation)
+        SqlCondition withLower = parser.parse("LOWER(commit_mgr_desc) != 'init'", ConstraintDatabaseType.H2);
+        SqlCondition withoutLower = parser.parse("commit_mgr_desc != 'init'", ConstraintDatabaseType.H2);
+        assertEquals(withoutLower, withLower);
+    }
+
+    @Test
+    public void testParseUpperFunction() throws SqlConditionParserException {
+        JSqlConditionParser parser = new JSqlConditionParser();
+        SqlCondition withUpper = parser.parse("UPPER(status) != 'ACTIVE'", ConstraintDatabaseType.H2);
+        SqlCondition withoutUpper = parser.parse("status != 'ACTIVE'", ConstraintDatabaseType.H2);
+        assertEquals(withoutUpper, withUpper);
+    }
+
+    @Test
+    public void testParseIsNotNullOrLower() throws SqlConditionParserException {
+        // Pattern seen in tracking-system: col IS NOT NULL OR LOWER(other_col) != 'init'
+        JSqlConditionParser parser = new JSqlConditionParser();
+        SqlCondition condition = parser.parse(
+                "commit_emp_desc IS NOT NULL OR LOWER(commit_mgr_desc) != 'init'",
+                ConstraintDatabaseType.H2);
+        assertInstanceOf(SqlOrCondition.class, condition);
+    }
+
+    @Test
+    public void testParseTimestampLiteral() throws SqlConditionParserException {
+        // Pattern seen in tracking-system: col = TIMESTAMP 'datetime-string'
+        JSqlConditionParser parser = new JSqlConditionParser();
+        SqlCondition condition = parser.parse(
+                "commit_date = TIMESTAMP '2020-11-26 10:49:41'",
+                ConstraintDatabaseType.H2);
+        assertInstanceOf(SqlComparisonCondition.class, condition);
+        SqlComparisonCondition cmp = (SqlComparisonCondition) condition;
+        assertInstanceOf(SqlBigIntegerLiteralValue.class, cmp.getRightOperand());
+        // The epoch value must be computed in UTC so that the round-trip in
+        // SMTLibZ3DbConstraintSolver (LocalDateTime.ofInstant(..., UTC)) preserves
+        // the original string representation regardless of JVM timezone.
+        SqlBigIntegerLiteralValue epoch = (SqlBigIntegerLiteralValue) cmp.getRightOperand();
+        long expected = java.time.LocalDateTime.parse("2020-11-26 10:49:41",
+                java.time.format.DateTimeFormatter.ofPattern("yyyy-MM-dd HH:mm:ss"))
+                .toEpochSecond(java.time.ZoneOffset.UTC);
+        assertEquals(java.math.BigInteger.valueOf(expected), epoch.getBigInteger());
+    }
+
 }

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/pom.xml

@@ -33,6 +33,10 @@
             <groupId>org.evomaster</groupId>
             <artifactId>evomaster-client-java-controller-api</artifactId>
         </dependency>
+        <dependency>
+            <groupId>org.evomaster</groupId>
+            <artifactId>evomaster-client-java-sql</artifactId>
+        </dependency>
         <dependency>
             <groupId>org.evomaster</groupId>
             <artifactId>evomaster-client-java-instrumentation-shared</artifactId>
@@ -473,6 +477,21 @@
                 <groupId>org.antlr</groupId>
                 <artifactId>antlr4-maven-plugin</artifactId>
             </plugin>
+
+            <!--
+                core has the heaviest gene test suite (GeneRandomizedTest: 1001 seeds × ~100 gene types).
+                On CI runners where algorithm tests complete faster than usual, less GC activity
+                accumulates before gene tests run, leaving the heap more fragmented and full.
+                5120m (vs the global 4096m) provides the headroom to survive runner variability.
+                GitHub Actions ubuntu-latest has 7 GB RAM: 5 GB heap + 1 GB Maven + 1 GB OS = 7 GB.
+            -->
+            <plugin>
+                <groupId>org.apache.maven.plugins</groupId>
+                <artifactId>maven-surefire-plugin</artifactId>
+                <configuration>
+                    <argLine>@{argLine} -ea -Xms1024m -Xmx5120m -Xss4m -Dfile.encoding=UTF-8 -Djdk.attach.allowAttachSelf=true -Duser.language=en -Duser.country=GB ${addOpens}</argLine>
+                </configuration>
+            </plugin>
         </plugins>
     </build>